1structure Induction :> Induction = 2struct 3 4open HolKernel boolLib Rules wfrecUtils; 5 6type thry = TypeBasePure.typeBase 7 8val ERR = mk_HOL_ERR "Induction"; 9 10fun induct_info db s = 11 Option.map (fn facts => {nchotomy = TypeBasePure.nchotomy_of facts, 12 constructors = TypeBasePure.constructors_of facts}) 13 (TypeBasePure.prim_get db s); 14 15(*---------------------------------------------------------------------------*) 16(* *) 17(* [x_1,...,x_n] ?v_1...v_n. M[v_1,...,v_n] *) 18(* ----------------------------------------------------------- *) 19(* ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]), *) 20(* ... *) 21(* (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] ) *) 22(* *) 23(* This function is totally ad hoc. It's used in the production of the *) 24(* induction theorem. The nchotomy theorem can have clauses that look like *) 25(* *) 26(* ?v1..vn. z = C vn..v1 *) 27(* *) 28(* in which the order of quantification is not the order of occurrence of the*) 29(* quantified variables as arguments to C. Since we have no control over this*) 30(* aspect of the nchotomy theorem, we make the correspondence explicit by *) 31(* pairing the incoming new variable with the term it gets beta-reduced into.*) 32(* ------------------------------------------------------------------------- *) 33 34(* fun assoc1 x = Lib.total(snd o Lib.first (aconv x o fst)); *) 35 36local fun assoc1 eq item = 37 let val eek = eq item 38 fun assc [] = NONE 39 | assc ((entry as (key,_))::rst) = 40 if eek key then SOME entry else assc rst 41 in assc 42 end 43 fun foo NONE = raise ERR "alpha_ex_unroll" "no correspondence" 44 | foo (SOME(_,v)) = v 45in 46fun alpha_ex_unroll xlist tm = 47 let open boolSyntax 48 val (qvars,body) = strip_exists tm 49 val vlist = #2(strip_comb (rhs body)) 50 val plist = zip vlist xlist 51 val args = map (C (assoc1 aconv) plist) qvars 52 val args' = map foo args 53 fun build ex [] = [] 54 | build ex (v::rst) = 55 let val ex1 = beta_conv(mk_comb(rand ex, v)) 56 in ex1::build ex1 rst 57 end 58 in 59 case rev (tm::build tm args') 60 of nex::exl => (nex, zip args' (rev exl)) 61 | [] => raise ERR "alpha_ex_unroll" "empty" 62 end 63end; 64 65 66(*---------------------------------------------------------------------------*) 67(* *) 68(* PROVING COMPLETENESS OF PATTERNS *) 69(* *) 70(*---------------------------------------------------------------------------*) 71 72fun ipartition gv (constructors,rows) = 73let fun pfail s = raise ERR"ipartition.part" s 74 fun part {constrs = [], rows = [], A} = rev A 75 | part {constrs = [], rows = _::_, A} = pfail"extra cases in defn" 76 | part {constrs = _::_, rows = [], A} = pfail"cases missing in defn" 77 | part {constrs = c::crst, rows, A} = 78 let val {Name,Thy,Ty} = dest_thy_const c 79 val (L,_) = strip_fun_type Ty 80 fun func (row as (p::rst, rhs)) (in_group,not_in_group) = 81 let val (pc,args) = strip_comb p 82 val {Name=nm,Thy=thyn,...} = dest_thy_const pc 83 in if (nm,thyn) = (Name,Thy) 84 then ((args@rst, rhs)::in_group, not_in_group) 85 else (in_group, row::not_in_group) 86 end 87 | func _ _ = pfail "func" "" 88 val (in_group, not_in_group) = itlist func rows ([],[]) 89 val col_types = #1(wfrecUtils.gtake type_of 90 (length L, #1(Lib.trye hd in_group))) 91 in 92 part{constrs = crst, 93 rows = not_in_group, 94 A = {constructor = c, 95 new_formals = map gv col_types, 96 group = in_group}::A} 97 end 98in 99 part {constrs=constructors, rows=rows, A=[]} 100end; 101 102(*---------------------------------------------------------------------------*) 103(* Partition rows where the first pattern is a literal (possibly a variable) *) 104(* We'll just use regular term equality to make the partition. *) 105(*---------------------------------------------------------------------------*) 106 107fun lpartition (lits,rows) = 108let fun lfail s = raise ERR"lpartition.part" s 109 fun lit_eq l1 l2 = if Literal.is_literal l1 then l1=l2 else 110 (is_var l1 andalso is_var l2) 111 fun pfun lit (row as (p::rst, rhs)) (in_group,not_in_group) = 112 if lit_eq lit p then ((rst,rhs)::in_group, not_in_group) 113 else (in_group, row::not_in_group) 114 | pfun _ _ _ = lfail "pfun" "" 115 fun part [] [] A = rev A 116 | part [] (_::_) A = lfail"extra cases in defn" 117 | part (_::_) [] A = lfail"cases missing in defn" 118 | part (lit::rst) rows A = 119 let val (in_group, not_in_group) = itlist (pfun lit) rows ([],[]) 120 in part rst not_in_group ((lit,in_group)::A) 121 end 122 in 123 part lits rows [] 124 end; 125 126fun rm x [] = [] | rm x (h::t) = if x=h then rm x t else h::rm x t; 127 128fun distinct [] = [] 129 | distinct (h::t) = h::distinct(rm h t); 130 131(*---------------------------------------------------------------------------*) 132(* Need to handle fact that 0 is both a literal and a constructor *) 133(*---------------------------------------------------------------------------*) 134 135type divide_ty 136 = term list 137 * (term list * (thm * (term, term) subst)) list 138 -> {constructor : term, 139 group : (term list * (thm * (term, term) subst)) list, 140 new_formals : term list} list; 141 142fun bring_to_front_list n l = let 143 val (l0, l1) = Lib.split_after n l 144 val (x, l1') = (hd l1, tl l1) 145 in x :: (l0 @ l1') end 146 147fun undo_bring_to_front n l = let 148 val (x, l') = (hd l, tl l) 149 val (l0, l1) = Lib.split_after n l' 150 in (l0 @ x::l1) end 151 152(* 153val org_in = {path=[z], rows=rows} 154 155val in_1 = hd news 156val in_2 = {path=rstp, rows=zip pat_rectangle' rights'} 157val in_3 = hd news 158 159mk in_2 160v 161val {path=u::rstp, rows as (p::_, _)::_} = in_3 162 163val {path=u::rstp, rows as (p::_, _)::_} = {path=rstp, rows=zip pat_rectangle' rights'} 164val mk = mk_case ty_info FV thy 165mk in_1 166val in 167 168hm = mk_case ty_info FV thy {path=[z], rows=rows} 169 170val arg0 = {path=[z], rows=rows} 171val {path=rstp0, rows = rows0} = el 1 news 172*) 173 174 175fun mk_case_choose_column i rows = 176let 177 val col_i = map (fn (l, _) => el (i+1) l) rows 178 179 val col_i_ok = 180 (all is_var col_i) orelse 181 (all (fn p => Literal.is_literal p orelse is_var p) col_i) orelse 182 (all (fn p => not (Literal.is_pure_literal p) andalso not (is_var p)) col_i) 183in 184 if col_i_ok then i else mk_case_choose_column (i+1) rows 185end handle HOL_ERR _ => 0 186 187val quiet_metis = Feedback.trace ("metis", 0) (metisLib.METIS_PROVE []) 188val quiet_meson = Feedback.trace ("meson", 0) (BasicProvers.PROVE []) 189 190fun mk_case ty_info FV thy = 191 let open boolSyntax 192 val gv = (wfrecUtils.vary FV) 193 val divide:divide_ty = ipartition gv 194 fun fail s = raise ERR "mk_case" s 195 fun mk{rows=[],...} = fail"no rows" 196 | mk{path=[], rows = [([], (thm, bindings))]} = IT_EXISTS bindings thm 197 | mk{path=rstp0, rows= rows0 as ((_::_, _)::_)} = 198 let val col_index = mk_case_choose_column 0 rows0 199 val rows = map (fn (pL, rhs) => (bring_to_front_list col_index pL, rhs)) rows0 200 val (pat_rectangle,rights) = unzip rows 201 val u_rstp = bring_to_front_list col_index rstp0 202 val (u, rstp) = (hd u_rstp, tl u_rstp) 203 val p = hd (fst (hd rows)) 204 val col0 = map (Lib.trye hd) pat_rectangle 205 val pat_rectangle' = map (Lib.trye tl) pat_rectangle 206 in 207 if all is_var col0 (* column 0 is all variables *) 208 then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[u|->v])) 209 (zip rights col0) 210 in mk{path=rstp, rows=zip pat_rectangle' rights'} 211 end 212 else 213 if exists Literal.is_pure_literal col0 (* col0 matches against literals *) 214 then let val lits = distinct col0 215 val (litpats, varpats) = Lib.partition (not o is_var) lits 216 val liteqs = map (curry mk_eq u) litpats 217 fun neglits v = map (fn lit => mk_neg(mk_eq(v,lit))) litpats 218 val altliteqs = map neglits varpats 219 val vareqs = map (curry mk_eq u) varpats 220 val var_constraints = map2 221 (fn veq => fn nlits => list_mk_conj(veq::nlits)) vareqs altliteqs 222 val eqs = liteqs @ var_constraints 223 fun exquant tm = 224 if is_conj tm 225 then let val x = rhs(fst(dest_conj tm)) 226 in mk_exists(x,tm) 227 end 228 else tm 229 val disjuncts = map exquant eqs 230 val thm' = quiet_metis (list_mk_disj disjuncts) 231 val subproblems = lpartition(lits,rows) 232 val groups = map snd subproblems 233 val geqs = zip groups eqs 234 fun expnd c (pats,(th,b)) = 235 if is_eq c then (pats, (SUBS[ASSUME c]th, b)) 236 else let val lem = ASSUME c 237 val veq = CONJUNCT1 lem 238 val v = rhs(concl veq) 239 val constraints = CONJUNCT2 lem 240 val b' = b@[v|->v] 241 in (pats, (CONJ (SUBS [veq]th) constraints, b')) 242 end 243 val news = map(fn(grp,c) => {path=rstp,rows=map (expnd c) grp}) geqs 244 val recursive_thms = map mk news 245 fun left_exists tm thm = 246 if is_exists tm 247 then let val (v,_) = dest_exists tm 248 in CHOOSE (v,ASSUME tm) thm 249 end 250 else thm 251 val vexl = liteqs @ map2 (curry mk_exists) varpats var_constraints 252 val thms' = map2 left_exists vexl recursive_thms 253 val same_concls = EVEN_ORS thms' 254 in 255 DISJ_CASESL thm' same_concls 256 end 257 else 258 (* column 0 matches against constructors (and perhaps variables) *) 259 let val {Thy, Tyop = ty_name,...} = dest_thy_type (type_of p) 260 in 261 case ty_info (Thy,ty_name) 262 of NONE => fail("Not a known datatype: "^ty_name) 263 (* tyinfo rqt: `constructors' must line up exactly with constrs 264 in disjuncts of `nchotomy'. *) 265 | SOME{constructors,nchotomy} => 266(* 267 val SOME{constructors,nchotomy} = ty_info (Thy,ty_name) 268*) 269 let val thm' = ISPEC u nchotomy 270 val disjuncts = strip_disj (concl thm') 271 val subproblems = divide(constructors, rows) 272 val groups = map #group subproblems 273 and new_formals = map #new_formals subproblems 274 val existentials = map2 alpha_ex_unroll new_formals disjuncts 275 val constraints = map #1 existentials 276 val vexl = map #2 existentials 277 fun expnd tm (pats,(th,b)) = (pats,(SUBS[ASSUME tm]th, b)) 278 val news = map (fn (nf,rows,c) => {path = nf@rstp, 279 rows = map (expnd c) rows}) 280 (zip3 new_formals groups constraints) 281 val recursive_thms = map mk news 282 val build_exists = itlist(CHOOSE o (I##ASSUME)) 283 val thms' = map2 build_exists vexl recursive_thms 284 val same_concls = EVEN_ORS thms' 285 in 286 DISJ_CASESL thm' same_concls 287 end 288 end end 289 | mk _ = fail"blunder" 290in 291 mk 292end; 293 294type row = term list * (thm * (term, term) subst) 295 296fun complete_cases thy = 297 let val ty_info = induct_info thy 298 in fn pats => 299 let val FV0 = free_varsl pats 300 val a = variant FV0 (mk_var("a",type_of(Lib.trye hd pats))) 301 val z = variant (a::FV0) (mk_var("z",type_of a)) 302 val FV = a::z::FV0 303 val a_eq_z = mk_eq(a,z) 304 val ex_th0 = EXISTS (mk_exists(z,a_eq_z),a) (REFL a) 305 val th0 = ASSUME a_eq_z 306 val rows:row list = map (fn x => ([x], (th0,[]))) pats 307 308 val cases_thm0 = mk_case ty_info FV thy {path=[z], rows=rows} 309 310 fun mk_pat_pred p = list_mk_exists (free_vars_lr p, mk_eq(a, p)) 311 val cases_tm = list_mk_disj (map mk_pat_pred pats) 312 val imp_thm = quiet_meson (mk_imp (concl cases_thm0, cases_tm)) 313 val cases_thm = MP imp_thm cases_thm0 314 in 315 GEN a (RIGHT_ASSOC (CHOOSE(z, ex_th0) cases_thm)) 316 end 317 end; 318 319 320(*---------------------------------------------------------------------------* 321 * Constructing induction hypotheses: one for each recursive call. * 322 *---------------------------------------------------------------------------*) 323 324local nonfix ^ ; infix 9 ^ ; infix 5 ==> 325 fun (tm1 ^ tm2) = mk_comb(tm1, tm2) 326 fun (tm1 ==> tm2) = mk_imp(tm1, tm2) 327 val /\ = list_mk_conj 328 val diff = op_set_diff aconv 329in 330fun build_ih f (P,R,SV) (pat,TCs) = 331 let val pat_vars = free_vars_lr pat 332 val globals = (if is_var R then [R] else [])@pat_vars@SV 333 fun nested tm = can(find_term (aconv f)) tm handle _ => false 334 fun dest_TC tm = 335 let val (cntxt,R_y_pat) = wfrecUtils.strip_imp(#2(strip_forall tm)) 336 val (R,y,_) = wfrecUtils.dest_relation R_y_pat 337 val P_y = if nested tm then R_y_pat ==> P^y else P^y 338 val ihyp = case cntxt of [] => P_y | _ => /\cntxt ==> P_y 339 val locals = diff (free_vars_lr ihyp) (P::globals) 340 in 341 (list_mk_forall(locals,ihyp), (tm,locals)) 342 end 343 in case TCs 344 of [] => (list_mk_forall(pat_vars, P^pat), []) 345 | _ => let val (ihs, TCs_locals) = unzip(map dest_TC TCs) 346 val ind_clause = /\ihs ==> P^pat 347 in 348 (list_mk_forall(pat_vars,ind_clause), TCs_locals) 349 end 350 end 351end; 352 353 354(*---------------------------------------------------------------------------* 355 * This function makes good on the promise made in "build_ih: it proves * 356 * each case of the induction. * 357 * * 358 * Input is tm = "(!y. R y pat ==> P y) ==> P pat", * 359 * TCs = TC_1[pat] ... TC_n[pat] * 360 * thm = ih1 /\ ... /\ ih_n ==> ih[pat] * 361 *---------------------------------------------------------------------------*) 362 363fun prove_case f thy (tm,TCs_locals,thm) = 364 let val antc = fst(dest_imp tm) 365 val thm' = SPEC_ALL thm 366 fun nested tm = can(find_term (aconv f)) tm handle HOL_ERR _ => false 367 fun get_cntxt TC = fst(dest_imp(#2(strip_forall(concl TC)))) 368 fun mk_ih ((TC,locals),th2,nested) = 369 GENL locals 370 (if nested 371 then DISCH (get_cntxt TC) th2 handle HOL_ERR _ => th2 372 else if is_imp(concl TC) 373 then IMP_TRANS TC th2 374 else MP th2 TC) 375 in 376 DISCH antc 377 (if is_imp(concl thm') (* recursive calls in this clause *) 378 then let val th1 = ASSUME antc 379 val TCs = map #1 TCs_locals 380 val ylist = map (#2 o dest_relation o #2 o 381 wfrecUtils.strip_imp o #2 o strip_forall) TCs 382 val TClist = map (fn(TC,lvs) => (SPECL (fst (strip_forall TC)) (ASSUME TC),lvs)) 383 TCs_locals 384 val th2list = map (C SPEC th1) ylist 385 val nlist = map nested TCs 386 val triples = zip3 TClist th2list nlist 387 val Pylist = map mk_ih triples 388 in 389 MP thm' (LIST_CONJ Pylist) 390 end 391 else thm') 392 end; 393 394 395fun detuple newvar = 396 let fun detup M = 397 if pairLib.is_pair M 398 then let val (M1,M2) = pairSyntax.dest_pair M 399 val ((M1',vars1), (M2',vars2)) = (detup M1, detup M2) 400 in (pairLib.mk_pair(M1',M2'), vars1@vars2) 401 end 402 else let val v = newvar (type_of M) in (v,[v]) end 403 in detup 404 end; 405 406(*---------------------------------------------------------------------------*) 407(* For monitoring how much time and inferences building the induction *) 408(* theorem takes. *) 409(*---------------------------------------------------------------------------*) 410 411val monitoring = ref 0; 412 413val _ = Feedback.register_trace("tfl_ind",monitoring,1); 414 415(*---------------------------------------------------------------------------* 416 * Input : f, R, SV, and [(pat1,TCs1),..., (patn,TCsn)] * 417 * * 418 * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove * 419 * recursion induction (Rinduct) by proving the antecedent of Sinduct from * 420 * the antecedent of Rinduct. * 421 *---------------------------------------------------------------------------*) 422 423(* 424fun mk_induction thy {fconst, R, SV, pat_TCs_list} = 425let fun f() = 426let val Sinduction = UNDISCH (ISPEC R relationTheory.WF_INDUCTION_THM) 427 val (pats,TCsl) = unzip pat_TCs_list 428 val case_thm = complete_cases thy pats 429 val domn = (type_of o (Lib.trye hd)) pats 430 val P = variant (all_varsl (pats@flatten TCsl)) (mk_var("P",domn-->bool)) 431 val Sinduct = SPEC P Sinduction 432 val Sinduct_assumf = rand ((fst o dest_imp o concl) Sinduct) 433 val Rassums_TCl' = map (build_ih fconst (P,R,SV)) pat_TCs_list 434 val (Rassums,TCl') = unzip Rassums_TCl' 435 val Rinduct_assum = ASSUME (list_mk_conj Rassums) 436 val cases = map (beta_conv o curry mk_comb Sinduct_assumf) pats 437 val tasks = zip3 cases TCl' (CONJUNCTS Rinduct_assum) 438 val proved_cases = map (prove_case fconst thy) tasks 439 val v = variant (free_varsl (map concl proved_cases)) (mk_var("v",domn)) 440 val substs = map (SYM o ASSUME o curry mk_eq v) pats 441 val proved_cases1 = map2 (fn th => SUBS[th]) substs proved_cases 442 val abs_cases = map Rules.LEFT_ABS_VSTRUCT proved_cases1 443 val dant = GEN v (DISJ_CASESL (ISPEC v case_thm) abs_cases) 444 val dc = MP Sinduct dant 445 val (vstruct,vars) = detuple (wfrecUtils.vary[P]) (hd pats) 446 val dc' = itlist GEN vars (SPEC vstruct dc) 447in 448 GEN P (DISCH (concl Rinduct_assum) dc') 449end 450handle e => raise wrap_exn "Induction" "mk_induction" e 451in 452 if !monitoring > 0 then Count.apply f () else f() 453end 454*) 455 456 457(*---------------------------------------------------------------------------*) 458(* A clause of the case_thm can have one of the following forms: *) 459(* *) 460(* ?vlist. (var = tm) *) 461(* ?vlist. (var = tm) /\ constraints (* literal pattern *) *) 462(* *) 463(* We want to match tm against pat, to get theta, which will be applied to *) 464(* the clause. The reason for this is that "proved_cases" needs to align *) 465(* with the clauses in case_thm. In case it doesn't, match_clauses is called *) 466(* to restore alignment. *) 467(*---------------------------------------------------------------------------*) 468 469fun var_pure theta = Lib.all (fn {redex,residue} => is_var residue) theta; 470 471fun match_clause pat clause = 472 let open boolSyntax 473 val (V,tm) = strip_exists clause 474 in case strip_conj tm 475 of [] => raise ERR "match_clause" "unexpected structure in case_thm" 476 | xeq::constraints => 477 let val (x,target) = dest_eq xeq 478 in case Term.match_term target pat 479 of ([],[]) => clause 480 | (theta,[]) => 481 if var_pure theta 482 then list_mk_exists(map (subst theta) V, subst theta tm) 483 else raise ERR "match_clause" "no match" 484 | (theta,tytheta) => raise ERR "match_clause" "inequal types" 485 end 486 end; 487 488fun match_clauses pats case_thm = 489 let val clauses = strip_disj (concl case_thm) 490 fun match [] [] = [] 491 | match (p1::rst) (clauses as (_::_)) = 492 let open Lib 493 val (cl,clauses') = trypluck (match_clause p1) clauses 494 in cl::match rst clauses' 495 end 496 | match other wise = raise ERR "match_clauses" "different lengths" 497 in 498 EQ_MP (EQT_ELIM 499 (AC_CONV (DISJ_ASSOC,DISJ_SYM) 500 (mk_eq(concl case_thm, 501 list_mk_disj (match pats clauses))))) 502 case_thm 503 end 504 handle e => raise wrap_exn "Induction" "match_clauses" e; 505 506(*---------------------------------------------------------------------------*) 507(* Input : f, R, SV, and [(pat1,TCs1),..., (patn,TCsn)] *) 508(* *) 509(* Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove *) 510(* recursion induction (Rinduct) by proving the antecedent of Sinduct from *) 511(* the antecedent of Rinduct. *) 512(*---------------------------------------------------------------------------*) 513 514(* 515val {fconst, R, SV, pat_TCs_list} = {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} 516val thy = facts 517 *) 518 519fun mk_induction thy {fconst, R, SV, pat_TCs_list} = 520let fun f() = 521let val Sinduction = UNDISCH (ISPEC R relationTheory.WF_INDUCTION_THM) 522 val (pats,TCsl) = unzip pat_TCs_list 523 val case_thm = complete_cases thy pats 524 val domn = (type_of o (Lib.trye hd)) pats 525 val P = variant (all_varsl (pats@flatten TCsl)) (mk_var("P",domn-->bool)) 526 val Sinduct = SPEC P Sinduction 527 val Sinduct_assumf = rand ((fst o dest_imp o concl) Sinduct) 528 val Rassums_TCl' = map (build_ih fconst (P,R,SV)) pat_TCs_list 529 val (Rassums,TCl') = unzip Rassums_TCl' 530 val Rinduct_assum = ASSUME (list_mk_conj Rassums) 531 val cases = map (beta_conv o curry mk_comb Sinduct_assumf) pats 532 val tasks = zip3 cases TCl' (CONJUNCTS Rinduct_assum) 533 val proved_cases = map (prove_case fconst thy) tasks 534 val v = variant (free_varsl (map concl proved_cases)) (mk_var("v",domn)) 535 val case_thm' = ISPEC v case_thm 536 val case_thm'' = match_clauses pats case_thm' (* align case_thm' with pats *) 537 fun mk_subst tm = 538 if is_eq tm then SYM (ASSUME tm) 539 else SYM (hd (CONJUNCTS (ASSUME (snd(strip_exists tm))))) 540 val substs = map mk_subst (strip_disj (concl case_thm'')) 541 (* Now elim pats in favour of variables *) 542 val proved_cases1 = map (PURE_REWRITE_RULE substs) proved_cases 543 val abs_cases = map LEFT_EXISTS proved_cases1 544 val dant = GEN v (DISJ_CASESL case_thm'' abs_cases) 545 val dc = MP Sinduct dant 546 val (vstruct,vars) = detuple (wfrecUtils.vary[P]) (hd pats) 547 val dc' = itlist GEN vars (SPEC vstruct dc) 548in 549 GEN P (DISCH (concl Rinduct_assum) dc') 550end 551handle e => raise wrap_exn "Induction" "mk_induction" e 552in 553 if !monitoring > 0 then Count.apply f () else f() 554end; 555 556(*---------------------------------------------------------------------------*) 557(* Recursion induction tactic. Taken from tflLib. *) 558(* *) 559(* Given a goal `!v1 ... vn. M`, and an induction theorem of the form *) 560(* returned by TFL, i.e., *) 561(* *) 562(* !P. clause_1 /\ ... /\ clause_n *) 563(* ==> *) 564(* !u1 ... uk. P vstr_1 ... vstr_j *) 565(* *) 566(* we use v1 ... vk to rename the varstructs vstr_1 ... vstr_j to variables *) 567(* in the goal. Thus the binding prefix of the goal is used to make the *) 568(* predicate with which P is instantiated. *) 569(*---------------------------------------------------------------------------*) 570 571fun rename_tuple tm [] = (tm,[]) 572 | rename_tuple tm (vlist as (h::t)) = 573 let open pairSyntax 574 in if is_var tm then (h,t) 575 else let val (p1,p2) = dest_pair tm 576 val (p1',vlist') = rename_tuple p1 vlist 577 val (p2',vlist'') = rename_tuple p2 vlist' 578 in (mk_pair (p1',p2'), vlist'') 579 end 580 end; 581 582fun rename_tuples [] vlist = ([],vlist) 583 | rename_tuples (tmlist as (h::t)) vlist = 584 let val (tuple,vlist') = rename_tuple h vlist 585 val (tuples,vlist'') = rename_tuples t vlist' 586 in (tuple::tuples, vlist'') 587 end 588 handle e => raise wrap_exn "Induction" "rename_tuples" e; 589 590fun ndest_forall n trm = 591 let fun dest (0,tm,V) = (rev V,tm) 592 | dest (n,tm,V) = 593 let val (Bvar,Body) = dest_forall tm 594 handle _ => raise ERR "ndest_forall" 595 "too few quantified variables in goal" 596 in dest(n-1,Body, Bvar::V) 597 end 598 in dest(n,trm,[]) 599 end; 600 601fun recInduct thm = 602 let open pairLib 603 val (prop,Body) = dest_forall(concl thm) 604 val c = snd (strip_imp Body) 605 val Pargs = snd(strip_comb(snd(strip_forall c))) 606 val n = (length o #1 o strip_forall o #2 o strip_imp) Body 607 fun tac (asl,w) = 608 let val (V,body) = ndest_forall n w 609 val (vstrl,extras) = rename_tuples Pargs V 610 val _ = if not (null extras) 611 then raise ERR "recInduct" "internal error" else () 612 val P = list_mk_pabs(vstrl,body) 613 val thm' = GEN_BETA_RULE (ISPEC P thm) 614 in MATCH_MP_TAC thm' (asl,w) 615 end 616 in tac 617 end 618 handle e => raise wrap_exn "Induction" "recInduct" e; 619 620(* 621fun mk_vstrl [] V A = rev A 622 | mk_vstrl (ty::rst) V A = 623 let val (vstr,V1) = unstrip_pair ty V 624 in mk_vstrl rst V1 (vstr::A) 625 end; 626 627fun recInduct thm = 628 let val (prop,Body) = dest_forall(concl thm) 629 val parg_tyl = #1(strip_fun (type_of prop)) 630 val n = (length o #1 o strip_forall o #2 o strip_imp) Body 631 fun ndest_forall trm = 632 let fun dest (0,tm,V) = (rev V,tm) 633 | dest (n,tm,V) = 634 let val (Bvar,Body) = dest_forall tm 635 in dest(n-1,Body, Bvar::V) end 636 in dest(n,trm,[]) 637 end 638 fun tac (asl,w) = 639 let val (V,body) = ndest_forall w 640 val P = (list_mk_pabs(mk_vstrl parg_tyl V [],body) 641 handle HOL_ERR _ => list_mk_abs(V,body)) 642 val thm' = GEN_BETA_RULE (ISPEC P thm) 643 in MATCH_MP_TAC thm' (asl,w) 644 end 645 in tac 646 end 647 handle e => raise wrap_exn "Induction" "recInduct" e 648*) 649 650end 651