1(* ========================================================================= *) 2(* Inductive (or free recursive) types. *) 3(* *) 4(* John Harrison, University of Cambridge Computer Laboratory *) 5(* *) 6(* (c) Copyright, University of Cambridge 1998 *) 7(* *) 8(* ported from Caml Light source by Michael Norrish, November 1999 *) 9(* ========================================================================= *) 10 11(* 12 app load [(* "HOLSimps", *) "Q", "numLib", "IndDefLib", "tautLib"]; 13*) 14 15structure ind_types :> ind_types = 16struct 17 18open HolKernel Parse boolLib InductiveDefinition 19 numTheory arithmeticTheory prim_recTheory 20 simpLib boolSimps ind_typeTheory; 21 22type constructor = string * hol_type list 23type tyspec = hol_type * constructor list 24 25val ERR = mk_HOL_ERR "ind_types"; 26 27(* Fix the grammar used by this file *) 28structure Parse = struct 29open Parse 30val (Type,Term) = parse_from_grammars ind_typeTheory.ind_type_grammars 31end 32open Parse; 33 34(*--------------------------------------------------------------------------- 35 First some JRH HOL-Light portability stuff. 36 ---------------------------------------------------------------------------*) 37 38fun chop_list 0 l = ([], l) 39 | chop_list n [] = raise ERR "chop_list" "Empty list" 40 | chop_list n (h::t) = let val (m,l') = chop_list (n-1) t in (h::m, l') end; 41 42val lhand = rand o rator; 43val LAND_CONV = RATOR_CONV o RAND_CONV; 44val RIGHT_BETAS = rev_itlist(fn a=>CONV_RULE(RAND_CONV BETA_CONV) o C AP_THM a) 45 46fun sucivate n = funpow n numSyntax.mk_suc numSyntax.zero_tm; 47(* fun sucivate n = numSyntax.term_of_int n; *) 48 49val make_args = 50 let fun margs n s avoid [] = [] 51 | margs n s avoid (h::t) = 52 let val v = variant avoid (mk_var(s^Int.toString n, h)) 53 in v::margs (n + 1) s (v::avoid) t 54 end 55 in fn s => fn avoid => fn tys => 56 if length tys = 1 57 then [variant avoid (mk_var(s, hd tys))] 58 else margs 0 s avoid tys 59 end handle _ => raise ERR "make_args" ""; 60 61fun mk_binop op_t tm1 tm2 = list_mk_comb(op_t, [tm1, tm2]) 62 63fun mk_const (thy, n, theta) = 64 let val c0 = prim_mk_const{Name = n, Thy = thy} 65 val ty = type_of c0 66 in Term.mk_thy_const{Name=n, Thy=thy, Ty=Type.type_subst theta ty} 67 end; 68 69fun mk_icomb(tm1,tm2) = 70 let val (ty, _) = Type.dom_rng (type_of tm1) 71 val tyins = Type.match_type ty (type_of tm2) 72 in 73 mk_comb(Term.inst tyins tm1, tm2) 74 end; 75 76fun list_mk_icomb (thy,cname) = 77 let val cnst = mk_const(thy,cname,[]) 78 in fn args => rev_itlist (C (curry mk_icomb)) args cnst 79 end; 80 81val variables = 82 let 83 fun ins t l = op_insert aconv t l 84 fun vars(acc,tm) = 85 if is_var tm then ins tm acc 86 else if is_const tm then acc 87 else if is_abs tm 88 then let val (v, bod) = dest_abs tm in vars(ins v acc,bod) end 89 else let val (l,r) = dest_comb tm in vars(vars(acc,l),r) end 90 in 91 fn tm => vars([],tm) 92 end; 93 94fun striplist dest = 95 let fun strip x acc = 96 let val (l,r) = dest x 97 in strip l (strip r acc) 98 end handle HOL_ERR _ => x::acc 99 in 100 fn x => strip x [] 101 end; 102 103(*--------------------------------------------------------------------------- 104 This is not the same as Type.type_subst, which only substitutes 105 for variables! 106 ---------------------------------------------------------------------------*) 107 108fun tysubst theta ty = 109 case subst_assoc (equal ty) theta 110 of SOME x => x 111 | NONE => 112 if is_vartype ty then ty 113 else let val {Tyop,Thy,Args} = dest_thy_type ty 114 in mk_thy_type{Tyop=Tyop,Thy=Thy, Args=map (tysubst theta) Args} 115 end; 116 117fun SUBS_CONV [] tm = REFL tm 118 | SUBS_CONV ths tm = 119 let val lefts = map (lhand o concl) ths 120 val gvs = map (genvar o type_of) lefts 121 val pat = Term.subst (map2 (curry op|->) lefts gvs) tm 122 val abs = list_mk_abs(gvs,pat) 123 val th = rev_itlist (fn y => fn x => 124 CONV_RULE (RAND_CONV BETA_CONV THENC 125 (RATOR_CONV o RAND_CONV) BETA_CONV)(MK_COMB(x,y))) 126 ths (REFL abs) 127 in 128 if aconv (rand(concl th)) tm then REFL tm else th 129 end 130 131val GEN_REWRITE_RULE = fn c => fn thl => GEN_REWRITE_RULE c empty_rewrites thl 132val GEN_REWRITE_CONV = fn c => fn thl => GEN_REWRITE_CONV c empty_rewrites thl 133 134fun SIMPLE_EXISTS v th = EXISTS (mk_exists(v, concl th),v) th; 135fun SIMPLE_CHOOSE v th = CHOOSE(v,ASSUME (mk_exists(v, hd(hyp th)))) th; 136 137fun new_basic_type_definition tyname (mkname, destname) thm = 138 let val (pred, witness) = dest_comb(concl thm) 139 val predty = type_of pred 140 val dom_ty = #1 (dom_rng predty) 141 val x = mk_var("x", dom_ty) 142 val witness_exists = EXISTS(mk_exists(x, mk_comb(pred,x)),witness) thm 143 val tyax = new_type_definition(tyname,witness_exists) 144 val (mk_dest, dest_mk) = 145 CONJ_PAIR(define_new_type_bijections 146 {name=temp_binding (tyname^"_repfns"), 147 ABS=mkname, REP=destname, tyax=tyax}) 148 in 149 (SPEC_ALL mk_dest, SPEC_ALL dest_mk) 150 end; 151 152 153(* ------------------------------------------------------------------------- *) 154(* Eliminate local "definitions" in hyps. *) 155(* ------------------------------------------------------------------------- *) 156 157fun SCRUB_EQUATION eq th = 158 let val (l,r) = dest_eq eq 159 in MP (INST [l |-> r] (DISCH eq th)) (REFL r) 160 end; 161 162(* ------------------------------------------------------------------------- *) 163(* Proves existence of model (inductively); use pseudo-constructors. *) 164(* *) 165(* Returns suitable definitions of constructors in terms of CONSTR, and the *) 166(* rule and induction theorems from the inductive relation package. *) 167(* ------------------------------------------------------------------------- *) 168 169 170val justify_inductive_type_model = let 171 val aty = Type.alpha 172 val T_tm = boolSyntax.T 173 and n_tm = mk_var("n",numSyntax.num) 174(* and beps_tm = Term`@x:bool. T` *) 175 and beps_tm = mk_arb bool 176 fun munion [] s2 = s2 177 | munion (h1::s1') s2 = 178 let val (_,s2') = Lib.pluck (fn h2 => h2 = h1) s2 179 in h1::munion s1' s2' 180 end handle HOL_ERR _ => h1::munion s1' s2 181in 182 fn def => let 183 val (newtys,rights) = unzip def 184 val tyargls = itlist (curry op@ o map snd) rights [] 185 val alltys = itlist (munion o C set_diff newtys) tyargls [] 186(* val epstms = map (fn ty => mk_select(mk_var("v",ty),T_tm)) alltys *) 187 val arb_tms = map mk_arb alltys 188 val pty = 189 end_itlist (fn ty1 => fn ty2 => mk_type("prod",[ty1,ty2])) alltys 190 handle HOL_ERR _ => Type.bool 191 val recty = mk_type("recspace",[pty]) 192 val constr = mk_const("ind_type","CONSTR",[aty |-> pty]) 193 val fcons = mk_const("ind_type", "FCONS",[aty |-> recty]) 194 val bot = mk_const("ind_type", "BOTTOM",[aty |-> pty]) 195 val bottail = mk_abs(n_tm,bot) 196 fun mk_constructor n (cname,cargs) = let 197 val ttys = map (fn ty => if mem ty newtys then recty else ty) cargs 198 val args = make_args "a" [] ttys 199 val (rargs,iargs) = partition (fn t => type_of t = recty) args 200 fun mk_injector arb_tms alltys iargs = 201 if alltys = [] then [] 202 else let 203 val ty = hd alltys 204 in 205 let 206 val (a,iargs') = Lib.pluck (fn t => type_of t = ty) iargs 207 in 208 a::(mk_injector (tl arb_tms) (tl alltys) iargs') 209 end handle HOL_ERR _ => 210 (hd arb_tms)::(mk_injector (tl arb_tms) (tl alltys) iargs) 211 end 212 val iarg = 213 end_itlist (curry pairSyntax.mk_pair) (mk_injector arb_tms alltys iargs) 214 handle HOL_ERR _ => beps_tm 215 val rarg = itlist (mk_binop fcons) rargs bottail 216 val conty = itlist (curry Type.-->) (map type_of args) recty 217 val condef = list_mk_comb(constr,[sucivate n, iarg, rarg]) 218 in 219 mk_eq(mk_var(cname,conty),list_mk_abs(args,condef)) 220 end 221 fun mk_constructors n rights = 222 if rights = [] then [] 223 else 224 (mk_constructor n (hd rights))::(mk_constructors (n + 1) (tl rights)) 225 val condefs = mk_constructors 0 (itlist (curry op@) rights []) 226 val conths = map ASSUME condefs 227 val predty = Type.-->(recty, Type.bool) 228 val rels = map (fn s => mk_var(dest_vartype s,predty)) newtys 229 val edefs = 230 itlist (fn (x,l) => fn acc => map (fn t => (x,t)) l @ acc) def [] 231 val idefs = 232 map2 (fn (r,(_,atys)) => fn def => ((r,atys),def)) edefs condefs 233 fun mk_rule ((r,a),condef) = let 234 val (left,right) = dest_eq condef 235 val (args,bod) = strip_abs right 236 val lapp = list_mk_comb(left,args) 237 val conds = itlist2 238 (fn arg => fn argty => fn sofar => 239 if mem argty newtys then 240 mk_comb(mk_var(dest_vartype argty,predty),arg)::sofar 241 else sofar) args a [] 242 val conc = mk_comb(mk_var(dest_vartype r,predty),lapp) 243 val rule = if null conds then conc 244 else mk_imp(list_mk_conj conds,conc) 245 in 246 list_mk_forall(args,rule) 247 end 248 val rules = list_mk_conj (map mk_rule idefs) 249 val th0 = derive_nonschematic_inductive_relations rules 250 val th1 = prove_monotonicity_hyps bool_monoset th0 251 val (th2a,th2bc) = CONJ_PAIR th1 252 val th2b = CONJUNCT1 th2bc 253 in 254 (conths,th2a,th2b) 255 end 256end 257 258(* ------------------------------------------------------------------------- *) 259(* Shows that the predicates defined by the rules are all nonempty. *) 260(* (This could be done much more efficiently/cleverly, but it's OK.) *) 261(* ------------------------------------------------------------------------- *) 262 263val tmem = op_mem aconv 264val tmk_set = op_mk_set aconv 265val tunion = op_union aconv 266fun prove_model_inhabitation rth = let 267 val srules = map SPEC_ALL (CONJUNCTS rth) 268 val (imps,bases) = partition (is_imp o concl) srules 269 val concs = map concl bases @ map (rand o concl) imps 270 val preds = op_mk_set aconv (map (repeat rator) concs) 271 fun exhaust_inhabitations ths sofar = let 272 val dunnit = tmk_set (map (fst o strip_comb o concl) sofar) 273 val useful = filter 274 (fn th => not (tmem (fst(strip_comb(rand(concl th)))) dunnit)) ths 275 in 276 if null useful then sofar 277 else let 278 fun follow_horn thm = let 279 val preds = map (fst o strip_comb) (strip_conj(lhand(concl thm))) 280 val asms = 281 map (fn p => 282 valOf (List.find 283 (fn th => aconv (fst(strip_comb(concl th))) p) 284 sofar)) 285 preds 286 in 287 MATCH_MP thm (end_itlist CONJ asms) 288 end 289 val newth = tryfind follow_horn useful 290 in 291 exhaust_inhabitations ths (newth::sofar) 292 end 293 end 294 val ithms = exhaust_inhabitations imps bases 295 val exths = map 296 (fn p => valOf 297 (List.find 298 (fn th => aconv (fst(strip_comb(concl th))) p) 299 ithms)) 300 preds 301in 302 exths 303end 304 305(* ------------------------------------------------------------------------- *) 306(* Makes a type definition for one of the defined subsets. *) 307(* ------------------------------------------------------------------------- *) 308 309val safepfx = " @ind_type" 310local 311 val count = ref 0 312 fun vary_to_avoid_constants () = let 313 val nm = 314 temp_binding (safepfx ^ current_theory() ^ Int.toString (!count)) 315 in 316 if (not (null (decls nm))) then (count := !count + 100; 317 vary_to_avoid_constants()) 318 else (count := !count + 1; nm) 319 end 320in 321 322fun safeid_genvar ty = Term.mk_var(vary_to_avoid_constants(), ty) 323val safeid_genname = vary_to_avoid_constants 324 325end (* local *) 326 327fun define_inductive_type cdefs exth = let 328 val extm = concl exth 329 val epred = fst(strip_comb extm) 330 val ename = String.extract(fst(dest_var epred), 1, NONE) 331 val th1 = ASSUME 332 (valOf (List.find (fn eq => aconv (lhand eq) epred) (hyp exth))) 333 val th2 = TRANS th1 (SUBS_CONV cdefs (rand(concl th1))) 334 val th3 = EQ_MP (AP_THM th2 (rand extm)) exth 335 fun scrubber th = case HOLset.find (fn _ => true) (hypset th) of 336 NONE => th 337 | SOME eq => scrubber (SCRUB_EQUATION eq th) 338 val th4 = scrubber th3 339 val mkname = safeid_genname() and destname = safeid_genname() 340 val (bij1,bij2) = new_basic_type_definition ename (mkname,destname) th4 341 val bij2a = AP_THM th2 (rand(rand(concl bij2))) 342 val bij2b = TRANS bij2a bij2 343in 344 (bij1,bij2b) 345end; 346 347(* ------------------------------------------------------------------------- *) 348(* Defines a type constructor corresponding to current pseudo-constructor. *) 349(* ------------------------------------------------------------------------- *) 350fun tmassoc t l = op_assoc aconv t l 351fun define_inductive_type_constructor defs consindex th = let 352 val (avs,bod) = strip_forall(concl th) 353 val (asms,conc) = 354 if is_imp bod then (strip_conj(lhand bod),rand bod) else ([],bod) 355 val asmlist = map dest_comb asms 356 val (cpred,cterm) = dest_comb conc 357 val (oldcon,oldargs) = strip_comb cterm 358 fun modify_arg v = let 359 val dest = snd(tmassoc (op_rev_assoc aconv v asmlist) consindex) 360 val ty' = hd(snd(dest_type(type_of dest))) 361 val v' = mk_var(fst(dest_var v),ty') 362 in 363 (mk_comb(dest,v'),v') 364 end handle HOL_ERR _ => (v,v) 365 val (newrights,newargs) = unzip(map modify_arg oldargs) 366 val retmk = fst(tmassoc cpred consindex) 367 val defbod = mk_comb(retmk,list_mk_comb(oldcon,newrights)) 368 val defrt = list_mk_abs(newargs,defbod) 369 val expth = valOf (List.find (fn th => aconv (lhand(concl th)) oldcon) defs) 370 val rexpth = SUBS_CONV [expth] defrt 371 val deflf = mk_var(fst(dest_var oldcon),type_of defrt) 372 val defth = new_definition(temp_binding (fst (dest_var oldcon) ^ "_def"), 373 mk_eq(deflf,rand(concl rexpth))) 374in 375 TRANS defth (SYM rexpth) 376end; 377 378(* ------------------------------------------------------------------------- *) 379(* Instantiate the induction theorem on the representatives to transfer *) 380(* it to the new type(s). Uses "\x. rep-pred(x) /\ P(mk x)" for "P". *) 381(* ------------------------------------------------------------------------- *) 382 383fun instantiate_induction_theorem consindex ith = let 384 val (avs,bod) = strip_forall(concl ith) 385 val corlist = 386 map((repeat rator ## repeat rator) o dest_imp o body o rand) 387 (strip_conj(rand bod)) 388 val consindex' = 389 map (fn v => let val w = op_rev_assoc aconv v corlist 390 in (w,tmassoc w consindex) end) 391 avs 392 val recty = (hd o snd o dest_type o type_of o fst o snd o hd) consindex 393 val newtys = map (hd o snd o dest_type o type_of o snd o snd) consindex' 394 val ptypes = map (C (curry op -->) Type.bool) newtys 395 val preds = make_args "P" [] ptypes 396 val args = make_args "x" [] (map (K recty) preds) 397 val lambs = map2 (fn (r,(m,d)) => fn (p,a) => 398 mk_abs(a,mk_conj(mk_comb(r,a),mk_comb(p,mk_comb(m,a))))) 399 consindex' (zip preds args) 400in 401 SPECL lambs ith 402end; 403 404(* ------------------------------------------------------------------------- *) 405(* Reduce a single clause of the postulated induction theorem (old_ver) back *) 406(* to the kind wanted for the new type (new_ver); |- new_ver ==> old_ver *) 407(* ------------------------------------------------------------------------- *) 408 409fun pullback_induction_clause tybijpairs conthms = let 410 val PRERULE = GEN_REWRITE_RULE (funpow 3 RAND_CONV) (map SYM conthms) 411 val IPRULE = SYM o GEN_REWRITE_RULE I (map snd tybijpairs) 412in 413 fn rthm => fn tm => let 414 val (avs,bimp) = strip_forall tm 415 in 416 if is_imp bimp then let 417 val (ant,con) = dest_imp bimp 418 val ths = map (CONV_RULE BETA_CONV) (CONJUNCTS (ASSUME ant)) 419 val (tths,pths) = unzip (map CONJ_PAIR ths) 420 val tth = MATCH_MP (SPEC_ALL rthm) (end_itlist CONJ tths) 421 val mths = map IPRULE (tth::tths) 422 val conth1 = BETA_CONV con 423 val contm1 = rand(concl conth1) 424 val conth2 = TRANS conth1 425 (AP_TERM (rator contm1) (SUBS_CONV (tl mths) (rand contm1))) 426 val conth3 = PRERULE conth2 427 val lctms = map concl pths 428 val asmin = mk_imp(list_mk_conj lctms,rand(rand(concl conth3))) 429 val argsin = map rand (strip_conj(lhand asmin)) 430 val argsgen = 431 map (fn tm => mk_var(fst(dest_var(rand tm)),type_of tm)) argsin 432 val asmgen = Term.subst (map2 (curry op |->) argsin argsgen) asmin 433 val asmquant = 434 list_mk_forall(snd(strip_comb(rand(rand asmgen))),asmgen) 435 val th1 = INST (map2 (curry op |->) argsgen argsin) 436 (SPEC_ALL (ASSUME asmquant)) 437 val th2 = MP th1 (end_itlist CONJ pths) 438 val th3 = EQ_MP (SYM conth3) (CONJ tth th2) 439 in 440 DISCH asmquant (GENL avs (DISCH ant th3)) 441 end 442 else let 443 val con = bimp 444 val conth2 = BETA_CONV con 445 val tth = HO_PART_MATCH I rthm (lhand(rand(concl conth2))) 446 val conth3 = PRERULE conth2 447 val asmgen = rand(rand(concl conth3)) 448 val asmquant = list_mk_forall(snd(strip_comb(rand asmgen)),asmgen) 449 val th2 = SPEC_ALL (ASSUME asmquant) 450 val th3 = EQ_MP (SYM conth3) (CONJ tth th2) 451 in 452 DISCH asmquant (GENL avs th3) 453 end 454 end 455end; 456 457(* ------------------------------------------------------------------------- *) 458(* Finish off a consequence of the induction theorem. *) 459(* ------------------------------------------------------------------------- *) 460 461fun finish_induction_conclusion consindex tybijpairs = let 462 val (tybij1,tybij2) = unzip tybijpairs 463 val PRERULE = 464 GEN_REWRITE_RULE (LAND_CONV o LAND_CONV o RAND_CONV) tybij1 o 465 GEN_REWRITE_RULE LAND_CONV tybij2 466 and FINRULE = GEN_REWRITE_RULE RAND_CONV tybij1 467in 468 fn th => let 469 val (av,bimp) = dest_forall(concl th) 470 val pv = lhand(body(rator(rand bimp))) 471 val (p,v) = dest_comb pv 472 val (mk,dest) = tmassoc p consindex 473 val ty = hd(snd(dest_type(type_of dest))) 474 val v' = mk_var(fst(dest_var v),ty) 475 val dv = mk_comb(dest,v') 476 val th1 = PRERULE (SPEC dv th) 477 val th2 = MP th1 (REFL (rand(lhand(concl th1)))) 478 val th3 = CONV_RULE BETA_CONV th2 479 in 480 GEN v' (FINRULE (CONJUNCT2 th3)) 481 end 482end; 483 484(* ------------------------------------------------------------------------- *) 485(* Derive the induction theorem. *) 486(* ------------------------------------------------------------------------- *) 487 488val conjuncts = strip_conj; 489 490fun derive_induction_theorem consindex tybijpairs conthms iith rth = let 491 val bths = map2 492 (pullback_induction_clause tybijpairs conthms) 493 (CONJUNCTS rth) (conjuncts(lhand(concl iith))) 494 val asm = list_mk_conj(map (lhand o concl) bths) 495 val ths = map2 MP bths (CONJUNCTS (ASSUME asm)) 496 val th1 = MP iith (end_itlist CONJ ths) 497 val th2 = end_itlist CONJ (map 498 (finish_induction_conclusion consindex tybijpairs) (CONJUNCTS th1)) 499 val th3 = DISCH asm th2 500 val preds = map (rator o body o rand) (conjuncts(rand(concl th3))) 501 val th4 = GENL preds th3 502 val pasms = filter (C tmem (map fst consindex) o lhand) (hyp th4) 503 val th5 = itlist DISCH pasms th4 504 val th6 = itlist SCRUB_EQUATION (hyp th5) th5 505 val th7 = UNDISCH_ALL th6 506in 507 itlist SCRUB_EQUATION (hyp th7) th7 508end; 509 510(* ------------------------------------------------------------------------- *) 511(* Create the recursive functions and eliminate pseudo-constructors. *) 512(* (These are kept just long enough to derive the key property.) *) 513(* ------------------------------------------------------------------------- *) 514 515fun create_recursive_functions tybijpairs consindex conthms rth = let 516 val domtys = map (hd o snd o dest_type o type_of o snd o snd) consindex 517 val recty = (hd o snd o dest_type o type_of o fst o snd o hd) consindex 518 val ranty = mk_vartype "'Z" 519 val fnn = mk_var("fn", recty --> ranty) 520 and fns = make_args "fn" [] (map (C (curry op -->) ranty) domtys) 521 val args = make_args "a" [] domtys 522 val rights = 523 map2 (fn (_,(_,d)) => fn a => 524 mk_abs(a,mk_comb(fnn,mk_comb(d,a)))) 525 consindex args 526 val eqs = map2 (curry mk_eq) fns rights 527 val fdefs = map ASSUME eqs 528 val fxths1 = 529 map (fn th1 => tryfind (fn th2 => MK_COMB(th2,th1)) fdefs) 530 conthms 531 val fxths2 = map (fn th => TRANS th (BETA_CONV (rand(concl th)))) fxths1 532 fun mk_tybijcons (th1,th2) = let 533 val th3 = INST [rand(lhand(concl th2)) |-> rand(lhand(concl th1))] th2 534 val th4 = AP_TERM (rator(lhand(rand(concl th2)))) th1 535 in 536 EQ_MP (SYM th3) th4 537 end 538 val SCONV = GEN_REWRITE_CONV I (map mk_tybijcons tybijpairs) 539 and ERULE = GEN_REWRITE_RULE I (map snd tybijpairs) 540 fun simplify_fxthm rthm fxth = let 541 val pat = funpow 4 rand (concl fxth) 542 in 543 if is_imp(repeat (snd o dest_forall) (concl rthm)) then let 544 val th1 = PART_MATCH (rand o rand) rthm pat 545 val tms1 = conjuncts(lhand(concl th1)) 546 val ths2 = map (fn t => EQ_MP (SYM(SCONV t)) TRUTH) tms1 547 in 548 ERULE (MP th1 (end_itlist CONJ ths2)) 549 end 550 else 551 ERULE (PART_MATCH rand rthm pat) 552 end 553 val fxths3 = map2 simplify_fxthm (CONJUNCTS rth) fxths2 554 val fxths4 = map2 (fn th1 => TRANS th1 o AP_TERM fnn) fxths2 fxths3 555 fun cleanup_fxthm cth fxth = let 556 val tms = snd(strip_comb(rand(rand(concl fxth)))) 557 val kth = RIGHT_BETAS tms (ASSUME (hd(hyp cth))) 558 in 559 TRANS fxth (AP_TERM fnn kth) 560 end 561 val fxth5 = end_itlist CONJ (map2 cleanup_fxthm conthms fxths4) 562 val pasms = filter (C tmem (map fst consindex) o lhand) (hyp fxth5) 563 val fxth6 = itlist DISCH pasms fxth5 564 val fxth7 = 565 itlist SCRUB_EQUATION (itlist (tunion o hyp) conthms []) fxth6 566 val fxth8 = UNDISCH_ALL fxth7 567in 568 itlist SCRUB_EQUATION (op_set_diff aconv (hyp fxth8) eqs) fxth8 569end; 570 571(* ------------------------------------------------------------------------- *) 572(* Create a function for recursion clause. *) 573(* ------------------------------------------------------------------------- *) 574 575fun SUBS ths = CONV_RULE (SUBS_CONV ths); 576 577fun upto n = let 578 fun down l n = if n < 0 then l else down (n::l) (n - 1) 579in 580 down [] n 581end; 582 583local 584 val zty = mk_vartype"'Z" 585 val numty = numSyntax.num 586 val s = mk_var("s",numty --> zty) 587 fun extract_arg tup v = 588 if aconv v tup then REFL tup 589 else let 590 val (t1,t2) = pairSyntax.dest_pair tup 591 val PAIR_th = ISPECL [t1,t2] (if free_in v t1 then pairTheory.FST 592 else pairTheory.SND) 593 val tup' = rand(concl PAIR_th) 594 in 595 if aconv tup' v then PAIR_th 596 else let 597 val th = extract_arg (rand(concl PAIR_th)) v 598 in 599 SUBS[SYM PAIR_th] th 600 end 601 end 602in 603 fun create_recursion_iso_constructor consindex = let 604 val recty = hd(snd(dest_type(type_of(fst(hd consindex))))) 605 val domty = hd(snd(dest_type recty)) 606 val i = mk_var("i",domty) 607 and r = mk_var("r", numty --> recty) 608 val mks = map (fst o snd) consindex 609 val mkindex = map (fn t => (hd(tl(snd(dest_type(type_of t)))),t)) mks 610 in 611 fn cth => let 612 val artms = snd(strip_comb(rand(rand(concl cth)))) 613 val artys = mapfilter (type_of o rand) artms 614 val (args,bod) = strip_abs(rand(hd(hyp cth))) 615 val (ccitm,rtm) = dest_comb bod 616 val (cctm,itm) = dest_comb ccitm 617 val (rargs,iargs) = partition (C free_in rtm) args 618 val xths = map (extract_arg itm) iargs 619 val cargs' = map (subst [itm |-> i] o lhand o concl) xths 620 val indices = map sucivate (upto (length rargs - 1)) 621 val rindexed = map (curry mk_comb r) indices 622 val rargs' = 623 map2 (fn a => fn rx => mk_comb(assoc a mkindex,rx)) 624 artys rindexed 625 val sargs' = map (curry mk_comb s) indices 626 val allargs = cargs'@ rargs' @ sargs' 627 val funty = itlist (curry op --> o type_of) allargs zty 628 val funname = fst(dest_const(repeat rator (lhand(concl cth))))^"'" 629 val funarg = mk_var(funname,funty) 630 in 631 list_mk_abs([i,r,s],list_mk_comb(funarg,allargs)) 632 end 633 end 634end; 635 636(* ------------------------------------------------------------------------- *) 637(* Derive the recursion theorem. *) 638(* ------------------------------------------------------------------------- *) 639 640val EXISTS_EQUATION = Prim_rec.EXISTS_EQUATION 641 642val bndvar = Term.bvar; 643 644local 645 val CCONV = funpow 3 RATOR_CONV (REPEATC (GEN_REWRITE_CONV I [FCONS])) 646(* val mycompset = reduceLib.num_compset() 647 val _ = computeLib.add_thms[FCONS_DEST] mycompset 648 val fcons_reduce = computeLib.CBV_CONV mycompset 649 val CCONV1 = funpow 3 RATOR_CONV fcons_reduce 650*) 651in 652 fun derive_recursion_theorem tybijpairs consindex conthms rath = let 653 val isocons = map (create_recursion_iso_constructor consindex) conthms 654 val ty = type_of(hd isocons) 655 val fcons = mk_const("ind_type", "FCONS",[Type.alpha |-> ty]) 656 and fnil = mk_const("ind_type", "FNIL",[Type.alpha |-> ty]) 657 val bigfun = itlist (mk_binop fcons) isocons fnil 658 val eth = ISPEC bigfun CONSTR_REC 659 val fnn = rator(rand(hd(conjuncts(concl rath)))) 660 val betm = let 661 val (v,bod) = dest_abs(rand(concl eth)) 662 in 663 subst[v |-> fnn] bod 664 end 665 val LCONV = REWR_CONV (ASSUME betm) 666 val fnths = 667 map (fn t => RIGHT_BETAS [bndvar(rand t)] (ASSUME t)) (hyp rath) 668 val SIMPER = SIMP_RULE bool_ss 669 (map SYM fnths @ map fst tybijpairs @ [pairTheory.FST, 670 pairTheory.SND, FCONS, BETA_THM]) 671 fun hackdown_rath th = let 672 val (ltm,rtm) = dest_eq(concl th) 673 val wargs = snd(strip_comb(rand ltm)) 674 val th1 = TRANS th (LCONV rtm) 675 val th2 = TRANS th1 (CCONV (rand(concl th1))) 676 val th3 = TRANS th2 (funpow 2 RATOR_CONV BETA_CONV (rand(concl th2))) 677 val th4 = TRANS th3 (RATOR_CONV BETA_CONV (rand(concl th3))) 678 val th5 = TRANS th4 (BETA_CONV (rand(concl th4))) 679 in 680 GENL wargs (SIMPER th5) 681 end 682 val rthm = end_itlist CONJ (map hackdown_rath (CONJUNCTS rath)) 683 val seqs = let 684 val unseqs = filter is_eq (hyp rthm) 685 val tys = map (hd o snd o dest_type o type_of o snd o snd) consindex 686 in 687 map (fn ty => valOf (List.find 688 (fn t => hd(snd(dest_type(type_of(lhand t)))) = ty) unseqs)) tys 689 end 690 val rethm = itlist EXISTS_EQUATION seqs rthm 691 val fethm = CHOOSE(fnn,eth) rethm 692 val pcons = 693 map (repeat rator o rand o repeat (snd o dest_forall)) 694 (conjuncts(concl rthm)) 695 in 696 GENL pcons fethm 697 end 698end 699 700(* ------------------------------------------------------------------------- *) 701(* Basic function: returns induction and recursion separately. No parser. *) 702(* ------------------------------------------------------------------------- *) 703 704fun define_type_raw def = let 705 val (defs,rth,ith) = justify_inductive_type_model def 706 val neths = prove_model_inhabitation rth 707 val tybijpairs = map (define_inductive_type defs) neths 708 val preds = map (repeat rator o concl) neths 709 val mkdests = 710 map 711 (fn (th,_) => 712 let val tm = lhand(concl th) in (rator tm,rator(rand tm)) end) 713 tybijpairs 714 val consindex = zip preds mkdests 715 val condefs = map (define_inductive_type_constructor defs consindex) 716 (CONJUNCTS rth) 717 val conthms = map 718 (fn th => let val args = fst(strip_abs(rand(concl th))) in 719 RIGHT_BETAS args th end) condefs 720 val iith = instantiate_induction_theorem consindex ith 721 val fth = derive_induction_theorem consindex tybijpairs conthms iith rth 722 val rath = create_recursive_functions tybijpairs consindex conthms rth 723 val kth = derive_recursion_theorem tybijpairs consindex conthms rath 724in 725 (fth,kth) 726end; 727 728(* Test the above with: 729 730 val def = [(Type`:'foo`, [("C1", []), ("C2", [Type`:num`])])]; 731 define_type_raw def; 732 733 val def = [(Type`:'bar`, [("D1", [Type`:num`]), ("D2", [Type`:'bar`])])] 734 define_type_raw def; 735 736 val def = [(Type`:'qux`, [("F1", []), ("F2", [Type`:'a`, Type`:'qux`])])]; 737 define_type_raw def; 738 739 val def = [(Type`:'qwerty`, [("G1", [Type`:num`]), 740 ("G2", [Type`:'asdf`])]), 741 (Type`:'asdf`, [("H1", []), ("H2", [Type`:'qwerty`])])]; 742 743 Form of recursion equation is not quite what hol98 expects. It doesn't 744 use ?! and it puts the recursive calls last as arguments, not first. 745 So, the list equivalent gets a theorem along the lines of: 746 !nil cons. 747 ?fn. 748 (fn NIL = nil) /\ (!x xs. fn (CONS x xs) = cons x xs (fn xs)) 749 not, 750 !nil cons. 751 ?!fn. 752 (fn NIL = nil) /\ (!x xs. fn (CONS x xs) = cons (fn xs) x xs) 753 754*) 755 756(*---------------------------------------------------------------------------* 757 * Required stuff for sum types * 758 *---------------------------------------------------------------------------*) 759 760val sum_INDUCT = TypeBase.induction_of ``:'a + 'b`` 761val sum_RECURSION = TypeBase.axiom_of ``:'a + 'b``; 762 763val OUTL = sumTheory.OUTL; 764val OUTR = sumTheory.OUTR; 765 766(* ------------------------------------------------------------------------- *) 767(* Generalize the recursion theorem to multiple domain types. *) 768(* (We needed to use a single type to justify it via a proforma theorem.) *) 769(* *) 770(* NB! Before this is called nontrivially (i.e. more than one new type) *) 771(* the type constructor ":sum", used internally, must have been defined. *) 772(* ------------------------------------------------------------------------- *) 773 774val generalize_recursion_theorem = let 775 val ELIM_OUTCOMBS = GEN_REWRITE_RULE TOP_DEPTH_CONV [OUTL, OUTR] 776 fun mk_sum tys = let 777 val k = length tys 778 in 779 if k = 1 then hd tys 780 else let 781 val (tys1,tys2) = chop_list (k div 2) tys 782 in 783 mk_type("sum", [mk_sum tys1, mk_sum tys2]) 784 end 785 end 786 val mk_inls = let 787 fun mk_inls ty = 788 if is_vartype ty then [mk_var("x",ty)] 789 else let 790 val (ty1,ty2) = case dest_type ty 791 of (_,[ty1,ty2]) => (ty1,ty2) 792 | _ => raise Match 793 val inls1 = mk_inls ty1 794 and inls2 = mk_inls ty2 795 val inl = 796 mk_const("sum", "INL",[(Type.alpha |-> ty1), (Type.beta |-> ty2)]) 797 and inr = 798 mk_const("sum", "INR",[(Type.alpha |-> ty1), (Type.beta |-> ty2)]) 799 in 800 map (curry mk_comb inl) inls1 @ map (curry mk_comb inr) inls2 801 end 802 in 803 fn ty => let 804 val bods = mk_inls ty 805 in 806 map (fn t => mk_abs(find_term is_var t,t)) bods 807 end 808 end 809 val mk_outls = let 810 fun mk_inls sof ty = 811 if is_vartype ty then [sof] 812 else let 813 val (ty1,ty2) = case dest_type ty 814 of (_,[ty1,ty2]) => (ty1,ty2) 815 | _ => raise Match 816 val outl = 817 mk_const("sum", "OUTL",[(Type.alpha |-> ty1), (Type.beta |-> ty2)]) 818 and outr = 819 mk_const("sum", "OUTR",[(Type.alpha |-> ty1), (Type.beta |-> ty2)]) 820 in 821 mk_inls (mk_comb(outl,sof)) ty1 @ mk_inls (mk_comb(outr,sof)) ty2 822 end 823 in 824 fn ty => let 825 val x = mk_var("x",ty) 826 in 827 map (curry mk_abs x) (mk_inls x ty) 828 end 829 end 830 fun mk_newfun fnn outl = let 831 val (s,ty) = dest_var fnn 832 val dty = hd(snd(dest_type ty)) 833 val x = mk_var("x",dty) 834 val (y,bod) = dest_abs outl 835 val r = mk_abs(x,subst[y |-> mk_comb(fnn,x)] bod) 836 val l = mk_var(s,type_of r) 837 val th1 = ASSUME (mk_eq(l,r)) 838 in 839 RIGHT_BETAS [x] th1 840 end 841in 842 fn th => let 843 val (avs,ebod) = strip_forall(concl th) 844 val (evs,bod) = strip_exists ebod 845 val n = length evs 846 in 847 if n = 1 then th 848 else let 849 val tys = 850 map (fn i => mk_vartype ("'Z"^Int.toString i)) (upto (n - 1)) 851 val sty = mk_sum tys 852 val inls = mk_inls sty 853 and outls = mk_outls sty 854 val zty = type_of(rand(snd(strip_forall(hd(conjuncts bod))))) 855 val ith = INST_TYPE [zty |-> sty] th 856 val (avs,ebod) = strip_forall(concl ith) 857 val (evs,bod) = strip_exists ebod 858 val fns' = map2 mk_newfun evs outls 859 val fnalist = zip evs (map (rator o lhs o concl) fns') 860 and inlalist = zip evs inls 861 and outlalist = zip evs outls 862 fun hack_clause tm = let 863 val (avs,bod) = strip_forall tm 864 val (l,r) = dest_eq bod 865 val (fnn,args) = strip_comb r 866 val pargs = map 867 (fn a => let 868 val g = genvar(type_of a) 869 in 870 if is_var a then (g,g) 871 else let 872 val outl = tmassoc (rator a) outlalist 873 in 874 (mk_comb(outl,g),g) 875 end 876 end) args 877 val (args',args'') = unzip pargs 878 val inl = tmassoc (rator l) inlalist 879 val rty = hd(snd(dest_type(type_of inl))) 880 val nty = itlist (curry op --> o type_of) args' rty 881 val fn' = mk_var(fst(dest_var fnn),nty) 882 val r' = list_mk_abs(args'',mk_comb(inl,list_mk_comb(fn',args'))) 883 in 884 (r',fnn) 885 end 886 val defs = map hack_clause (conjuncts bod) 887 val jth = BETA_RULE (SPECL (map fst defs) ith) 888 val bth = ASSUME (snd(strip_exists(concl jth))) 889 fun finish_clause th = let 890 val (avs,bod) = strip_forall (concl th) 891 val outl = tmassoc (rator (lhand bod)) outlalist 892 in 893 GENL avs (BETA_RULE (AP_TERM outl (SPECL avs th))) 894 end 895 val cth = end_itlist CONJ (map finish_clause (CONJUNCTS bth)) 896 val dth = ELIM_OUTCOMBS cth 897 val eth = GEN_REWRITE_RULE ONCE_DEPTH_CONV (map SYM fns') dth 898 val fth = itlist SIMPLE_EXISTS (map snd fnalist) eth 899 val dtms = map (hd o hyp) fns' 900 val gth = 901 itlist (fn e => fn th => let 902 val (l,r) = dest_eq e 903 in 904 MP (Thm.INST [l |-> r] (DISCH e th)) (REFL r) 905 end) dtms fth 906 val hth = PROVE_HYP jth (itlist SIMPLE_CHOOSE evs gth) 907 val xvs = 908 map (fst o strip_comb o rand o snd o strip_forall) 909 (conjuncts(concl eth)) 910 in 911 GENL xvs hth 912 end 913 end 914end; 915 916fun define_type_mutual def = let 917 val (ith,rth) = define_type_raw def 918in 919 (ith,generalize_recursion_theorem rth) 920end 921 922(* Test the above with: 923 924 val def = [(Type`:'foo`, [("C1", []), ("C2", [Type`:num`])])]; 925 define_type_mutual def; 926 927 val def = [(Type`:'bar`, [("D1", [Type`:num`]), ("D2", [Type`:'bar`])])]; 928 define_type_mutual def; 929 930 val def = [(Type`:'qux`, [("F1", []), ("F2", [Type`:'a`, Type`:'qux`])])]; 931 define_type_mutual def; 932 933 val def = [(Type`:'qwerty`, [("G1", [Type`:num`]), 934 ("G2", [Type`:'asdf`])]), 935 (Type`:'asdf`, [("H1", []), ("H2", [Type`:'qwerty`])])]; 936 define_type_mutual def; 937 938 (* HOL Light equivalent *) 939 let def = 940 let q = mk_vartype("qwerty") 941 and a = mk_vartype("asdf") in 942 [(q, [("G1", [`:num`]); ("G2", [a])]); (a, [("H1", []); ("H2", [q])])];; 943 define_type_mutual def;; 944 945*) 946 947 948(* ------------------------------------------------------------------------- *) 949(* Now deal with nested recursion. *) 950(* ------------------------------------------------------------------------- *) 951 952 953(* ------------------------------------------------------------------------- *) 954(* Convenient functions for manipulating types. *) 955(* ------------------------------------------------------------------------- *) 956 957val dest_fun_ty = Type.dom_rng 958 959fun occurs_in ty bigty = 960 bigty = ty orelse 961 (not (is_vartype bigty) andalso 962 exists (occurs_in ty) (snd(dest_type bigty))) 963 964(* ------------------------------------------------------------------------- *) 965(* Dispose of trivial antecedent. *) 966(* ------------------------------------------------------------------------- *) 967 968val TRIV_ANTE_RULE = let 969 fun TRIV_IMP_CONV tm = let 970 val (avs,bod) = strip_forall tm 971 val bth = 972 if is_eq bod then REFL (rand bod) 973 else let 974 val (ant,con) = dest_imp bod 975 val ith = SUBS_CONV (CONJUNCTS(ASSUME ant)) (lhs con) 976 in 977 DISCH ant ith 978 end 979 in 980 GENL avs bth 981 end 982in 983 fn th => let 984 val tm = concl th 985 in 986 if is_imp tm then let 987 val (ant,con) = dest_imp(concl th) 988 val cjs = conjuncts ant 989 val cths = map TRIV_IMP_CONV cjs 990 in 991 MP th (end_itlist CONJ cths) 992 end 993 else th 994 end 995end 996 997(* ------------------------------------------------------------------------- *) 998(* Lift type bijections to "arbitrary" (well, free rec or function) type. *) 999(* ------------------------------------------------------------------------- *) 1000 1001val CONJ_ACI_CONV = EQT_ELIM o AC_CONV (CONJ_ASSOC, CONJ_COMM); 1002val ISO_EXPAND_CONV = PURE_ONCE_REWRITE_CONV[ISO]; 1003 1004fun lift_type_bijections iths cty = 1005 let val itys = map (hd o snd o dest_type o type_of o lhand o concl) iths 1006 in assoc cty (zip itys iths) 1007 handle HOL_ERR _ => 1008 if not (List.exists (C occurs_in cty) itys) 1009 then Thm.INST_TYPE [Type.alpha |-> cty] ISO_REFL 1010 else let val (tycon,isotys) = dest_type cty 1011 in if tycon = "fun" 1012 then MATCH_MP ISO_FUN 1013 (end_itlist CONJ (map (lift_type_bijections iths) isotys)) 1014 else raise ERR "lift_type_bijections" 1015 ("Unexpected type operator \""^tycon^"\"") 1016 end 1017 end; 1018 1019(* ------------------------------------------------------------------------- *) 1020(* Prove isomorphism of nested types where former is the smaller. *) 1021(* ------------------------------------------------------------------------- *) 1022 1023val T_tm = boolSyntax.T 1024 1025val DE_EXISTENTIALIZE_RULE = let 1026 val pth = prove( 1027 ``$? P ==> (c:'a = $@ P) ==> P c``, 1028 CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV (GSYM ETA_AX)))) THEN 1029 DISCH_TAC THEN DISCH_THEN SUBST1_TAC THEN 1030 MATCH_MP_TAC SELECT_AX THEN POP_ASSUM ACCEPT_TAC) 1031 val USE_PTH = MATCH_MP pth 1032 fun DE_EXISTENTIALIZE_RULE th = 1033 if not (is_exists(concl th)) then ([],th) 1034 else let 1035 val th1 = USE_PTH th 1036 val v1 = rand(rand(concl th1)) 1037 val gv = genvar(type_of v1) 1038 val th2 = CONV_RULE BETA_CONV (UNDISCH (Thm.INST [v1 |-> gv] th1)) 1039 val (vs,th3) = DE_EXISTENTIALIZE_RULE th2 1040 in 1041 (gv::vs,th3) 1042 end 1043in 1044 DE_EXISTENTIALIZE_RULE 1045end; 1046 1047val grab_type = type_of o rand o lhand o snd o strip_forall;; 1048 1049fun clause_corresponds cl0 = 1050 let val (f0,ctm0) = dest_comb (lhs cl0) 1051 val c0 = fst(dest_const(fst(strip_comb ctm0))) 1052 val (dty0,rty0) = dest_fun_ty (type_of f0) 1053 in 1054 fn cl1 => 1055 let val (f1,ctm1) = dest_comb (lhs cl1) 1056 val c1 = fst(dest_const(fst(strip_comb ctm1))) 1057 val (dty1,rty1) = dest_fun_ty (type_of f1) 1058 in 1059 (c0 = c1) andalso (dty0 = rty1) andalso (rty0 = dty1) 1060 end 1061 end 1062 1063fun INSTANTIATE (tmsubst, tysubst) thm = INST tmsubst (INST_TYPE tysubst thm) 1064 1065fun find P l = 1066 case List.find P l 1067 of NONE => raise ERR "find" "No element satisfying predicate" 1068 | SOME x => x; 1069 1070fun pair2recd (M,v) = {redex=v, residue=M} 1071fun hol98_subst_of s = map pair2recd s; 1072 1073fun prove_inductive_types_isomorphic n k (ith0,rth0) (ith1,rth1) = let 1074 val sth0 = SPEC_ALL rth0 1075 and sth1 = SPEC_ALL rth1 1076 val (pevs0,pbod0) = strip_exists (concl sth0) 1077 and (pevs1,pbod1) = strip_exists (concl sth1) 1078 val (pcjs0,qcjs0) = chop_list k (conjuncts pbod0) 1079 and (pcjs1,qcjs1) = chop_list k (snd(chop_list n (conjuncts pbod1))) 1080 val tyal0 = hol98_subst_of 1081 (mk_set (zip (map grab_type pcjs1) (map grab_type pcjs0))) 1082 val tyal1 = map (fn {redex,residue} => {redex=residue,residue=redex}) tyal0 1083 val tyins0 = map (fn f => 1084 let val (domty,ranty) = dest_fun_ty (type_of f) 1085 in ranty |-> tysubst tyal0 domty 1086 end) pevs0 1087 and tyins1 = map (fn f => 1088 let val (domty,ranty) = dest_fun_ty (type_of f) 1089 in ranty |-> tysubst tyal1 domty 1090 end) pevs1 1091 val tth0 = Thm.INST_TYPE tyins0 sth0 1092 and tth1 = Thm.INST_TYPE tyins1 sth1 1093 val (evs0,bod0) = strip_exists(concl tth0) 1094 and (evs1,bod1) = strip_exists(concl tth1) 1095 val (lcjs0,rcjs0) = chop_list k (map (snd o strip_forall) (conjuncts bod0)) 1096 and (lcjs1,rcjsx) = chop_list k (map (snd o strip_forall) 1097 (snd(chop_list n (conjuncts bod1)))) 1098 val rcjs1 = map (fn t => find (clause_corresponds t) rcjsx) rcjs0 1099 fun proc_clause tm0 tm1 = let 1100 val (l0,r0) = dest_eq tm0 1101 and (l1,r1) = dest_eq tm1 1102 val (vc0,wargs0) = strip_comb r0 1103 val (con0,vargs0) = strip_comb(rand l0) 1104 val gargs0 = map (genvar o type_of) wargs0 1105 val nestf0 = 1106 map (fn a => can (find (fn t => is_comb t andalso aconv (rand t) a)) 1107 wargs0) 1108 vargs0 1109 val targs0 = 1110 map2 (fn a => fn f => 1111 if f then 1112 find (fn t => is_comb t andalso aconv (rand t) a) wargs0 1113 else a) 1114 vargs0 nestf0 1115 val gvlist0 = zip wargs0 gargs0 1116 val xargs = map (fn v => tmassoc v gvlist0) targs0 1117 val inst0 = 1118 (vc0 |-> 1119 list_mk_abs(gargs0,list_mk_comb(fst(strip_comb(rand l1)),xargs))) 1120 val (vc1,wargs1) = strip_comb r1 1121 val (con1,vargs1) = strip_comb(rand l1) 1122 val gargs1 = map (genvar o type_of) wargs1 1123 val targs1 = 1124 map2 (fn a => fn f => 1125 if f then find (fn t => is_comb t andalso aconv (rand t) a) wargs1 1126 else a) 1127 vargs1 nestf0 1128 val gvlist1 = zip wargs1 gargs1 1129 val xargs = map (fn v => tmassoc v gvlist1) targs1 1130 val inst1 = 1131 (vc1 |-> 1132 list_mk_abs(gargs1,list_mk_comb(fst(strip_comb(rand l0)),xargs))) 1133 in 1134 (inst0,inst1) 1135 end 1136 val (insts0,insts1) = unzip (map2 proc_clause (lcjs0@rcjs0) (lcjs1@rcjs1)) 1137 val uth0 = BETA_RULE(Thm.INST insts0 tth0) 1138 and uth1 = BETA_RULE(Thm.INST insts1 tth1) 1139 val (efvs0,sth0) = DE_EXISTENTIALIZE_RULE uth0 1140 and (efvs1,sth1) = DE_EXISTENTIALIZE_RULE uth1 1141 val efvs2 = 1142 map (fn t1 => find (fn t2 => 1143 hd(tl(snd(dest_type(type_of t1)))) = 1144 hd(snd(dest_type(type_of t2)))) 1145 efvs1) 1146 efvs0 1147 val isotms = map2 (fn ff => fn gg => 1148 list_mk_icomb ("ind_type", "ISO") [ff,gg]) 1149 efvs0 efvs2 1150 val ctm = list_mk_conj isotms 1151 val cth1 = ISO_EXPAND_CONV ctm 1152 val ctm1 = rand(concl cth1) 1153 val cjs = conjuncts ctm1 1154 val eee = map (fn n => n mod 2 = 0) (upto (length cjs - 1)) 1155 val (cjs1,cjs2) = partition fst (zip eee cjs) 1156 val ctm2 = mk_conj(list_mk_conj (map snd cjs1), 1157 list_mk_conj (map snd cjs2)) 1158 val cth2 = CONJ_ACI_CONV (mk_eq(ctm1,ctm2)) 1159 val cth3 = TRANS cth1 cth2 1160 val DETRIV_RULE = TRIV_ANTE_RULE o REWRITE_RULE[sth0, sth1] 1161 val jth0 = let 1162 val itha = SPEC_ALL ith0 1163 val icjs = conjuncts(rand(concl itha)) 1164 val cinsts = 1165 map (fn tm => 1166 tryfind (fn vtm => ho_match_term [] empty_tmset vtm tm) icjs) 1167 (conjuncts (rand ctm2)) 1168 val tvs = op_set_diff aconv 1169 (fst(strip_forall(concl ith0))) 1170 (itlist (fn (x,_) => tunion (map #redex x)) cinsts []) 1171 val ctvs = 1172 map (fn p => let val x = mk_var("x",hd(snd(dest_type(type_of p)))) 1173 in (p |-> mk_abs(x,T_tm)) end) tvs 1174 in 1175 DETRIV_RULE (BETA_RULE (Thm.INST ctvs (itlist INSTANTIATE cinsts itha))) 1176 end 1177 and jth1 = let 1178 val itha = SPEC_ALL ith1 1179 val icjs = conjuncts(rand(concl itha)) 1180 val cinsts = map (fn tm => tryfind 1181 (fn vtm => ho_match_term [] empty_tmset vtm tm) icjs) 1182 (conjuncts (lhand ctm2)) 1183 val tvs = 1184 op_set_diff aconv (fst(strip_forall(concl ith1))) 1185 (itlist (fn (x,_) => tunion (map #redex x)) cinsts []) 1186 val ctvs = 1187 map (fn p => let val x = mk_var("x",hd(snd(dest_type(type_of p)))) in 1188 (p |-> mk_abs(x,T_tm)) end) tvs 1189 in 1190 DETRIV_RULE (BETA_RULE (Thm.INST ctvs (itlist INSTANTIATE cinsts itha))) 1191 end 1192 val cths4 = map2 CONJ (CONJUNCTS jth0) (CONJUNCTS jth1) 1193 val cths5 = map (PURE_ONCE_REWRITE_RULE[GSYM ISO]) cths4 1194 val cth6 = end_itlist CONJ cths5 1195in 1196 (cth6,CONJ sth0 sth1) 1197end; 1198 1199(* ------------------------------------------------------------------------- *) 1200(* Define nested type by doing a 1-level unwinding. *) 1201(* ------------------------------------------------------------------------- *) 1202 1203fun SCRUB_ASSUMPTION th = 1204 let val hyps = hyp th 1205 val eqn = find (fn t => 1206 let val x = lhs t 1207 in List.all (fn u => not (free_in x (rand u))) hyps 1208 end) hyps 1209 val (l,r) = dest_eq eqn 1210 in 1211 MP (Thm.INST [l |-> r] (DISCH eqn th)) (REFL r) 1212 end 1213 1214 1215fun define_type_basecase def = 1216 let fun add_id s = fst(dest_var(safeid_genvar Type.bool)) 1217 val def' = map (I ## (map (add_id ## I))) def 1218 in define_type_mutual def' 1219 end 1220 1221val SIMPLE_BETA_RULE = GSYM o SIMP_RULE bool_ss [FUN_EQ_THM]; 1222val ISO_USAGE_RULE = MATCH_MP ISO_USAGE; 1223val SIMPLE_ISO_EXPAND_RULE = CONV_RULE(REWR_CONV ISO); 1224 1225fun REWRITE_FUN_EQ_RULE thl = SIMP_RULE bool_ss (FUN_EQ_THM::thl) 1226 1227fun get_nestedty_info tyname = 1228 let fun hol98_to_jrh_ind ind0 = 1229 let fun CONJUNCTS_CONV c tm = 1230 if is_conj tm then BINOP_CONV (CONJUNCTS_CONV c) tm else c tm 1231 in 1232 CONV_RULE (STRIP_QUANT_CONV 1233 (RATOR_CONV (RAND_CONV 1234 (CONJUNCTS_CONV 1235 (REDEPTH_CONV RIGHT_IMP_FORALL_CONV))))) ind0 1236 end 1237 open TypeBasePure 1238 in 1239 case TypeBase.read tyname 1240 of SOME tyinfo => SOME (length (constructors_of tyinfo), 1241 hol98_to_jrh_ind (induction_of tyinfo), 1242 axiom_of tyinfo) 1243 | NONE => NONE 1244 end 1245 1246 1247 1248(*--------------------------------------------------------------------------- 1249 JRH's package returns the list type's induction theorem as: 1250 !P. P [] /\ (!h t. P t ==> P (h::t)) ==> !l. P l 1251 hol90 tradition is to have induction theorems where the universal 1252 variables in the hypotheses are pushed as far to the right as possible, so 1253 that the above appears as: 1254 !P. P [] /\ (!t. P t ==> !h. P (h::t)) ==> !l. P l 1255 A small difference you might think, but it causes the venerable 1256 INDUCT_THEN code to cark, and who am I to fiddle with INDUCT_THEN? 1257 And haven't I already introduced enough gratuitous incompatibilities? 1258 So, push_in_vars below performs this conversion. 1259 1260 Further, the old induction theorems automatically proved by 1261 prove_induction_thm picked names for bound variables that were appropriate 1262 for the type (the first letter of the type, basically). So, rename_bvars 1263 below does this too. 1264 1265 Finally, munge_ind_thm composes the two functions. 1266 ---------------------------------------------------------------------------*) 1267 1268local 1269 fun CONJUNCTS_CONV c tm = 1270 if is_conj tm then BINOP_CONV (CONJUNCTS_CONV c) tm else c tm 1271 fun SWAP_TILL_BOTTOM_THEN c t = 1272 ((SWAP_VARS_CONV THENC BINDER_CONV (SWAP_TILL_BOTTOM_THEN c)) ORELSEC c) t 1273 fun app_letter ty = 1274 if is_vartype ty then String.sub(dest_vartype ty, 1) 1275 else let 1276 val {Thy,Tyop=outerop,Args} = dest_thy_type ty 1277 in 1278 if Thy = "list" andalso outerop = "list" then 1279 case Lib.total dest_thy_type (hd Args) of 1280 SOME {Thy,Tyop,...} => 1281 if Thy = "string" andalso Tyop = "char" then #"s" 1282 else String.sub(outerop, 0) 1283 | NONE => #"l" 1284 else String.sub(outerop,0) 1285 end 1286 fun new_name ctxt ty = let 1287 fun nvary ctxt nm n = let 1288 val fullname = nm ^ Int.toString n 1289 in 1290 if Lib.mem fullname ctxt then nvary ctxt nm (n + 1) else fullname 1291 end 1292 val name = str (app_letter ty) 1293 in 1294 if Lib.mem name ctxt then nvary ctxt name 0 else name 1295 end 1296in 1297 fun push_in_vars thm = let 1298 fun each_conj tm = 1299 if is_forall tm then let 1300 val (vs, body) = strip_forall tm 1301 in 1302 if is_imp body then let 1303 val (ant,con) = Psyntax.dest_imp body 1304 in 1305 if tmem (hd vs) (free_vars ant) then 1306 BINDER_CONV each_conj tm 1307 else 1308 (SWAP_TILL_BOTTOM_THEN FORALL_IMP_CONV THENC each_conj) tm 1309 end 1310 else REFL tm 1311 end 1312 else REFL tm 1313 val c = 1314 STRIP_QUANT_CONV (RATOR_CONV (RAND_CONV (CONJUNCTS_CONV each_conj))) 1315 in 1316 CONV_RULE c thm 1317 end 1318 1319 fun rename_bvars thm = let 1320 fun renCONV ctxt tm = 1321 if is_forall tm orelse is_exists tm then let 1322 val dest = if is_forall tm then dest_forall else dest_exists 1323 val (Bvar, Body) = dest tm 1324 val vname = new_name ctxt (type_of Bvar) 1325 in 1326 (RENAME_VARS_CONV [vname] THENC 1327 BINDER_CONV (renCONV (vname::ctxt))) tm 1328 end 1329 else if is_abs tm then ABS_CONV (renCONV ctxt) tm 1330 else if is_comb tm then (RATOR_CONV (renCONV ctxt) THENC 1331 RAND_CONV (renCONV ctxt)) tm 1332 else REFL tm 1333 val Pvars = map (#1 o dest_var) (#1 (strip_forall (concl thm))) 1334 in 1335 CONV_RULE (STRIP_QUANT_CONV (renCONV Pvars)) thm 1336 end 1337 1338 val munge_ind_thm = rename_bvars o push_in_vars 1339 1340end 1341 1342fun canonicalise_tyvars def thm = let 1343 val thm_tyvars = Term.type_vars_in_term (concl thm) 1344 val utys = Lib.U (itlist (union o map snd o snd) def []) 1345 val def_tyvars = Type.type_varsl utys 1346 fun gen_canonicals tyvs avoids = 1347 case tyvs of 1348 [] => [] 1349 | (tyv::tyvs) => let 1350 val newtyname = Lexis.gen_variant Lexis.tyvar_vary avoids "'a" 1351 in 1352 (tyv |-> mk_vartype newtyname) :: 1353 gen_canonicals tyvs (newtyname :: avoids) 1354 end 1355 val names_to_avoid = map dest_vartype def_tyvars 1356in 1357 Thm.INST_TYPE 1358 (gen_canonicals (Lib.set_diff thm_tyvars def_tyvars) names_to_avoid) 1359 thm 1360end 1361 1362local 1363 fun is_nested vs ty = 1364 not (is_vartype ty) andalso not (intersect (type_vars ty) vs = []) 1365 fun modify_type theta ty = 1366 case subst_assoc (equal ty) theta 1367 of SOME x => x 1368 | NONE => (let val {Tyop,Thy,Args} = dest_thy_type ty 1369 in mk_thy_type{Tyop=Tyop,Thy=Thy, 1370 Args=map (modify_type theta) Args} 1371 end handle HOL_ERR _ => ty) 1372 1373 fun modify_item alist (s,l) = (s,map (modify_type alist) l) 1374 fun modify_clause alist (l,lis) = (l,map (modify_item alist) lis) 1375 fun recover_clause id tm = 1376 let val (con,args) = strip_comb tm 1377 in (fst(dest_const con)^id, map type_of args) 1378 end 1379 1380 (* ------------------------------------------------------------------------- 1381 Returns a substitution that will map elements of check_these to 1382 things not in check_these or avoids0. Won't map an element of 1383 check_these away unless it is in avoids0. 1384 -------------------------------------------------------------------------- *) 1385 1386 fun mk_thm_avoid check_these avoids0 = let 1387 fun recurse [] avoids = [] 1388 | recurse (tyv1::tyvs) avoids = 1389 if Lib.mem tyv1 avoids 1390 then let val newtyv = 1391 Lexis.gen_variant Lexis.tyvar_vary (check_these@avoids) "'a" 1392 in (mk_vartype tyv1 |-> mk_vartype newtyv) 1393 :: recurse tyvs (newtyv::avoids) 1394 end 1395 else recurse tyvs avoids 1396 in 1397 recurse check_these avoids0 1398 end 1399 1400 fun create_auxiliary_clauses nty avoids = let 1401 val id = fst(dest_var(safeid_genvar Type.bool)) 1402 val {Thy,Tyop=tycon,Args=tyargs} = dest_thy_type nty 1403 val (k,ith0,rth0) = 1404 valOf (get_nestedty_info {Thy = Thy, Tyop = tycon}) 1405 handle Option.Option => 1406 raise ERR "define_type_nested" 1407 ("Can't find definition for nested type: "^ tycon) 1408 val rth0_tvs = map dest_vartype (Term.type_vars_in_term (concl rth0)) 1409 val avoid_tyal = mk_thm_avoid rth0_tvs avoids 1410 val rth = Thm.INST_TYPE avoid_tyal rth0 1411 val ith = Thm.INST_TYPE avoid_tyal ith0 1412 1413 val (evs,bod) = strip_exists(snd(strip_forall(concl rth))) 1414 val cjs = map (lhand o snd o strip_forall) (conjuncts bod) 1415 val rtys = map (hd o snd o dest_type o type_of) evs 1416 val tyins = tryfind (fn vty => Type.match_type vty nty) rtys 1417 val cjs' = map (Term.inst tyins o rand) (fst(chop_list k cjs)) 1418 val mtys = itlist (insert o type_of) cjs' [] 1419 val pcons = map (fn ty => filter (fn t => type_of t = ty) cjs') mtys 1420 val cls' = zip mtys (map (map (recover_clause id)) pcons) 1421 val tyal = map (fn ty => ty |-> mk_vartype("'"^id^fst(dest_type ty))) mtys 1422 val cls'' = map (modify_type tyal ## map (modify_item tyal)) cls' 1423 in 1424 (k,tyal,cls'',Thm.INST_TYPE tyins ith, Thm.INST_TYPE tyins rth) 1425 end 1426 1427 fun define_type_nested def = let 1428 val n = length(itlist (curry op@) (map (map fst o snd) def) []) 1429 val newtys = map fst def 1430 val utys = Lib.U (itlist (union o map snd o snd) def []) 1431 val utyvars = type_varsl utys 1432 val rectys = filter (is_nested newtys) utys 1433 in 1434 if rectys = [] then let 1435 val (th1,th2) = define_type_basecase def 1436 in 1437 (n,th1,th2) 1438 end 1439 else let 1440 val nty = hd (Listsort.sort (flip_cmp (measure_cmp type_size)) rectys) 1441 val (k,tyal,ncls,ith,rth) = 1442 create_auxiliary_clauses nty (map dest_vartype utyvars) 1443 val cls = map (modify_clause tyal) def @ ncls 1444 val (_,ith1,rth1) = define_type_nested cls 1445 val xnewtys = map (hd o snd o dest_type o type_of) 1446 (fst(strip_exists(snd(strip_forall(concl rth1))))) 1447 val xtyal = let 1448 fun mapthis ty = let 1449 val s = dest_vartype ty 1450 in 1451 (ty |-> find(fn t => "'"^fst(dest_type t) = s) xnewtys) 1452 end 1453 in 1454 map (mapthis o fst) cls 1455 end 1456 val ith0 = Thm.INST_TYPE xtyal ith 1457 and rth0 = Thm.INST_TYPE xtyal rth 1458 val (isoth,rclauses) = 1459 prove_inductive_types_isomorphic n k (ith0,rth0) (ith1,rth1) 1460 val irth3 = CONJ ith1 rth1 1461 val vtylist = itlist (insert o type_of) (variables(concl irth3)) [] 1462 val isoths = CONJUNCTS isoth 1463 val isotys = 1464 map (hd o snd o dest_type o type_of o lhand o concl) isoths 1465 val ctylist = 1466 filter 1467 (fn ty => List.exists (fn t => occurs_in t ty) isotys) 1468 vtylist 1469 val atylist = itlist (union o striplist dest_fun_ty) ctylist [] 1470 val isoths' = map (lift_type_bijections isoths) 1471 (filter (fn ty => List.exists 1472 (fn t => occurs_in t ty) 1473 isotys) 1474 atylist) 1475 val cisoths = 1476 map (BETA_RULE o lift_type_bijections isoths') ctylist 1477 val uisoths = map ISO_USAGE_RULE cisoths 1478 val visoths = map (ASSUME o concl) uisoths 1479 val irth4 = 1480 itlist PROVE_HYP uisoths (REWRITE_FUN_EQ_RULE visoths irth3) 1481 val irth5 = REWRITE_RULE 1482 (rclauses :: map SIMPLE_ISO_EXPAND_RULE isoths') irth4 1483 val irth6 = repeat SCRUB_ASSUMPTION irth5 1484 val ncjs = 1485 filter (fn t => List.exists (not o is_var) 1486 (snd(strip_comb(rand(lhs(snd(strip_forall t))))))) 1487 (conjuncts(snd(strip_exists 1488 (snd(strip_forall(rand(concl irth6))))))) 1489 val id = fst(dest_var(genvar Type.bool)) 1490 fun mk_newcon tm = let 1491 val (vs,bod) = strip_forall tm 1492 val rdeb = rand(lhs bod) 1493 val rdef = list_mk_abs(vs,rdeb) 1494 val newname = fst(dest_var(safeid_genvar Type.bool)) 1495 val def = mk_eq(mk_var(newname,type_of rdef),rdef) 1496 val dth = new_definition (newname, def) 1497 in 1498 SIMPLE_BETA_RULE dth 1499 end 1500 val dths = map mk_newcon ncjs 1501 val (ith6,rth6) = CONJ_PAIR(PURE_REWRITE_RULE dths irth6) 1502 in 1503 (n,ith6,rth6) 1504 end 1505 end 1506 1507 fun remove_intermediate_junk () = let 1508 val cs = Theory.constants (current_theory()) 1509 fun c_appthis c = let 1510 val {Name, Thy, ...} = dest_thy_const c 1511 in 1512 if String.isSubstring safepfx Name then 1513 (Parse.temp_remove_ovl_mapping Name {Name = Name, Thy = Thy}; 1514 Theory.delete_const Name) 1515 else () 1516 end 1517 1518 val tys = Theory.types (current_theory()) 1519 fun ty_appthis (tyn,arity) = 1520 if String.isSubstring safepfx tyn then Theory.delete_type tyn 1521 else () 1522 in 1523 List.app c_appthis cs; 1524 List.app ty_appthis tys 1525 end 1526in 1527val define_type_nested = fn def => 1528 let val newtys = map fst def 1529 val truecons = itlist (curry op@) (map (map fst o snd) def) [] 1530 val defnested = define_type_nested 1531 |> trace ("Vartype Format Complaint", 0) 1532 |> with_flag (Globals.checking_type_names, false) 1533 |> with_flag (Globals.checking_const_names, false) 1534 val (p,ith0,rth0) = defnested def 1535 val (avs,etm) = strip_forall(concl rth0) 1536 val allcls = conjuncts(snd(strip_exists etm)) 1537 val relcls = fst(chop_list (length truecons) allcls) 1538 val gencons = map(repeat rator o rand o lhand o snd o strip_forall) relcls 1539 val cdefs = 1540 map2 (fn s => fn r => 1541 SYM(new_definition (temp_binding s, 1542 mk_eq(mk_var(s,type_of r),r)))) 1543 truecons 1544 gencons 1545 val tavs = make_args "f" [] (map type_of avs) 1546 val ith1 = SUBS cdefs ith0 1547 and rth1 = GENL tavs (SUBS cdefs (SPECL tavs rth0)) 1548 val retval = (p,ith1,rth1) 1549 in 1550 {induction = munge_ind_thm ith1, 1551 recursion = canonicalise_tyvars def rth1} before 1552 remove_intermediate_junk() 1553 end 1554end; 1555 1556fun define_type d = 1557 define_type_nested d 1558 handle e => raise (wrap_exn "ind_types" "define_type" e); 1559 1560(* test this with: 1561 1562 val def = [(Type`:'foo`, [("C1", []), ("C2", [Type`:num`])])]; 1563 (* HOL Light equivalent: 1564 let def = 1565 let foo = mk_vartype "foo" in 1566 [(foo, [("C1", []); ("C2", [`:num`])])];; 1567 *) 1568 1569 define_type_nested def; 1570 1571 val def = [(Type`:'bar`, [("D1", [Type`:num`]), ("D2", [Type`:'bar`])])]; 1572 define_type_nested def; 1573 1574 val def = [(Type`:'qux`, [("F1", []), ("##", [Type`:'qux option`])])]; 1575 (* HOL Light equivalent : 1576 let def = 1577 let qux = mk_vartype "qux" in 1578 [(qux, [("F1", []); ("F2", [mk_type("option", [qux])])])];; *) 1579 define_type_nested def; 1580 1581 val def = [(Type`:'bozz`, [("G1", [Type`:num`, Type`:'fozz`])]), 1582 (Type`:'fozz`, [("G2", [Type`:'bozz option`]), 1583 ("G3", [Type`:num + 'fozz`])])] 1584 (* HOL Light equivalent : 1585 let def = 1586 let bozz = mk_vartype "bozz" 1587 and fozz = mk_vartype "fozz" in 1588 [(bozz, [("G1", [`:num`; fozz])]); 1589 (fozz, [("G2", [mk_type("option", [bozz])]); 1590 ("G3", [mk_type("sum", [`:num`; fozz])])])];; 1591 let (bozz_ind, bozz_rec) = define_type_nested def;; 1592 *) 1593 1594 val (bozz_ind, bozz_rec) = define_type_nested def; 1595 1596*) 1597 1598end; 1599