<commit_before>(*

Copyright 2013 <NAME>, <NAME>

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.

*)

#I "./../packages"

#r "FSharp.Compatibility.OCaml.0.1.10/lib/net40/FSharp.Compatibility.OCaml.dll"
#r "FSharp.Compatibility.OCaml.Format.0.1.10/lib/net40/FSharp.Compatibility.OCaml.Format.dll"
#r "FSharp.Compatibility.OCaml.System.0.1.10/lib/net40/FSharp.Compatibility.OCaml.System.dll"
#r "ExtCore.0.8.29/lib/net40/ExtCore.dll"

#I "./../NHol"
#r @"bin/Debug/NHol.dll"

#nowarn "25"
#nowarn "40"
#nowarn "49"
#nowarn "62"

open FSharp.Compatibility.OCaml;;
open FSharp.Compatibility.OCaml.Num;;

open NHol
open NHol.lib
open NHol.fusion
open NHol.basics
open NHol.nets
open NHol.printer
open NHol.preterm
open NHol.parser
open NHol.equal
open NHol.bool
open NHol.drule
open NHol.tactics
open NHol.itab
open NHol.simp
open NHol.theorems
open NHol.ind_defs
open NHol.``class``
open NHol.trivia
open NHol.canon
open NHol.meson
open NHol.quot
open NHol.pair //pair module has to be checked
open NHol.nums
open NHol.recursion
open NHol.arith   
open NHol.wf //
open NHol.calc_num
open NHol.normalizer
open NHol.grobner
open NHol.ind_types //
open NHol.lists
open NHol.realax   
open NHol.calc_int 
open NHol.realarith
open NHol.real  //  
//open NHol.calc_rat 
//open NHol.int     
//open NHol.sets     
//open NHol.iterate
//open NHol.cart     
//open NHol.define   

fsi.AddPrinter string_of_type;;
fsi.AddPrinter string_of_term;;
fsi.AddPrinter string_of_thm;;

//* Initial databases status *//

types();;                                                                           // internal database the_type_constants
//val it : (string * int) list = [("bool", 0); ("fun", 2)]

constants();;                                                                       // internal database the_term_constants
//val it : (string * hol_type) list =
//  [("=",
//    Tyapp ("fun",[Tyvar "A"; Tyapp ("fun",[Tyvar "A"; Tyapp ("bool",[])])]))]

infixes();;
//val it : (string * (int * string)) list = []

axioms();;                                                                          // internal database the_axioms
//val it : thm list = []

definitions();;                                                                     // internal database the_definitions
//val it : thm list = []

!the_implicit_types;;                                                               // internal database the_implicit_types
//val it : (string * hol_type) list = []

type_abbrevs();;                                                                    // internal database the_type_abbreviations
//val it : (string * hol_type) list = []

//monotonicity_theorems;;       only in ind_defs
//the_inductive_definitions;;   only in ind_defs
//inductive_type_store;;        only after class

//* Parser Module *//
types();;                                                                           // the_type_constants database doesn't change
constants();;
infixes();;
//val it : (string * (int * string)) list = [(",", (14, "right"))]
axioms();;                                                                          // the_axioms database doesn't change
definitions();;                                                                     // the_definitions doesn't change
!the_implicit_types;;                                                               // no change
type_abbrevs();;  

//* Bool Module *//

mk_iff;; // forces bool module evaluation

types();;                                                                           // the_type_constants database doesn't change
constants();;                                                                       // new boolean constants
//  [("?!", (A->bool)->bool); ("~", bool->bool); ("F", bool);
//   ("\/", bool->bool->bool); ("?", (A->bool)->bool); ("!", (A->bool)->bool);
//   ("==>", bool->bool->bool); ("/\", bool->bool->bool); ("T", bool);
//   ("=", A->A->bool)]
infixes();;
//val it : (string * (int * string)) list =
//  [("<=>", (2, "right")); ("==>", (4, "right")); ("\/", (6, "right"));
//   ("/\", (8, "right")); ("=", (12, "right")); (",", (14, "right"))]
axioms();;                                                                          // the_axioms database doesn't change
definitions();;                                                                     // the_definitions doesn't change
!the_implicit_types;;                                                               // no change
type_abbrevs();;                                                                    // no change

// after population of constants this parses
parse_term @"~(p /\ q) <=> ~p \/ ~q";;


