|
1 (* Title: FOL/simpdata |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Simplification data for FOL |
|
7 *) |
|
8 |
|
9 (*** Rewrite rules ***) |
|
10 |
|
11 fun int_prove_fun_raw s = |
|
12 (writeln s; prove_goal IFOLP.thy s |
|
13 (fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ])); |
|
14 |
|
15 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s); |
|
16 |
|
17 val conj_rews = map int_prove_fun |
|
18 ["P & True <-> P", "True & P <-> P", |
|
19 "P & False <-> False", "False & P <-> False", |
|
20 "P & P <-> P", |
|
21 "P & ~P <-> False", "~P & P <-> False", |
|
22 "(P & Q) & R <-> P & (Q & R)"]; |
|
23 |
|
24 val disj_rews = map int_prove_fun |
|
25 ["P | True <-> True", "True | P <-> True", |
|
26 "P | False <-> P", "False | P <-> P", |
|
27 "P | P <-> P", |
|
28 "(P | Q) | R <-> P | (Q | R)"]; |
|
29 |
|
30 val not_rews = map int_prove_fun |
|
31 ["~ False <-> True", "~ True <-> False"]; |
|
32 |
|
33 val imp_rews = map int_prove_fun |
|
34 ["(P --> False) <-> ~P", "(P --> True) <-> True", |
|
35 "(False --> P) <-> True", "(True --> P) <-> P", |
|
36 "(P --> P) <-> True", "(P --> ~P) <-> ~P"]; |
|
37 |
|
38 val iff_rews = map int_prove_fun |
|
39 ["(True <-> P) <-> P", "(P <-> True) <-> P", |
|
40 "(P <-> P) <-> True", |
|
41 "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"]; |
|
42 |
|
43 val quant_rews = map int_prove_fun |
|
44 ["(ALL x.P) <-> P", "(EX x.P) <-> P"]; |
|
45 |
|
46 (*These are NOT supplied by default!*) |
|
47 val distrib_rews = map int_prove_fun |
|
48 ["~(P|Q) <-> ~P & ~Q", |
|
49 "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P", |
|
50 "(P | Q --> R) <-> (P --> R) & (Q --> R)", |
|
51 "~(EX x.NORM(P(x))) <-> (ALL x. ~NORM(P(x)))", |
|
52 "((EX x.NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)", |
|
53 "(EX x.NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))", |
|
54 "NORM(Q) & (EX x.NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"]; |
|
55 |
|
56 val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)"; |
|
57 |
|
58 fun make_iff_T th = th RS P_Imp_P_iff_T; |
|
59 |
|
60 val refl_iff_T = make_iff_T refl; |
|
61 |
|
62 val norm_thms = [(norm_eq RS sym, norm_eq), |
|
63 (NORM_iff RS iff_sym, NORM_iff)]; |
|
64 |
|
65 |
|
66 (* Conversion into rewrite rules *) |
|
67 |
|
68 val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)"; |
|
69 |
|
70 fun mk_eq th = case concl_of th of |
|
71 _ $ (Const("op <->",_)$_$_) $ _ => th |
|
72 | _ $ (Const("op =",_)$_$_) $ _ => th |
|
73 | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F |
|
74 | _ => make_iff_T th; |
|
75 |
|
76 fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*) |
|
77 _ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp) |
|
78 | _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @ |
|
79 atomize(th RS conjunct2) |
|
80 | _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec) |
|
81 | _ $ (Const("True",_)) $ _ => [] |
|
82 | _ $ (Const("False",_)) $ _ => [] |
|
83 | _ => [th]; |
|
84 |
|
85 fun mk_rew_rules th = map mk_eq (atomize th); |
|
86 |
|
87 (*destruct function for analysing equations*) |
|
88 fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs) |
|
89 | dest_red t = raise TERM("FOL/dest_red", [t]); |
|
90 |
|
91 structure FOLP_SimpData : SIMP_DATA = |
|
92 struct |
|
93 val refl_thms = [refl, iff_refl] |
|
94 val trans_thms = [trans, iff_trans] |
|
95 val red1 = iffD1 |
|
96 val red2 = iffD2 |
|
97 val mk_rew_rules = mk_rew_rules |
|
98 val case_splits = [] (*NO IF'S!*) |
|
99 val norm_thms = norm_thms |
|
100 val subst_thms = [subst]; |
|
101 val dest_red = dest_red |
|
102 end; |
|
103 |
|
104 structure FOLP_Simp = SimpFun(FOLP_SimpData); |
|
105 structure Induction = InductionFun(struct val spec=IFOLP.spec end); |
|
106 |
|
107 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *) |
|
108 val FOLP_congs = |
|
109 [all_cong,ex_cong,eq_cong, |
|
110 conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs; |
|
111 |
|
112 val IFOLP_rews = |
|
113 [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ |
|
114 imp_rews @ iff_rews @ quant_rews; |
|
115 |
|
116 open FOLP_Simp Induction; |
|
117 |
|
118 val auto_ss = empty_ss setauto ares_tac [TrueI]; |
|
119 |
|
120 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews; |
|
121 |
|
122 (*Classical version...*) |
|
123 fun prove_fun s = |
|
124 (writeln s; prove_goal FOLP.thy s |
|
125 (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ])); |
|
126 |
|
127 val cla_rews = map prove_fun |
|
128 ["?p:P | ~P", "?p:~P | P", |
|
129 "?p:~ ~ P <-> P", "?p:(~P --> P) <-> P"]; |
|
130 |
|
131 val FOLP_rews = IFOLP_rews@cla_rews; |
|
132 |
|
133 val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews; |
|
134 |
|
135 |