author  wenzelm 
Sat, 25 Jul 2015 23:41:53 +0200  
changeset 60781  2da59cdf531c 
parent 60774  6c28d8ed2488 
child 60825  bacfb7c45d81 
permissions  rwrr 
60520  1 
(* Title: HOL/Tools/old_recdef.ML 
2 
Author: Konrad Slind, Cambridge University Computer Laboratory 

3 
Author: Lucas Dixon, University of Edinburgh 

4 

5 
Old TFL/recdef package. 

6 
*) 

7 

8 
signature CASE_SPLIT = 

9 
sig 

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

11 
val splitto : Proof.context > thm list > thm > thm 

12 
end; 

13 

14 
signature UTILS = 

15 
sig 

16 
exception ERR of {module: string, func: string, mesg: string} 

17 
val end_itlist: ('a > 'a > 'a) > 'a list > 'a 

18 
val itlist2: ('a > 'b > 'c > 'c) > 'a list > 'b list > 'c > 'c 

19 
val pluck: ('a > bool) > 'a list > 'a * 'a list 

20 
val zip3: 'a list > 'b list > 'c list > ('a*'b*'c) list 

21 
val take: ('a > 'b) > int * 'a list > 'b list 

22 
end; 

23 

24 
signature USYNTAX = 

25 
sig 

26 
datatype lambda = VAR of {Name : string, Ty : typ} 

27 
 CONST of {Name : string, Ty : typ} 

28 
 COMB of {Rator: term, Rand : term} 

29 
 LAMB of {Bvar : term, Body : term} 

30 

31 
val alpha : typ 

32 

33 
(* Types *) 

34 
val type_vars : typ > typ list 

35 
val type_varsl : typ list > typ list 

36 
val mk_vartype : string > typ 

37 
val is_vartype : typ > bool 

38 
val strip_prod_type : typ > typ list 

39 

40 
(* Terms *) 

41 
val free_vars_lr : term > term list 

42 
val type_vars_in_term : term > typ list 

43 
val dest_term : term > lambda 

44 

45 
(* Prelogic *) 

46 
val inst : (typ*typ) list > term > term 

47 

48 
(* Construction routines *) 

49 
val mk_abs :{Bvar : term, Body : term} > term 

50 

51 
val mk_imp :{ant : term, conseq : term} > term 

52 
val mk_select :{Bvar : term, Body : term} > term 

53 
val mk_forall :{Bvar : term, Body : term} > term 

54 
val mk_exists :{Bvar : term, Body : term} > term 

55 
val mk_conj :{conj1 : term, conj2 : term} > term 

56 
val mk_disj :{disj1 : term, disj2 : term} > term 

57 
val mk_pabs :{varstruct : term, body : term} > term 

58 

59 
(* Destruction routines *) 

60 
val dest_const: term > {Name : string, Ty : typ} 

61 
val dest_comb : term > {Rator : term, Rand : term} 

62 
val dest_abs : string list > term > {Bvar : term, Body : term} * string list 

63 
val dest_eq : term > {lhs : term, rhs : term} 

64 
val dest_imp : term > {ant : term, conseq : term} 

65 
val dest_forall : term > {Bvar : term, Body : term} 

66 
val dest_exists : term > {Bvar : term, Body : term} 

67 
val dest_neg : term > term 

68 
val dest_conj : term > {conj1 : term, conj2 : term} 

69 
val dest_disj : term > {disj1 : term, disj2 : term} 

70 
val dest_pair : term > {fst : term, snd : term} 

71 
val dest_pabs : string list > term > {varstruct : term, body : term, used : string list} 

72 

73 
val lhs : term > term 

74 
val rhs : term > term 

75 
val rand : term > term 

76 

77 
(* Query routines *) 

78 
val is_imp : term > bool 

79 
val is_forall : term > bool 

80 
val is_exists : term > bool 

81 
val is_neg : term > bool 

82 
val is_conj : term > bool 

83 
val is_disj : term > bool 

84 
val is_pair : term > bool 

85 
val is_pabs : term > bool 

86 

87 
(* Construction of a term from a list of Preterms *) 

88 
val list_mk_abs : (term list * term) > term 

89 
val list_mk_imp : (term list * term) > term 

90 
val list_mk_forall : (term list * term) > term 

91 
val list_mk_conj : term list > term 

92 

93 
(* Destructing a term to a list of Preterms *) 

94 
val strip_comb : term > (term * term list) 

95 
val strip_abs : term > (term list * term) 

96 
val strip_imp : term > (term list * term) 

97 
val strip_forall : term > (term list * term) 

98 
val strip_exists : term > (term list * term) 

99 
val strip_disj : term > term list 

100 

101 
(* Miscellaneous *) 

102 
val mk_vstruct : typ > term list > term 

103 
val gen_all : term > term 

104 
val find_term : (term > bool) > term > term option 

105 
val dest_relation : term > term * term * term 

106 
val is_WFR : term > bool 

107 
val ARB : typ > term 

108 
end; 

109 

110 
signature DCTERM = 

111 
sig 

112 
val dest_comb: cterm > cterm * cterm 

113 
val dest_abs: string option > cterm > cterm * cterm 

114 
val capply: cterm > cterm > cterm 

115 
val cabs: cterm > cterm > cterm 

116 
val mk_conj: cterm * cterm > cterm 

117 
val mk_disj: cterm * cterm > cterm 

118 
val mk_exists: cterm * cterm > cterm 

119 
val dest_conj: cterm > cterm * cterm 

120 
val dest_const: cterm > {Name: string, Ty: typ} 

121 
val dest_disj: cterm > cterm * cterm 

122 
val dest_eq: cterm > cterm * cterm 

123 
val dest_exists: cterm > cterm * cterm 

124 
val dest_forall: cterm > cterm * cterm 

125 
val dest_imp: cterm > cterm * cterm 

126 
val dest_neg: cterm > cterm 

127 
val dest_pair: cterm > cterm * cterm 

128 
val dest_var: cterm > {Name:string, Ty:typ} 

129 
val is_conj: cterm > bool 

130 
val is_disj: cterm > bool 

131 
val is_eq: cterm > bool 

132 
val is_exists: cterm > bool 

133 
val is_forall: cterm > bool 

134 
val is_imp: cterm > bool 

135 
val is_neg: cterm > bool 

136 
val is_pair: cterm > bool 

137 
val list_mk_disj: cterm list > cterm 

138 
val strip_abs: cterm > cterm list * cterm 

139 
val strip_comb: cterm > cterm * cterm list 

140 
val strip_disj: cterm > cterm list 

141 
val strip_exists: cterm > cterm list * cterm 

142 
val strip_forall: cterm > cterm list * cterm 

143 
val strip_imp: cterm > cterm list * cterm 

144 
val drop_prop: cterm > cterm 

145 
val mk_prop: cterm > cterm 

146 
end; 

147 

148 
signature RULES = 

149 
sig 

150 
val dest_thm: thm > term list * term 

151 

152 
(* Inference rules *) 

153 
val REFL: cterm > thm 

154 
val ASSUME: cterm > thm 

155 
val MP: thm > thm > thm 

156 
val MATCH_MP: thm > thm > thm 

157 
val CONJUNCT1: thm > thm 

158 
val CONJUNCT2: thm > thm 

159 
val CONJUNCTS: thm > thm list 

160 
val DISCH: cterm > thm > thm 

161 
val UNDISCH: thm > thm 

162 
val SPEC: cterm > thm > thm 

163 
val ISPEC: cterm > thm > thm 

164 
val ISPECL: cterm list > thm > thm 

165 
val GEN: Proof.context > cterm > thm > thm 

166 
val GENL: Proof.context > cterm list > thm > thm 

167 
val LIST_CONJ: thm list > thm 

168 

169 
val SYM: thm > thm 

170 
val DISCH_ALL: thm > thm 

171 
val FILTER_DISCH_ALL: (term > bool) > thm > thm 

172 
val SPEC_ALL: thm > thm 

173 
val GEN_ALL: Proof.context > thm > thm 

174 
val IMP_TRANS: thm > thm > thm 

175 
val PROVE_HYP: thm > thm > thm 

176 

177 
val CHOOSE: Proof.context > cterm * thm > thm > thm 

60781  178 
val EXISTS: Proof.context > cterm * cterm > thm > thm 
60520  179 
val IT_EXISTS: Proof.context > (cterm * cterm) list > thm > thm 
180 

181 
val EVEN_ORS: thm list > thm list 

182 
val DISJ_CASESL: thm > thm list > thm 

183 

184 
val list_beta_conv: cterm > cterm list > thm 

185 
val SUBS: Proof.context > thm list > thm > thm 

186 
val simpl_conv: Proof.context > thm list > cterm > thm 

187 

188 
val rbeta: thm > thm 

189 
val tracing: bool Unsynchronized.ref 

190 
val CONTEXT_REWRITE_RULE: Proof.context > 

191 
term * term list * thm * thm list > thm > thm * term list 

192 
val RIGHT_ASSOC: Proof.context > thm > thm 

193 

194 
val prove: Proof.context > bool > term * tactic > thm 

195 
end; 

196 

197 
signature THRY = 

198 
sig 

199 
val match_term: theory > term > term > (term * term) list * (typ * typ) list 

200 
val match_type: theory > typ > typ > (typ * typ) list 

201 
val typecheck: theory > term > cterm 

202 
(*datatype facts of various flavours*) 

203 
val match_info: theory > string > {constructors: term list, case_const: term} option 

204 
val induct_info: theory > string > {constructors: term list, nchotomy: thm} option 

205 
val extract_info: theory > {case_congs: thm list, case_rewrites: thm list} 

206 
end; 

207 

208 
signature PRIM = 

209 
sig 

210 
val trace: bool Unsynchronized.ref 

211 
val trace_thms: Proof.context > string > thm list > unit 

212 
val trace_cterm: Proof.context > string > cterm > unit 

213 
type pattern 

214 
val mk_functional: theory > term list > {functional: term, pats: pattern list} 

215 
val wfrec_definition0: string > term > term > theory > thm * theory 

216 
val post_definition: Proof.context > thm list > thm * pattern list > 

217 
{rules: thm, 

218 
rows: int list, 

219 
TCs: term list list, 

220 
full_pats_TCs: (term * term list) list} 

60699  221 
val mk_induction: Proof.context > 
60520  222 
{fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} > thm 
223 
val postprocess: Proof.context > bool > 

224 
{wf_tac: tactic, terminator: tactic, simplifier: cterm > thm} > 

225 
{rules: thm, induction: thm, TCs: term list list} > 

226 
{rules: thm, induction: thm, nested_tcs: thm list} 

227 
end; 

228 

229 
signature TFL = 

230 
sig 

231 
val define_i: bool > thm list > thm list > xstring > term > term list > Proof.context > 

232 
{lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context 

233 
val define: bool > thm list > thm list > xstring > string > string list > Proof.context > 

234 
{lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context 

235 
end; 

236 

237 
signature OLD_RECDEF = 

238 
sig 

239 
val get_recdef: theory > string 

240 
> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option 

241 
val get_hints: Proof.context > {simps: thm list, congs: (string * thm) list, wfs: thm list} 

242 
val simp_add: attribute 

243 
val simp_del: attribute 

244 
val cong_add: attribute 

245 
val cong_del: attribute 

246 
val wf_add: attribute 

247 
val wf_del: attribute 

248 
val add_recdef: bool > xstring > string > ((binding * string) * Token.src list) list > 

249 
Token.src option > theory > theory 

250 
* {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} 

251 
val add_recdef_i: bool > xstring > term > ((binding * term) * attribute list) list > 

252 
theory > theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} 

253 
end; 

254 

255 
structure Old_Recdef: OLD_RECDEF = 

256 
struct 

257 

258 
(*** extra case splitting for TFL ***) 

259 

260 
structure CaseSplit: CASE_SPLIT = 

261 
struct 

262 

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

60752  264 
fun cases_thm_of_induct_thm ctxt = 
265 
Seq.hd o (ALLGOALS (fn i => REPEAT (eresolve_tac ctxt [Drule.thin_rl] i))); 

60520  266 

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

60752  268 
fun case_thm_of_ty ctxt ty = 
60520  269 
let 
60752  270 
val thy = Proof_Context.theory_of ctxt 
60520  271 
val ty_str = case ty of 
272 
Type(ty_str, _) => ty_str 

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

60521  274 
 TVar((s,_),_) => error ("Free variable: " ^ s) 
60520  275 
val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str 
276 
in 

60752  277 
cases_thm_of_induct_thm ctxt induct 
60520  278 
end; 
279 

280 

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

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

283 
fun mk_casesplit_goal_thm ctxt (vstr,ty) gt = 

284 
let 

285 
val thy = Proof_Context.theory_of ctxt; 

286 

287 
val x = Free(vstr,ty); 

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

289 

60752  290 
val case_thm = case_thm_of_ty ctxt ty; 
60520  291 

292 
val abs_ct = Thm.cterm_of ctxt abst; 

293 
val free_ct = Thm.cterm_of ctxt x; 

294 

295 
val (Pv, Dv, type_insts) = 

296 
case (Thm.concl_of case_thm) of 

60521  297 
(_ $ (Pv $ (Dv as Var(_, Dty)))) => 
60520  298 
(Pv, Dv, 
299 
Sign.typ_match thy (Dty, ty) Vartab.empty) 

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

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60524
diff
changeset

301 
val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) 
60520  302 
(Vartab.dest type_insts); 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60524
diff
changeset

303 
val Pv = dest_Var (Envir.subst_term_types type_insts Pv); 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60524
diff
changeset

304 
val Dv = dest_Var (Envir.subst_term_types type_insts Dv); 
60520  305 
in 
306 
Conv.fconv_rule Drule.beta_eta_conversion 

307 
(case_thm 

308 
> Thm.instantiate (type_cinsts, []) 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60524
diff
changeset

309 
> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)])) 
60520  310 
end; 
311 

