|
1 (* Title: HOL/ROOT |
|
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"; |
|
11 writeln banner; |
|
12 |
|
13 print_depth 1; |
|
14 eta_contract := true; |
|
15 use_thy "hol"; |
|
16 use "../Provers/hypsubst.ML"; |
|
17 use "../Provers/classical.ML"; |
|
18 use "../Provers/simplifier.ML"; |
|
19 use "../Provers/splitter.ML"; |
|
20 use "../Provers/ind.ML"; |
|
21 |
|
22 (** Applying HypsubstFun to generate hyp_subst_tac **) |
|
23 |
|
24 structure Hypsubst_Data = |
|
25 struct |
|
26 (*Take apart an equality judgement; otherwise raise Match!*) |
|
27 fun dest_eq (Const("Trueprop",_) $ (Const("op =",_) $ t $ u)) = (t,u); |
|
28 |
|
29 val imp_intr = impI |
|
30 |
|
31 (*etac rev_cut_eq moves an equality to be the last premise. *) |
|
32 val rev_cut_eq = prove_goal HOL.thy "[| a=b; a=b ==> R |] ==> R" |
|
33 (fn prems => [ REPEAT(resolve_tac prems 1) ]); |
|
34 |
|
35 val rev_mp = rev_mp |
|
36 val subst = subst |
|
37 val sym = sym |
|
38 end; |
|
39 |
|
40 structure Hypsubst = HypsubstFun(Hypsubst_Data); |
|
41 open Hypsubst; |
|
42 |
|
43 (** Applying ClassicalFun to create a classical prover **) |
|
44 structure Classical_Data = |
|
45 struct |
|
46 val sizef = size_of_thm |
|
47 val mp = mp |
|
48 val not_elim = notE |
|
49 val swap = swap |
|
50 val hyp_subst_tacs=[hyp_subst_tac] |
|
51 end; |
|
52 |
|
53 structure Classical = ClassicalFun(Classical_Data); |
|
54 open Classical; |
|
55 |
|
56 (*Propositional rules*) |
|
57 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] |
|
58 addSEs [conjE,disjE,impCE,FalseE,iffE]; |
|
59 |
|
60 (*Quantifier rules*) |
|
61 val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] |
|
62 addSEs [exE,ex1E] addEs [allE]; |
|
63 |
|
64 val HOL_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] |
|
65 addSEs [exE,ex1E] addEs [all_dupE]; |
|
66 |
|
67 structure HOL_Induction = InductionFun(struct val spec=spec end); |
|
68 open HOL_Induction; |
|
69 |
|
70 use "simpdata.ML"; |
|
71 use_thy "ord"; |
|
72 use_thy "set"; |
|
73 use "fun.ML"; |
|
74 use "subset.ML"; |
|
75 use "equalities.ML"; |
|
76 use_thy "prod"; |
|
77 use_thy "sum"; |
|
78 use "mono.ML"; |
|
79 use_thy "lfp"; |
|
80 use_thy "gfp"; |
|
81 use_thy "trancl"; |
|
82 use_thy "wf"; |
|
83 use_thy "nat"; |
|
84 use_thy "arith"; |
|
85 use_thy "univ"; |
|
86 use_thy "sexp"; |
|
87 use_thy "list"; |
|
88 use_thy "llist"; |
|
89 |
|
90 use "../Pure/install_pp.ML"; |
|
91 print_depth 8; |
|
92 |
|
93 val HOL_build_completed = (); (*indicate successful build*) |