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