312 

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

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

315 

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

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

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

319 
exception find_split_exp of string 

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

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

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

60521  323 
 find_term_split (Free _, Var _) = NONE (* keep searching *) 
60520  324 
 find_term_split (a $ b, a2 $ b2) = 
325 
(case find_term_split (a, a2) of 

326 
NONE => find_term_split (b,b2) 

327 
 vopt => vopt) 

60521  328 
 find_term_split (Abs(_,_,t1), Abs(_,_,t2)) = 
60520  329 
find_term_split (t1, t2) 
60521  330 
 find_term_split (Const (x,_), Const(x2,_)) = 
60520  331 
if x = x2 then NONE else (* keep searching *) 
332 
raise find_split_exp (* stop now *) 

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

334 
 find_term_split (Bound i, Bound j) = 

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

336 
raise find_split_exp (* stop now *) 

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

338 
 find_term_split _ = 

339 
raise find_split_exp (* stop now *) 

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

341 

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

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

344 
splitth. *) 

345 
fun find_thm_split splitth i genth = 

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

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

348 

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

350 
fun find_thms_split splitths i genth = 

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

352 

353 

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

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

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

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

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

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

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

361 
useful, drop it? *) 

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

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

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

365 
fun splitto ctxt splitths genth = 

366 
let 

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

