author  wenzelm 
Thu, 01 Dec 2005 22:03:01 +0100  
changeset 18324  d1c4b1112e33 
parent 18176  ae9bd644d106 
child 18407  fa075b606571 
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"; 

16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

72 
val simp_impliesE = thm "simp_impliesI"; 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

73 
val simp_impliesI = thm "simp_impliesI"; 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

74 
val simp_implies_cong = thm "simp_implies_cong"; 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

75 
val simp_implies_def = thm "simp_implies_def"; 
12281  76 
val simp_thms = thms "simp_thms"; 
77 
val split_if = thm "split_if"; 

78 
val split_if_asm = thm "split_if_asm"; 

14749  79 
val atomize_not = thm"atomize_not"; 
2134  80 

11232  81 
local 
82 
val uncurry = prove_goal (the_context()) "P > Q > R ==> P & Q > R" 

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

84 

85 
val iff_allI = allI RS 

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

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

12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

88 
val iff_exI = allI RS 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

89 
prove_goal (the_context()) "!x. P x = Q x ==> (? x. P x) = (? x. Q x)" 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

90 
(fn prems => [cut_facts_tac prems 1, Blast_tac 1]) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

91 

66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

92 
val all_comm = prove_goal (the_context()) "(!x y. P x y) = (!y x. P x y)" 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

93 
(fn _ => [Blast_tac 1]) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

94 
val ex_comm = prove_goal (the_context()) "(? x y. P x y) = (? y x. P x y)" 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

95 
(fn _ => [Blast_tac 1]) 
11232  96 
in 
4351  97 

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

99 

9851  100 
structure Quantifier1 = Quantifier1Fun 
101 
(struct 

4351  102 
(*abstract syntax*) 
15531  103 
fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t) 
104 
 dest_eq _ = NONE; 

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

106 
 dest_conj _ = NONE; 

107 
fun dest_imp((c as Const("op >",_)) $ s $ t) = SOME(c,s,t) 

108 
 dest_imp _ = NONE; 

4351  109 
val conj = HOLogic.conj 
110 
val imp = HOLogic.imp 

111 
(*rules*) 

112 
val iff_reflection = eq_reflection 

113 
val iffI = iffI 

12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

114 
val iff_trans = trans 
4351  115 
val conjI= conjI 
116 
val conjE= conjE 

117 
val impI = impI 

118 
val mp = mp 

11232  119 
val uncurry = uncurry 
4351  120 
val exI = exI 
121 
val exE = exE 

11232  122 
val iff_allI = iff_allI 
12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

123 
val iff_exI = iff_exI 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

124 
val all_comm = all_comm 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
12475
diff
changeset

125 
val ex_comm = ex_comm 
4351  126 
end); 
127 

11232  128 
end; 
129 

13462  130 
val defEX_regroup = 
131 
Simplifier.simproc (Theory.sign_of (the_context ())) 

132 
"defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; 

133 

134 
val defALL_regroup = 

135 
Simplifier.simproc (Theory.sign_of (the_context ())) 

136 
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; 

3913  137 

17778  138 

139 
(*** simproc for proving "(y = x) == False" from prmise "~(x = y)" ***) 

140 

141 
val use_neq_simproc = ref true; 

142 

143 
local 

144 

145 
val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI; 

146 

147 
fun neq_prover sg ss (eq $ lhs $ rhs) = 

148 
let 

