author  wenzelm 
Thu, 15 Oct 2009 23:28:10 +0200  
changeset 32952  aeb1e44fbc19 
parent 32727  9072201cd69d 
child 36945  9bec62c10714 
permissions  rwrr 
23150  1 
(* Title: HOL/Tools/TFL/casesplit.ML 
2 
Author: Lucas Dixon, University of Edinburgh 

3 

4 
A structure that defines a tactic to program case splits. 

5 

6 
casesplit_free : 

7 
string * typ > int > thm > thm Seq.seq 

8 

9 
casesplit_name : 

10 
string > int > thm > thm Seq.seq 

11 

12 
These use the induction theorem associated with the recursive data 

13 
type to be split. 

14 

15 
The structure includes a function to try and recursively split a 

16 
conjecture into a list subtheorems: 

17 

18 
splitto : thm list > thm > thm 

19 
*) 

20 

21 
(* logicspecific *) 

22 
signature CASE_SPLIT_DATA = 

23 
sig 

24 
val dest_Trueprop : term > term 

25 
val mk_Trueprop : term > term 

26 
val atomize : thm list 

27 
val rulify : thm list 

28 
end; 

29 

30 
structure CaseSplitData_HOL : CASE_SPLIT_DATA = 

31 
struct 

32 
val dest_Trueprop = HOLogic.dest_Trueprop; 

33 
val mk_Trueprop = HOLogic.mk_Trueprop; 

34 

35 
val atomize = thms "induct_atomize"; 

36 
val rulify = thms "induct_rulify"; 

37 
val rulify_fallback = thms "induct_rulify_fallback"; 

38 

39 
end; 

40 

41 

42 
signature CASE_SPLIT = 

43 
sig 

44 
(* failure to find a free to split on *) 

45 
exception find_split_exp of string 

46 

47 
(* getting a case split thm from the induction thm *) 

48 
val case_thm_of_ty : theory > typ > thm 

49 
val cases_thm_of_induct_thm : thm > thm 

50 

51 
(* case split tactics *) 

52 
val casesplit_free : 

53 
string * typ > int > thm > thm Seq.seq 

54 
val casesplit_name : string > int > thm > thm Seq.seq 

55 

56 
(* finding a free var to split *) 

57 
val find_term_split : 

58 
term * term > (string * typ) option 

59 
val find_thm_split : 

60 
thm > int > thm > (string * typ) option 

61 
val find_thms_split : 

62 
thm list > int > thm > (string * typ) option 

63 

64 
(* try to recursively split conjectured thm to given list of thms *) 

65 
val splitto : thm list > thm > thm 

66 

67 
(* for use with the recdef package *) 

68 
val derive_init_eqs : 

69 
theory > 

70 
(thm * int) list > term list > (thm * int) list 

71 
end; 

72 

73 
functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = 

74 
struct 

75 

76 
val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify; 

77 
val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize; 

78 

79 
(* betaeta contract the theorem *) 

80 
fun beta_eta_contract thm = 

81 
let 

82 
val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm 

83 
val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 

84 
in thm3 end; 

85 

86 
(* make a casethm from an induction thm *) 

87 
val cases_thm_of_induct_thm = 

88 
Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i))); 

89 

90 
(* get the case_thm (my version) from a type *) 

31784  91 
fun case_thm_of_ty thy ty = 
23150  92 
let 
93 
val ty_str = case ty of 

94 
Type(ty_str, _) => ty_str 

95 
 TFree(s,_) => error ("Free type: " ^ s) 

96 
 TVar((s,i),_) => error ("Free variable: " ^ s) 

31784  97 
val dt = Datatype.the_info thy ty_str 
23150  98 
in 
32727  99 
cases_thm_of_induct_thm (#induct dt) 
23150  100 
end; 
101 

102 
(* 

29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
23150
diff
changeset

103 
val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t; 
23150  104 
*) 
105 

106 

107 
(* for use when there are no prems to the subgoal *) 

108 
(* does a case split on the given variable *) 

109 
fun mk_casesplit_goal_thm sgn (vstr,ty) gt = 

110 
let 

111 
val x = Free(vstr,ty) 

112 
val abst = Abs(vstr, ty, Term.abstract_over (x, gt)); 

113 

114 
val ctermify = Thm.cterm_of sgn; 

115 
val ctypify = Thm.ctyp_of sgn; 

116 
val case_thm = case_thm_of_ty sgn ty; 

117 

118 
val abs_ct = ctermify abst; 

119 
val free_ct = ctermify x; 

120 

29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
23150
diff
changeset

121 
val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm)); 
23150  122 