//* Drule Module *//

MK_CONJ;; // forces drule module evaluation

types();;                                                                           // the_type_constants database doesn't change
constants();;                                                                       // the_term_constants database doesn't change
infixes();;                                                                         // no change
axioms();;                                                                          // the_axioms database doesn't change
definitions();;                                                                     // new boolean definitions
//  [|- (?!) = (\P. (?) P /\ (!x y. P x /\ P y ==> x = y));
//   |- (~) = (\p. p ==> F); |- F <=> (!p. p);
//   |- (\/) = (\p q. !r. (p ==> r) ==> (q ==> r) ==> r);
//   |- (?) = (\P. !q. (!x. P x ==> q) ==> q); |- (!) = (\P. P = (\x. T));
//   |- (==>) = (\p q. p /\ q <=> p);
//   |- (/\) = (\p q. (\f. f p q) = (\f. f T T)); |- T <=> (\p. p) = (\p. p)]

!the_implicit_types;;                                                               // no change
type_abbrevs();;                                                                    // no change


//* Tactitcs Module *//

_FALSITY_;; // forces tactics module evaluation

types();;                                                                           // the_type_constants database doesn't change
constants();;                                                                       // new constant _FALSITY_
//  [("_FALSITY_", bool); ("?!", (A->bool)->bool); ("~", bool->bool);
//   ("F", bool); ("\/", bool->bool->bool); ("?", (A->bool)->bool);
//   ("!", (A->bool)->bool); ("==>", bool->bool->bool); ("/\", bool->bool->bool);
//   ("T", bool); ("=", A->A->bool)]
infixes();;                                                                         // no change
axioms();;                                                                          // the_axioms database doesn't change
definitions();;                                                                     // new _FALSITY_ definition
//  [|- _FALSITY_ <=> F; |- (?!) = (\P. (?) P /\ (!x y. P x /\ P y ==> x = y));
//   |- (~) = (\p. p ==> F); |- F <=> (!p. p);
//   |- (\/) = (\p q. !r. (p ==> r) ==> (q ==> r) ==> r);
//   |- (?) = (\P. !q. (!x. P x ==> q) ==> q); |- (!) = (\P. P = (\x. T));
//   |- (==>) = (\p q. p /\ q <=> p);
//   |- (/\) = (\p q. (\f. f p q) = (\f. f T T)); |- T <=> (\p. p) = (\p. p)]
!the_implicit_types;;                                                               // no change
type_abbrevs();;                                                                    // no change

//* Itab Module *//
ITAUT_TAC;; // forces itab module evaluation
// No Changes in internal databases status

//* Simp Module *//
mk_rewrites;; // forces simp module evaluation
// No Changes in internal databases status: to be checked better

//* Theorems Module *//
EQ_REFL;; // forces theorems module evaluation
// No Changes in internal databases status: to be checked better

//* ind_defs Module *//
EXISTS_EQUATION;; // forces ind_defs module evaluation
!the_implicit_types;;                                                               // no change
type_abbrevs();;                                                                    // no change
// No Changes in internal databases status: to be checked better

// Class Module *//

ETA_AX;;    // forces class module evaluation

types();;                                                                           // the_type_constants database doesn't change
constants();;                                                                       // new constants COND, @
//  [("COND", bool->A->A->A); ("@", (A->bool)->A);<commit_msg>added basic_rewrites mutable just after theorems evaluation<commit_after>(*

Copyright 2013 <NAME>, <NAME>

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.

*)

#I "./../packages"

#r "FSharp.Compatibility.OCaml.0.1.10/lib/net40/FSharp.Compatibility.OCaml.dll"
#r "FSharp.Compatibility.OCaml.Format.0.1.10/lib/net40/FSharp.Compatibility.OCaml.Format.dll"
#r "FSharp.Compatibility.OCaml.System.0.1.10/lib/net40/FSharp.Compatibility.OCaml.System.dll"
#r "ExtCore.0.8.29/lib/net40/ExtCore.dll"

#I "./../NHol"
#r @"bin/Debug/NHol.dll"

#nowarn "25"
#nowarn "40"
#nowarn "49"
#nowarn "62"

open FSharp.Compatibility.OCaml;;
open FSharp.Compatibility.OCaml.Num;;