149 
fun test thm = (case #prop(rep_thm thm) of 

150 
_ $ (Not $ (eq' $ l' $ r')) => 

151 
Not = HOLogic.Not andalso eq' = eq andalso 

152 
r' aconv lhs andalso l' aconv rhs 

153 
 _ => false) 

154 
in 

155 
if !use_neq_simproc then 

156 
case Library.find_first test (prems_of_ss ss) of NONE => NONE 

157 
 SOME thm => SOME (thm RS neq_to_EQ_False) 

158 
else NONE 

159 
end 

160 

161 
in 

162 

163 
val neq_simproc = 

164 
Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover; 

165 

166 
end; 

167 

168 

169 

170 

15423  171 
(*** Simproc for Let ***) 
172 

173 
val use_let_simproc = ref true; 

174 

175 
local 

176 
val Let_folded = thm "Let_folded"; 

177 
val Let_unfold = thm "Let_unfold"; 

178 

179 
val f_Let_unfold = 

180 
let val [(_$(f$_)$_)] = prems_of Let_unfold in cterm_of (sign_of (the_context ())) f end 

181 
val f_Let_folded = 

182 
let val [(_$(f$_)$_)] = prems_of Let_folded in cterm_of (sign_of (the_context ())) f end; 

183 
val g_Let_folded = 

184 
let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end; 

185 
in 

186 
val let_simproc = 

187 
Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"] 

188 
(fn sg => fn ss => fn t => 

189 
(case t of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) 

15531  190 
if not (!use_let_simproc) then NONE 
15423  191 
else if is_Free x orelse is_Bound x orelse is_Const x 
15531  192 
then SOME Let_def 
15423  193 
else 
194 
let 

195 
val n = case f of (Abs (x,_,_)) => x  _ => "x"; 

196 
val cx = cterm_of sg x; 

197 
val {T=xT,...} = rep_cterm cx; 

198 
val cf = cterm_of sg f; 

199 
val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); 

200 
val (_$_$g) = prop_of fx_g; 

201 
val g' = abstract_over (x,g); 

202 
in (if (g aconv g') 

203 
then 

204 
let 

205 
val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold; 

15531  206 
in SOME (rl OF [fx_g]) end 
18176  207 
else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*) 
15423  208 
else let 
209 
val abs_g'= Abs (n,xT,g'); 

210 
val g'x = abs_g'$x; 

211 
val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x)); 

212 
val rl = cterm_instantiate 

213 
[(f_Let_folded,cterm_of sg f), 

214 
(g_Let_folded,cterm_of sg abs_g')] 

215 
Let_folded; 

15531  216 
in SOME (rl OF [transitive fx_g g_g'x]) end) 
15423  217 
end 
15531  218 
 _ => NONE)) 
15423  219 
end 
4351  220 

221 
(*** Case splitting ***) 

3913  222 

12278  223 
(*Make metaequalities. The operator below is Trueprop*) 
224 

13600
9702c8636a7b
Removed nRS again because extract_rews now takes care of preserving names.
berghofe
parents:
13568
diff
changeset

225 
fun mk_meta_eq r = r RS eq_reflection; 
12278  226 
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; 
227 

228 
fun mk_eq th = case concl_of th of 

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

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

13600
9702c8636a7b
Removed nRS again because extract_rews now takes care of preserving names.
berghofe
parents:
13568
diff
changeset

231 
 _$(Const("Not",_)$_) => th RS Eq_FalseI 
9702c8636a7b
Removed nRS again because extract_rews now takes care of preserving names.
berghofe
parents:
13568
diff
changeset

232 
 _ => th RS Eq_TrueI; 
13568
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset

233 
(* Expects Trueprop(.) if not == *) 
12278  234 

235 
fun mk_eq_True r = 

15531  236 
SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; 
12278  237 

16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

238 
(* Produce theorems of the form 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

239 
(P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

240 
*) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

241 
fun lift_meta_eq_to_obj_eq i st = 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

242 
let 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

243 
val {sign, ...} = rep_thm st; 
17197  244 
fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

245 
 count_imp _ = 0; 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

246 
val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i  1))) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

247 
in if j = 0 then meta_eq_to_obj_eq 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

248 
else 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

249 
let 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

250 
val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

251 
fun mk_simp_implies Q = foldr (fn (R, S) => 
17197  252 
Const ("HOL.simp_implies", propT > propT > propT) $ R $ S) Q Ps 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