29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29265
diff
changeset

123 
val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm); 
23150  124 
val (Pv, Dv, type_insts) = 
125 
case (Thm.concl_of case_thm) of 

126 
(_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => 

127 
(Pv, Dv, 

128 
Sign.typ_match sgn (Dty, ty) Vartab.empty) 

129 
 _ => error "not a valid case thm"; 

130 
val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T)) 

131 
(Vartab.dest type_insts); 

32035  132 
val cPv = ctermify (Envir.subst_term_types type_insts Pv); 
133 
val cDv = ctermify (Envir.subst_term_types type_insts Dv); 

23150  134 
in 
135 
(beta_eta_contract 

136 
(case_thm 

137 
> Thm.instantiate (type_cinsts, []) 

138 
> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))) 

139 
end; 

140 

141 

142 
(* for use when there are no prems to the subgoal *) 

143 
(* does a case split on the given variable (Free fv) *) 

144 
fun casesplit_free fv i th = 

145 
let 

146 
val (subgoalth, exp) = IsaND.fix_alls i th; 

147 
val subgoalth' = atomize_goals subgoalth; 

148 
val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); 

149 
val sgn = Thm.theory_of_thm th; 

150 

151 
val splitter_thm = mk_casesplit_goal_thm sgn fv gt; 

152 
val nsplits = Thm.nprems_of splitter_thm; 

153 

154 
val split_goal_th = splitter_thm RS subgoalth'; 

155 
val rulified_split_goal_th = rulify_goals split_goal_th; 

156 
in 

157 
IsaND.export_back exp rulified_split_goal_th 

158 
end; 

159 

160 

161 
(* for use when there are no prems to the subgoal *) 

162 
(* does a case split on the given variable *) 

163 
fun casesplit_name vstr i th = 

164 
let 

165 
val (subgoalth, exp) = IsaND.fix_alls i th; 

166 
val subgoalth' = atomize_goals subgoalth; 

167 
val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); 

168 

29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
23150
diff
changeset

169 
val freets = OldTerm.term_frees gt; 
23150  170 
fun getter x = 
171 
let val (n,ty) = Term.dest_Free x in 

172 
(if vstr = n orelse vstr = Name.dest_skolem n 

173 
then SOME (n,ty) else NONE ) 

174 
handle Fail _ => NONE (* dest_skolem *) 

175 
end; 

176 
val (n,ty) = case Library.get_first getter freets 

177 
of SOME (n, ty) => (n, ty) 

178 
 _ => error ("no such variable " ^ vstr); 

179 
val sgn = Thm.theory_of_thm th; 

180 

181 
val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt; 

182 
val nsplits = Thm.nprems_of splitter_thm; 

183 

184 
val split_goal_th = splitter_thm RS subgoalth'; 

185 

186 
val rulified_split_goal_th = rulify_goals split_goal_th; 

187 
in 

188 
IsaND.export_back exp rulified_split_goal_th 

189 
end; 

190 

191 

192 
(* small example: 

193 
Goal "P (x :: nat) & (C y > Q (y :: nat))"; 

194 
by (rtac (thm "conjI") 1); 

195 
val th = topthm(); 

196 
val i = 2; 

197 
val vstr = "y"; 

198 

199 
by (casesplit_name "y" 2); 

200 

201 
val th = topthm(); 

202 
val i = 1; 

203 
val th' = casesplit_name "x" i th; 

204 
*) 

205 

206 

207 
(* the find_XXX_split functions are simply doing a lightwieght (I 

208 
think) term matching equivalent to find where to do the next split *) 

209 

210 
(* assuming two twems are identical except for a free in one at a 

211 
subterm, or constant in another, ie assume that one term is a plit of 

212 
another, then gives back the free variable that has been split. *) 

213 
exception find_split_exp of string 

214 
fun find_term_split (Free v, _ $ _) = SOME v 

215 
 find_term_split (Free v, Const _) = SOME v 

216 
 find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *) 

217 
 find_term_split (Free v, Var _) = NONE (* keep searching *) 

218 
 find_term_split (a $ b, a2 $ b2) = 

219 
(case find_term_split (a, a2) of 

220 
NONE => find_term_split (b,b2) 

221 
 vopt => vopt) 

222 
 find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) = 

223 
find_term_split (t1, t2) 

224 
 find_term_split (Const (x,ty), Const(x2,ty2)) = 

225 
if x = x2 then NONE else (* keep searching *) 

226 
raise find_split_exp (* stop now *) 

