1 (* Title: FOLP/ROOT |
1 (* Title: FOLP/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: martin Coen, Cambridge University Computer Laboratory |
3 Author: martin Coen, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Modifed version of Lawrence Paulson's FOL that contains proof terms. |
6 Modifed version of Lawrence Paulson's FOL that contains proof terms. |
7 |
7 |
8 Presence of unknown proof term means that matching does not behave as expected. |
8 Presence of unknown proof term means that matching does not behave as expected. |
9 *) |
9 *) |
10 |
10 |
11 val banner = "First-Order Logic with Natural Deduction with Proof Terms"; |
11 val banner = "First-Order Logic with Natural Deduction with Proof Terms"; |
12 |
|
13 writeln banner; |
12 writeln banner; |
14 |
13 |
15 print_depth 1; |
|
16 |
|
17 use_thy "IFOLP"; |
|
18 use_thy "FOLP"; |
14 use_thy "FOLP"; |
19 |
|
20 use "hypsubst.ML"; |
|
21 use "classical.ML"; (* Patched 'cos matching won't instantiate proof *) |
|
22 use "simp.ML"; (* Patched 'cos matching won't instantiate proof *) |
|
23 |
|
24 |
|
25 (*** Applying HypsubstFun to generate hyp_subst_tac ***) |
|
26 |
|
27 structure Hypsubst_Data = |
|
28 struct |
|
29 (*Take apart an equality judgement; otherwise raise Match!*) |
|
30 fun dest_eq (Const("Proof",_) $ (Const("op =",_) $ t $ u) $ _) = (t,u); |
|
31 |
|
32 val imp_intr = impI |
|
33 |
|
34 (*etac rev_cut_eq moves an equality to be the last premise. *) |
|
35 val rev_cut_eq = prove_goal IFOLP.thy |
|
36 "[| p:a=b; !!x. x:a=b ==> f(x):R |] ==> ?p:R" |
|
37 (fn prems => [ REPEAT(resolve_tac prems 1) ]); |
|
38 |
|
39 val rev_mp = rev_mp |
|
40 val subst = subst |
|
41 val sym = sym |
|
42 val thin_refl = prove_goal IFOLP.thy |
|
43 "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]); |
|
44 end; |
|
45 |
|
46 structure Hypsubst = HypsubstFun(Hypsubst_Data); |
|
47 open Hypsubst; |
|
48 |
|
49 use "intprover.ML"; |
|
50 |
|
51 (*** Applying ClassicalFun to create a classical prover ***) |
|
52 structure Classical_Data = |
|
53 struct |
|
54 val sizef = size_of_thm |
|
55 val mp = mp |
|
56 val not_elim = notE |
|
57 val swap = swap |
|
58 val hyp_subst_tacs=[hyp_subst_tac] |
|
59 end; |
|
60 |
|
61 structure Cla = ClassicalFun(Classical_Data); |
|
62 open Cla; |
|
63 |
|
64 (*Propositional rules |
|
65 -- iffCE might seem better, but in the examples in ex/cla |
|
66 run about 7% slower than with iffE*) |
|
67 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] |
|
68 addSEs [conjE,disjE,impCE,FalseE,iffE]; |
|
69 |
|
70 (*Quantifier rules*) |
|
71 val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I] |
|
72 addSEs [exE,ex1E] addEs [allE]; |
|
73 |
|
74 val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] |
|
75 addSEs [exE,ex1E] addEs [all_dupE]; |
|
76 |
|
77 use "simpdata.ML"; |
|
78 |
|
79 |
|
80 print_depth 8; |
|