author | wenzelm |
Fri, 04 Aug 2000 22:54:49 +0200 | |
changeset 9525 | 46fb9ccae463 |
parent 9300 | ee5c9672d208 |
child 9713 | 2c5b42311eb0 |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: FOL/simpdata |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
282 | 4 |
Copyright 1994 University of Cambridge |
0 | 5 |
|
6 |
Simplification data for FOL |
|
7 |
*) |
|
8 |
||
9300 | 9 |
(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *) |
10 |
||
11 |
infix 4 addIffs delIffs; |
|
12 |
||
13 |
(*Takes UNCONDITIONAL theorems of the form A<->B to |
|
14 |
the Safe Intr rule B==>A and |
|
15 |
the Safe Destruct rule A==>B. |
|
16 |
Also ~A goes to the Safe Elim rule A ==> ?R |
|
17 |
Failing other cases, A is added as a Safe Intr rule*) |
|
18 |
local |
|
19 |
fun addIff ((cla, simp), th) = |
|
20 |
(case FOLogic.dest_Trueprop (#prop (rep_thm th)) of |
|
21 |
(Const("Not", _) $ A) => |
|
22 |
cla addSEs [zero_var_indexes (th RS notE)] |
|
23 |
| (Const("op <->", _) $ _ $ _) => |
|
24 |
cla addSIs [zero_var_indexes (th RS iffD2)] |
|
25 |
addSDs [zero_var_indexes (th RS iffD1)] |
|
26 |
| _ => cla addSIs [th], |
|
27 |
simp addsimps [th]) |
|
28 |
handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ |
|
29 |
string_of_thm th); |
|
30 |
||
31 |
fun delIff ((cla, simp), th) = |
|
32 |
(case FOLogic.dest_Trueprop (#prop (rep_thm th)) of |
|
33 |
(Const ("Not", _) $ A) => |
|
34 |
cla delrules [zero_var_indexes (th RS notE)] |
|
35 |
| (Const("op <->", _) $ _ $ _) => |
|
36 |
cla delrules [zero_var_indexes (th RS iffD2), |
|
37 |
cla_make_elim (zero_var_indexes (th RS iffD1))] |
|
38 |
| _ => cla delrules [th], |
|
39 |
simp delsimps [th]) |
|
40 |
handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ |
|
41 |
string_of_thm th); (cla, simp)); |
|
42 |
||
43 |
fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp) |
|
44 |
in |
|
45 |
val op addIffs = foldl addIff; |
|
46 |
val op delIffs = foldl delIff; |
|
47 |
fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms); |
|
48 |
fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms); |
|
49 |
end; |
|
50 |
||
51 |
||
52 |
||
5496 | 53 |
(* Elimination of True from asumptions: *) |
54 |
||
55 |
val True_implies_equals = prove_goal IFOL.thy |
|
56 |
"(True ==> PROP P) == PROP P" |
|
57 |
(K [rtac equal_intr_rule 1, atac 2, |
|
58 |
METAHYPS (fn prems => resolve_tac prems 1) 1, |
|
59 |
rtac TrueI 1]); |
|
60 |
||
61 |
||
0 | 62 |
(*** Rewrite rules ***) |
63 |
||
64 |
fun int_prove_fun s = |
|
282 | 65 |
(writeln s; |
66 |
prove_goal IFOL.thy s |
|
67 |
(fn prems => [ (cut_facts_tac prems 1), |
|
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2469
diff
changeset
|
68 |
(IntPr.fast_tac 1) ])); |
0 | 69 |
|
1953 | 70 |
val conj_simps = map int_prove_fun |
1459 | 71 |
["P & True <-> P", "True & P <-> P", |
0 | 72 |
"P & False <-> False", "False & P <-> False", |
2801 | 73 |
"P & P <-> P", "P & P & Q <-> P & Q", |
1459 | 74 |
"P & ~P <-> False", "~P & P <-> False", |
0 | 75 |
"(P & Q) & R <-> P & (Q & R)"]; |
76 |
||
1953 | 77 |
val disj_simps = map int_prove_fun |
1459 | 78 |
["P | True <-> True", "True | P <-> True", |
79 |
"P | False <-> P", "False | P <-> P", |
|
2801 | 80 |
"P | P <-> P", "P | P | Q <-> P | Q", |
0 | 81 |
"(P | Q) | R <-> P | (Q | R)"]; |
82 |
||
1953 | 83 |
val not_simps = map int_prove_fun |
282 | 84 |
["~(P|Q) <-> ~P & ~Q", |
1459 | 85 |
"~ False <-> True", "~ True <-> False"]; |
0 | 86 |
|
1953 | 87 |
val imp_simps = map int_prove_fun |
1459 | 88 |
["(P --> False) <-> ~P", "(P --> True) <-> True", |
89 |
"(False --> P) <-> True", "(True --> P) <-> P", |
|
90 |
"(P --> P) <-> True", "(P --> ~P) <-> ~P"]; |
|
0 | 91 |
|
1953 | 92 |
val iff_simps = map int_prove_fun |
1459 | 93 |
["(True <-> P) <-> P", "(P <-> True) <-> P", |
0 | 94 |
"(P <-> P) <-> True", |
1459 | 95 |
"(False <-> P) <-> ~P", "(P <-> False) <-> ~P"]; |
0 | 96 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
97 |
(*The x=t versions are needed for the simplification procedures*) |
1953 | 98 |
val quant_simps = map int_prove_fun |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
99 |
["(ALL x. P) <-> P", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
100 |
"(ALL x. x=t --> P(x)) <-> P(t)", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
101 |
"(ALL x. t=x --> P(x)) <-> P(t)", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
102 |
"(EX x. P) <-> P", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
103 |
"(EX x. x=t & P(x)) <-> P(t)", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
104 |
"(EX x. t=x & P(x)) <-> P(t)"]; |
0 | 105 |
|
106 |
(*These are NOT supplied by default!*) |
|
1953 | 107 |
val distrib_simps = map int_prove_fun |
282 | 108 |
["P & (Q | R) <-> P&Q | P&R", |
109 |
"(Q | R) & P <-> Q&P | R&P", |
|
0 | 110 |
"(P | Q --> R) <-> (P --> R) & (Q --> R)"]; |
111 |
||
282 | 112 |
(** Conversion into rewrite rules **) |
0 | 113 |
|
53 | 114 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
115 |
||
282 | 116 |
val P_iff_F = int_prove_fun "~P ==> (P <-> False)"; |
117 |
val iff_reflection_F = P_iff_F RS iff_reflection; |
|
118 |
||
119 |
val P_iff_T = int_prove_fun "P ==> (P <-> True)"; |
|
120 |
val iff_reflection_T = P_iff_T RS iff_reflection; |
|
121 |
||
122 |
(*Make meta-equalities. The operator below is Trueprop*) |
|
5555 | 123 |
|
282 | 124 |
fun mk_meta_eq th = case concl_of th of |
5555 | 125 |
_ $ (Const("op =",_)$_$_) => th RS eq_reflection |
126 |
| _ $ (Const("op <->",_)$_$_) => th RS iff_reflection |
|
127 |
| _ => |
|
128 |
error("conclusion must be a =-equality or <->");; |
|
129 |
||
130 |
fun mk_eq th = case concl_of th of |
|
394
432bb9995893
Modified mk_meta_eq to leave meta-equlities on unchanged.
nipkow
parents:
371
diff
changeset
|
131 |
Const("==",_)$_$_ => th |
5555 | 132 |
| _ $ (Const("op =",_)$_$_) => mk_meta_eq th |
133 |
| _ $ (Const("op <->",_)$_$_) => mk_meta_eq th |
|
282 | 134 |
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F |
135 |
| _ => th RS iff_reflection_T; |
|
0 | 136 |
|
6114
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
137 |
(*Replace premises x=y, X<->Y by X==Y*) |
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
138 |
val mk_meta_prems = |
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
139 |
rule_by_tactic |
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
140 |
(REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff])); |
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
141 |
|
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
142 |
fun mk_meta_cong rl = |
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
143 |
standard(mk_meta_eq (mk_meta_prems rl)) |
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
144 |
handle THM _ => |
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
145 |
error("Premises and conclusion of congruence rules must use =-equality or <->"); |
5555 | 146 |
|
5304 | 147 |
val mksimps_pairs = |
148 |
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
|
149 |
("All", [spec]), ("True", []), ("False", [])]; |
|
150 |
||
5555 | 151 |
(* ###FIXME: move to Provers/simplifier.ML |
5304 | 152 |
val mk_atomize: (string * thm list) list -> thm -> thm list |
153 |
*) |
|
5555 | 154 |
(* ###FIXME: move to Provers/simplifier.ML *) |
5304 | 155 |
fun mk_atomize pairs = |
156 |
let fun atoms th = |
|
157 |
(case concl_of th of |
|
158 |
Const("Trueprop",_) $ p => |
|
159 |
(case head_of p of |
|
160 |
Const(a,_) => |
|
161 |
(case assoc(pairs,a) of |
|
162 |
Some(rls) => flat (map atoms ([th] RL rls)) |
|
163 |
| None => [th]) |
|
164 |
| _ => [th]) |
|
165 |
| _ => [th]) |
|
166 |
in atoms end; |
|
167 |
||
5555 | 168 |
fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all); |
981 | 169 |
|
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
170 |
(*** Classical laws ***) |
282 | 171 |
|
0 | 172 |
fun prove_fun s = |
282 | 173 |
(writeln s; |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset
|
174 |
prove_goal (the_context ()) s |
282 | 175 |
(fn prems => [ (cut_facts_tac prems 1), |
1459 | 176 |
(Cla.fast_tac FOL_cs 1) ])); |
745 | 177 |
|
1953 | 178 |
(*Avoids duplication of subgoals after expand_if, when the true and false |
179 |
cases boil down to the same thing.*) |
|
180 |
val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q"; |
|
181 |
||
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
182 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
183 |
(*** Miniscoping: pushing quantifiers in |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
184 |
We do NOT distribute of ALL over &, or dually that of EX over | |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
185 |
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
186 |
show that this step can increase proof length! |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
187 |
***) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
188 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
189 |
(*existential miniscoping*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
190 |
val int_ex_simps = map int_prove_fun |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
191 |
["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
192 |
"(EX x. P & Q(x)) <-> P & (EX x. Q(x))", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
193 |
"(EX x. P(x) | Q) <-> (EX x. P(x)) | Q", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
194 |
"(EX x. P | Q(x)) <-> P | (EX x. Q(x))"]; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
195 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
196 |
(*classical rules*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
197 |
val cla_ex_simps = map prove_fun |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
198 |
["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
199 |
"(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"]; |
0 | 200 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
201 |
val ex_simps = int_ex_simps @ cla_ex_simps; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
202 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
203 |
(*universal miniscoping*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
204 |
val int_all_simps = map int_prove_fun |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
205 |
["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
206 |
"(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
207 |
"(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
208 |
"(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"]; |
1953 | 209 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
210 |
(*classical rules*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
211 |
val cla_all_simps = map prove_fun |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
212 |
["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
213 |
"(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"]; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
214 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
215 |
val all_simps = int_all_simps @ cla_all_simps; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
216 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
217 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
218 |
(*** Named rewrite rules proved for IFOL ***) |
1953 | 219 |
|
1914 | 220 |
fun int_prove nm thm = qed_goal nm IFOL.thy thm |
221 |
(fn prems => [ (cut_facts_tac prems 1), |
|
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2469
diff
changeset
|
222 |
(IntPr.fast_tac 1) ]); |
1914 | 223 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset
|
224 |
fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [Blast_tac 1]); |
1914 | 225 |
|
226 |
int_prove "conj_commute" "P&Q <-> Q&P"; |
|
227 |
int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)"; |
|
228 |
val conj_comms = [conj_commute, conj_left_commute]; |
|
229 |
||
230 |
int_prove "disj_commute" "P|Q <-> Q|P"; |
|
231 |
int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)"; |
|
232 |
val disj_comms = [disj_commute, disj_left_commute]; |
|
233 |
||
234 |
int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)"; |
|
235 |
int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)"; |
|
236 |
||
237 |
int_prove "disj_conj_distribL" "P|(Q&R) <-> (P|Q) & (P|R)"; |
|
238 |
int_prove "disj_conj_distribR" "(P&Q)|R <-> (P|R) & (Q|R)"; |
|
239 |
||
240 |
int_prove "imp_conj_distrib" "(P --> (Q&R)) <-> (P-->Q) & (P-->R)"; |
|
241 |
int_prove "imp_conj" "((P&Q)-->R) <-> (P --> (Q --> R))"; |
|
242 |
int_prove "imp_disj" "(P|Q --> R) <-> (P-->R) & (Q-->R)"; |
|
243 |
||
3910 | 244 |
prove "imp_disj1" "(P-->Q) | R <-> (P-->Q | R)"; |
245 |
prove "imp_disj2" "Q | (P-->R) <-> (P-->Q | R)"; |
|
246 |
||
1914 | 247 |
int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)"; |
248 |
prove "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)"; |
|
249 |
||
250 |
prove "not_iff" "~(P <-> Q) <-> (P <-> ~Q)"; |
|
251 |
||
3835 | 252 |
prove "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))"; |
253 |
prove "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)"; |
|
254 |
int_prove "not_ex" "(~ (EX x. P(x))) <-> (ALL x.~P(x))"; |
|
1914 | 255 |
int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)"; |
256 |
||
257 |
int_prove "ex_disj_distrib" |
|
258 |
"(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))"; |
|
259 |
int_prove "all_conj_distrib" |
|
260 |
"(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))"; |
|
261 |
||
262 |
||
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
263 |
(** make simplification procedures for quantifier elimination **) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
264 |
structure Quantifier1 = Quantifier1Fun( |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
265 |
struct |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
266 |
(*abstract syntax*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
267 |
fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
268 |
| dest_eq _ = None; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
269 |
fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
270 |
| dest_conj _ = None; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
271 |
val conj = FOLogic.conj |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
272 |
val imp = FOLogic.imp |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
273 |
(*rules*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
274 |
val iff_reflection = iff_reflection |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
275 |
val iffI = iffI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
276 |
val sym = sym |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
277 |
val conjI= conjI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
278 |
val conjE= conjE |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
279 |
val impI = impI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
280 |
val impE = impE |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
281 |
val mp = mp |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
282 |
val exI = exI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
283 |
val exE = exE |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
284 |
val allI = allI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
285 |
val allE = allE |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
286 |
end); |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
287 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
288 |
local |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset
|
289 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
290 |
val ex_pattern = |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset
|
291 |
read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT) |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
292 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
293 |
val all_pattern = |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset
|
294 |
read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT) |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
295 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
296 |
in |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
297 |
val defEX_regroup = |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
298 |
mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
299 |
val defALL_regroup = |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
300 |
mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
301 |
end; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
302 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
303 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
304 |
(*** Case splitting ***) |
0 | 305 |
|
5304 | 306 |
val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y" |
307 |
(fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]); |
|
1722 | 308 |
|
5304 | 309 |
structure SplitterData = |
310 |
struct |
|
311 |
structure Simplifier = Simplifier |
|
5555 | 312 |
val mk_eq = mk_eq |
5304 | 313 |
val meta_eq_to_iff = meta_eq_to_iff |
314 |
val iffD = iffD2 |
|
315 |
val disjE = disjE |
|
316 |
val conjE = conjE |
|
317 |
val exE = exE |
|
318 |
val contrapos = contrapos |
|
319 |
val contrapos2 = contrapos2 |
|
320 |
val notnotD = notnotD |
|
321 |
end; |
|
1722 | 322 |
|
5304 | 323 |
structure Splitter = SplitterFun(SplitterData); |
1722 | 324 |
|
5304 | 325 |
val split_tac = Splitter.split_tac; |
326 |
val split_inside_tac = Splitter.split_inside_tac; |
|
327 |
val split_asm_tac = Splitter.split_asm_tac; |
|
5307 | 328 |
val op addsplits = Splitter.addsplits; |
329 |
val op delsplits = Splitter.delsplits; |
|
5304 | 330 |
val Addsplits = Splitter.Addsplits; |
331 |
val Delsplits = Splitter.Delsplits; |
|
4325 | 332 |
|
333 |
||
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
334 |
(*** Standard simpsets ***) |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
335 |
|
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
336 |
structure Induction = InductionFun(struct val spec=IFOL.spec end); |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
337 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
338 |
open Induction; |
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
339 |
|
5555 | 340 |
|
341 |
(* Add congruence rules for = or <-> (instead of ==) *) |
|
342 |
||
343 |
(* ###FIXME: Move to simplifier, |
|
344 |
taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *) |
|
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
345 |
infix 4 addcongs delcongs; |
5555 | 346 |
fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs); |
347 |
fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs); |
|
4094 | 348 |
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); |
349 |
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); |
|
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
350 |
|
8643 | 351 |
val cong_add_global = Simplifier.change_global_ss (op addcongs); |
352 |
val cong_del_global = Simplifier.change_global_ss (op delcongs); |
|
353 |
val cong_add_local = Simplifier.change_local_ss (op addcongs); |
|
354 |
val cong_del_local = Simplifier.change_local_ss (op delcongs); |
|
355 |
||
356 |
val cong_attrib_setup = |
|
357 |
[Attrib.add_attributes [("cong", |
|
358 |
(Attrib.add_del_args cong_add_global cong_del_global, |
|
359 |
Attrib.add_del_args cong_add_local cong_del_local), |
|
360 |
"declare Simplifier congruence rules")]]; |
|
361 |
||
5115 | 362 |
|
5496 | 363 |
val meta_simps = |
364 |
[triv_forall_equality, (* prunes params *) |
|
365 |
True_implies_equals]; (* prune asms `True' *) |
|
366 |
||
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
367 |
val IFOL_simps = |
6114
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
368 |
[refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ |
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
369 |
imp_simps @ iff_simps @ quant_simps; |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
370 |
|
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
371 |
val notFalseI = int_prove_fun "~False"; |
6114
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
372 |
val triv_rls = [TrueI,refl,reflexive_thm,iff_refl,notFalseI]; |
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
373 |
|
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
374 |
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems), |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
375 |
atac, etac FalseE]; |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
376 |
(*No premature instantiation of variables during simplification*) |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
377 |
fun safe_solver prems = FIRST'[match_tac (triv_rls@prems), |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
378 |
eq_assume_tac, ematch_tac [FalseE]]; |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
379 |
|
3910 | 380 |
(*No simprules, but basic infastructure for simplification*) |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
381 |
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
382 |
addsimprocs [defALL_regroup,defEX_regroup] |
7570 | 383 |
setSSolver (mk_solver "FOL safe" safe_solver) |
384 |
setSolver (mk_solver "FOL unsafe" unsafe_solver) |
|
5304 | 385 |
setmksimps (mksimps mksimps_pairs); |
386 |
||
387 |
||
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
388 |
|
3910 | 389 |
(*intuitionistic simprules only*) |
5496 | 390 |
val IFOL_ss = |
391 |
FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ |
|
392 |
int_ex_simps @ int_all_simps) |
|
393 |
addcongs [imp_cong]; |
|
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
394 |
|
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
395 |
val cla_simps = |
3910 | 396 |
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, |
397 |
not_all, not_ex, cases_simp] @ |
|
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
398 |
map prove_fun |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
399 |
["~(P&Q) <-> ~P | ~Q", |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
400 |
"P | ~P", "~P | P", |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
401 |
"~ ~ P <-> P", "(~P --> P) <-> P", |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
402 |
"(~P <-> ~Q) <-> (P<->Q)"]; |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
403 |
|
3910 | 404 |
(*classical simprules too*) |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
405 |
val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps); |
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
406 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset
|
407 |
val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)]; |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
408 |
|
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
409 |
|
5219 | 410 |
(*** integration of simplifier with classical reasoner ***) |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
411 |
|
5219 | 412 |
structure Clasimp = ClasimpFun |
8472 | 413 |
(structure Simplifier = Simplifier and Splitter = Splitter |
414 |
and Classical = Cla and Blast = Blast); |
|
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset
|
415 |
open Clasimp; |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
416 |
|
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
417 |
val FOL_css = (FOL_cs, FOL_ss); |