|
1 (* Title: CHOL/ROOT.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Adds Classical Higher-order Logic to a database containing Pure Isabelle. |
|
7 Should be executed in the subdirectory HOL. |
|
8 *) |
|
9 |
|
10 val banner = "Higher-Order Logic with curried functions"; |
|
11 writeln banner; |
|
12 |
|
13 print_depth 1; |
|
14 set eta_contract; |
|
15 |
|
16 (* Add user sections *) |
|
17 use "../Pure/section_utils.ML"; |
|
18 use "thy_syntax.ML"; |
|
19 |
|
20 use_thy "HOL"; |
|
21 use "../Provers/hypsubst.ML"; |
|
22 use "../Provers/classical.ML"; |
|
23 use "../Provers/simplifier.ML"; |
|
24 use "../Provers/splitter.ML"; |
|
25 |
|
26 (** Applying HypsubstFun to generate hyp_subst_tac **) |
|
27 |
|
28 structure Hypsubst_Data = |
|
29 struct |
|
30 (*Take apart an equality judgement; otherwise raise Match!*) |
|
31 fun dest_eq (Const("Trueprop",_) $ (Const("op =",_) $ t $ u)) = (t,u); |
|
32 val imp_intr = impI |
|
33 val rev_mp = rev_mp |
|
34 val subst = subst |
|
35 val sym = sym |
|
36 end; |
|
37 |
|
38 structure Hypsubst = HypsubstFun(Hypsubst_Data); |
|
39 open Hypsubst; |
|
40 |
|
41 (*** Applying ClassicalFun to create a classical prover ***) |
|
42 structure Classical_Data = |
|
43 struct |
|
44 val sizef = size_of_thm |
|
45 val mp = mp |
|
46 val not_elim = notE |
|
47 val classical = classical |
|
48 val hyp_subst_tacs=[hyp_subst_tac] |
|
49 end; |
|
50 |
|
51 structure Classical = ClassicalFun(Classical_Data); |
|
52 open Classical; |
|
53 |
|
54 (*Propositional rules*) |
|
55 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] |
|
56 addSEs [conjE,disjE,impCE,FalseE,iffE]; |
|
57 |
|
58 (*Quantifier rules*) |
|
59 val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] |
|
60 addSEs [exE,ex1E] addEs [allE]; |
|
61 |
|
62 use "simpdata.ML"; |
|
63 use_thy "Ord"; |
|
64 use_thy "subset"; |
|
65 use_thy "equalities"; |
|
66 use "hologic.ML"; |
|
67 use "subtype.ML"; |
|
68 use_thy "Prod"; |
|
69 use_thy "Sum"; |
|
70 use_thy "Gfp"; |
|
71 use_thy "Nat"; |
|
72 |
|
73 use "datatype.ML"; |
|
74 use "ind_syntax.ML"; |
|
75 use "add_ind_def.ML"; |
|
76 use "intr_elim.ML"; |
|
77 use "indrule.ML"; |
|
78 use_thy "Inductive"; |
|
79 |
|
80 use_thy "Finite"; |
|
81 use_thy "Sexp"; |
|
82 use_thy "List"; |
|
83 |
|
84 init_pps (); |
|
85 print_depth 8; |
|
86 |
|
87 val CHOL_build_completed = (); (*indicate successful build*) |