368 

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

370 
more flexible with discrim net. *) 

371 
fun solve_by_splitth th split = 

372 
Thm.biresolution (SOME ctxt) false [(false,split)] 1 th; 

373 

374 
fun split th = 

375 
(case find_thms_split splitths 1 th of 

376 
NONE => 

377 
(writeln (cat_lines 

378 
(["th:", Display.string_of_thm ctxt th, "split ths:"] @ 

379 
map (Display.string_of_thm ctxt) splitths @ ["\n"])); 

380 
error "splitto: cannot find variable to split on") 

381 
 SOME v => 

382 
let 

383 
val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th))); 

384 
val split_thm = mk_casesplit_goal_thm ctxt v gt; 

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

386 
in 

387 
expf (map recsplitf subthms) 

388 
end) 

389 

390 
and recsplitf th = 

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

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

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

394 
NONE => split th 

395 
 SOME (solved_th, _) => solved_th); 

396 
in 

397 
recsplitf genth 

398 
end; 

399 

400 
end; 

401 

402 

60521  403 

60520  404 
(*** basic utilities ***) 
405 

406 
structure Utils: UTILS = 

407 
struct 

408 

409 
(*standard exception for TFL*) 

410 
exception ERR of {module: string, func: string, mesg: string}; 

411 

412 
fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg}; 

413 

414 

60521  415 
fun end_itlist _ [] = raise (UTILS_ERR "end_itlist" "list too short") 
416 
 end_itlist _ [x] = x 

60520  417 
 end_itlist f (x :: xs) = f x (end_itlist f xs); 
418 

419 
fun itlist2 f L1 L2 base_value = 

420 
let fun it ([],[]) = base_value 

421 
 it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2)) 

422 
 it _ = raise UTILS_ERR "itlist2" "different length lists" 

423 
in it (L1,L2) 

424 
end; 

425 

426 
fun pluck p = 

427 
let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found" 

428 
 remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A) 

429 
in fn L => remv(L,[]) 

430 
end; 

431 

432 
fun take f = 

60521  433 
let fun grab(0, _) = [] 
60520  434 
 grab(n, x::rst) = f x::grab(n1,rst) 
435 
in grab 

436 
end; 

437 

438 
fun zip3 [][][] = [] 

439 
 zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3 

440 
 zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths"; 

441 

442 

443 
end; 

444 

445 

60521  446 

60520  447 
(*** emulation of HOL's abstract syntax functions ***) 
448 

449 
structure USyntax: USYNTAX = 

450 
struct 

451 

452 
infix 4 ##; 

453 

454 
fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg}; 

455 

456 

457 
(* 

458 
* 

459 
* Types 

460 
* 

461 
**) 

462 
val mk_prim_vartype = TVar; 

463 
fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type}); 

464 

465 
(* But internally, it's useful *) 

466 
fun dest_vtype (TVar x) = x 

467 
 dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable"; 

468 

469 
val is_vartype = can dest_vtype; 

470 

471 
val type_vars = map mk_prim_vartype o Misc_Legacy.typ_tvars 

472 
fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []); 

473 

474 
val alpha = mk_vartype "'a" 

475 

476 
val strip_prod_type = HOLogic.flatten_tupleT; 

477 

478 

479 

480 
(* 

481 
* 

482 
* Terms 

483 
* 

484 
**) 

485 

486 
(* Free variables, in order of occurrence, from left to right in the 

487 
* syntax tree. *) 

488 
fun free_vars_lr tm = 

489 
let fun memb x = let fun m[] = false  m(y::rst) = (x=y)orelse m rst in m end 

490 
fun add (t, frees) = case t of 

491 
Free _ => if (memb t frees) then frees else t::frees 

492 
 Abs (_,_,body) => add(body,frees) 

493 
 f$t => add(t, add(f, frees)) 

494 
 _ => frees 

495 
in rev(add(tm,[])) 

496 
end; 

497 

498 

499 

500 
val type_vars_in_term = map mk_prim_vartype o Misc_Legacy.term_tvars; 

501 

502 

503 

504 
(* Prelogic *) 

505 
fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty) 

506 
fun inst theta = subst_vars (map dest_tybinding theta,[]) 

507 

508 

509 
(* Construction routines *) 

510 

511 
fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) 

512 
 mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) 

513 
 mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable"; 

514 

515 

516 
fun mk_imp{ant,conseq} = 

517 
let val c = Const(@{const_name HOL.implies},HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

518 
in list_comb(c,[ant,conseq]) 

519 
end; 

520 

521 
fun mk_select (r as {Bvar,Body}) = 

522 
let val ty = type_of Bvar 

523 
val c = Const(@{const_name Eps},(ty > HOLogic.boolT) > ty) 

524 
in list_comb(c,[mk_abs r]) 

525 
end; 

526 

527 
fun mk_forall (r as {Bvar,Body}) = 

528 
let val ty = type_of Bvar 

529 
val c = Const(@{const_name All},(ty > HOLogic.boolT) > HOLogic.boolT) 

530 
in list_comb(c,[mk_abs r]) 

531 
end; 

532 

533 
fun mk_exists (r as {Bvar,Body}) = 

534 
let val ty = type_of Bvar 

535 
val c = Const(@{const_name Ex},(ty > HOLogic.boolT) > HOLogic.boolT) 

536 
in list_comb(c,[mk_abs r]) 

537 
end; 

538 

539 

540 
fun mk_conj{conj1,conj2} = 

541 
let val c = Const(@{const_name HOL.conj},HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

542 
in list_comb(c,[conj1,conj2]) 

543 
end; 

544 

545 
fun mk_disj{disj1,disj2} = 

546 
let val c = Const(@{const_name HOL.disj},HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

547 
in list_comb(c,[disj1,disj2]) 

548 
end; 

549 

550 
fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2); 

551 

552 
local 

553 
fun mk_uncurry (xt, yt, zt) = 

554 
Const(@{const_name case_prod}, (xt > yt > zt) > prod_ty xt yt > zt) 

555 
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N} 

556 
 dest_pair _ = raise USYN_ERR "dest_pair" "not a pair" 

557 
fun is_var (Var _) = true  is_var (Free _) = true  is_var _ = false 

558 
in 

559 
fun mk_pabs{varstruct,body} = 

560 
let fun mpa (varstruct, body) = 

561 
if is_var varstruct 

562 
then mk_abs {Bvar = varstruct, Body = body} 

563 
else let val {fst, snd} = dest_pair varstruct 

564 
in mk_uncurry (type_of fst, type_of snd, type_of body) $ 

565 
mpa (fst, mpa (snd, body)) 

566 
end 

567 
in mpa (varstruct, body) end 

568 
handle TYPE _ => raise USYN_ERR "mk_pabs" ""; 

569 
end; 

570 

571 
(* Destruction routines *) 

572 

573 
datatype lambda = VAR of {Name : string, Ty : typ} 

574 
 CONST of {Name : string, Ty : typ} 

575 
 COMB of {Rator: term, Rand : term} 

576 
 LAMB of {Bvar : term, Body : term}; 

577 

578 

60521  579 
fun dest_term(Var((s,_),ty)) = VAR{Name = s, Ty = ty} 
60520  580 
 dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} 
