author  berghofe 
Fri, 01 Jul 2005 13:54:12 +0200  
changeset 16633  208ebc9311f2 
parent 16587  b34c8aa657a5 
child 16999  307b2ec590ff 
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 

15423  138 
(*** Simproc for Let ***) 
139 

140 
val use_let_simproc = ref true; 

141 

142 
local 

143 
val Let_folded = thm "Let_folded"; 

144 
val Let_unfold = thm "Let_unfold"; 

145 

146 
val f_Let_unfold = 

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

148 
val f_Let_folded = 

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

150 
val g_Let_folded = 

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

152 
in 

153 
val let_simproc = 

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

155 
(fn sg => fn ss => fn t => 

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

15531  157 
if not (!use_let_simproc) then NONE 
15423  158 
else if is_Free x orelse is_Bound x orelse is_Const x 
15531  159 
then SOME Let_def 
15423  160 
else 
161 
let 

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

163 
val cx = cterm_of sg x; 

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

165 
val cf = cterm_of sg f; 

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

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

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

169 
in (if (g aconv g') 

170 
then 

171 
let 

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

15531  173 
in SOME (rl OF [fx_g]) end 
174 
else if betapply (f,x) aconv g then NONE (* avoid identity conversion *) 

15423  175 
else let 
176 
val abs_g'= Abs (n,xT,g'); 

177 
val g'x = abs_g'$x; 

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

179 
val rl = cterm_instantiate 

180 
[(f_Let_folded,cterm_of sg f), 

181 
(g_Let_folded,cterm_of sg abs_g')] 

182 
Let_folded; 

15531  183 
in SOME (rl OF [transitive fx_g g_g'x]) end) 
15423  184 
end 
15531  185 
 _ => NONE)) 
15423  186 
end 
4351  187 

188 
(*** Case splitting ***) 

3913  189 

12278  190 
(*Make metaequalities. The operator below is Trueprop*) 
191 

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

192 
fun mk_meta_eq r = r RS eq_reflection; 
12278  193 
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; 
194 

195 
fun mk_eq th = case concl_of th of 

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

197 
 _$(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

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

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

200 
(* Expects Trueprop(.) if not == *) 
12278  201 

202 
fun mk_eq_True r = 

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

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

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

206 
(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

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

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

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

210 
val {sign, ...} = rep_thm st; 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

211 
fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

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

213 
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

214 
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

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

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

217 
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

218 
fun mk_simp_implies Q = foldr (fn (R, S) => 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

219 
Const ("HOL.simp_implies", propT > propT > propT) $ R $ S) Q Ps 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

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

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

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

223 
in prove_goalw_cterm [simp_implies_def] 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

224 
(cterm_of sign (Logic.mk_implies 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

225 
(mk_simp_implies (Logic.mk_equals (x, y)), 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

226 
mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))))) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

227 
(fn hyps => [REPEAT (ares_tac (meta_eq_to_obj_eq :: hyps) 1)]) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

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

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

230 

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

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

233 
(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

234 
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

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

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

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

238 
end); 
12278  239 

240 
(* Elimination of True from asumptions: *) 

241 

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

243 
in val True_implies_equals = standard' (equal_intr 

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

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

246 
end; 

247 

248 

5304  249 
structure SplitterData = 
250 
struct 

251 
structure Simplifier = Simplifier 

5552  252 
val mk_eq = mk_eq 
5304  253 
val meta_eq_to_iff = meta_eq_to_obj_eq 
254 
val iffD = iffD2 

255 
val disjE = disjE 

256 
val conjE = conjE 

257 
val exE = exE 

10231  258 
val contrapos = contrapos_nn 
259 
val contrapos2 = contrapos_pp 

5304  260 
val notnotD = notnotD 
261 
end; 

4681  262 

5304  263 
structure Splitter = SplitterFun(SplitterData); 
2263  264 

5304  265 
val split_tac = Splitter.split_tac; 
266 
val split_inside_tac = Splitter.split_inside_tac; 

267 
val split_asm_tac = Splitter.split_asm_tac; 

5307  268 
val op addsplits = Splitter.addsplits; 
269 
val op delsplits = Splitter.delsplits; 

5304  270 
val Addsplits = Splitter.Addsplits; 
271 
val Delsplits = Splitter.Delsplits; 

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

272 

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

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

16587  276 
("HOL.If", [if_bool_eq_conj RS iffD1])]; 
1758  277 

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

278 
(* 
5304  279 
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

280 
looks too specific to move it somewhere else 
5304  281 
*) 
282 
fun mk_atomize pairs = 

283 
let fun atoms th = 

284 
(case concl_of th of 

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

286 
(case head_of p of 

287 
Const(a,_) => 

288 
(case assoc(pairs,a) of 

15570  289 
SOME(rls) => List.concat (map atoms ([th] RL rls)) 
15531  290 
 NONE => [th]) 
5304  291 
 _ => [th]) 
292 
 _ => [th]) 

293 
in atoms end; 

294 

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

295 
fun mksimps pairs = 
15570  296 
(List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all); 
5304  297 

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

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

302 

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

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

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

308 
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

309 

9713  310 
val HOL_basic_ss = 
311 
empty_ss setsubgoaler asm_simp_tac 

312 
setSSolver safe_solver 

313 
setSolver unsafe_solver 

314 
setmksimps (mksimps mksimps_pairs) 

315 
setmkeqTrue mk_eq_True 

316 
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

317 

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

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

319 
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

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

321 
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

322 
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

323 

9713  324 
val HOL_ss = 
325 
HOL_basic_ss addsimps 

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

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

329 
if_True, if_False, if_cancel, if_eq_cancel, 
5304  330 
imp_disjL, conj_assoc, disj_assoc, 
3904  331 
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

332 
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

333 
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

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

336 
addcongs [imp_cong, simp_implies_cong] 
4830  337 
addsplits [split_if]; 
2082  338 

11034  339 
fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); 
340 

341 

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

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

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

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

347 
qed "if_cong"; 

348 

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

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

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

353 
qed "if_weak_cong"; 

6293  354 

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

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

358 
qed "let_weak_cong"; 

6293  359 

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

362 
by (asm_simp_tac HOL_ss 1); 

363 
qed "eq_cong2"; 

364 

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

367 
qed "if_distrib"; 

1655  368 

4327  369 
(*For expand_case_tac*) 
7584  370 
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

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

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

374 

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

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

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

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

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

381 

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

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

385 
by (asm_simp_tac HOL_ss 1); 

386 
qed "restrict_to_left"; 

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

387 

7357  388 
(* default simpset *) 
9713  389 
val simpsetup = 
390 
[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

391 

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

392 

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

394 

5219  395 
structure Clasimp = ClasimpFun 
8473  396 
(structure Simplifier = Simplifier and Splitter = Splitter 
9851  397 
and Classical = Classical and Blast = Blast 
11344  398 
val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE 
9851  399 
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

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

401 

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

402 
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

403 

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

404 

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

405 

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

406 
(*** A general refutation procedure ***) 
9713  407 

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

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

409 

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

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

411 
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

412 
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

413 
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

414 

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

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

416 
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

417 
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

418 

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

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

420 
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

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

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

424 

15184  425 
local 
426 
val nnf_simps = 

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

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

428 
not_all,not_ex,not_not]; 
15184  429 
val nnf_simpset = 
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset

430 
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

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

432 
addsimps nnf_simps; 
15184  433 
val prem_nnf_tac = full_simp_tac nnf_simpset 
434 
in 

435 
fun refute_tac test prep_tac ref_tac = 

436 
let val refute_prems_tac = 

12475  437 
REPEAT_DETERM 
438 
(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

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

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

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

443 
in EVERY'[TRY o filter_prems_tac test, 
12475  444 
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

445 
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

446 
end; 
15184  447 
end; 