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