author | oheimb |
Thu, 14 May 1998 16:50:09 +0200 | |
changeset 4930 | 89271bc4e7ed |
parent 4794 | 9db0916ecdae |
child 5115 | caf39b7b7a12 |
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 |
||
9 |
(*** Rewrite rules ***) |
|
10 |
||
11 |
fun int_prove_fun s = |
|
282 | 12 |
(writeln s; |
13 |
prove_goal IFOL.thy s |
|
14 |
(fn prems => [ (cut_facts_tac prems 1), |
|
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2469
diff
changeset
|
15 |
(IntPr.fast_tac 1) ])); |
0 | 16 |
|
1953 | 17 |
val conj_simps = map int_prove_fun |
1459 | 18 |
["P & True <-> P", "True & P <-> P", |
0 | 19 |
"P & False <-> False", "False & P <-> False", |
2801 | 20 |
"P & P <-> P", "P & P & Q <-> P & Q", |
1459 | 21 |
"P & ~P <-> False", "~P & P <-> False", |
0 | 22 |
"(P & Q) & R <-> P & (Q & R)"]; |
23 |
||
1953 | 24 |
val disj_simps = map int_prove_fun |
1459 | 25 |
["P | True <-> True", "True | P <-> True", |
26 |
"P | False <-> P", "False | P <-> P", |
|
2801 | 27 |
"P | P <-> P", "P | P | Q <-> P | Q", |
0 | 28 |
"(P | Q) | R <-> P | (Q | R)"]; |
29 |
||
1953 | 30 |
val not_simps = map int_prove_fun |
282 | 31 |
["~(P|Q) <-> ~P & ~Q", |
1459 | 32 |
"~ False <-> True", "~ True <-> False"]; |
0 | 33 |
|
1953 | 34 |
val imp_simps = map int_prove_fun |
1459 | 35 |
["(P --> False) <-> ~P", "(P --> True) <-> True", |
36 |
"(False --> P) <-> True", "(True --> P) <-> P", |
|
37 |
"(P --> P) <-> True", "(P --> ~P) <-> ~P"]; |
|
0 | 38 |
|
1953 | 39 |
val iff_simps = map int_prove_fun |
1459 | 40 |
["(True <-> P) <-> P", "(P <-> True) <-> P", |
0 | 41 |
"(P <-> P) <-> True", |
1459 | 42 |
"(False <-> P) <-> ~P", "(P <-> False) <-> ~P"]; |
0 | 43 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
44 |
(*The x=t versions are needed for the simplification procedures*) |
1953 | 45 |
val quant_simps = map int_prove_fun |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
46 |
["(ALL x. P) <-> P", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
47 |
"(ALL x. x=t --> P(x)) <-> P(t)", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
48 |
"(ALL x. t=x --> P(x)) <-> P(t)", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
49 |
"(EX x. P) <-> P", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
50 |
"(EX x. x=t & P(x)) <-> P(t)", |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
51 |
"(EX x. t=x & P(x)) <-> P(t)"]; |
0 | 52 |
|
53 |
(*These are NOT supplied by default!*) |
|
1953 | 54 |
val distrib_simps = map int_prove_fun |
282 | 55 |
["P & (Q | R) <-> P&Q | P&R", |
56 |
"(Q | R) & P <-> Q&P | R&P", |
|
0 | 57 |
"(P | Q --> R) <-> (P --> R) & (Q --> R)"]; |
58 |
||
282 | 59 |
(** Conversion into rewrite rules **) |
0 | 60 |
|
53 | 61 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
62 |
||
282 | 63 |
(*Make atomic rewrite rules*) |
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
64 |
fun atomize r = |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
65 |
case concl_of r of |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
66 |
Const("Trueprop",_) $ p => |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
67 |
(case p of |
1459 | 68 |
Const("op -->",_)$_$_ => atomize(r RS mp) |
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
69 |
| Const("op &",_)$_$_ => atomize(r RS conjunct1) @ |
1459 | 70 |
atomize(r RS conjunct2) |
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
71 |
| Const("All",_)$_ => atomize(r RS spec) |
1459 | 72 |
| Const("True",_) => [] (*True is DELETED*) |
73 |
| Const("False",_) => [] (*should False do something?*) |
|
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
74 |
| _ => [r]) |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
75 |
| _ => [r]; |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
76 |
|
282 | 77 |
|
78 |
val P_iff_F = int_prove_fun "~P ==> (P <-> False)"; |
|
79 |
val iff_reflection_F = P_iff_F RS iff_reflection; |
|
80 |
||
81 |
val P_iff_T = int_prove_fun "P ==> (P <-> True)"; |
|
82 |
val iff_reflection_T = P_iff_T RS iff_reflection; |
|
83 |
||
84 |
(*Make meta-equalities. The operator below is Trueprop*) |
|
85 |
fun mk_meta_eq th = case concl_of th of |
|
394
432bb9995893
Modified mk_meta_eq to leave meta-equlities on unchanged.
nipkow
parents:
371
diff
changeset
|
86 |
Const("==",_)$_$_ => th |
432bb9995893
Modified mk_meta_eq to leave meta-equlities on unchanged.
nipkow
parents:
371
diff
changeset
|
87 |
| _ $ (Const("op =",_)$_$_) => th RS eq_reflection |
282 | 88 |
| _ $ (Const("op <->",_)$_$_) => th RS iff_reflection |
89 |
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F |
|
90 |
| _ => th RS iff_reflection_T; |
|
0 | 91 |
|
981 | 92 |
|
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
93 |
(*** Classical laws ***) |
282 | 94 |
|
0 | 95 |
fun prove_fun s = |
282 | 96 |
(writeln s; |
97 |
prove_goal FOL.thy s |
|
98 |
(fn prems => [ (cut_facts_tac prems 1), |
|
1459 | 99 |
(Cla.fast_tac FOL_cs 1) ])); |
745 | 100 |
|
1953 | 101 |
(*Avoids duplication of subgoals after expand_if, when the true and false |
102 |
cases boil down to the same thing.*) |
|
103 |
val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q"; |
|
104 |
||
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
105 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
106 |
(*** Miniscoping: pushing quantifiers in |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
107 |
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
|
108 |
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
109 |
show that this step can increase proof length! |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
110 |
***) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
111 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
112 |
(*existential miniscoping*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
113 |
val int_ex_simps = map int_prove_fun |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
114 |
["(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
|
115 |
"(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
|
116 |
"(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
|
117 |
"(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
|
118 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
119 |
(*classical rules*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
120 |
val cla_ex_simps = map prove_fun |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
121 |
["(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
|
122 |
"(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"]; |
0 | 123 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
124 |
val ex_simps = int_ex_simps @ cla_ex_simps; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
125 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
126 |
(*universal miniscoping*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
127 |
val int_all_simps = map int_prove_fun |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
128 |
["(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
|
129 |
"(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
|
130 |
"(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
|
131 |
"(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"]; |
1953 | 132 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
133 |
(*classical rules*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
134 |
val cla_all_simps = map prove_fun |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
135 |
["(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
|
136 |
"(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
|
137 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
138 |
val all_simps = int_all_simps @ cla_all_simps; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
139 |
|
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 |
(*** Named rewrite rules proved for IFOL ***) |
1953 | 142 |
|
1914 | 143 |
fun int_prove nm thm = qed_goal nm IFOL.thy thm |
144 |
(fn prems => [ (cut_facts_tac prems 1), |
|
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2469
diff
changeset
|
145 |
(IntPr.fast_tac 1) ]); |
1914 | 146 |
|
3910 | 147 |
fun prove nm thm = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]); |
1914 | 148 |
|
149 |
int_prove "conj_commute" "P&Q <-> Q&P"; |
|
150 |
int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)"; |
|
151 |
val conj_comms = [conj_commute, conj_left_commute]; |
|
152 |
||
153 |
int_prove "disj_commute" "P|Q <-> Q|P"; |
|
154 |
int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)"; |
|
155 |
val disj_comms = [disj_commute, disj_left_commute]; |
|
156 |
||
157 |
int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)"; |
|
158 |
int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)"; |
|
159 |
||
160 |
int_prove "disj_conj_distribL" "P|(Q&R) <-> (P|Q) & (P|R)"; |
|
161 |
int_prove "disj_conj_distribR" "(P&Q)|R <-> (P|R) & (Q|R)"; |
|
162 |
||
163 |
int_prove "imp_conj_distrib" "(P --> (Q&R)) <-> (P-->Q) & (P-->R)"; |
|
164 |
int_prove "imp_conj" "((P&Q)-->R) <-> (P --> (Q --> R))"; |
|
165 |
int_prove "imp_disj" "(P|Q --> R) <-> (P-->R) & (Q-->R)"; |
|
166 |
||
3910 | 167 |
prove "imp_disj1" "(P-->Q) | R <-> (P-->Q | R)"; |
168 |
prove "imp_disj2" "Q | (P-->R) <-> (P-->Q | R)"; |
|
169 |
||
1914 | 170 |
int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)"; |
171 |
prove "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)"; |
|
172 |
||
173 |
prove "not_iff" "~(P <-> Q) <-> (P <-> ~Q)"; |
|
174 |
||
3835 | 175 |
prove "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))"; |
176 |
prove "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)"; |
|
177 |
int_prove "not_ex" "(~ (EX x. P(x))) <-> (ALL x.~P(x))"; |
|
1914 | 178 |
int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)"; |
179 |
||
180 |
int_prove "ex_disj_distrib" |
|
181 |
"(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))"; |
|
182 |
int_prove "all_conj_distrib" |
|
183 |
"(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))"; |
|
184 |
||
185 |
||
1088
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset
|
186 |
(*Used in ZF, perhaps elsewhere?*) |
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset
|
187 |
val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y" |
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset
|
188 |
(fn [prem] => [rewtac prem, rtac refl 1]); |
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset
|
189 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
190 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
191 |
(** make simplification procedures for quantifier elimination **) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
192 |
structure Quantifier1 = Quantifier1Fun( |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
193 |
struct |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
194 |
(*abstract syntax*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
195 |
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
|
196 |
| dest_eq _ = None; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
197 |
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
|
198 |
| dest_conj _ = None; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
199 |
val conj = FOLogic.conj |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
200 |
val imp = FOLogic.imp |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
201 |
(*rules*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
202 |
val iff_reflection = iff_reflection |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
203 |
val iffI = iffI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
204 |
val sym = sym |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
205 |
val conjI= conjI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
206 |
val conjE= conjE |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
207 |
val impI = impI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
208 |
val impE = impE |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
209 |
val mp = mp |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
210 |
val exI = exI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
211 |
val exE = exE |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
212 |
val allI = allI |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
213 |
val allE = allE |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
214 |
end); |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
215 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
216 |
local |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
217 |
val ex_pattern = |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
218 |
read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
219 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
220 |
val all_pattern = |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
221 |
read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
222 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
223 |
in |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
224 |
val defEX_regroup = |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
225 |
mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
226 |
val defALL_regroup = |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
227 |
mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
228 |
end; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
229 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
230 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
231 |
(*** Case splitting ***) |
0 | 232 |
|
1088
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset
|
233 |
qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P" |
756 | 234 |
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]); |
282 | 235 |
|
942 | 236 |
local val mktac = mk_case_split_tac meta_iffD |
237 |
in |
|
238 |
fun split_tac splits = mktac (map mk_meta_eq splits) |
|
239 |
end; |
|
1722 | 240 |
|
241 |
local val mktac = mk_case_split_inside_tac meta_iffD |
|
242 |
in |
|
243 |
fun split_inside_tac splits = mktac (map mk_meta_eq splits) |
|
244 |
end; |
|
245 |
||
4203 | 246 |
val split_asm_tac = mk_case_split_asm_tac split_tac |
247 |
(disjE,conjE,exE,contrapos,contrapos2,notnotD); |
|
1722 | 248 |
|
4325 | 249 |
|
250 |
||
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
251 |
(*** Standard simpsets ***) |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
252 |
|
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
253 |
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
|
254 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
255 |
open Induction; |
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
256 |
|
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
257 |
(*Add congruence rules for = or <-> (instead of ==) *) |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
258 |
infix 4 addcongs delcongs; |
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
259 |
fun ss addcongs congs = |
3566 | 260 |
ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection])); |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
261 |
fun ss delcongs congs = |
3566 | 262 |
ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection])); |
2469 | 263 |
|
4094 | 264 |
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); |
265 |
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
|
266 |
|
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
267 |
infix 4 addsplits delsplits; |
4669 | 268 |
fun ss addsplits splits = |
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
269 |
let fun addsplit (ss,split) = |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
270 |
let val (name,asm) = split_thm_info split |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
271 |
in ss addloop (name ^ (if asm then " asm" else ""), |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
272 |
(if asm then split_asm_tac else split_tac) [split]) end |
4669 | 273 |
in foldl addsplit (ss,splits) end; |
4325 | 274 |
|
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
275 |
fun ss delsplits splits = |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
276 |
let fun delsplit(ss,split) = |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
277 |
let val (name,asm) = split_thm_info split |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
278 |
in ss delloop (name ^ (if asm then " asm" else "")) end |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
279 |
in foldl delsplit (ss,splits) end; |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset
|
280 |
|
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
281 |
val IFOL_simps = |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
282 |
[refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
283 |
imp_simps @ iff_simps @ quant_simps; |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
284 |
|
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
285 |
val notFalseI = int_prove_fun "~False"; |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
286 |
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
287 |
|
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
288 |
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
|
289 |
atac, etac FalseE]; |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
290 |
(*No premature instantiation of variables during simplification*) |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
291 |
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
|
292 |
eq_assume_tac, ematch_tac [FalseE]]; |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
293 |
|
3910 | 294 |
(*No simprules, but basic infastructure for simplification*) |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
295 |
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
|
296 |
addsimprocs [defALL_regroup,defEX_regroup] |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
297 |
setSSolver safe_solver |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
298 |
setSolver unsafe_solver |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
299 |
setmksimps (map mk_meta_eq o atomize o gen_all); |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
300 |
|
3910 | 301 |
(*intuitionistic simprules only*) |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
302 |
val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps) |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
303 |
addcongs [imp_cong]; |
2074
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 |
val cla_simps = |
3910 | 306 |
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, |
307 |
not_all, not_ex, cases_simp] @ |
|
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
308 |
map prove_fun |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
309 |
["~(P&Q) <-> ~P | ~Q", |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
310 |
"P | ~P", "~P | P", |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
311 |
"~ ~ P <-> P", "(~P --> P) <-> P", |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
312 |
"(~P <-> ~Q) <-> (P<->Q)"]; |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
313 |
|
3910 | 314 |
(*classical simprules too*) |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
315 |
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
|
316 |
|
4094 | 317 |
simpset_ref() := FOL_ss; |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
318 |
|
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
319 |
|
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
320 |
|
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset
|
321 |
|
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset
|
322 |
|
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset
|
323 |
|
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset
|
324 |
|
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
325 |
(*** Integration of simplifier with classical reasoner ***) |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
326 |
|
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
327 |
(* rot_eq_tac rotates the first equality premise of subgoal i to the front, |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
328 |
fails if there is no equaliy or if an equality is already at the front *) |
3537 | 329 |
local |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
330 |
fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true |
3537 | 331 |
| is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true |
332 |
| is_eq _ = false; |
|
4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4094
diff
changeset
|
333 |
val find_eq = find_index is_eq; |
3537 | 334 |
in |
335 |
val rot_eq_tac = |
|
4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4094
diff
changeset
|
336 |
SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in |
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4094
diff
changeset
|
337 |
if n>0 then rotate_tac n i else no_tac end) |
3537 | 338 |
end; |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
339 |
|
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset
|
340 |
use "$ISABELLE_HOME/src/Provers/clasimp.ML"; |
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset
|
341 |
open Clasimp; |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
342 |
|
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
343 |
val FOL_css = (FOL_cs, FOL_ss); |
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
344 |