581 
 dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} 

582 
 dest_term(M$N) = COMB{Rator=M,Rand=N} 

583 
 dest_term(Abs(s,ty,M)) = let val v = Free(s,ty) 

584 
in LAMB{Bvar = v, Body = Term.betapply (M,v)} 

585 
end 

586 
 dest_term(Bound _) = raise USYN_ERR "dest_term" "Bound"; 

587 

588 
fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} 

589 
 dest_const _ = raise USYN_ERR "dest_const" "not a constant"; 

590 

591 
fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} 

592 
 dest_comb _ = raise USYN_ERR "dest_comb" "not a comb"; 

593 

60524  594 
fun dest_abs used (a as Abs(s, ty, _)) = 
60520  595 
let 
596 
val s' = singleton (Name.variant_list used) s; 

597 
val v = Free(s', ty); 

598 
in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used) 

599 
end 

600 
 dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction"; 

601 

602 
fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N} 

603 
 dest_eq _ = raise USYN_ERR "dest_eq" "not an equality"; 

604 

605 
fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N} 

606 
 dest_imp _ = raise USYN_ERR "dest_imp" "not an implication"; 

607 

608 
fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a) 

609 
 dest_forall _ = raise USYN_ERR "dest_forall" "not a forall"; 

610 

611 
fun dest_exists(Const(@{const_name Ex},_) $ (a as Abs _)) = fst (dest_abs [] a) 

612 
 dest_exists _ = raise USYN_ERR "dest_exists" "not an existential"; 

613 

614 
fun dest_neg(Const(@{const_name Not},_) $ M) = M 

615 
 dest_neg _ = raise USYN_ERR "dest_neg" "not a negation"; 

616 

617 
fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N} 

618 
 dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction"; 

619 

620 
fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N} 

621 
 dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction"; 

622 

623 
fun mk_pair{fst,snd} = 

624 
let val ty1 = type_of fst 

625 
val ty2 = type_of snd 

626 
val c = Const(@{const_name Pair},ty1 > ty2 > prod_ty ty1 ty2) 

627 
in list_comb(c,[fst,snd]) 

628 
end; 

629 

630 
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N} 

631 
 dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"; 

632 

633 

634 
local fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t 

635 
else raise Match) 

636 
in 

637 
fun dest_pabs used tm = 

638 
let val ({Bvar,Body}, used') = dest_abs used tm 

639 
in {varstruct = Bvar, body = Body, used = used'} 

640 
end handle Utils.ERR _ => 

641 
let val {Rator,Rand} = dest_comb tm 

642 
val _ = ucheck Rator 

643 
val {varstruct = lv, body, used = used'} = dest_pabs used Rand 

644 
val {varstruct = rv, body, used = used''} = dest_pabs used' body 

645 
in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''} 

646 
end 

647 
end; 

648 

649 

650 
val lhs = #lhs o dest_eq 

651 
val rhs = #rhs o dest_eq 

652 
val rand = #Rand o dest_comb 

653 

654 

655 
(* Query routines *) 

656 
val is_imp = can dest_imp 

657 
val is_forall = can dest_forall 

658 
val is_exists = can dest_exists 

659 
val is_neg = can dest_neg 

660 
val is_conj = can dest_conj 

661 
val is_disj = can dest_disj 

662 
val is_pair = can dest_pair 

663 
val is_pabs = can (dest_pabs []) 

664 

665 

666 
(* Construction of a cterm from a list of Terms *) 

667 

668 
fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm; 

669 

670 
(* These others are almost never used *) 

671 
fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c; 

672 
fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t; 

673 
val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm}) 

674 

675 

676 
(* Need to reverse? *) 

677 
fun gen_all tm = list_mk_forall(Misc_Legacy.term_frees tm, tm); 

678 

679 
(* Destructing a cterm to a list of Terms *) 

680 
fun strip_comb tm = 

681 
let fun dest(M$N, A) = dest(M, N::A) 

682 
 dest x = x 

683 
in dest(tm,[]) 

684 
end; 

685 

686 
fun strip_abs(tm as Abs _) = 

687 
let val ({Bvar,Body}, _) = dest_abs [] tm 

688 
val (bvs, core) = strip_abs Body 

689 
in (Bvar::bvs, core) 

690 
end 

691 
 strip_abs M = ([],M); 

692 

693 

694 
fun strip_imp fm = 

695 
if (is_imp fm) 

696 
then let val {ant,conseq} = dest_imp fm 

697 
val (was,wb) = strip_imp conseq 

698 
in ((ant::was), wb) 

699 
end 

700 
else ([],fm); 

701 

702 
fun strip_forall fm = 

703 
if (is_forall fm) 

704 
then let val {Bvar,Body} = dest_forall fm 

705 
val (bvs,core) = strip_forall Body 

706 
in ((Bvar::bvs), core) 

707 
end 

708 
else ([],fm); 

709 

710 

711 
fun strip_exists fm = 

712 
if (is_exists fm) 

713 
then let val {Bvar, Body} = dest_exists fm 

714 
val (bvs,core) = strip_exists Body 

715 
in (Bvar::bvs, core) 

716 
end 

717 
else ([],fm); 

718 

719 
fun strip_disj w = 

720 
if (is_disj w) 

721 
then let val {disj1,disj2} = dest_disj w 

722 
in (strip_disj disj1@strip_disj disj2) 

723 
end 

724 
else [w]; 

725 

726 

727 
(* Miscellaneous *) 

728 

729 
fun mk_vstruct ty V = 

730 
let fun follow_prod_type (Type(@{type_name Product_Type.prod},[ty1,ty2])) vs = 

731 
let val (ltm,vs1) = follow_prod_type ty1 vs 

732 
val (rtm,vs2) = follow_prod_type ty2 vs1 

733 
in (mk_pair{fst=ltm, snd=rtm}, vs2) end 

734 
 follow_prod_type _ (v::vs) = (v,vs) 

735 
in #1 (follow_prod_type ty V) end; 

736 

737 

738 
(* Search a term for a subterm satisfying the predicate p. *) 

739 
fun find_term p = 

740 
let fun find tm = 

741 
if (p tm) then SOME tm 

742 
else case tm of 

743 
Abs(_,_,body) => find body 

744 
 (t$u) => (case find t of NONE => find u  some => some) 

745 
 _ => NONE 

746 
in find 

747 
end; 

748 

749 
fun dest_relation tm = 

750 
if (type_of tm = HOLogic.boolT) 

