12 (writeln s; |
12 (writeln s; |
13 prove_goal IFOL.thy s |
13 prove_goal IFOL.thy s |
14 (fn prems => [ (cut_facts_tac prems 1), |
14 (fn prems => [ (cut_facts_tac prems 1), |
15 (Int.fast_tac 1) ])); |
15 (Int.fast_tac 1) ])); |
16 |
16 |
17 val conj_rews = map int_prove_fun |
17 val conj_simps = map int_prove_fun |
18 ["P & True <-> P", "True & P <-> P", |
18 ["P & True <-> P", "True & P <-> P", |
19 "P & False <-> False", "False & P <-> False", |
19 "P & False <-> False", "False & P <-> False", |
20 "P & P <-> P", |
20 "P & P <-> P", |
21 "P & ~P <-> False", "~P & P <-> False", |
21 "P & ~P <-> False", "~P & P <-> False", |
22 "(P & Q) & R <-> P & (Q & R)"]; |
22 "(P & Q) & R <-> P & (Q & R)"]; |
23 |
23 |
24 val disj_rews = map int_prove_fun |
24 val disj_simps = map int_prove_fun |
25 ["P | True <-> True", "True | P <-> True", |
25 ["P | True <-> True", "True | P <-> True", |
26 "P | False <-> P", "False | P <-> P", |
26 "P | False <-> P", "False | P <-> P", |
27 "P | P <-> P", |
27 "P | P <-> P", |
28 "(P | Q) | R <-> P | (Q | R)"]; |
28 "(P | Q) | R <-> P | (Q | R)"]; |
29 |
29 |
30 val not_rews = map int_prove_fun |
30 val not_simps = map int_prove_fun |
31 ["~(P|Q) <-> ~P & ~Q", |
31 ["~(P|Q) <-> ~P & ~Q", |
32 "~ False <-> True", "~ True <-> False"]; |
32 "~ False <-> True", "~ True <-> False"]; |
33 |
33 |
34 val imp_rews = map int_prove_fun |
34 val imp_simps = map int_prove_fun |
35 ["(P --> False) <-> ~P", "(P --> True) <-> True", |
35 ["(P --> False) <-> ~P", "(P --> True) <-> True", |
36 "(False --> P) <-> True", "(True --> P) <-> P", |
36 "(False --> P) <-> True", "(True --> P) <-> P", |
37 "(P --> P) <-> True", "(P --> ~P) <-> ~P"]; |
37 "(P --> P) <-> True", "(P --> ~P) <-> ~P"]; |
38 |
38 |
39 val iff_rews = map int_prove_fun |
39 val iff_simps = map int_prove_fun |
40 ["(True <-> P) <-> P", "(P <-> True) <-> P", |
40 ["(True <-> P) <-> P", "(P <-> True) <-> P", |
41 "(P <-> P) <-> True", |
41 "(P <-> P) <-> True", |
42 "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"]; |
42 "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"]; |
43 |
43 |
44 val quant_rews = map int_prove_fun |
44 val quant_simps = map int_prove_fun |
45 ["(ALL x.P) <-> P", "(EX x.P) <-> P"]; |
45 ["(ALL x.P) <-> P", "(EX x.P) <-> P"]; |
46 |
46 |
47 (*These are NOT supplied by default!*) |
47 (*These are NOT supplied by default!*) |
48 val distrib_rews = map int_prove_fun |
48 val distrib_simps = map int_prove_fun |
49 ["P & (Q | R) <-> P&Q | P&R", |
49 ["P & (Q | R) <-> P&Q | P&R", |
50 "(Q | R) & P <-> Q&P | R&P", |
50 "(Q | R) & P <-> Q&P | R&P", |
51 "(P | Q --> R) <-> (P --> R) & (Q --> R)"]; |
51 "(P | Q --> R) <-> (P --> R) & (Q --> R)"]; |
52 |
52 |
53 (** Conversion into rewrite rules **) |
53 (** Conversion into rewrite rules **) |
109 setmksimps (map mk_meta_eq o atomize o gen_all) |
109 setmksimps (map mk_meta_eq o atomize o gen_all) |
110 setsolver (fn prems => resolve_tac (triv_rls@prems) |
110 setsolver (fn prems => resolve_tac (triv_rls@prems) |
111 ORELSE' assume_tac |
111 ORELSE' assume_tac |
112 ORELSE' etac FalseE) |
112 ORELSE' etac FalseE) |
113 setsubgoaler asm_simp_tac |
113 setsubgoaler asm_simp_tac |
114 addsimps IFOL_rews |
114 addsimps IFOL_simps |
115 addcongs [imp_cong]; |
115 addcongs [imp_cong]; |
116 |
116 |
117 (*Classical version...*) |
117 (*Classical version...*) |
118 fun prove_fun s = |
118 fun prove_fun s = |
119 (writeln s; |
119 (writeln s; |
120 prove_goal FOL.thy s |
120 prove_goal FOL.thy s |
121 (fn prems => [ (cut_facts_tac prems 1), |
121 (fn prems => [ (cut_facts_tac prems 1), |
122 (Cla.fast_tac FOL_cs 1) ])); |
122 (Cla.fast_tac FOL_cs 1) ])); |
123 |
123 |
124 val cla_rews = map prove_fun |
124 (*Avoids duplication of subgoals after expand_if, when the true and false |
125 ["~(P&Q) <-> ~P | ~Q", |
125 cases boil down to the same thing.*) |
126 "P | ~P", "~P | P", |
126 val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q"; |
127 "~ ~ P <-> P", "(~P --> P) <-> P"]; |
127 |
128 |
128 val cla_simps = |
129 val FOL_ss = IFOL_ss addsimps cla_rews; |
129 cases_simp:: |
|
130 map prove_fun |
|
131 ["~(P&Q) <-> ~P | ~Q", |
|
132 "P | ~P", "~P | P", |
|
133 "~ ~ P <-> P", "(~P --> P) <-> P", |
|
134 "(~P <-> ~Q) <-> (P<->Q)"]; |
|
135 |
|
136 (*At present, miniscoping is for classical logic only. We do NOT include |
|
137 distribution of ALL over &, or dually that of EX over |.*) |
|
138 |
|
139 (*Miniscoping: pushing in existential quantifiers*) |
|
140 val ex_simps = map prove_fun |
|
141 ["(EX x. P) <-> P", |
|
142 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q", |
|
143 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))", |
|
144 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q", |
|
145 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))", |
|
146 "(EX x. P(x) --> Q) <-> (ALL x.P(x)) --> Q", |
|
147 "(EX x. P --> Q(x)) <-> P --> (EX x.Q(x))"]; |
|
148 |
|
149 (*Miniscoping: pushing in universal quantifiers*) |
|
150 val all_simps = map prove_fun |
|
151 ["(ALL x. P) <-> P", |
|
152 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q", |
|
153 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))", |
|
154 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q", |
|
155 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))", |
|
156 "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q", |
|
157 "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"]; |
|
158 |
|
159 val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps); |
130 |
160 |
131 fun int_prove nm thm = qed_goal nm IFOL.thy thm |
161 fun int_prove nm thm = qed_goal nm IFOL.thy thm |
132 (fn prems => [ (cut_facts_tac prems 1), |
162 (fn prems => [ (cut_facts_tac prems 1), |
133 (Int.fast_tac 1) ]); |
163 (Int.fast_tac 1) ]); |
134 |
164 |