253 
val aT = TFree ("'a", HOLogic.typeS); 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

254 
val x = Free ("x", aT); 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

255 
val y = Free ("y", aT) 
17985  256 
in standard (Goal.prove (Thm.theory_of_thm st) [] 
257 
[mk_simp_implies (Logic.mk_equals (x, y))] 

258 
(mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) 

259 
(fn prems => EVERY 

260 
[rewrite_goals_tac [simp_implies_def], 

261 
REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])) 

16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

262 
end 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

263 
end; 
17985  264 

12278  265 
(*Congruence rules for = (instead of ==)*) 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

266 
fun mk_meta_cong rl = zero_var_indexes 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

267 
(let val rl' = Seq.hd (TRYALL (fn i => fn st => 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

268 
rtac (lift_meta_eq_to_obj_eq i st) i st) rl) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

269 
in mk_meta_eq rl' handle THM _ => 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

270 
if Logic.is_equals (concl_of rl') then rl' 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

271 
else error "Conclusion of congruence rules must be =equality" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

272 
end); 
12278  273 

274 
(* Elimination of True from asumptions: *) 

275 

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

277 
in val True_implies_equals = standard' (equal_intr 

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

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

280 
end; 

281 

282 

5304  283 
structure SplitterData = 
284 
struct 

285 
structure Simplifier = Simplifier 

5552  286 
val mk_eq = mk_eq 
5304  287 
val meta_eq_to_iff = meta_eq_to_obj_eq 
288 
val iffD = iffD2 

289 
val disjE = disjE 

290 
val conjE = conjE 

291 
val exE = exE 

10231  292 
val contrapos = contrapos_nn 
293 
val contrapos2 = contrapos_pp 

5304  294 
val notnotD = notnotD 
295 
end; 

4681  296 

5304  297 
structure Splitter = SplitterFun(SplitterData); 
2263  298 

5304  299 
val split_tac = Splitter.split_tac; 
300 
val split_inside_tac = Splitter.split_inside_tac; 

301 
val split_asm_tac = Splitter.split_asm_tac; 

5307  302 
val op addsplits = Splitter.addsplits; 
303 
val op delsplits = Splitter.delsplits; 

5304  304 
val Addsplits = Splitter.Addsplits; 
305 
val Delsplits = Splitter.Delsplits; 

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

306 

2134  307 
val mksimps_pairs = 
308 
[("op >", [mp]), ("op &", [conjunct1,conjunct2]), 

309 
("All", [spec]), ("True", []), ("False", []), 

16587  310 
("HOL.If", [if_bool_eq_conj RS iffD1])]; 
1758  311 

13568
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset

312 
(* 
5304  313 
val mk_atomize: (string * thm list) list > thm > thm list 
13568
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset

314 
looks too specific to move it somewhere else 
5304  315 
*) 
316 
fun mk_atomize pairs = 

317 
let fun atoms th = 

318 
(case concl_of th of 

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

320 
(case head_of p of 

321 
Const(a,_) => 

17325  322 
(case AList.lookup (op =) pairs a of 
15570  323 
SOME(rls) => List.concat (map atoms ([th] RL rls)) 
15531  324 
 NONE => [th]) 
5304  325 
 _ => [th]) 
326 
 _ => [th]) 

327 
in atoms end; 

328 

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

329 
fun mksimps pairs = 
15570  330 
(List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all); 
5304  331 

7570  332 
fun unsafe_solver_tac prems = 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

333 
(fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' 
7570  334 
FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE]; 
335 
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; 

336 

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

337 
(*No premature instantiation of variables during simplification*) 
7570  338 
fun safe_solver_tac prems = 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

339 
(fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' 
7570  340 
FIRST'[match_tac(reflexive_thm::TrueI::refl::prems), 
341 
eq_assume_tac, ematch_tac [FalseE]]; 

342 
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

343 