751 
then let val (Const(@{const_name Set.member},_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm 

752 
in (R,y,x) 

753 
end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure" 

754 
else raise USYN_ERR "dest_relation" "not a boolean term"; 

755 

756 
fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true 

757 
 is_WFR _ = false; 

758 

759 
fun ARB ty = mk_select{Bvar=Free("v",ty), 

760 
Body=Const(@{const_name True},HOLogic.boolT)}; 

761 

762 
end; 

763 

764 

60521  765 

60520  766 
(*** derived cterm destructors ***) 
767 

768 
structure Dcterm: DCTERM = 

769 
struct 

770 

771 
fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg}; 

772 

773 

774 
fun dest_comb t = Thm.dest_comb t 

775 
handle CTERM (msg, _) => raise ERR "dest_comb" msg; 

776 

777 
fun dest_abs a t = Thm.dest_abs a t 

778 
handle CTERM (msg, _) => raise ERR "dest_abs" msg; 

779 

780 
fun capply t u = Thm.apply t u 

781 
handle CTERM (msg, _) => raise ERR "capply" msg; 

782 

783 
fun cabs a t = Thm.lambda a t 

784 
handle CTERM (msg, _) => raise ERR "cabs" msg; 

785 

786 

787 
(* 

788 
* Some simple constructor functions. 

789 
**) 

790 

791 
val mk_hol_const = Thm.cterm_of @{theory_context HOL} o Const; 

792 

793 
fun mk_exists (r as (Bvar, Body)) = 

794 
let val ty = Thm.typ_of_cterm Bvar 

795 
val c = mk_hol_const(@{const_name Ex}, (ty > HOLogic.boolT) > HOLogic.boolT) 

796 
in capply c (uncurry cabs r) end; 

797 

798 

799 
local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

800 
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2 

801 
end; 

802 

803 
local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

804 
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2 

805 
end; 

806 

807 

808 
(* 

809 
* The primitives. 

810 
**) 

811 
fun dest_const ctm = 

812 
(case Thm.term_of ctm 

813 
of Const(s,ty) => {Name = s, Ty = ty} 

814 
 _ => raise ERR "dest_const" "not a constant"); 

815 

816 
fun dest_var ctm = 

817 
(case Thm.term_of ctm 

60521  818 
of Var((s,_),ty) => {Name=s, Ty=ty} 
60520  819 
 Free(s,ty) => {Name=s, Ty=ty} 
820 
 _ => raise ERR "dest_var" "not a variable"); 

821 

822 

823 
(* 

824 
* Derived destructor operations. 

825 
**) 

826 

827 
fun dest_monop expected tm = 

828 
let 

829 
fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected); 

830 
val (c, N) = dest_comb tm handle Utils.ERR _ => err (); 

831 
val name = #Name (dest_const c handle Utils.ERR _ => err ()); 

832 
in if name = expected then N else err () end; 

833 

834 
fun dest_binop expected tm = 

835 
let 

836 
fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected); 

837 
val (M, N) = dest_comb tm handle Utils.ERR _ => err () 

838 
in (dest_monop expected M, N) handle Utils.ERR _ => err () end; 

839 

840 
fun dest_binder expected tm = 

841 
dest_abs NONE (dest_monop expected tm) 

842 
handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected); 

843 

844 

845 
val dest_neg = dest_monop @{const_name Not} 

846 
val dest_pair = dest_binop @{const_name Pair} 

847 
val dest_eq = dest_binop @{const_name HOL.eq} 

848 
val dest_imp = dest_binop @{const_name HOL.implies} 

849 
val dest_conj = dest_binop @{const_name HOL.conj} 

850 
val dest_disj = dest_binop @{const_name HOL.disj} 

851 
val dest_exists = dest_binder @{const_name Ex} 

852 
val dest_forall = dest_binder @{const_name All} 

853 

854 
(* Query routines *) 

855 

856 
val is_eq = can dest_eq 

857 
val is_imp = can dest_imp 

858 
val is_forall = can dest_forall 

859 
val is_exists = can dest_exists 

860 
val is_neg = can dest_neg 

861 
val is_conj = can dest_conj 

862 
val is_disj = can dest_disj 

863 
val is_pair = can dest_pair 

864 

865 

866 
(* 

867 
* Iterated creation. 

868 
**) 

869 
val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm)); 

870 

871 
(* 

872 
* Iterated destruction. (To the "right" in a term.) 

873 
**) 

874 
fun strip break tm = 

875 
let fun dest (p as (ctm,accum)) = 

876 
let val (M,N) = break ctm 

877 
in dest (N, M::accum) 

878 
end handle Utils.ERR _ => p 

879 
in dest (tm,[]) 

880 
end; 

881 

882 
fun rev2swap (x,l) = (rev l, x); 

883 

884 
val strip_comb = strip (Library.swap o dest_comb) (* Goes to the "left" *) 

885 
val strip_imp = rev2swap o strip dest_imp 

886 
val strip_abs = rev2swap o strip (dest_abs NONE) 

887 
val strip_forall = rev2swap o strip dest_forall 

888 
val strip_exists = rev2swap o strip dest_exists 

889 

890 
val strip_disj = rev o (op::) o strip dest_disj 

891 

892 

893 
(* 

894 
* Going into and out of prop 

895 
**) 

896 

897 
fun is_Trueprop ct = 

898 
(case Thm.term_of ct of 

899 
Const (@{const_name Trueprop}, _) $ _ => true 

900 
 _ => false); 

901 

902 
fun mk_prop ct = if is_Trueprop ct then ct else Thm.apply @{cterm Trueprop} ct; 

903 
fun drop_prop ct = if is_Trueprop ct then Thm.dest_arg ct else ct; 

904 

905 
end; 

906 

907 

60521  908 

60520  909 
(*** emulation of HOL inference rules for TFL ***) 
910 

911 
structure Rules: RULES = 

912 
struct 

913 

914 
fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg}; 

915 

916 

917 
fun cconcl thm = Dcterm.drop_prop (#prop (Thm.crep_thm thm)); 

918 
fun chyps thm = map Dcterm.drop_prop (#hyps (Thm.crep_thm thm)); 

919 

920 
fun dest_thm thm = 

921 
let val {prop,hyps,...} = Thm.rep_thm thm 

922 
in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end 

923 
handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop"; 

924 

925 

926 
(* Inference rules *) 

927 

928 
(* 

929 
* Equality (one step) 

930 
**) 

931 

932 
fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq 

933 
handle THM (msg, _, _) => raise RULES_ERR "REFL" msg; 

934 

935 
fun SYM thm = thm RS sym 

936 
handle THM (msg, _, _) => raise RULES_ERR "SYM" msg; 

937 

938 
fun ALPHA thm ctm1 = 

939 
let 

940 
val ctm2 = Thm.cprop_of thm; 

941 
val ctm2_eq = Thm.reflexive ctm2; 

942 
val ctm1_eq = Thm.reflexive ctm1; 

943 
in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end 

944 
handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg; 

945 

946 
fun rbeta th = 

947 
(case Dcterm.strip_comb (cconcl th) of 

60521  948 
(_, [_, r]) => Thm.transitive th (Thm.beta_conversion false r) 
60520  949 
 _ => raise RULES_ERR "rbeta" ""); 
950 

951 

952 
(* 

953 
* Implication and the assumption list 

954 
* 

955 
* Assumptions get stuck on the metalanguage assumption list. Implications 

956 
* are in the object language, so discharging an assumption "A" from theorem 

957 
* "B" results in something that looks like "A > B". 

958 
**) 

959 

960 
fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm); 

961 

962 

963 
(* 

964 
* Implication in TFL is >. Metalanguage implication (==>) is only used 

965 
* in the implementation of some of the inference rules below. 

966 
**) 

967 
fun MP th1 th2 = th2 RS (th1 RS mp) 

968 
handle THM (msg, _, _) => raise RULES_ERR "MP" msg; 

969 

970 
(*forces the first argument to be a proposition if necessary*) 

971 
fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI 

972 
handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg; 

973 

974 
fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm; 

975 

976 

977 
fun FILTER_DISCH_ALL P thm = 

978 
let fun check tm = P (Thm.term_of tm) 

979 
in fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm 

980 
end; 

981 

982 
fun UNDISCH thm = 

983 
let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm))) 

