author  wenzelm 
Sat, 24 Nov 2001 16:54:10 +0100  
changeset 12281  3bd113b8f7a6 
parent 12278  75103ba03035 
child 12475  18ba10cc782f 
permissions  rwrr 
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 

12281  9 
(* legacy ML bindings *) 
3904  10 

12281  11 
val Eq_FalseI = thm "Eq_FalseI"; 
12 
val Eq_TrueI = thm "Eq_TrueI"; 

13 
val all_conj_distrib = thm "all_conj_distrib"; 

14 
val all_simps = thms "all_simps"; 

15 
val cases_simp = thm "cases_simp"; 

16 
val conj_assoc = thm "conj_assoc"; 

17 
val conj_comms = thms "conj_comms"; 

18 
val conj_commute = thm "conj_commute"; 

19 
val conj_cong = thm "conj_cong"; 

20 
val conj_disj_distribL = thm "conj_disj_distribL"; 

21 
val conj_disj_distribR = thm "conj_disj_distribR"; 

22 
val conj_left_commute = thm "conj_left_commute"; 

23 
val de_Morgan_conj = thm "de_Morgan_conj"; 

24 
val de_Morgan_disj = thm "de_Morgan_disj"; 

25 
val disj_assoc = thm "disj_assoc"; 

26 
val disj_comms = thms "disj_comms"; 

27 
val disj_commute = thm "disj_commute"; 

28 
val disj_cong = thm "disj_cong"; 

29 
val disj_conj_distribL = thm "disj_conj_distribL"; 

30 
val disj_conj_distribR = thm "disj_conj_distribR"; 

31 
val disj_left_commute = thm "disj_left_commute"; 

32 
val disj_not1 = thm "disj_not1"; 

33 
val disj_not2 = thm "disj_not2"; 

34 
val eq_ac = thms "eq_ac"; 

35 
val eq_assoc = thm "eq_assoc"; 

36 
val eq_commute = thm "eq_commute"; 

37 
val eq_left_commute = thm "eq_left_commute"; 

38 
val eq_sym_conv = thm "eq_sym_conv"; 

39 
val eta_contract_eq = thm "eta_contract_eq"; 

40 
val ex_disj_distrib = thm "ex_disj_distrib"; 

41 
val ex_simps = thms "ex_simps"; 

42 
val if_False = thm "if_False"; 

43 
val if_P = thm "if_P"; 

44 
val if_True = thm "if_True"; 

45 
val if_bool_eq_conj = thm "if_bool_eq_conj"; 

46 
val if_bool_eq_disj = thm "if_bool_eq_disj"; 

47 
val if_cancel = thm "if_cancel"; 

48 
val if_def2 = thm "if_def2"; 

49 
val if_eq_cancel = thm "if_eq_cancel"; 

50 
val if_not_P = thm "if_not_P"; 

51 
val if_splits = thms "if_splits"; 

52 
val iff_conv_conj_imp = thm "iff_conv_conj_imp"; 

53 
val imp_all = thm "imp_all"; 

54 
val imp_cong = thm "imp_cong"; 

55 
val imp_conjL = thm "imp_conjL"; 

56 
val imp_conjR = thm "imp_conjR"; 

57 
val imp_conv_disj = thm "imp_conv_disj"; 

58 
val imp_disj1 = thm "imp_disj1"; 

59 
val imp_disj2 = thm "imp_disj2"; 

60 
val imp_disjL = thm "imp_disjL"; 

61 
val imp_disj_not1 = thm "imp_disj_not1"; 

62 
val imp_disj_not2 = thm "imp_disj_not2"; 

63 
val imp_ex = thm "imp_ex"; 

64 
val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; 

65 
val neq_commute = thm "neq_commute"; 

66 
val not_all = thm "not_all"; 

67 
val not_ex = thm "not_ex"; 

68 
val not_iff = thm "not_iff"; 

69 
val not_imp = thm "not_imp"; 

70 
val not_not = thm "not_not"; 

71 
val rev_conj_cong = thm "rev_conj_cong"; 

72 
val simp_thms = thms "simp_thms"; 

73 
val split_if = thm "split_if"; 

74 
val split_if_asm = thm "split_if_asm"; 

