author | wenzelm |
Thu, 17 Aug 2000 10:33:37 +0200 | |
changeset 9619 | 6125cc9efc18 |
parent 9511 | bb029080ff8b |
child 9713 | 2c5b42311eb0 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/simpdata.ML |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
923 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
5304 | 6 |
Instantiation of the generic simplifier for HOL. |
923 | 7 |
*) |
8 |
||
1984 | 9 |
section "Simplifier"; |
10 |
||
6514 | 11 |
(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *) |
1984 | 12 |
|
5190
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
13 |
infix 4 addIffs delIffs; |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
14 |
|
1984 | 15 |
(*Takes UNCONDITIONAL theorems of the form A<->B to |
2031 | 16 |
the Safe Intr rule B==>A and |
17 |
the Safe Destruct rule A==>B. |
|
1984 | 18 |
Also ~A goes to the Safe Elim rule A ==> ?R |
19 |
Failing other cases, A is added as a Safe Intr rule*) |
|
20 |
local |
|
21 |
val iff_const = HOLogic.eq_const HOLogic.boolT; |
|
22 |
||
5190
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
23 |
fun addIff ((cla, simp), th) = |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
24 |
(case HOLogic.dest_Trueprop (#prop (rep_thm th)) of |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
25 |
(Const("Not", _) $ A) => |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
26 |
cla addSEs [zero_var_indexes (th RS notE)] |
2031 | 27 |
| (con $ _ $ _) => |
5190
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
28 |
if con = iff_const |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
29 |
then cla addSIs [zero_var_indexes (th RS iffD2)] |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
30 |
addSDs [zero_var_indexes (th RS iffD1)] |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
31 |
else cla addSIs [th] |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
32 |
| _ => cla addSIs [th], |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
33 |
simp addsimps [th]) |
6968 | 34 |
handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ |
5190
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
35 |
string_of_thm th); |
1984 | 36 |
|
5190
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
37 |
fun delIff ((cla, simp), th) = |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
38 |
(case HOLogic.dest_Trueprop (#prop (rep_thm th)) of |
9164 | 39 |
(Const ("Not", _) $ A) => |
40 |
cla delrules [zero_var_indexes (th RS notE)] |
|
41 |
| (con $ _ $ _) => |
|
42 |
if con = iff_const |
|
43 |
then cla delrules |
|
44 |
[zero_var_indexes (th RS iffD2), |
|
45 |
cla_make_elim (zero_var_indexes (th RS iffD1))] |
|
46 |
else cla delrules [th] |
|
47 |
| _ => cla delrules [th], |
|
5190
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
48 |
simp delsimps [th]) |
6968 | 49 |
handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ |
9164 | 50 |
string_of_thm th); (cla, simp)); |
5190
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
51 |
|
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
52 |
fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp) |
1984 | 53 |
in |
5190
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
54 |
val op addIffs = foldl addIff; |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
55 |
val op delIffs = foldl delIff; |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
56 |
fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms); |
4ae031622592
Added functions addIffs and delIffs which operate on clasimpsets.
berghofe
parents:
4930
diff
changeset
|
57 |
fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms); |
1984 | 58 |
end; |
59 |
||
5304 | 60 |
|
7357 | 61 |
val [prem] = goal (the_context ()) "x==y ==> x=y"; |
7031 | 62 |
by (rewtac prem); |
63 |
by (rtac refl 1); |
|
64 |
qed "meta_eq_to_obj_eq"; |
|
4640 | 65 |
|
9023 | 66 |
Goal "(%s. f s) = f"; |
67 |
br refl 1; |
|
68 |
qed "eta_contract_eq"; |
|
69 |
||
923 | 70 |
local |
71 |
||
7357 | 72 |
fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]); |
923 | 73 |
|
2134 | 74 |
in |
75 |
||
5552 | 76 |
(*Make meta-equalities. The operator below is Trueprop*) |
77 |
||
6128 | 78 |
fun mk_meta_eq r = r RS eq_reflection; |
79 |
||
80 |
val Eq_TrueI = mk_meta_eq(prover "P --> (P = True)" RS mp); |
|
81 |
val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp); |
|
5304 | 82 |
|
6128 | 83 |
fun mk_eq th = case concl_of th of |
84 |
Const("==",_)$_$_ => th |
|
85 |
| _$(Const("op =",_)$_$_) => mk_meta_eq th |
|
86 |
| _$(Const("Not",_)$_) => th RS Eq_FalseI |
|
87 |
| _ => th RS Eq_TrueI; |
|
88 |
(* last 2 lines requires all formulae to be of the from Trueprop(.) *) |
|
5304 | 89 |
|
6128 | 90 |
fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI); |
5552 | 91 |
|
6128 | 92 |
fun mk_meta_cong rl = |
93 |
standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl)) |
|
94 |
handle THM _ => |
|
95 |
error("Premises and conclusion of congruence rules must be =-equalities"); |
|
3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3842
diff
changeset
|
96 |
|
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
97 |
val not_not = prover "(~ ~ P) = P"; |
923 | 98 |
|
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
99 |
val simp_thms = [not_not] @ map prover |
2082 | 100 |
[ "(x=x) = True", |
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
101 |
"(~True) = False", "(~False) = True", |
2082 | 102 |
"(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))", |
4640 | 103 |
"(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)", |
2082 | 104 |
"(True --> P) = P", "(False --> P) = True", |
105 |
"(P --> True) = True", "(P --> P) = True", |
|
106 |
"(P --> False) = (~P)", "(P --> ~P) = (~P)", |
|
107 |
"(P & True) = P", "(True & P) = P", |
|
2800 | 108 |
"(P & False) = False", "(False & P) = False", |
109 |
"(P & P) = P", "(P & (P & Q)) = (P & Q)", |
|
3913 | 110 |
"(P & ~P) = False", "(~P & P) = False", |
2082 | 111 |
"(P | True) = True", "(True | P) = True", |
2800 | 112 |
"(P | False) = P", "(False | P) = P", |
113 |
"(P | P) = P", "(P | (P | Q)) = (P | Q)", |
|
3913 | 114 |
"(P | ~P) = True", "(~P | P) = True", |
2082 | 115 |
"((~P) = (~Q)) = (P=Q)", |
3842 | 116 |
"(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", |
4351 | 117 |
(*two needed for the one-point-rule quantifier simplification procs*) |
118 |
"(? x. x=t & P(x)) = P(t)", (*essential for termination!!*) |
|
119 |
"(! x. t=x --> P(x)) = P(t)" ]; (*covers a stray case*) |
|
923 | 120 |
|
5552 | 121 |
(* Add congruence rules for = (instead of ==) *) |
4351 | 122 |
|
5552 | 123 |
(* ###FIXME: Move to simplifier, |
124 |
taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *) |
|
125 |
infix 4 addcongs delcongs; |
|
4640 | 126 |
fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs); |
127 |
fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs); |
|
4086 | 128 |
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); |
129 |
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); |
|
1264 | 130 |
|
8641
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
131 |
val cong_add_global = Simplifier.change_global_ss (op addcongs); |
8644 | 132 |
val cong_del_global = Simplifier.change_global_ss (op delcongs); |
8641
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
133 |
val cong_add_local = Simplifier.change_local_ss (op addcongs); |
8644 | 134 |
val cong_del_local = Simplifier.change_local_ss (op delcongs); |
8641
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
135 |
|
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
136 |
val cong_attrib_setup = |
8644 | 137 |
[Attrib.add_attributes [("cong", |
138 |
(Attrib.add_del_args cong_add_global cong_del_global, |
|
139 |
Attrib.add_del_args cong_add_local cong_del_local), |
|
140 |
"declare Simplifier congruence rules")]]; |
|
8641
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
141 |
|
5552 | 142 |
|
1922 | 143 |
val imp_cong = impI RSN |
7357 | 144 |
(2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
7031 | 145 |
(fn _=> [(Blast_tac 1)]) RS mp RS mp); |
1922 | 146 |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
147 |
(*Miniscoping: pushing in existential quantifiers*) |
7648 | 148 |
val ex_simps = map prover |
3842 | 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))", |
|
153 |
"(EX x. P x --> Q) = ((ALL x. P x) --> Q)", |
|
154 |
"(EX x. P --> Q x) = (P --> (EX x. Q x))"]; |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
155 |
|
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
156 |
(*Miniscoping: pushing in universal quantifiers*) |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
157 |
val all_simps = map prover |
3842 | 158 |
["(ALL x. P x & Q) = ((ALL x. P x) & Q)", |
159 |
"(ALL x. P & Q x) = (P & (ALL x. Q x))", |
|
160 |
"(ALL x. P x | Q) = ((ALL x. P x) | Q)", |
|
161 |
"(ALL x. P | Q x) = (P | (ALL x. Q x))", |
|
162 |
"(ALL x. P x --> Q) = ((EX x. P x) --> Q)", |
|
163 |
"(ALL x. P --> Q x) = (P --> (ALL x. Q x))"]; |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
164 |
|
923 | 165 |
|
2022 | 166 |
(* elimination of existential quantifiers in assumptions *) |
923 | 167 |
|
168 |
val ex_all_equiv = |
|
7357 | 169 |
let val lemma1 = prove_goal (the_context ()) |
923 | 170 |
"(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)" |
171 |
(fn prems => [resolve_tac prems 1, etac exI 1]); |
|
7357 | 172 |
val lemma2 = prove_goalw (the_context ()) [Ex_def] |
923 | 173 |
"(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)" |
7031 | 174 |
(fn prems => [(REPEAT(resolve_tac prems 1))]) |
923 | 175 |
in equal_intr lemma1 lemma2 end; |
176 |
||
177 |
end; |
|
178 |
||
7648 | 179 |
bind_thms ("ex_simps", ex_simps); |
180 |
bind_thms ("all_simps", all_simps); |
|
7711
4dae7a4fceaf
Rule not_not is now stored in theory (needed by Inductive).
berghofe
parents:
7648
diff
changeset
|
181 |
bind_thm ("not_not", not_not); |
7648 | 182 |
|
3654 | 183 |
(* Elimination of True from asumptions: *) |
184 |
||
7357 | 185 |
val True_implies_equals = prove_goal (the_context ()) |
3654 | 186 |
"(True ==> PROP P) == PROP P" |
7031 | 187 |
(fn _ => [rtac equal_intr_rule 1, atac 2, |
3654 | 188 |
METAHYPS (fn prems => resolve_tac prems 1) 1, |
189 |
rtac TrueI 1]); |
|
190 |
||
7357 | 191 |
fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]); |
923 | 192 |
|
9511 | 193 |
prove "eq_commute" "(a=b) = (b=a)"; |
7623 | 194 |
prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))"; |
195 |
prove "eq_assoc" "((P=Q)=R) = (P=(Q=R))"; |
|
196 |
val eq_ac = [eq_commute, eq_left_commute, eq_assoc]; |
|
197 |
||
9511 | 198 |
prove "neq_commute" "(a~=b) = (b~=a)"; |
199 |
||
923 | 200 |
prove "conj_commute" "(P&Q) = (Q&P)"; |
201 |
prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
|
202 |
val conj_comms = [conj_commute, conj_left_commute]; |
|
2134 | 203 |
prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; |
923 | 204 |
|
1922 | 205 |
prove "disj_commute" "(P|Q) = (Q|P)"; |
206 |
prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))"; |
|
207 |
val disj_comms = [disj_commute, disj_left_commute]; |
|
2134 | 208 |
prove "disj_assoc" "((P|Q)|R) = (P|(Q|R))"; |
1922 | 209 |
|
923 | 210 |
prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; |
211 |
prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
212 |
|
1892 | 213 |
prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))"; |
214 |
prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))"; |
|
215 |
||
2134 | 216 |
prove "imp_conjR" "(P --> (Q&R)) = ((P-->Q) & (P-->R))"; |
217 |
prove "imp_conjL" "((P&Q) -->R) = (P --> (Q --> R))"; |
|
218 |
prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))"; |
|
1892 | 219 |
|
3448 | 220 |
(*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*) |
8114 | 221 |
prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)"; |
222 |
prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)"; |
|
3448 | 223 |
|
3904 | 224 |
prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)"; |
225 |
prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)"; |
|
226 |
||
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
227 |
prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)"; |
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
228 |
prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)"; |
3446
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3282
diff
changeset
|
229 |
prove "not_imp" "(~(P --> Q)) = (P & ~Q)"; |
1922 | 230 |
prove "not_iff" "(P~=Q) = (P = (~Q))"; |
4743 | 231 |
prove "disj_not1" "(~P | Q) = (P --> Q)"; |
232 |
prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *) |
|
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
233 |
prove "imp_conv_disj" "(P --> Q) = ((~P) | Q)"; |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
234 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
235 |
prove "iff_conv_conj_imp" "(P = Q) = ((P --> Q) & (Q --> P))"; |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
236 |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
237 |
|
4830 | 238 |
(*Avoids duplication of subgoals after split_if, when the true and false |
2134 | 239 |
cases boil down to the same thing.*) |
240 |
prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q"; |
|
241 |
||
3842 | 242 |
prove "not_all" "(~ (! x. P(x))) = (? x.~P(x))"; |
1922 | 243 |
prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)"; |
3842 | 244 |
prove "not_ex" "(~ (? x. P(x))) = (! x.~P(x))"; |
1922 | 245 |
prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)"; |
1660 | 246 |
|
1655 | 247 |
prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))"; |
248 |
prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
|
249 |
||
2134 | 250 |
(* '&' congruence rule: not included by default! |
251 |
May slow rewrite proofs down by as much as 50% *) |
|
252 |
||
7357 | 253 |
let val th = prove_goal (the_context ()) |
2134 | 254 |
"(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
7031 | 255 |
(fn _=> [(Blast_tac 1)]) |
2134 | 256 |
in bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
257 |
||
7357 | 258 |
let val th = prove_goal (the_context ()) |
2134 | 259 |
"(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
7031 | 260 |
(fn _=> [(Blast_tac 1)]) |
2134 | 261 |
in bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
262 |
||
263 |
(* '|' congruence rule: not included by default! *) |
|
264 |
||
7357 | 265 |
let val th = prove_goal (the_context ()) |
2134 | 266 |
"(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
7031 | 267 |
(fn _=> [(Blast_tac 1)]) |
2134 | 268 |
in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
269 |
||
270 |
prove "eq_sym_conv" "(x=y) = (y=x)"; |
|
271 |
||
5278 | 272 |
|
273 |
(** if-then-else rules **) |
|
274 |
||
7031 | 275 |
Goalw [if_def] "(if True then x else y) = x"; |
276 |
by (Blast_tac 1); |
|
277 |
qed "if_True"; |
|
2134 | 278 |
|
7031 | 279 |
Goalw [if_def] "(if False then x else y) = y"; |
280 |
by (Blast_tac 1); |
|
281 |
qed "if_False"; |
|
2134 | 282 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7031
diff
changeset
|
283 |
Goalw [if_def] "P ==> (if P then x else y) = x"; |
7031 | 284 |
by (Blast_tac 1); |
285 |
qed "if_P"; |
|
5304 | 286 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7031
diff
changeset
|
287 |
Goalw [if_def] "~P ==> (if P then x else y) = y"; |
7031 | 288 |
by (Blast_tac 1); |
289 |
qed "if_not_P"; |
|
2134 | 290 |
|
7031 | 291 |
Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"; |
292 |
by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1); |
|
293 |
by (stac if_P 2); |
|
294 |
by (stac if_not_P 1); |
|
295 |
by (ALLGOALS (Blast_tac)); |
|
296 |
qed "split_if"; |
|
297 |
||
298 |
Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"; |
|
299 |
by (stac split_if 1); |
|
300 |
by (Blast_tac 1); |
|
301 |
qed "split_if_asm"; |
|
2134 | 302 |
|
9384
8e8941c491e6
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
wenzelm
parents:
9164
diff
changeset
|
303 |
bind_thms ("if_splits", [split_if, split_if_asm]); |
8e8941c491e6
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
wenzelm
parents:
9164
diff
changeset
|
304 |
|
7031 | 305 |
Goal "(if c then x else x) = x"; |
306 |
by (stac split_if 1); |
|
307 |
by (Blast_tac 1); |
|
308 |
qed "if_cancel"; |
|
5304 | 309 |
|
7031 | 310 |
Goal "(if x = y then y else x) = x"; |
311 |
by (stac split_if 1); |
|
312 |
by (Blast_tac 1); |
|
313 |
qed "if_eq_cancel"; |
|
5304 | 314 |
|
4769
bb60149fe21b
changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj
paulson
parents:
4744
diff
changeset
|
315 |
(*This form is useful for expanding IFs on the RIGHT of the ==> symbol*) |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7031
diff
changeset
|
316 |
Goal "(if P then Q else R) = ((P-->Q) & (~P-->R))"; |
7031 | 317 |
by (rtac split_if 1); |
318 |
qed "if_bool_eq_conj"; |
|
4769
bb60149fe21b
changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj
paulson
parents:
4744
diff
changeset
|
319 |
|
bb60149fe21b
changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj
paulson
parents:
4744
diff
changeset
|
320 |
(*And this form is useful for expanding IFs on the LEFT*) |
7031 | 321 |
Goal "(if P then Q else R) = ((P&Q) | (~P&R))"; |
322 |
by (stac split_if 1); |
|
323 |
by (Blast_tac 1); |
|
324 |
qed "if_bool_eq_disj"; |
|
2134 | 325 |
|
4351 | 326 |
|
327 |
(*** make simplification procedures for quantifier elimination ***) |
|
328 |
||
329 |
structure Quantifier1 = Quantifier1Fun( |
|
330 |
struct |
|
331 |
(*abstract syntax*) |
|
332 |
fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t) |
|
333 |
| dest_eq _ = None; |
|
334 |
fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t) |
|
335 |
| dest_conj _ = None; |
|
336 |
val conj = HOLogic.conj |
|
337 |
val imp = HOLogic.imp |
|
338 |
(*rules*) |
|
339 |
val iff_reflection = eq_reflection |
|
340 |
val iffI = iffI |
|
341 |
val sym = sym |
|
342 |
val conjI= conjI |
|
343 |
val conjE= conjE |
|
344 |
val impI = impI |
|
345 |
val impE = impE |
|
346 |
val mp = mp |
|
347 |
val exI = exI |
|
348 |
val exE = exE |
|
349 |
val allI = allI |
|
350 |
val allE = allE |
|
351 |
end); |
|
352 |
||
4320
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
353 |
local |
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
354 |
val ex_pattern = |
7357 | 355 |
Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)",HOLogic.boolT) |
3913 | 356 |
|
4320
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
357 |
val all_pattern = |
7357 | 358 |
Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT) |
4320
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
359 |
|
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
360 |
in |
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
361 |
val defEX_regroup = |
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
362 |
mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex; |
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
363 |
val defALL_regroup = |
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
364 |
mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all; |
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset
|
365 |
end; |
3913 | 366 |
|
4351 | 367 |
|
368 |
(*** Case splitting ***) |
|
3913 | 369 |
|
5304 | 370 |
structure SplitterData = |
371 |
struct |
|
372 |
structure Simplifier = Simplifier |
|
5552 | 373 |
val mk_eq = mk_eq |
5304 | 374 |
val meta_eq_to_iff = meta_eq_to_obj_eq |
375 |
val iffD = iffD2 |
|
376 |
val disjE = disjE |
|
377 |
val conjE = conjE |
|
378 |
val exE = exE |
|
379 |
val contrapos = contrapos |
|
380 |
val contrapos2 = contrapos2 |
|
381 |
val notnotD = notnotD |
|
382 |
end; |
|
4681 | 383 |
|
5304 | 384 |
structure Splitter = SplitterFun(SplitterData); |
2263 | 385 |
|
5304 | 386 |
val split_tac = Splitter.split_tac; |
387 |
val split_inside_tac = Splitter.split_inside_tac; |
|
388 |
val split_asm_tac = Splitter.split_asm_tac; |
|
5307 | 389 |
val op addsplits = Splitter.addsplits; |
390 |
val op delsplits = Splitter.delsplits; |
|
5304 | 391 |
val Addsplits = Splitter.Addsplits; |
392 |
val Delsplits = Splitter.Delsplits; |
|
4718
fc2ba9fb2135
new rewrite rules not1_or, not2_or, and if_eq_cancel
oheimb
parents:
4681
diff
changeset
|
393 |
|
2134 | 394 |
(*In general it seems wrong to add distributive laws by default: they |
395 |
might cause exponential blow-up. But imp_disjL has been in for a while |
|
396 |
and cannot be removed without affecting existing proofs. Moreover, |
|
397 |
rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |
|
398 |
grounds that it allows simplification of R in the two cases.*) |
|
399 |
||
5304 | 400 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
401 |
||
2134 | 402 |
val mksimps_pairs = |
403 |
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
|
404 |
("All", [spec]), ("True", []), ("False", []), |
|
4769
bb60149fe21b
changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj
paulson
parents:
4744
diff
changeset
|
405 |
("If", [if_bool_eq_conj RS iffD1])]; |
1758 | 406 |
|
5552 | 407 |
(* ###FIXME: move to Provers/simplifier.ML |
5304 | 408 |
val mk_atomize: (string * thm list) list -> thm -> thm list |
409 |
*) |
|
5552 | 410 |
(* ###FIXME: move to Provers/simplifier.ML *) |
5304 | 411 |
fun mk_atomize pairs = |
412 |
let fun atoms th = |
|
413 |
(case concl_of th of |
|
414 |
Const("Trueprop",_) $ p => |
|
415 |
(case head_of p of |
|
416 |
Const(a,_) => |
|
417 |
(case assoc(pairs,a) of |
|
418 |
Some(rls) => flat (map atoms ([th] RL rls)) |
|
419 |
| None => [th]) |
|
420 |
| _ => [th]) |
|
421 |
| _ => [th]) |
|
422 |
in atoms end; |
|
423 |
||
5552 | 424 |
fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all); |
5304 | 425 |
|
7570 | 426 |
fun unsafe_solver_tac prems = |
427 |
FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE]; |
|
428 |
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; |
|
429 |
||
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
430 |
(*No premature instantiation of variables during simplification*) |
7570 | 431 |
fun safe_solver_tac prems = |
432 |
FIRST'[match_tac(reflexive_thm::TrueI::refl::prems), |
|
433 |
eq_assume_tac, ematch_tac [FalseE]]; |
|
434 |
val safe_solver = mk_solver "HOL safe" safe_solver_tac; |
|
2443
a81d4c219c3c
factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss
oheimb
parents:
2263
diff
changeset
|
435 |
|
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
436 |
val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
7570 | 437 |
setSSolver safe_solver |
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
438 |
setSolver unsafe_solver |
4677 | 439 |
setmksimps (mksimps mksimps_pairs) |
5552 | 440 |
setmkeqTrue mk_eq_True; |
2443
a81d4c219c3c
factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss
oheimb
parents:
2263
diff
changeset
|
441 |
|
3446
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3282
diff
changeset
|
442 |
val HOL_ss = |
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3282
diff
changeset
|
443 |
HOL_basic_ss addsimps |
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3282
diff
changeset
|
444 |
([triv_forall_equality, (* prunes params *) |
3654 | 445 |
True_implies_equals, (* prune asms `True' *) |
9023 | 446 |
eta_contract_eq, (* prunes eta-expansions *) |
4718
fc2ba9fb2135
new rewrite rules not1_or, not2_or, and if_eq_cancel
oheimb
parents:
4681
diff
changeset
|
447 |
if_True, if_False, if_cancel, if_eq_cancel, |
5304 | 448 |
imp_disjL, conj_assoc, disj_assoc, |
3904 | 449 |
de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, |
8955 | 450 |
disj_not1, not_all, not_ex, cases_simp, Eps_eq, Eps_sym_eq, |
451 |
thm"plus_ac0.zero", thm"plus_ac0_zero_right"] |
|
3446
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3282
diff
changeset
|
452 |
@ ex_simps @ all_simps @ simp_thms) |
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3919
diff
changeset
|
453 |
addsimprocs [defALL_regroup,defEX_regroup] |
4744
4469d498cd48
moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
wenzelm
parents:
4743
diff
changeset
|
454 |
addcongs [imp_cong] |
4830 | 455 |
addsplits [split_if]; |
2082 | 456 |
|
6293 | 457 |
(*Simplifies x assuming c and y assuming ~c*) |
458 |
val prems = Goalw [if_def] |
|
459 |
"[| b=c; c ==> x=u; ~c ==> y=v |] ==> \ |
|
460 |
\ (if b then x else y) = (if c then u else v)"; |
|
461 |
by (asm_simp_tac (HOL_ss addsimps prems) 1); |
|
462 |
qed "if_cong"; |
|
463 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7031
diff
changeset
|
464 |
(*Prevents simplification of x and y: faster and allows the execution |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7031
diff
changeset
|
465 |
of functional programs. NOW THE DEFAULT.*) |
7031 | 466 |
Goal "b=c ==> (if b then x else y) = (if c then x else y)"; |
467 |
by (etac arg_cong 1); |
|
468 |
qed "if_weak_cong"; |
|
6293 | 469 |
|
470 |
(*Prevents simplification of t: much faster*) |
|
7031 | 471 |
Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"; |
472 |
by (etac arg_cong 1); |
|
473 |
qed "let_weak_cong"; |
|
6293 | 474 |
|
7031 | 475 |
Goal "f(if c then x else y) = (if c then f x else f y)"; |
476 |
by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1); |
|
477 |
qed "if_distrib"; |
|
1655 | 478 |
|
4327 | 479 |
(*For expand_case_tac*) |
7584 | 480 |
val prems = Goal "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
481 |
by (case_tac "P" 1); |
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
482 |
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems))); |
7584 | 483 |
qed "expand_case"; |
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
484 |
|
4327 | 485 |
(*Used in Auth proofs. Typically P contains Vars that become instantiated |
486 |
during unification.*) |
|
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
487 |
fun expand_case_tac P i = |
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
488 |
res_inst_tac [("P",P)] expand_case i THEN |
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
489 |
Simp_tac (i+1) THEN |
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
490 |
Simp_tac i; |
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
491 |
|
7584 | 492 |
(*This lemma restricts the effect of the rewrite rule u=v to the left-hand |
493 |
side of an equality. Used in {Integ,Real}/simproc.ML*) |
|
494 |
Goal "x=y ==> (x=z) = (y=z)"; |
|
495 |
by (asm_simp_tac HOL_ss 1); |
|
496 |
qed "restrict_to_left"; |
|
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
497 |
|
7357 | 498 |
(* default simpset *) |
7584 | 499 |
val simpsetup = |
500 |
[fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; |
|
501 |
thy)]; |
|
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3577
diff
changeset
|
502 |
|
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4651
diff
changeset
|
503 |
|
5219 | 504 |
(*** integration of simplifier with classical reasoner ***) |
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
505 |
|
5219 | 506 |
structure Clasimp = ClasimpFun |
8473 | 507 |
(structure Simplifier = Simplifier and Splitter = Splitter |
508 |
and Classical = Classical and Blast = Blast); |
|
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4651
diff
changeset
|
509 |
open Clasimp; |
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
510 |
|
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
511 |
val HOL_css = (HOL_cs, HOL_ss); |
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
512 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
513 |
|
8641
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
514 |
(* "iff" attribute *) |
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
515 |
|
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
516 |
val iff_add_global = Clasimp.change_global_css (op addIffs); |
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
517 |
val iff_add_local = Clasimp.change_local_css (op addIffs); |
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
518 |
|
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
519 |
val iff_attrib_setup = |
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
520 |
[Attrib.add_attributes [("iff", (Attrib.no_args iff_add_global, Attrib.no_args iff_add_local), |
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
521 |
"add rules to simpset and claset simultaneously")]]; |
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
522 |
|
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
523 |
|
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
524 |
|
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
525 |
(*** A general refutation procedure ***) |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
526 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
527 |
(* Parameters: |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
528 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
529 |
test: term -> bool |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
530 |
tests if a term is at all relevant to the refutation proof; |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
531 |
if not, then it can be discarded. Can improve performance, |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
532 |
esp. if disjunctions can be discarded (no case distinction needed!). |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
533 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
534 |
prep_tac: int -> tactic |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
535 |
A preparation tactic to be applied to the goal once all relevant premises |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
536 |
have been moved to the conclusion. |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
537 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
538 |
ref_tac: int -> tactic |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
539 |
the actual refutation tactic. Should be able to deal with goals |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
540 |
[| A1; ...; An |] ==> False |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
541 |
where the Ai are atomic, i.e. no top-level &, | or ? |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
542 |
*) |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
543 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
544 |
fun refute_tac test prep_tac ref_tac = |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
545 |
let val nnf_simps = |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
546 |
[imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
547 |
not_all,not_ex,not_not]; |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
548 |
val nnf_simpset = |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
549 |
empty_ss setmkeqTrue mk_eq_True |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
550 |
setmksimps (mksimps mksimps_pairs) |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
551 |
addsimps nnf_simps; |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
552 |
val prem_nnf_tac = full_simp_tac nnf_simpset; |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
553 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
554 |
val refute_prems_tac = |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
555 |
REPEAT(eresolve_tac [conjE, exE] 1 ORELSE |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
556 |
filter_prems_tac test 1 ORELSE |
6301 | 557 |
etac disjE 1) THEN |
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
558 |
ref_tac 1; |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
559 |
in EVERY'[TRY o filter_prems_tac test, |
6128 | 560 |
DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, |
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
561 |
SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
562 |
end; |