984 
in Thm.implies_elim (thm RS mp) (ASSUME tm) end 

985 
handle Utils.ERR _ => raise RULES_ERR "UNDISCH" "" 

986 
 THM _ => raise RULES_ERR "UNDISCH" ""; 

987 

988 
fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath; 

989 

60522  990 
fun IMP_TRANS th1 th2 = th2 RS (th1 RS @{thm tfl_imp_trans}) 
60520  991 
handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg; 
992 

993 

994 
(* 

995 
* Conjunction 

996 
**) 

997 

998 
fun CONJUNCT1 thm = thm RS conjunct1 

999 
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg; 

1000 

1001 
fun CONJUNCT2 thm = thm RS conjunct2 

1002 
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg; 

1003 

1004 
fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th]; 

1005 

1006 
fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list" 

1007 
 LIST_CONJ [th] = th 

1008 
 LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst) 

1009 
handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg; 

1010 

1011 

1012 
(* 

1013 
* Disjunction 

1014 
**) 

1015 
local 

1016 
val prop = Thm.prop_of disjI1 

60524  1017 
val [_,Q] = Misc_Legacy.term_vars prop 
60520  1018 
val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1 
1019 
in 

1020 
fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1) 

1021 
handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg; 

1022 
end; 

1023 

1024 
local 

1025 
val prop = Thm.prop_of disjI2 

60521  1026 
val [P,_] = Misc_Legacy.term_vars prop 
60520  1027 
val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2 
1028 
in 

1029 
fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2) 

1030 
handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg; 

1031 
end; 

1032 

1033 

1034 
(* 

1035 
* 

1036 
* A1  M1, ..., An  Mn 

1037 
*  

1038 
* [A1  M1 \/ ... \/ Mn, ..., An  M1 \/ ... \/ Mn] 

1039 
* 

1040 
**) 

1041 

1042 

1043 
fun EVEN_ORS thms = 

1044 
let fun blue ldisjs [] _ = [] 

1045 
 blue ldisjs (th::rst) rdisjs = 

1046 
let val tail = tl rdisjs 

1047 
val rdisj_tl = Dcterm.list_mk_disj tail 

1048 
in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl) 

1049 
:: blue (ldisjs @ [cconcl th]) rst tail 

1050 
end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th] 

1051 
in blue [] thms (map cconcl thms) end; 

1052 

1053 

1054 
(* 

1055 
* 

1056 
* A  P \/ Q B,P  R C,Q  R 

1057 
*  

1058 
* A U B U C  R 

1059 
* 

1060 
**) 

1061 

1062 
fun DISJ_CASES th1 th2 th3 = 

1063 
let 

1064 
val c = Dcterm.drop_prop (cconcl th1); 

1065 
val (disj1, disj2) = Dcterm.dest_disj c; 

1066 
val th2' = DISCH disj1 th2; 

1067 
val th3' = DISCH disj2 th3; 

1068 
in 

60522  1069 
th3' RS (th2' RS (th1 RS @{thm tfl_disjE})) 
60520  1070 
handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg 
1071 
end; 

1072 

1073 

1074 
(* 

1075 
* 

1076 
*  A1 \/ ... \/ An [A1  M, ..., An  M] 

1077 
*  

1078 
*  M 

1079 
* 

1080 
* Note. The list of theorems may be all jumbled up, so we have to 

1081 
* first organize it to align with the first argument (the disjunctive 

1082 
* theorem). 

1083 
**) 

1084 

1085 
fun organize eq = (* a bit slow  analogous to insertion sort *) 

1086 
let fun extract a alist = 

1087 
let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1" 

1088 
 ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t) 

1089 
in ex ([],alist) 

1090 
end 

1091 
fun place [] [] = [] 

1092 
 place (a::rst) alist = 

1093 
let val (item,next) = extract a alist 

1094 
in item::place rst next 

1095 
end 

1096 
 place _ _ = raise RULES_ERR "organize" "not a permutation.2" 

1097 
in place 

1098 
end; 

1099 

1100 
fun DISJ_CASESL disjth thl = 

1101 
let val c = cconcl disjth 

1102 
fun eq th atm = 

1103 
exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th) 

1104 
val tml = Dcterm.strip_disj c 

60521  1105 
fun DL _ [] = raise RULES_ERR "DISJ_CASESL" "no cases" 
60520  1106 
 DL th [th1] = PROVE_HYP th th1 
1107 
 DL th [th1,th2] = DISJ_CASES th th1 th2 

1108 
 DL th (th1::rst) = 

1109 
let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th))) 

1110 
in DISJ_CASES th th1 (DL (ASSUME tm) rst) end 

1111 
in DL disjth (organize eq tml thl) 

1112 
end; 

1113 

1114 

1115 
(* 

1116 
* Universals 

1117 
**) 

1118 
local (* this is fragile *) 

1119 
val prop = Thm.prop_of spec 

1120 
val x = hd (tl (Misc_Legacy.term_vars prop)) 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60524
diff
changeset

1121 
val TV = dest_TVar (type_of x) 
60520  1122 
val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec 
1123 
in 

1124 
fun SPEC tm thm = 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60524
diff
changeset

1125 
let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec 
60520  1126 
in thm RS (Thm.forall_elim tm gspec') end 
1127 
end; 

1128 

1129 
fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm; 

1130 

1131 
val ISPEC = SPEC 

1132 
val ISPECL = fold ISPEC; 

1133 

1134 
(* Not optimized! Too complicated. *) 

1135 
local 

1136 
val prop = Thm.prop_of allI 

1137 
val [P] = Misc_Legacy.add_term_vars (prop, []) 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60524
diff
changeset

1138 
fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty)) 
60520  1139 
fun ctm_theta ctxt = 
1140 
map (fn (i, (_, tm2)) => 

1141 
let val ctm2 = Thm.cterm_of ctxt tm2 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60524
diff
changeset

1142 
in ((i, Thm.typ_of_cterm ctm2), ctm2) end) 
60520  1143 
fun certify ctxt (ty_theta,tm_theta) = 
1144 
(cty_theta ctxt (Vartab.dest ty_theta), 

1145 
ctm_theta ctxt (Vartab.dest tm_theta)) 

1146 
in 

1147 
fun GEN ctxt v th = 

1148 
let val gth = Thm.forall_intr v th 

