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