5278  75 

2134  76 

11232  77 
local 
78 
val uncurry = prove_goal (the_context()) "P > Q > R ==> P & Q > R" 

79 
(fn prems => [cut_facts_tac prems 1, Blast_tac 1]); 

80 

81 
val iff_allI = allI RS 

82 
prove_goal (the_context()) "!x. P x = Q x ==> (!x. P x) = (!x. Q x)" 

83 
(fn prems => [cut_facts_tac prems 1, Blast_tac 1]) 

84 
in 

4351  85 

86 
(*** make simplification procedures for quantifier elimination ***) 

87 

9851  88 
structure Quantifier1 = Quantifier1Fun 
89 
(struct 

4351  90 
(*abstract syntax*) 
91 
fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t) 

92 
 dest_eq _ = None; 

93 
fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t) 

94 
 dest_conj _ = None; 

11232  95 
fun dest_imp((c as Const("op >",_)) $ s $ t) = Some(c,s,t) 
96 
 dest_imp _ = None; 

4351  97 
val conj = HOLogic.conj 
98 
val imp = HOLogic.imp 

99 
(*rules*) 

100 
val iff_reflection = eq_reflection 

101 
val iffI = iffI 

102 
val conjI= conjI 

103 
val conjE= conjE 

104 
val impI = impI 

105 
val mp = mp 

11232  106 
val uncurry = uncurry 
4351  107 
val exI = exI 
108 
val exE = exE 

11232  109 
val iff_allI = iff_allI 
4351  110 
end); 
111 

11232  112 
end; 
113 

4320
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset

114 
local 
11220  115 
val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) 
116 
("EX x. P(x) & Q(x)",HOLogic.boolT) 

117 
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) 

11232  118 
("ALL x. P(x) > Q(x)",HOLogic.boolT) 
4320
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset

119 
in 
11220  120 
val defEX_regroup = mk_simproc "defined EX" [ex_pattern] 
121 
Quantifier1.rearrange_ex 

122 
val defALL_regroup = mk_simproc "defined ALL" [all_pattern] 

123 
Quantifier1.rearrange_all 

4320
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4205
diff
changeset

124 
end; 
3913  125 

4351  126 

127 
(*** Case splitting ***) 

3913  128 

12278  129 
(*Make metaequalities. The operator below is Trueprop*) 
130 

131 
fun mk_meta_eq r = r RS eq_reflection; 

132 
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; 

133 

134 
fun mk_eq th = case concl_of th of 

135 
Const("==",_)$_$_ => th 

136 
 _$(Const("op =",_)$_$_) => mk_meta_eq th 

137 
 _$(Const("Not",_)$_) => th RS Eq_FalseI 

138 
 _ => th RS Eq_TrueI; 

139 
(* last 2 lines requires all formulae to be of the from Trueprop(.) *) 

140 

141 
fun mk_eq_True r = 

142 
Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None; 

143 

144 
(*Congruence rules for = (instead of ==)*) 

145 
fun mk_meta_cong rl = 

146 
standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl)) 

147 
handle THM _ => 

148 
error("Premises and conclusion of congruence rules must be =equalities"); 

149 

150 
(* Elimination of True from asumptions: *) 

151 

152 
local fun rd s = read_cterm (sign_of (the_context())) (s, propT); 

153 
in val True_implies_equals = standard' (equal_intr 

154 
(implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI)) 