1149 
val thy = Proof_Context.theory_of ctxt 

1150 
val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth 

1151 
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) 

1152 
val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty); 

1153 
val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI 

1154 
val thm = Thm.implies_elim allI2 gth 

1155 
val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm 

1156 
val prop' = tp $ (A $ Abs(x,ty,M)) 

1157 
in ALPHA thm (Thm.cterm_of ctxt prop') end 

1158 
end; 

1159 

1160 
fun GENL ctxt = fold_rev (GEN ctxt); 

1161 

1162 
fun GEN_ALL ctxt thm = 

1163 
let 

1164 
val prop = Thm.prop_of thm 

1165 
val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, [])) 

1166 
in GENL ctxt vlist thm end; 

1167 

1168 

1169 
fun MATCH_MP th1 th2 = 

1170 
if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1))) 

1171 
then MATCH_MP (th1 RS spec) th2 

1172 
else MP th1 th2; 

1173 

1174 

1175 
(* 

1176 
* Existentials 

1177 
**) 

1178 

1179 

1180 

1181 
(* 

1182 
* Existential elimination 

1183 
* 

1184 
* A1  ?x.t[x] , A2, "t[v]"  t' 

1185 
*  (variable v occurs nowhere) 

1186 
* A1 u A2  t' 

1187 
* 

1188 
**) 

1189 

1190 
fun CHOOSE ctxt (fvar, exth) fact = 

1191 
let 

1192 
val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth))) 

1193 
val redex = Dcterm.capply lam fvar 

1194 
val t$u = Thm.term_of redex 

1195 
val residue = Thm.cterm_of ctxt (Term.betapply (t, u)) 

1196 
in 

60522  1197 
GEN ctxt fvar (DISCH residue fact) RS (exth RS @{thm tfl_exE}) 
60520  1198 
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg 
1199 
end; 

1200 

60781  1201 
fun EXISTS ctxt (template,witness) thm = 
60520  1202 
let val abstr = #2 (Dcterm.dest_comb template) in 
60781  1203 
thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI) 
60520  1204 
handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg 
60781  1205 
end; 
60520  1206 

1207 
(* 

1208 
* 

1209 
* A  M[x_1,...,x_n] 

1210 
*  [(x > y)_1,...,(x > y)_n] 

1211 
* A  ?y_1...y_n. M 

1212 
* 

1213 
**) 

1214 
(* Could be improved, but needs "subst_free" for certified terms *) 

1215 

1216 
fun IT_EXISTS ctxt blist th = 

1217 
let 

1218 
val blist' = map (apply2 Thm.term_of) blist 

1219 
fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M}) 

1220 
in 

1221 
fold_rev (fn (b as (r1,r2)) => fn thm => 

60781  1222 
EXISTS ctxt (ex r2 (subst_free [b] 
60520  1223 
(HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1) 
1224 
thm) 

1225 
blist' th 

1226 
end; 

1227 

1228 
(* 

1229 
* Faster version, that fails for some as yet unknown reason 

1230 
* fun IT_EXISTS blist th = 

1231 
* let val {thy,...} = rep_thm th 

1232 
* val tych = cterm_of thy 

1233 
* fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y) 

1234 
* in 

1235 
* fold (fn (b as (r1,r2), thm) => 

1236 
* EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))), 

1237 
* r1) thm) blist th 

1238 
* end; 

1239 
**) 

1240 

1241 
(* 

1242 
* Rewriting 

1243 
**) 

1244 

1245 
fun SUBS ctxt thl = 

1246 
rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl); 

1247 

1248 
val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)); 

1249 

1250 
fun simpl_conv ctxt thl ctm = 

1251 
rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq; 

1252 

1253 

60522  1254 
fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc}; 
60520  1255 

1256 

1257 

1258 
(* 

1259 
* TERMINATION CONDITION EXTRACTION 

1260 
**) 

1261 

1262 

1263 
(* Object language quantifier, i.e., "!" *) 

1264 
fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M}; 

1265 

1266 

1267 
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *) 

1268 
fun is_cong thm = 

1269 
case (Thm.prop_of thm) of 

1270 
(Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $ 

60524  1271 
(Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ _ $ _ $ _ $ _) $ _)) => 
60520  1272 
false 
1273 
 _ => true; 

1274 

1275 

1276 
fun dest_equal(Const (@{const_name Pure.eq},_) $ 

1277 
(Const (@{const_name Trueprop},_) $ lhs) 

1278 
$ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs} 

1279 
 dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs} 

1280 
 dest_equal tm = USyntax.dest_eq tm; 

1281 

1282 
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm)); 

1283 

1284 
fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a 

1285 
 dest_all _ _ = raise RULES_ERR "dest_all" "not a !!"; 

1286 

1287 
val is_all = can (dest_all []); 

1288 

1289 
fun strip_all used fm = 

1290 
if (is_all fm) 

1291 
then let val ({Bvar, Body}, used') = dest_all used fm 

1292 
val (bvs, core, used'') = strip_all used' Body 

1293 
in ((Bvar::bvs), core, used'') 

1294 
end 

1295 
else ([], fm, used); 

1296 

1297 
fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) = 

1298 
let val (L,core) = list_break_all body 

1299 
in ((s,ty)::L, core) 

1300 
end 

1301 
 list_break_all tm = ([],tm); 

1302 

1303 
(* 

1304 
* Rename a term of the form 

1305 
* 

1306 
* !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn 

1307 
* ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn. 

1308 
* to one of 

1309 
* 

1310 
* !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn 

1311 
* ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn. 

1312 
* 

1313 
* This prevents name problems in extraction, and helps the result to read 

1314 
* better. There is a problem with varstructs, since they can introduce more 

1315 
* than n variables, and some extra reasoning needs to be done. 

1316 
**) 

1317 

1318 
fun get ([],_,L) = rev L 

1319 
 get (ant::rst,n,L) = 

1320 
case (list_break_all ant) 

1321 
of ([],_) => get (rst, n+1,L) 

60521  1322 
 (_,body) => 
60520  1323 
let val eq = Logic.strip_imp_concl body 
60521  1324 
val (f,_) = USyntax.strip_comb (get_lhs eq) 
60520  1325 
val (vstrl,_) = USyntax.strip_abs f 
1326 
val names = 

1327 
Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl) 

1328 
in get (rst, n+1, (names,n)::L) end 

1329 
handle TERM _ => get (rst, n+1, L) 

1330 
 Utils.ERR _ => get (rst, n+1, L); 

1331 

1332 
(* Note: Thm.rename_params_rule counts from 1, not 0 *) 

1333 
fun rename thm = 

1334 
let 

1335 
val ants = Logic.strip_imp_prems (Thm.prop_of thm) 

1336 
val news = get (ants,1,[]) 

1337 
in fold Thm.rename_params_rule news thm end; 

1338 

1339 

1340 
(* 

1341 
* Betaconversion to the rhs of an equation (taken from hol90/drule.sml) 

1342 
**) 

1343 

1344 
fun list_beta_conv tm = 

1345 
let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th)))) 

1346 
fun iter [] = Thm.reflexive tm 

1347 
 iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v)) 

1348 
in iter end; 

1349 

1350 

1351 
(* 

1352 
* Trace information for the rewriter 

1353 
**) 

1354 
val tracing = Unsynchronized.ref false; 