9713  344 
val HOL_basic_ss = 
17892  345 
Simplifier.theory_context (the_context ()) empty_ss 
346 
setsubgoaler asm_simp_tac 

9713  347 
setSSolver safe_solver 
348 
setSolver unsafe_solver 

349 
setmksimps (mksimps mksimps_pairs) 

350 
setmkeqTrue mk_eq_True 

351 
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

352 

18324  353 
fun unfold_tac ths = 
354 
let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths 

355 
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; 

17003  356 

13568
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset

357 
(*In general it seems wrong to add distributive laws by default: they 
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset

358 
might cause exponential blowup. But imp_disjL has been in for a while 
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset

359 
and cannot be removed without affecting existing proofs. Moreover, 
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset

360 
rewriting by "(PQ > R) = ((P>R)&(Q>R))" might be justified on the 
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset

361 
grounds that it allows simplification of R in the two cases.*) 
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset

362 

9713  363 
val HOL_ss = 
364 
HOL_basic_ss addsimps 

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

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

368 
if_True, if_False, if_cancel, if_eq_cancel, 
5304  369 
imp_disjL, conj_assoc, disj_assoc, 
3904  370 
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

371 
disj_not1, not_all, not_ex, cases_simp, 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
13743
diff
changeset

372 
thm "the_eq_trivial", the_sym_eq_trivial] 
3446
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3282
diff
changeset

373 
@ ex_simps @ all_simps @ simp_thms) 
17778  374 
addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc] 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

375 
addcongs [imp_cong, simp_implies_cong] 
4830  376 
addsplits [split_if]; 
2082  377 

11034  378 
fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); 
379 

380 

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

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

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

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

386 
qed "if_cong"; 

387 

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

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

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

392 
qed "if_weak_cong"; 

6293  393 

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

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

397 
qed "let_weak_cong"; 

6293  398 

12975  399 
(*To tidy up the result of a simproc. Only the RHS will be simplified.*) 
400 
Goal "u = u' ==> (t==u) == (t==u')"; 

401 
by (asm_simp_tac HOL_ss 1); 

402 
qed "eq_cong2"; 

403 

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

406 
qed "if_distrib"; 

1655  407 

4327  408 
(*For expand_case_tac*) 
7584  409 
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

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

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

413 

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

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

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

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

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

420 

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

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

424 
by (asm_simp_tac HOL_ss 1); 

425 
qed "restrict_to_left"; 

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

426 

7357  427 
(* default simpset *) 
9713  428 
val simpsetup = 
17875  429 
[fn thy => (change_simpset_of thy (fn _ => 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

430 

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

431 

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

433 

5219  434 
structure Clasimp = ClasimpFun 
8473  435 
(structure Simplifier = Simplifier and Splitter = Splitter 
9851  436 
and Classical = Classical and Blast = Blast 
11344  437 
val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE 
9851  438 
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

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

440 

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

441 
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

442 

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

443 

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

444 

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

445 
(*** A general refutation procedure ***) 
9713  446 

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

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

448 

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

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

450 
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

451 
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

452 
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

453 

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

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

455 
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

456 
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

457 

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

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

459 
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

460 
[ A1; ...; An ] ==> False 
9876  461 
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

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

463 

15184  464 
local 
465 
val nnf_simpset = 

17892  466 
empty_ss setmkeqTrue mk_eq_True 
467 
setmksimps (mksimps mksimps_pairs) 

468 
addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, 

469 
not_all,not_ex,not_not]; 

470 
fun prem_nnf_tac i st = 

471 
full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st; 

15184  472 
in 
473 
fun refute_tac test prep_tac ref_tac = 

474 
let val refute_prems_tac = 

12475  475 
REPEAT_DETERM 
476 
(eresolve_tac [conjE, exE] 1 ORELSE 

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

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

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

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

481 
in EVERY'[TRY o filter_prems_tac test, 
12475  482 
REPEAT_DETERM 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

483 
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

484 
end; 
17003  485 
end; 