open NHol
open NHol.lib
open NHol.fusion
open NHol.basics
open NHol.nets
open NHol.printer
open NHol.preterm
open NHol.parser
open NHol.equal
open NHol.bool
open NHol.drule
open NHol.tactics
open NHol.itab
open NHol.simp
open NHol.theorems
open NHol.ind_defs
open NHol.``class``
open NHol.trivia
open NHol.canon
open NHol.meson
open NHol.quot
open NHol.pair //pair module has to be checked
open NHol.nums
open NHol.recursion
open NHol.arith   
open NHol.wf //
open NHol.calc_num
open NHol.normalizer
open NHol.grobner
open NHol.ind_types //
open NHol.lists
open NHol.realax   
open NHol.calc_int 
open NHol.realarith
open NHol.real  //  
//open NHol.calc_rat 
//open NHol.int     
//open NHol.sets     
//open NHol.iterate
//open NHol.cart     
//open NHol.define   

fsi.AddPrinter string_of_type;;
fsi.AddPrinter string_of_term;;
fsi.AddPrinter string_of_thm;;

//* Initial databases status *//

types();;                                                                           // internal database the_type_constants
//val it : (string * int) list = [("bool", 0); ("fun", 2)]

constants();;                                                                       // internal database the_term_constants
//val it : (string * hol_type) list =
//  [("=",
//    Tyapp ("fun",[Tyvar "A"; Tyapp ("fun",[Tyvar "A"; Tyapp ("bool",[])])]))]

infixes();;
//val it : (string * (int * string)) list = []

axioms();;                                                                          // internal database the_axioms
//val it : thm list = []

definitions();;                                                                     // internal database the_definitions
//val it : thm list = []

!the_implicit_types;;                                                               // internal database the_implicit_types
//val it : (string * hol_type) list = []

type_abbrevs();;                                                                    // internal database the_type_abbreviations
//val it : (string * hol_type) list = []

//monotonicity_theorems;;       only in ind_defs
//the_inductive_definitions;;   only in ind_defs
//inductive_type_store;;        only after class

//* Parser Module *//
types();;                                                                           // the_type_constants database doesn't change
constants();;
infixes();;
//val it : (string * (int * string)) list = [(",", (14, "right"))]
axioms();;                                                                          // the_axioms database doesn't change
definitions();;                                                                     // the_definitions doesn't change
!the_implicit_types;;                                                               // no change
type_abbrevs();;  

//* Bool Module *//

mk_iff;; // forces bool module evaluation

types();;                                                                           // the_type_constants database doesn't change
constants();;                                                                       // new boolean constants
//  [("?!", (A->bool)->bool); ("~", bool->bool); ("F", bool);
//   ("\/", bool->bool->bool); ("?", (A->bool)->bool); ("!", (A->bool)->bool);
//   ("==>", bool->bool->bool); ("/\", bool->bool->bool); ("T", bool);
//   ("=", A->A->bool)]
infixes();;
//val it : (string * (int * string)) list =
//  [("<=>", (2, "right")); ("==>", (4, "right")); ("\/", (6, "right"));
//   ("/\", (8, "right")); ("=", (12, "right")); (",", (14, "right"))]
axioms();;                                                                          // the_axioms database doesn't change
definitions();;                                                                     // the_definitions doesn't change
!the_implicit_types;;                                                               // no change
type_abbrevs();;                                                                    // no change

// after population of constants this parses
parse_term @"~(p /\ q) <=> ~p \/ ~q";;


//* Drule Module *//

MK_CONJ;; // forces drule module evaluation

types();;                                                                           // the_type_constants database doesn't change
constants();;                                                                       // the_term_constants database doesn't change
infixes();;                                                                         // no change
axioms();;                                                                          // the_axioms database doesn't change
definitions();;                                                                     // new boolean definitions
//  [|- (?!) = (\P. (?) P /\ (!x y. P x /\ P y ==> x = y));
//   |- (~) = (\p. p ==> F); |- F <=> (!p. p);
//   |- (\/) = (\p q. !r. (p ==> r) ==> (q ==> r) ==> r);
//   |- (?) = (\P. !q. (!x. P x ==> q) ==> q); |- (!) = (\P. P = (\x. T));
//   |- (==>) = (\p q. p /\ q <=> p);
//   |- (/\) = (\p q. (\f. f p q) = (\f. f T T)); |- T <=> (\p. p) = (\p. p)]