1355 

1356 
fun say s = if !tracing then writeln s else (); 

1357 

1358 
fun print_thms ctxt s L = 

1359 
say (cat_lines (s :: map (Display.string_of_thm ctxt) L)); 

1360 

1361 
fun print_term ctxt s t = 

1362 
say (cat_lines [s, Syntax.string_of_term ctxt t]); 

1363 

1364 

1365 
(* 

1366 
* General abstraction handlers, should probably go in USyntax. 

1367 
**) 

1368 
fun mk_aabs (vstr, body) = 

1369 
USyntax.mk_abs {Bvar = vstr, Body = body} 

1370 
handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body}; 

1371 

1372 
fun list_mk_aabs (vstrl,tm) = 

1373 
fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm; 

1374 

1375 
fun dest_aabs used tm = 

1376 
let val ({Bvar,Body}, used') = USyntax.dest_abs used tm 

1377 
in (Bvar, Body, used') end 

1378 
handle Utils.ERR _ => 

1379 
let val {varstruct, body, used} = USyntax.dest_pabs used tm 

1380 
in (varstruct, body, used) end; 

1381 

1382 
fun strip_aabs used tm = 

1383 
let val (vstr, body, used') = dest_aabs used tm 

1384 
val (bvs, core, used'') = strip_aabs used' body 

1385 
in (vstr::bvs, core, used'') end 

1386 
handle Utils.ERR _ => ([], tm, used); 

1387 

1388 
fun dest_combn tm 0 = (tm,[]) 

1389 
 dest_combn tm n = 

1390 
let val {Rator,Rand} = USyntax.dest_comb tm 

1391 
val (f,rands) = dest_combn Rator (n1) 

1392 
in (f,Rand::rands) 

1393 
end; 

1394 

1395 

1396 

1397 

1398 
local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end 

1399 
fun mk_fst tm = 

1400 
let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm 

1401 
in Const (@{const_name Product_Type.fst}, ty > fty) $ tm end 

1402 
fun mk_snd tm = 

1403 
let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm 

1404 
in Const (@{const_name Product_Type.snd}, ty > sty) $ tm end 

1405 
in 

1406 
fun XFILL tych x vstruct = 

1407 
let fun traverse p xocc L = 

1408 
if (is_Free p) 

1409 
then tych xocc::L 

1410 
else let val (p1,p2) = dest_pair p 

1411 
in traverse p1 (mk_fst xocc) (traverse p2 (mk_snd xocc) L) 

1412 
end 

1413 
in 

1414 
traverse vstruct x [] 

1415 
end end; 

1416 

1417 
(* 

1418 
* Replace a free tuple (vstr) by a universally quantified variable (a). 

1419 
* Note that the notion of "freeness" for a tuple is different than for a 

1420 
* variable: if variables in the tuple also occur in any other place than 

1421 
* an occurrences of the tuple, they aren't "free" (which is thus probably 

1422 
* the wrong word to use). 

1423 
**) 

1424 

1425 
fun VSTRUCT_ELIM ctxt tych a vstr th = 

1426 
let val L = USyntax.free_vars_lr vstr 

1427 
val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr))) 

1428 
val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th) 

1429 
val thm2 = forall_intr_list (map tych L) thm1 

1430 
val thm3 = forall_elim_list (XFILL tych a vstr) thm2 

1431 
in refl RS 

1432 
rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3 

1433 
end; 

1434 

1435 
fun PGEN ctxt tych a vstr th = 

1436 
let val a1 = tych a 

60781  1437 
in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end; 
60520  1438 

1439 

1440 
(* 

1441 
* Takes apart a paired betaredex, looking like "(\(x,y).N) vstr", into 

1442 
* 

1443 
* (([x,y],N),vstr) 

1444 
**) 

1445 
fun dest_pbeta_redex used M n = 

1446 
let val (f,args) = dest_combn M n 

60521  1447 
val _ = dest_aabs used f 
60520  1448 
in (strip_aabs used f,args) 
1449 
end; 

1450 

1451 
fun pbeta_redex M n = can (fn t => dest_pbeta_redex [] t n) M; 

1452 

1453 
fun dest_impl tm = 

1454 
let val ants = Logic.strip_imp_prems tm 

1455 
val eq = Logic.strip_imp_concl tm 

1456 
in (ants,get_lhs eq) 

1457 
end; 

1458 

1459 
fun restricted t = is_some (USyntax.find_term 

1460 
(fn (Const(@{const_name Wfrec.cut},_)) =>true  _ => false) 

1461 
t) 

1462 

1463 
fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th = 

1464 
let val globals = func::G 

1465 
val ctxt0 = empty_simpset main_ctxt 

1466 
val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection]; 

1467 
val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref 

1468 
val cut_lemma' = cut_lemma RS eq_reflection 

1469 
fun prover used ctxt thm = 

1470 
let fun cong_prover ctxt thm = 

60521  1471 
let val _ = say "cong_prover:" 
60520  1472 
val cntxt = Simplifier.prems_of ctxt 
60521  1473 
val _ = print_thms ctxt "cntxt:" cntxt 
1474 
val _ = say "cong rule:" 

1475 
val _ = say (Display.string_of_thm ctxt thm) 

60520  1476 
(* Unquantified eliminate *) 
1477 
fun uq_eliminate (thm,imp) = 

1478 
let val tych = Thm.cterm_of ctxt 

1479 
val _ = print_term ctxt "To eliminate:" imp 

1480 
val ants = map tych (Logic.strip_imp_prems imp) 

1481 
val eq = Logic.strip_imp_concl imp 

1482 
val lhs = tych(get_lhs eq) 

1483 
val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt 

1484 
val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs 

1485 
handle Utils.ERR _ => Thm.reflexive lhs 

1486 
val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1] 

1487 
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 

1488 
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq 

1489 
in 

1490 
lhs_eeq_lhs2 COMP thm 

1491 
end 

1492 
fun pq_eliminate (thm, vlist, imp_body, lhs_eq) = 

1493 
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist) 

60521  1494 
val _ = forall (op aconv) (ListPair.zip (vlist, args)) 
60520  1495 
orelse error "assertion failed in CONTEXT_REWRITE_RULE" 
1496 
val imp_body1 = subst_free (ListPair.zip (args, vstrl)) 

1497 
imp_body 

1498 
val tych = Thm.cterm_of ctxt 

1499 
val ants1 = map tych (Logic.strip_imp_prems imp_body1) 

1500 
val eq1 = Logic.strip_imp_concl imp_body1 

1501 
val Q = get_lhs eq1 

1502 
val QeqQ1 = pbeta_reduce (tych Q) 

1503 
val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1)) 

1504 
val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt 

1505 
val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1 

1506 
handle Utils.ERR _ => Thm.reflexive Q1 

1507 
val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2)) 

1508 
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl)) 

1509 
val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection) 

1510 
val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2 

1511 
val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ => 

1512 
((Q2eeqQ3 RS meta_eq_to_obj_eq) 

1513 
RS ((thA RS meta_eq_to_obj_eq) RS trans)) 

1514 
RS eq_reflection 

1515 
val impth = implies_intr_list ants1 QeeqQ3 

1516 
val impth1 = impth RS meta_eq_to_obj_eq 

1517 
(* Need to abstract *) 
