1 (* Title: FOLP/simpdata.ML |
1 (* Title: FOLP/simpdata.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
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 ***) |
9 (*** Rewrite rules ***) |
10 |
10 |
11 fun int_prove_fun_raw s = |
11 fun int_prove_fun_raw s = |
12 (writeln s; prove_goal IFOLP.thy s |
12 (writeln s; prove_goal (the_context ()) s |
13 (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ])); |
13 (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ])); |
14 |
14 |
15 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s); |
15 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s); |
16 |
16 |
17 val conj_rews = map int_prove_fun |
17 val conj_rews = map int_prove_fun |
30 val not_rews = map int_prove_fun |
30 val not_rews = map int_prove_fun |
31 ["~ False <-> True", "~ True <-> False"]; |
31 ["~ False <-> True", "~ True <-> False"]; |
32 |
32 |
33 val imp_rews = map int_prove_fun |
33 val imp_rews = map int_prove_fun |
34 ["(P --> False) <-> ~P", "(P --> True) <-> True", |
34 ["(P --> False) <-> ~P", "(P --> True) <-> True", |
35 "(False --> P) <-> True", "(True --> P) <-> P", |
35 "(False --> P) <-> True", "(True --> P) <-> P", |
36 "(P --> P) <-> True", "(P --> ~P) <-> ~P"]; |
36 "(P --> P) <-> True", "(P --> ~P) <-> ~P"]; |
37 |
37 |
38 val iff_rews = map int_prove_fun |
38 val iff_rews = map int_prove_fun |
39 ["(True <-> P) <-> P", "(P <-> True) <-> P", |
39 ["(True <-> P) <-> P", "(P <-> True) <-> P", |
40 "(P <-> P) <-> True", |
40 "(P <-> P) <-> True", |
68 val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)"; |
68 val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)"; |
69 |
69 |
70 fun mk_eq th = case concl_of th of |
70 fun mk_eq th = case concl_of th of |
71 _ $ (Const("op <->",_)$_$_) $ _ => th |
71 _ $ (Const("op <->",_)$_$_) $ _ => th |
72 | _ $ (Const("op =",_)$_$_) $ _ => th |
72 | _ $ (Const("op =",_)$_$_) $ _ => th |
73 | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F |
73 | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F |
74 | _ => make_iff_T th; |
74 | _ => make_iff_T th; |
75 |
75 |
76 |
76 |
77 val mksimps_pairs = |
77 val mksimps_pairs = |
78 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
78 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
111 end; |
111 end; |
112 |
112 |
113 structure FOLP_Simp = SimpFun(FOLP_SimpData); |
113 structure FOLP_Simp = SimpFun(FOLP_SimpData); |
114 |
114 |
115 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *) |
115 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *) |
116 val FOLP_congs = |
116 val FOLP_congs = |
117 [all_cong,ex_cong,eq_cong, |
117 [all_cong,ex_cong,eq_cong, |
118 conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs; |
118 conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs; |
119 |
119 |
120 val IFOLP_rews = |
120 val IFOLP_rews = |
121 [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ |
121 [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ |
122 imp_rews @ iff_rews @ quant_rews; |
122 imp_rews @ iff_rews @ quant_rews; |
123 |
123 |
124 open FOLP_Simp; |
124 open FOLP_Simp; |
125 |
125 |
126 val auto_ss = empty_ss setauto ares_tac [TrueI]; |
126 val auto_ss = empty_ss setauto ares_tac [TrueI]; |
127 |
127 |
128 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews; |
128 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews; |
129 |
129 |
130 (*Classical version...*) |
130 (*Classical version...*) |
131 fun prove_fun s = |
131 fun prove_fun s = |
132 (writeln s; prove_goal FOLP.thy s |
132 (writeln s; prove_goal (the_context ()) s |
133 (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ])); |
133 (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ])); |
134 |
134 |
135 val cla_rews = map prove_fun |
135 val cla_rews = map prove_fun |
136 ["?p:P | ~P", "?p:~P | P", |
136 ["?p:P | ~P", "?p:~P | P", |
137 "?p:~ ~ P <-> P", "?p:(~P --> P) <-> P"]; |
137 "?p:~ ~ P <-> P", "?p:(~P --> P) <-> P"]; |
138 |
138 |
139 val FOLP_rews = IFOLP_rews@cla_rews; |
139 val FOLP_rews = IFOLP_rews@cla_rews; |
140 |
140 |
141 val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews; |
141 val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews; |
142 |
|
143 |
|