!the_implicit_types;;                                                               // no change
type_abbrevs();;                                                                    // no change


//* Tactitcs Module *//

_FALSITY_;; // forces tactics module evaluation

types();;                                                                           // the_type_constants database doesn't change
constants();;                                                                       // new constant _FALSITY_
//  [("_FALSITY_", bool); ("?!", (A->bool)->bool); ("~", bool->bool);
//   ("F", bool); ("\/", bool->bool->bool); ("?", (A->bool)->bool);
//   ("!", (A->bool)->bool); ("==>", bool->bool->bool); ("/\", bool->bool->bool);
//   ("T", bool); ("=", A->A->bool)]
infixes();;                                                                         // no change
axioms();;                                                                          // the_axioms database doesn't change
definitions();;                                                                     // new _FALSITY_ definition
//  [|- _FALSITY_ <=> F; |- (?!) = (\P. (?) P /\ (!x y. P x /\ P y ==> x = y));
//   |- (~) = (\p. p ==> F); |- F <=> (!p. p);
//   |- (\/) = (\p q. !r. (p ==> r) ==> (q ==> r) ==> r);
//   |- (?) = (\P. !q. (!x. P x ==> q) ==> q); |- (!) = (\P. P = (\x. T));
//   |- (==>) = (\p q. p /\ q <=> p);
//   |- (/\) = (\p q. (\f. f p q) = (\f. f T T)); |- T <=> (\p. p) = (\p. p)]
!the_implicit_types;;                                                               // no change
type_abbrevs();;                                                                    // no change

//* Itab Module *//
ITAUT_TAC;; // forces itab module evaluation
// No Changes in internal databases status

//* Simp Module *//
mk_rewrites;; // forces simp module evaluation
// No Changes in internal databases status: to be checked better

//* Theorems Module *//
EQ_REFL;; // forces theorems module evaluation
basic_rewrites();;
//val it : Protected<thm0> list =
//  [Choice1Of2 |- x = x <=> T; Choice1Of2 |- (T <=> t) <=> t;
//   Choice1Of2 |- (t <=> T) <=> t; Choice1Of2 |- (F <=> t) <=> ~t;
//   Choice1Of2 |- (t <=> F) <=> ~t; Choice1Of2 |- ~T <=> F;
//   Choice1Of2 |- ~F <=> T; Choice1Of2 |- T /\ t <=> t;
//   Choice1Of2 |- t /\ T <=> t; Choice1Of2 |- F /\ t <=> F;
//   Choice1Of2 |- t /\ F <=> F; Choice1Of2 |- t /\ t <=> t;
//   Choice1Of2 |- T \/ t <=> T; Choice1Of2 |- t \/ T <=> T;
//   Choice1Of2 |- F \/ t <=> t; Choice1Of2 |- t \/ F <=> t;
//   Choice1Of2 |- t \/ t <=> t; Choice1Of2 |- T ==> t <=> t;
//   Choice1Of2 |- t ==> T <=> T; Choice1Of2 |- F ==> t <=> T;
//   Choice1Of2 |- t ==> t <=> T; Choice1Of2 |- t ==> F <=> ~t;
//   Choice1Of2 |- (!x. t) <=> t; Choice1Of2 |- (?x. t) <=> t;
//   Choice1Of2 |- (\x. f x) y = f y; Choice1Of2 |- x = x ==> p <=> p]

//* ind_defs Module *//
EXISTS_EQUATION;; // forces ind_defs module evaluation
!the_implicit_types;;                                                               // no change
type_abbrevs();;                                                                    // no change
// No Changes in internal databases status: to be checked better

// Class Module *//

ETA_AX;;    // forces class module evaluation

types();;                                                                           // the_type_constants database doesn't change
constants();;                                                                       // new constants COND, @
//  [("COND", bool->A->A->A); ("@", (A->bool)->A);
{'fraction_non_alphanumeric': 0.16989143287111685, 'fraction_numerical': 0.008438138234977964, 'mean_word_length': 1.297444128904803, 'pattern_counts': {'":': 0, '<': 55, '<?xml version=': 0, '>': 173, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 192, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2811440', 'n_tokens_mistral': 5365, 'n_tokens_neox': 5202, 'n_words': 1458}