227 
"Terms are not identical upto a free varaible! (Consts)" 

228 
 find_term_split (Bound i, Bound j) = 

229 
if i = j then NONE else (* keep searching *) 

230 
raise find_split_exp (* stop now *) 

231 
"Terms are not identical upto a free varaible! (Bound)" 

232 
 find_term_split (a, b) = 

233 
raise find_split_exp (* stop now *) 

234 
"Terms are not identical upto a free varaible! (Other)"; 

235 

236 
(* assume that "splitth" is a case split form of subgoal i of "genth", 

237 
then look for a free variable to split, breaking the subgoal closer to 

238 
splitth. *) 

239 
fun find_thm_split splitth i genth = 

240 
find_term_split (Logic.get_goal (Thm.prop_of genth) i, 

241 
Thm.concl_of splitth) handle find_split_exp _ => NONE; 

242 

243 
(* as above but searches "splitths" for a theorem that suggest a case split *) 

244 
fun find_thms_split splitths i genth = 

245 
Library.get_first (fn sth => find_thm_split sth i genth) splitths; 

246 

247 

248 
(* split the subgoal i of "genth" until we get to a member of 

249 
splitths. Assumes that genth will be a general form of splitths, that 

250 
can be casesplit, as needed. Otherwise fails. Note: We assume that 

251 
all of "splitths" are split to the same level, and thus it doesn't 

252 
matter which one we choose to look for the next split. Simply add 

253 
search on splitthms and split variable, to change this. *) 

254 
(* Note: possible efficiency measure: when a case theorem is no longer 

255 
useful, drop it? *) 

256 
(* Note: This should not be a separate tactic but integrated into the 

257 
case split done during recdef's case analysis, this would avoid us 

258 
having to (re)search for variables to split. *) 

259 
fun splitto splitths genth = 

260 
let 

261 
val _ = not (null splitths) orelse error "splitto: no given splitths"; 

262 
val sgn = Thm.theory_of_thm genth; 

263 

264 
(* check if we are a member of splitths  FIXME: quicker and 

265 
more flexible with discrim net. *) 

266 
fun solve_by_splitth th split = 

267 
Thm.biresolution false [(false,split)] 1 th; 

268 

269 
fun split th = 

270 
(case find_thms_split splitths 1 th of 

271 
NONE => 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32035
diff
changeset

272 
(writeln (cat_lines 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32035
diff
changeset

273 
(["th:", Display.string_of_thm_without_context th, "split ths:"] @ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32035
diff
changeset

274 
map Display.string_of_thm_without_context splitths @ ["\n"])); 
23150  275 
error "splitto: cannot find variable to split on") 
276 
 SOME v => 

277 
let 

278 
val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0)); 

279 
val split_thm = mk_casesplit_goal_thm sgn v gt; 

280 
val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm; 

281 
in 

282 
expf (map recsplitf subthms) 

283 
end) 

284 

285 
and recsplitf th = 

286 
(* note: multiple unifiers! we only take the first element, 

287 
probably fine  there is probably only one anyway. *) 

288 
(case Library.get_first (Seq.pull o solve_by_splitth th) splitths of 

289 
NONE => split th 

290 
 SOME (solved_th, more) => solved_th) 

291 
in 

292 
recsplitf genth 

293 
end; 

294 

295 

296 
(* Note: We dont do this if wf conditions fail to be solved, as each 

297 
case may have a different wf condition  we could group the conditions 

298 
togeather and say that they must be true to solve the general case, 

299 
but that would hide from the user which subcase they were related 

300 
to. Probably this is not important, and it would work fine, but I 

301 
prefer leaving more fine grain control to the user. *) 

302 

303 
(* derive eqs, assuming strict, ie the rules have no assumptions = all 

304 
the wellfoundness conditions have been solved. *) 

305 
fun derive_init_eqs sgn rules eqs = 

306 
let 

307 
fun get_related_thms i = 

32952  308 
map_filter ((fn (r, x) => if x = i then SOME r else NONE)); 
23150  309 
fun add_eq (i, e) xs = 
310 
(e, (get_related_thms i rules), i) :: xs 

311 
fun solve_eq (th, [], i) = 

312 
error "derive_init_eqs: missing rules" 

313 
 solve_eq (th, [a], i) = (a, i) 

314 
 solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i); 

315 
val eqths = 

316 
map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs; 

317 
in 

318 
[] 

319 
> fold_index add_eq eqths 

320 
> map solve_eq 

321 
> rev 

322 
end; 

323 

324 
end; 

325 

326 

327 
structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL); 