155 
(implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P"))))); 

156 
end; 

157 

158 

5304  159 
structure SplitterData = 
160 
struct 

161 
structure Simplifier = Simplifier 

5552  162 
val mk_eq = mk_eq 
5304  163 
val meta_eq_to_iff = meta_eq_to_obj_eq 
164 
val iffD = iffD2 

165 
val disjE = disjE 

166 
val conjE = conjE 

167 
val exE = exE 

10231  168 
val contrapos = contrapos_nn 
169 
val contrapos2 = contrapos_pp 

5304  170 
val notnotD = notnotD 
171 
end; 

4681  172 

5304  173 
structure Splitter = SplitterFun(SplitterData); 
2263  174 

5304  175 
val split_tac = Splitter.split_tac; 
176 
val split_inside_tac = Splitter.split_inside_tac; 

177 
val split_asm_tac = Splitter.split_asm_tac; 

5307  178 
val op addsplits = Splitter.addsplits; 
179 
val op delsplits = Splitter.delsplits; 

5304  180 
val Addsplits = Splitter.Addsplits; 
181 
val Delsplits = Splitter.Delsplits; 

4718
fc2ba9fb2135
new rewrite rules not1_or, not2_or, and if_eq_cancel
oheimb
parents:
4681
diff
changeset

182 

2134  183 
(*In general it seems wrong to add distributive laws by default: they 
184 
might cause exponential blowup. But imp_disjL has been in for a while 

9713  185 
and cannot be removed without affecting existing proofs. Moreover, 
2134  186 
rewriting by "(PQ > R) = ((P>R)&(Q>R))" might be justified on the 
187 
grounds that it allows simplification of R in the two cases.*) 

188 

189 
val mksimps_pairs = 

190 
[("op >", [mp]), ("op &", [conjunct1,conjunct2]), 

191 
("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

192 
("If", [if_bool_eq_conj RS iffD1])]; 
1758  193 

5552  194 
(* ###FIXME: move to Provers/simplifier.ML 
5304  195 
val mk_atomize: (string * thm list) list > thm > thm list 
196 
*) 

5552  197 
(* ###FIXME: move to Provers/simplifier.ML *) 
5304  198 
fun mk_atomize pairs = 
199 
let fun atoms th = 

200 
(case concl_of th of 

201 
Const("Trueprop",_) $ p => 

202 
(case head_of p of 

203 
Const(a,_) => 

204 
(case assoc(pairs,a) of 

205 
Some(rls) => flat (map atoms ([th] RL rls)) 

206 
 None => [th]) 

207 
 _ => [th]) 

208 
 _ => [th]) 

209 
in atoms end; 

210 

11624
8a45c7abef04
mksimps and mk_eq_True no longer raise THM exception.
berghofe
parents:
11534
diff
changeset

211 
fun mksimps pairs = 
8a45c7abef04
mksimps and mk_eq_True no longer raise THM exception.
berghofe
parents:
11534
diff
changeset

212 
(mapfilter (try mk_eq) o mk_atomize pairs o forall_elim_vars_safe); 
5304  213 

7570  214 
fun unsafe_solver_tac prems = 
215 
FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE]; 

216 
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; 

217 

2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset

218 
(*No premature instantiation of variables during simplification*) 
7570  219 
fun safe_solver_tac prems = 
220 
FIRST'[match_tac(reflexive_thm::TrueI::refl::prems), 

221 
eq_assume_tac, ematch_tac [FalseE]]; 

222 
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

223 

9713  224 
val HOL_basic_ss = 
225 
empty_ss setsubgoaler asm_simp_tac 

226 
setSSolver safe_solver 

227 
setSolver unsafe_solver 

228 
setmksimps (mksimps mksimps_pairs) 

229 
setmkeqTrue mk_eq_True 

230 
setmkcong mk_meta_cong; 

2443
a81d4c219c3c
factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss
oheimb
parents:
2263
diff
changeset

231 

9713  232 
val HOL_ss = 
233 
HOL_basic_ss addsimps 

3446
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3282
diff
changeset

234 
([triv_forall_equality, (* prunes params *) 
3654  235 
True_implies_equals, (* prune asms `True' *) 
9023  236 
eta_contract_eq, (* prunes etaexpansions *) 
4718
fc2ba9fb2135
new rewrite rules not1_or, not2_or, and if_eq_cancel
oheimb
parents:
4681
diff
changeset

237 
if_True, if_False, if_cancel, if_eq_cancel, 
5304  238 
imp_disjL, conj_assoc, disj_assoc, 
3904  239 
de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11434
diff
changeset

240 
disj_not1, not_all, not_ex, cases_simp, 
11434  241 
thm "the_eq_trivial", the_sym_eq_trivial, 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

242 
@ 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

243 
addsimprocs [defALL_regroup,defEX_regroup] 
4744
4469d498cd48
moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
wenzelm
parents:
4743
diff
changeset

244 
addcongs [imp_cong] 
4830  245 
addsplits [split_if]; 
2082  246 

11034  247 
fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); 
248 

249 

6293  250 
(*Simplifies x assuming c and y assuming ~c*) 
251 
val prems = Goalw [if_def] 

252 
"[ b=c; c ==> x=u; ~c ==> y=v ] ==> \ 

253 
\ (if b then x else y) = (if c then u else v)"; 

254 
by (asm_simp_tac (HOL_ss addsimps prems) 1); 

255 
qed "if_cong"; 

256 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7031
diff
changeset

257 
(*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

258 
of functional programs. NOW THE DEFAULT.*) 
7031  259 
Goal "b=c ==> (if b then x else y) = (if c then x else y)"; 
260 
by (etac arg_cong 1); 

261 
qed "if_weak_cong"; 

6293  262 

263 
(*Prevents simplification of t: much faster*) 

7031  264 
Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"; 
265 
by (etac arg_cong 1); 

266 
qed "let_weak_cong"; 

6293  267 

7031  268 
Goal "f(if c then x else y) = (if c then f x else f y)"; 
269 
by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1); 

270 
qed "if_distrib"; 

1655  271 

4327  272 
(*For expand_case_tac*) 
7584  273 
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

274 
by (case_tac "P" 1); 
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset

275 
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems))); 
7584  276 
qed "expand_case"; 
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset

277 

4327  278 
(*Used in Auth proofs. Typically P contains Vars that become instantiated 
279 
during unification.*) 

2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset

280 
fun expand_case_tac P i = 
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset

281 
res_inst_tac [("P",P)] expand_case i THEN 
9713  282 
Simp_tac (i+1) THEN 
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset

283 
Simp_tac i; 
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset

284 

7584  285 
(*This lemma restricts the effect of the rewrite rule u=v to the lefthand 
286 
side of an equality. Used in {Integ,Real}/simproc.ML*) 

287 
Goal "x=y ==> (x=z) = (y=z)"; 

288 
by (asm_simp_tac HOL_ss 1); 

289 
qed "restrict_to_left"; 

2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset

290 

7357  291 
(* default simpset *) 
9713  292 
val simpsetup = 
293 
[fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)]; 

3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3577
diff
changeset

294 

4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4651
diff
changeset

295 

5219  296 
(*** integration of simplifier with classical reasoner ***) 
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset

297 

5219  298 
structure Clasimp = ClasimpFun 
8473  299 
(structure Simplifier = Simplifier and Splitter = Splitter 
9851  300 
and Classical = Classical and Blast = Blast 
11344  301 
val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE 
9851  302 
val cla_make_elim = cla_make_elim); 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4651
diff
changeset

303 
open Clasimp; 
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset

304 

4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset

305 
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

306 

cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

307 

8641
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset

308 

5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

309 
(*** A general refutation procedure ***) 
9713  310 

5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

311 
(* Parameters: 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

312 

cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

313 
test: term > bool 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

314 
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

315 
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

316 
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

317 

cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

318 
prep_tac: int > tactic 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

319 
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

320 
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

321 

cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

322 
ref_tac: int > tactic 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

323 
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

324 
[ A1; ...; An ] ==> False 
9876  325 
where the Ai are atomic, i.e. no toplevel &,  or EX 
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

326 
*) 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

327 

cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

328 
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

329 
let val nnf_simps = 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

330 
[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

331 
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

332 
val nnf_simpset = 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

333 
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

334 
setmksimps (mksimps mksimps_pairs) 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

335 
addsimps nnf_simps; 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

336 
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

337 

cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

338 
val refute_prems_tac = 
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

339 
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

340 
filter_prems_tac test 1 ORELSE 
6301  341 
etac disjE 1) THEN 
11200
f43fa07536c0
arith_tac now copes with propositional reasoning as well.
nipkow
parents:
11162
diff
changeset

342 
((etac notE 1 THEN eq_assume_tac 1) ORELSE 
f43fa07536c0
arith_tac now copes with propositional reasoning as well.
nipkow
parents:
11162
diff
changeset

343 
ref_tac 1); 
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

344 
in EVERY'[TRY o filter_prems_tac test, 
6128  345 
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

346 
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

347 
end; 