1(* =====================================================================*) 2(* FILE : mut_rec_ty.sml *) 3(* DESCRIPTION : functor for defining mutually recursive types. *) 4(* *) 5(* AUTHOR : Elsa Gunter and Myra VanInwegen, based on comments *) 6(* by Tom Melham *) 7(* DATE : 92.08.08 *) 8(* *) 9(* MODIFIED : 93.12.28 Fixed to handle polymorphism. ELG. *) 10(* *) 11(* =====================================================================*) 12 13(* Copyright 1992, 1993 by AT&T Bell Laboratories *) 14(* Share and Enjoy *) 15 16structure MutRecDef :> MutRecDef = 17struct 18 19open MutRecMask; 20nonfix quot ; 21nonfix rem; 22val quot = Int.quot 23val rem = Int.rem; 24infix 7 quot rem; 25 26open HolKernel Parse basicHol90Lib TypeInfo; 27 28type thm = Thm.thm 29 30val ambient_grammars = Parse.current_grammars(); 31val _ = Parse.temp_set_grammars boolTheory.bool_grammars; 32 33fun MUT_REC_ERR {function,message} = HOL_ERR{origin_structure = "MutRecDef", 34 origin_function = function, 35 message = message} 36 37(* Some general functions and values we need *) 38 39val num = Type`:num` 40val bool = Type.bool 41fun mk_fun{Range,Domain} = mk_type{Tyop="fun",Args=[Domain,Range]} 42fun dest_fun ty = 43 (case dest_type ty 44 of {Tyop = "fun", Args = [Domain,Range]} 45 => {Domain = Domain, Range = Range} 46 | _ => raise MUT_REC_ERR {function = "dest_fun", 47 message = "Not a function type"}) 48fun mk_prod{Fst,Snd} = mk_type{Tyop="prod",Args=[Fst,Snd]} 49fun dest_prod ty = 50 (case dest_type ty 51 of {Tyop = "prod", Args = [Fst,Snd]} 52 => {Fst = Fst, Snd = Snd} 53 | _ => raise MUT_REC_ERR {function = "dest_prod", 54 message = "Not a product type"}) 55fun mk_sum{Inl,Inr} = mk_type{Tyop="sum",Args=[Inl,Inr]} 56fun dest_sum ty = 57 (case dest_type ty 58 of {Tyop = "sum",Args = [Inl,Inr]} 59 => {Inl = Inl, Inr = Inr} 60 | _ => raise MUT_REC_ERR{function = "dest_sum", 61 message = "Not a sum type"}) 62 63 64(* mk_const {Name = int_to_string n, Ty = num} *) 65fun mk_hol_num n = Term.mk_numeral(Arbnum.fromInt n); 66 67fun find test [] = NONE 68 | find test (x::xs) = if test x then SOME x else find test xs 69 70 71(* 72 is_closed determines whether there is a witness for each type in the 73 arg_info for a constructor. 74*) 75fun is_closed {constructor_arg_info = [], ...} = true 76 | is_closed {constructor_arg_info = (existing ty) :: rest, witnesses} = 77 is_closed {constructor_arg_info = rest, witnesses = witnesses} 78 | is_closed {constructor_arg_info = (being_defined tyname) :: rest, 79 witnesses} = 80 if exists 81 (fn {type_name, witness = {name,arg_info}} => type_name = tyname) 82 witnesses 83 then is_closed {constructor_arg_info = rest, witnesses = witnesses} 84 else false 85 86 87(* 88 find_witnesses repeatedly searches through all the types and all their 89 constructors to find the information necessary to prove the existence 90 theorems for all of the types being defined 91*) 92 93(* 94 Base Case: We have found witnesses for all the types being constructed 95*) 96fun find_witnesses {seen_new_witness_this_pass, 97 types_to_be_looked_at = [], 98 no_witness_this_pass = [], 99 witnesses} = witnesses 100 101(* 102 Next Pass Case: We are done with a pass through the types. If any new 103 witnesses were found then we need to start a new pass looking at all the 104 types that still don't have witnesses. Otherwise, we need to abort. 105*) 106 | find_witnesses {seen_new_witness_this_pass, 107 types_to_be_looked_at = [], 108 no_witness_this_pass, 109 witnesses} = 110 if seen_new_witness_this_pass 111 then find_witnesses 112 {seen_new_witness_this_pass = false, 113 types_to_be_looked_at = no_witness_this_pass, 114 no_witness_this_pass = [], 115 witnesses = witnesses} 116 else Raise (MUT_REC_ERR {function = "find_witnesses", 117 message = "Not all the types are non-empty."}) 118 119(* 120 General Case: We need to try to find a witness for a type being defined. 121 We need to ask of each of it's constructors, whether there are witnesses 122 for each of its argument types (i.e. is th constructor closed in the current 123 world). If we find such a constructor, it is a witness, and so we put it 124 with the type being defined into the witnesses, and set the flag 125 seen_new_witness_this_pass to true. If none of the constructors are closed 126 yet, we move that type over to no_witness_this_pass, and contintinue with 127 the rest of types_to_be_looked_at, leaving seen_new_witness_this_pass alone. 128*) 129 | find_witnesses {seen_new_witness_this_pass, 130 types_to_be_looked_at = 131 (ty as {type_name, constructors}) :: types, 132 no_witness_this_pass, 133 witnesses} = 134 let 135 val witness = find 136 (fn {name,arg_info} => 137 is_closed {constructor_arg_info = arg_info, 138 witnesses = witnesses}) 139 constructors 140 in 141 case witness 142 of NONE => 143 find_witnesses {seen_new_witness_this_pass = 144 seen_new_witness_this_pass, 145 types_to_be_looked_at = types, 146 no_witness_this_pass = 147 ty :: no_witness_this_pass, 148 witnesses = witnesses} 149 | SOME constr => 150 find_witnesses {seen_new_witness_this_pass = true, 151 types_to_be_looked_at = types, 152 no_witness_this_pass = no_witness_this_pass, 153 witnesses = 154 {type_name = type_name,witness = constr} :: 155 witnesses} 156 end; 157 158fun change_arg (existing ty) = SOME ty 159 | change_arg (being_defined _) = NONE 160fun change_entry {name,arg_info} = {constructor = "JOINT_"^name, 161 args = map change_arg arg_info, 162 fixity = Prefix}; 163 164fun type_num_aux name num_types_seen [] = 165 raise MUT_REC_ERR{function="type_num", 166 message = "name not in type_names"} 167 | type_num_aux name num_types_seen (n::ns) = 168 if name = n then num_types_seen 169 else type_num_aux name (num_types_seen + 1) ns; 170 171 172(* Big definition *) 173fun define_type mut_rec_ty_spec = 174let 175(* type_names is the list of names of types being defined *) 176val type_names = map (#type_name) mut_rec_ty_spec 177 178(* 179 The first thing we need to do is to establish that every type that will 180 eventually be defined will be non-empty, and to construct the information 181 necessary to construct the witnesses to this, after the representing type 182 has been built. 183*) 184 185 186(* 187 existence_witnesses is a list of the type names together with a descrition 188 of a constructor for that type. The list is given the order in which the 189 existence theorems for the mutually recursive types should be proved. The 190 constructor description given with the type name is tthe information 191 sufficient for proving the existence theorem for the type, assuming that 192 all the existence theorems for the earlier types have already been proven. 193*) 194val existence_witnesses = 195 rev (find_witnesses {seen_new_witness_this_pass = false, 196 types_to_be_looked_at = mut_rec_ty_spec, 197 no_witness_this_pass = [], 198 witnesses = []}) 199 200 201 202 203(* First we'll define a type that is a combinition of all types being 204 defined, and use this as a base for defining other types. The name of 205 this combinition type (the joint_name) is the concatenation (separated 206 by _) of all the type names being defined, preceded by "joint_ty" *) 207val joint_name = rev_itlist 208 (fn tyname => fn str => str ^ "_" ^ tyname) 209 type_names 210 "joint_ty" 211 212(* To make a specification for this combo type, we take all the constructors 213 for the individual types, add "JOINT_" to the front, and replace the 214 being_defined args of the constructors with our joint type. 215*) 216val big_simple_spec = 217 itlist (fn {constructors,...} => fn part_result => 218 (itlist (fn elt => fn lst => (change_entry elt)::lst) 219 constructors part_result)) 220 mut_rec_ty_spec 221 []; 222 223val JointTypeAxiom = Define_type.dtype 224 {save_name = joint_name^"_Axiom", 225 ty_name = joint_name, 226 clauses = big_simple_spec} 227 228 229val joint_type = 230 #Domain (dest_fun (type_of (#Bvar (dest_abs (rand (snd (strip_forall 231 (concl JointTypeAxiom)))))))) 232 233val type_arg_vars = type_vars joint_type; 234 235(* Our next goal is to define a function (called joint_name^"_select", 236 I'll refer to it as the joint select function) that, given an item in 237 the joint type, will return a number indicating which type (if any) it 238 would be if the constructors used to make it had the JOINT_ removed. 239 It will return 1 for the first element in type_names, 2 for the 240 second, etc, and 0 if the term would not be a well-formed term at all. 241 We make it by defining the functions f0, f1, e0, e1, ... (the functions 242 and constants, one for each constructor of the joint type, that compute 243 return values for the joint select function; I'll refer to them 244 as the return functions) in the JointTypeAxiom. *) 245 246 247(* 248 type_num looks up the number associated with a given type 249*) 250 251fun type_num name = type_num_aux name 1 type_names 252 253 254(* 255 In order to be able to use JointTypeAxiom, we are going to need values to 256 which to specialize the values making up the case statements (i.e. the 257 e0, f1, f2, ...). Each of these functions corresponds to a constructor. 258 It takes as arguments first all of the recursive values (ie the values 259 gotten by recursively applying the function being defined) for each each of 260 recursive types in the arguments to the constructor, next the constructor 261 arguments of non-recursive type, and last the constructor arguments of 262 recursive type. 263*) 264 265(* get_var_info is used to create the variables (and numbers) we will 266 need to create the return functions for our joint select function. 267 The recN vars returned are the vars representing the return values of 268 the recursive calls to the joint select function, the number terms will 269 be the values these recursive calls should return for the item to be a 270 legitimate member of a particular type, and the xN vars are the vars 271 representing the arguments to the constructor the return function 272 is for. We build up the being_defined & existing constructor arg lists 273 separately since the return functions take the existing args before 274 the ones being defined *) 275 276(* 277 Base Case: We are through looking at the constructor arguments. Return the 278 information for making the type checks (equations of the form f xi = ni) 279 to guarantee that the term is well-formed, and return the variables to 280 be abstracted. 281*) 282fun get_var_info {arg_info =[], 283 type_case_num, 284 var_num, 285 recvar_eq_num_list, 286 being_defined_args, 287 existing_args} = 288 {recvar_eq_num_list = rev recvar_eq_num_list, 289 plain_then_rec_var_type_info = 290 rev (being_defined_args@existing_args)} 291 292(* 293 Case: We are looking at an argument of existing type. We need to generate 294 a variable of the existing type from var_num and add it to the 295 existing_args. 296*) 297 | get_var_info {arg_info = (existing ty)::arg_info, 298 type_case_num, 299 var_num, 300 recvar_eq_num_list, 301 being_defined_args, 302 existing_args} = 303 get_var_info {arg_info = arg_info, 304 type_case_num = type_case_num, 305 var_num = var_num + 1, 306 recvar_eq_num_list = recvar_eq_num_list, 307 being_defined_args = being_defined_args, 308 existing_args = 309 (mk_var {Name = "x"^(int_to_string var_num), 310 Ty = ty})::existing_args} 311 312(* 313 Case: We are looking at an argument of a type being defined. We need to 314 generate a variable of type num and record the information for the equation 315 that gives well-formedness. We also need to generate a variable of the 316 joint type from var_num and add it to the being_defined_args. 317*) 318 | get_var_info {arg_info = (being_defined str)::arg_info, 319 type_case_num, 320 var_num, 321 recvar_eq_num_list, 322 being_defined_args, 323 existing_args} = 324 let val recvar = mk_var {Name = "rec"^(int_to_string type_case_num), 325 Ty = num} 326 val rec_num_term = mk_hol_num (type_num str) 327 in 328 get_var_info {arg_info = arg_info, 329 type_case_num = type_case_num + 1, 330 var_num = var_num + 1, 331 recvar_eq_num_list = 332 {lhs = recvar, rhs = rec_num_term}:: 333 recvar_eq_num_list, 334 being_defined_args = 335 (mk_var {Name = "x"^(int_to_string var_num), 336 Ty = joint_type})::being_defined_args, 337 existing_args = existing_args} 338 end 339 340 341 (* if constructor has no args, the return "function" is just a constant *) 342fun make_return_ftn {name, arg_info = []} type_num = mk_hol_num type_num 343 344 (* if the constructor has args, get variables (and numbers) to 345 correspond to return values of recursive calls and variables 346 to correspond to arguments of the constructor *) 347 | make_return_ftn {name, arg_info} type_num = 348 let val {recvar_eq_num_list, plain_then_rec_var_type_info} = 349 get_var_info {arg_info = arg_info, 350 type_case_num = 1, 351 var_num = 1, 352 recvar_eq_num_list = [], 353 being_defined_args = [], 354 existing_args = []} 355 val body = 356 (* if all the args are existing types, then the body of 357 our return function will be just a constant giving the 358 type; otherwise we need to test that the return values 359 of the recursive calls are what we expect *) 360 if recvar_eq_num_list = nil then 361 mk_hol_num type_num 362 else 363 mk_cond {cond = list_mk_conj (map mk_eq recvar_eq_num_list), 364 larm = mk_hol_num type_num, 365 rarm = mk_hol_num 0} 366 in 367 list_mk_abs (map (#lhs) recvar_eq_num_list, 368 list_mk_abs (plain_then_rec_var_type_info, body)) 369 end 370 371fun make_return_ftns ({type_name, constructors}::spec) n = 372 (map (fn c => make_return_ftn c n) constructors)@ 373 make_return_ftns spec (n + 1) 374 | make_return_ftns [] n = [] 375 376 377(* fn_lemma says there exists a unique function satisfying the 378 desired properties of our joint selection function *) 379val fn_lemma = 380 CONV_RULE (DEPTH_CONV BETA_CONV) 381 (ISPECL (make_return_ftns mut_rec_ty_spec 1) JointTypeAxiom) 382 383(* we want to make a name, joint_name ^ "_select", for the fn in fn_lemma *) 384val joint_select_name = joint_name ^ "_select" 385 386(* define our joint_select function *) 387val joint_select_def = 388 new_specification {name = joint_name ^ "_select_DEF", 389 consts = [{fixity = Prefix, 390 const_name = joint_select_name}], 391 sat_thm = EXISTENCE fn_lemma} 392 393 394(* make a constant for our joint select function *) 395val joint_select = mk_const {Name = joint_select_name, 396 Ty = mk_fun {Domain = joint_type, 397 Range = num}} 398 399(* 400 Next we make the predicates for representing the types to be defined, 401 prove the existence theorems for those predicates, define the types, 402 and define the REP and ABS functions. 403*) 404val Joint_x = mk_var {Name = "x", Ty = joint_type} 405 406fun joint_select_x ty_name = 407 {Bvar = Joint_x, 408 Body = mk_eq {lhs = mk_comb {Rator = joint_select, Rand = Joint_x}, 409 rhs = mk_hol_num (type_num ty_name)}} 410 411fun mk_joint_arg_ty_and_arg (existing ty) = 412 {ty = ty, 413 arg = mk_select{Bvar = mk_var{Name = "x", Ty = ty}, 414 Body = mk_const{Name = "T", Ty = bool}}} 415 | mk_joint_arg_ty_and_arg (being_defined ty_name) = 416 {ty = joint_type, 417 arg = mk_select (joint_select_x ty_name)} 418 419fun prove_exists 420 {type_name, witness = {arg_info,name}} 421 {exist_thms, prop_thms}= 422 let 423 val {args, ty} = 424 itlist 425 (fn ty_info => fn {args, ty} => 426 let 427 val next = mk_joint_arg_ty_and_arg ty_info 428 in 429 {args = (#arg next) :: args, 430 ty = mk_fun {Domain = (#ty next), Range = ty}} 431 end) 432 arg_info 433 {args = [], ty = joint_type} 434 val witness = 435 list_mk_comb ((mk_const{Name = "JOINT_"^name, Ty = ty}),args) 436 val goal = ([],mk_exists (joint_select_x type_name)) 437 val tac = (EXISTS_TAC witness) THEN 438 (REWRITE_TAC (joint_select_def::prop_thms)) 439 val ethm = TAC_PROOF(goal,tac) 440 val pthm = SELECT_RULE ethm 441 in 442 {exist_thms = {type_name = type_name, exists_thm = ethm} :: 443 exist_thms, 444 prop_thms = pthm :: prop_thms} 445 end 446 447(* 448 Here are the existence theorems 449*) 450 451val {exist_thms = existence_thms,...} = 452 rev_itlist 453 prove_exists 454 existence_witnesses 455 {exist_thms = [], prop_thms = []} 456 457 458fun mk_abs_name tyname = tyname ^ "_abs" 459fun mk_rep_name tyname = tyname ^ "_rep" 460fun mk_bij_name tyname = tyname ^ "_REP_ABS" 461 462fun rev_map_aux f acc [] = acc 463 | rev_map_aux f acc (x::xs) = rev_map_aux f ((f x)::acc) xs 464 465fun rev_map f l = rev_map_aux f [] l 466 467 468(* 469 Here is the WONDERFUL computation of the type definitions and the REP 470 and ABS functions 471*) 472 473val ty_defs = 474 rev_map 475 (fn {exists_thm, type_name} => 476 let 477 val pred = (rand o concl) exists_thm 478 val sel = mk_exists {Bvar = Joint_x, 479 Body = mk_comb{Rator = pred, Rand = Joint_x}} 480 val inhab_thm = 481 EQ_MP (SYM (DEPTH_CONV BETA_CONV sel)) exists_thm 482 val type_def = new_type_definition{inhab_thm = inhab_thm, 483 name = type_name, 484 pred = pred} 485 val new_type = 486 #Domain(dest_fun (type_of (#Bvar(dest_exists (concl type_def))))) 487 val rep_name = mk_rep_name type_name 488 val abs_name = mk_abs_name type_name 489 val rep_abs_thm = 490 define_new_type_bijections {name = mk_bij_name type_name, 491 ABS = abs_name, 492 REP = rep_name, 493 tyax = type_def} 494 val rep = mk_const{Name = rep_name, 495 Ty = mk_fun {Domain = new_type, 496 Range = joint_type}} 497 val abs = mk_const{Name = abs_name, 498 Ty = mk_fun {Domain = joint_type, 499 Range = new_type}} 500 in 501 {type_name = type_name, 502 new_type = new_type, 503 rep_abs_thm = rep_abs_thm, 504 rep = rep, abs = abs} 505 end) 506 existence_thms 507 508 509(* Now we have to define all the constructors for the individual types. 510 We make them from the constructors for the joint type, with some 511 *_abs and *_rep functions thrown in for typecasting. All of the functions 512 up to define_constructors are essentiall helper functions *) 513 514(* mk_constructor_app makes a constructor and creates variables of the 515 right type for it to be applied to, applies it to the variables, 516 returns the applied constructor and list of vars that were created. *) 517fun mk_constructor_app type_name {name, arg_info} = 518 let 519 val result_type = mk_type {Tyop=type_name,Args=type_arg_vars} 520 val (constructor_type, dom_ty_list) = 521 itlist 522 (fn (existing ty) => 523 (fn (range_ty, dom_ty_list) => 524 (mk_fun{Domain = ty, Range = range_ty}, 525 ty::dom_ty_list)) 526 | (being_defined str) => 527 (fn (range_ty, dom_ty_list) => 528 let val ty = mk_type{Tyop = str, Args = type_arg_vars} 529 in 530 (mk_fun{Domain = ty, Range = range_ty}, 531 ty::dom_ty_list) 532 end)) 533 arg_info 534 (result_type,[]) 535 val constructor = mk_var {Name = name, Ty = constructor_type} 536 fun mk_c_app C_app [] n vars_seen = 537 {Applied_Constructor = C_app, Var_Args = rev vars_seen} 538 | mk_c_app C_app (ty::tys) n vars_seen = 539 let val v = mk_var{Name = ("x"^(int_to_string n)), Ty = ty} 540 in mk_c_app 541 (mk_comb {Rator = C_app, Rand = v}) 542 tys 543 (n + 1) 544 (v::vars_seen) 545 end 546 in 547 mk_c_app constructor dom_ty_list 1 [] 548 end 549 550(* apply_constructor takes a constructor name, the args it's to be applied 551 to, and the type the result should be after it's applied, creates a 552 constant for the constructor and applies it *) 553fun apply_constructor (cons_name, result_type, args) = 554 let val constructor_type = 555 foldr (fn (arg, range_ty) => mk_fun{Domain = type_of arg, 556 Range = range_ty}) 557 result_type 558 args 559 fun apply_args (tm, []) = tm 560 | apply_args (tm, first_arg :: rest_args) = 561 apply_args (mk_comb {Rator = tm, Rand = first_arg}, 562 rest_args) 563 in 564 apply_args (mk_const {Name = cons_name, Ty = constructor_type}, 565 args) 566 end 567 568(* get_type returns the type of the given type_name *) 569fun get_type str = 570 (case find (fn entry => str = #type_name entry) ty_defs 571 of SOME entry => #new_type entry 572 | NONE => raise MUT_REC_ERR{function = "mk_case", 573 message = "Impossible"}) 574 575(* get_abs returns the abstraction function associated with type of tyname *) 576fun get_abs tyname = 577 let fun helper ({type_name, abs, rep, new_type, rep_abs_thm}::names) = 578 if tyname = type_name then abs 579 else helper names 580 | helper (_) = raise MUT_REC_ERR 581 {function = "get_abs", message = "no abs for " ^ tyname} 582 in 583 helper ty_defs 584 end 585 586(* get_rep returns the representation function associated with tyname *) 587fun get_rep tyname = 588 let fun helper ({type_name, abs, rep, new_type, rep_abs_thm}::names) = 589 if tyname = type_name then rep 590 else helper names 591 | helper (_) = raise MUT_REC_ERR 592 {function = "get_rep", message = "no rep for " ^ tyname} 593 in 594 helper ty_defs 595 end 596 597(* the joint constructor must be applied to the variables returned by 598 mk_constructor_app, so the variables that are of types being defined 599 must be coerced to be in the joint type *) 600fun coerce_arg (arg, existing ty) = arg 601 | coerce_arg (arg, being_defined tyname) = 602 mk_comb {Rator = get_rep tyname, Rand = arg} 603 604(* define_constructor does the coersions, assembles the definitions, and 605 defines one constructor for the type with name tyname *) 606fun define_constructor tyname (cons_info as {name, arg_info}) = 607 let val {Applied_Constructor = lhs, Var_Args} = 608 mk_constructor_app tyname cons_info 609 val args_of_joint_cons = map coerce_arg 610 (combine (Var_Args, arg_info)) 611 val applied_joint_cons = apply_constructor 612 ("JOINT_" ^ name, joint_type, args_of_joint_cons) 613 val cons_def = mk_eq {lhs = lhs, 614 rhs = mk_comb {Rator = get_abs tyname , 615 Rand = applied_joint_cons}} 616 in 617 (new_definition (name ^ "_DEF", cons_def); ()) 618 end 619 620(* the purpose of define_constructors is to essentially feed info to 621 define_constructor *) 622fun define_constructors (tyname, cons_info::more_info, type_data) = 623 (define_constructor tyname (cons_info); 624 define_constructors (tyname, more_info, type_data)) 625 | define_constructors (tyname, [], {type_name, constructors}::more_data) = 626 define_constructors (type_name, constructors, more_data) 627 | define_constructors (tyname, [], []) = () 628 629val _ = define_constructors ("", [], mut_rec_ty_spec) 630 631 632 633(* 634 Having defined the individual types and the constructors for those types, 635 we next need to prove the theorem that allows us to define functions by 636 mutual recursion over these types. The theorem states that given the 637 cases for a mutually recursive definition, there exists a unique collection 638 of functions satisfying the mutually recursive definition. 639 640 In order to prove such a theorem, we are going to need to use JointTypeAxiom 641 again. In order to be to use JointTypeAxiom, we are going to need values 642 to which to specialize the case statements. 643*) 644 645(* 646 sum_type is the disjoint sum of all the range types of the functions being 647 defined by mutual recursion 648*) 649 650 651 val ord_a = 97 652 fun name_of_num n = 653 if n < 26 then Char.toString(Char.chr(n + ord_a)) 654 else name_of_num ((n quot 26) - 1) 655 ^ Char.toString(Char.chr((n rem 26) + ord_a)) 656 657 fun mk_new_tyvar_name {type_num, avoiding_tyvar_names} = 658 let val new_tyvar_name = "'" ^ (name_of_num type_num) 659 in 660 if Lib.mem new_tyvar_name avoiding_tyvar_names 661 then mk_new_tyvar_name {type_num = type_num +1, 662 avoiding_tyvar_names = 663 avoiding_tyvar_names} 664 else {next_type_num = type_num + 1, new_type_name = new_tyvar_name} 665 end 666 fun get_sum_type {type_names = [], types_made = [], ...} = 667 raise MUT_REC_ERR{function = "get_sum_type", message = "No types!?!"} 668 | get_sum_type {type_names = [], types_made = inl::rest, type_num} = 669 rev_itlist 670 (fn Inl => fn Inr => mk_sum{Inl = Inl, Inr = Inr}) 671 rest 672 inl 673 674 | get_sum_type {type_names = (type_name::type_names), 675 types_made, 676 type_num} = 677 let 678 679 val {new_type_name, next_type_num} = 680 mk_new_tyvar_name {type_num = type_num, 681 avoiding_tyvar_names = 682 map Type.dest_vartype type_arg_vars} 683 val new_type = mk_vartype new_type_name 684 in 685 get_sum_type {type_names = type_names, 686 types_made = new_type :: types_made, 687 type_num = next_type_num} 688 end 689 690 val sum_type = get_sum_type {type_names = type_names, 691 types_made = [], 692 type_num = 0} 693 694 695(* 696 Ins_Outs is a table of the range type (type_summand) associated with a 697 type name and the list of INR(L)s and OUTR(L)s need to inject that type 698 into the sum_type and project it out. 699*) 700 701 fun mk_rights [] = 702 raise MUT_REC_ERR 703 {function = "mk_rights", message = "Impossible"} 704 | mk_rights [last] = {Ins = [], Outs = []} 705 | mk_rights (ty1::(tys as ty2::_)) = 706 let 707 val {Ins, Outs} = mk_rights tys 708 in 709 {Ins = 710 (mk_const{Name = "INR", Ty = mk_fun{Domain = ty1, Range = ty2}}) 711 :: Ins, 712 Outs = 713 (mk_const{Name = "OUTR", Ty = mk_fun{Domain = ty2, Range = ty1}}) 714 :: Outs} 715 end 716 717 fun get_ins_outs {type_names = [],...} = 718 raise MUT_REC_ERR 719 {function = "get_ins_outs", message = "Impossible - No type names"} 720 | get_ins_outs {sum_types = [], ...} = 721 raise MUT_REC_ERR 722 {function = "get_ins_outs", message = "Impossible - No types"} 723 | get_ins_outs {type_names = [last], sum_types = [ty]} = 724 let val id = mk_const {Name = "I", Ty = mk_fun{Domain=ty, Range=ty}} 725 in 726 [{type_name = last, type_summand = ty, Ins = [id], Outs = [id]}] 727 end 728 | get_ins_outs {type_names = [last], sum_types = tys as ty1 :: _} = 729 let 730 val {Ins, Outs} = mk_rights tys 731 in 732 [{type_name = last, 733 type_summand = ty1, 734 Ins = Ins, 735 Outs = Outs}] 736 end 737 | get_ins_outs {type_names = type_name :: type_names, 738 sum_types = tys as ty1 :: _} = 739 let 740 val {Ins, Outs} = mk_rights tys 741 val {Inl = type_summand, Inr = top_sum_type} = dest_sum ty1 742 val Inl = mk_const{Name = "INL", 743 Ty = mk_fun{Domain = type_summand, Range = ty1}} 744 val Outl = mk_const{Name = "OUTL", 745 Ty = mk_fun{Domain = ty1, 746 Range = type_summand}} 747 val ins_outs = get_ins_outs {type_names = type_names, 748 sum_types = top_sum_type :: tys} 749 in 750 {type_name = type_name, 751 type_summand = type_summand, 752 Ins = Inl :: Ins, 753 Outs = Outl :: Outs} 754 :: ins_outs 755 end 756 757val Ins_Outs = get_ins_outs{type_names = type_names,sum_types = [sum_type]} 758 759 760fun new_list_mk_conj [] = mk_const{Name = "T", Ty = bool} 761 | new_list_mk_conj l = list_mk_conj l 762 763val JointProp = mk_var{Name = "Prop", 764 Ty = mk_fun{Domain = joint_type, Range = bool}} 765 766fun new_ty_Prop type_name = mk_var{Name = type_name^"_Prop", 767 Ty = mk_fun {Domain = get_type type_name, 768 Range = bool}} 769 770fun joint_select_x ty_name = 771 mk_eq {lhs = mk_comb {Rator = joint_select, Rand = Joint_x}, 772 rhs = mk_hol_num (type_num ty_name)} 773 774 775(* 776 mk_case_aux is used to create the types, variables and arguments we will 777 need to create the return functions for our joint mutual recursion function. 778 The summand_types are the recursive argument types to the case, the 779 exisiting_types are the types of the arguments to the operators of 780 previously existing type, and the being_defined_types are the types of the 781 arguments to the operators of types that are being defined. The rec_vars 782 returned are the vars representing the return values (of sum_type) of the 783 recursive call to the joint function, the plain_vars are the vars 784 representing the arguments to the operators of existing type, the new_ty_vars 785 are the vars representing arguments to the operators of types being defined, 786 and the joint_ty_vars are the vars representing arguments to the operators of 787 the joint type. The new_ty_const_arg_vars are all the variable arguments 788 to the operators of the types being defined and the joint_constructor_arg_vars 789 are all the variable arguments to the operators of the joint type. The 790 abs_args are the abstractions from the joint type to the specific new types 791 and the proj_args are the projections from the sum_type to the individual 792 result types the mutually recursive functions being defined. 793 exists_specl is the set of specializations for the conjuncts. 794*) 795 796(* 797 Base Case: We are through looking at the constructor arguments. Return the 798 case information. 799*) 800 801 802fun mk_case_aux {arg_info = [] : type_info list, 803 constructor_name : string, 804 type_name : string, 805 xy_var_num : int, 806 rec_var_num : int, 807 summand_types : hol_type list, 808 existing_types : hol_type list, 809 being_defined_types : hol_type list, 810 rec_vars : term list, 811 new_ty_vars : term list, 812 joint_ty_vars : term list, 813 proj_args : term list, 814 plain_vars : term list, 815 abs_args : term list, 816 exists_specl : term list, 817 new_ty_const_arg_vars : term list, 818 new_ty_const_arg_types : hol_type list, 819 new_ty_props : term list, 820 joint_constructor_arg_types : hol_type list, 821 joint_constructor_arg_vars : term list, 822 joint_induct_rec_vars :term list} = 823 let 824 val {type_summand,Ins,...} = 825 case find (fn entry => type_name = #type_name entry) Ins_Outs 826 of SOME entry => entry 827 | NONE => raise MUT_REC_ERR{function = "mk_case", 828 message = "Impossible"} 829 fun rev_list_mk_fun {Domain_list, Range}= 830 rev_itlist 831 (fn Domain => fn Range => 832 (mk_fun {Domain = Domain, Range = Range})) 833 Domain_list 834 Range 835 val case_type = 836 rev_list_mk_fun 837 {Domain_list = summand_types, 838 Range = rev_list_mk_fun 839 {Domain_list = existing_types, 840 Range = rev_list_mk_fun 841 {Domain_list = being_defined_types, 842 Range = type_summand}}} 843 val case_var = mk_var{Name = constructor_name^"_case",Ty = case_type} 844 val sym_cons_def = 845 GEN_ALL(SYM(SPEC_ALL 846 (definition (constructor_name^"_DEF")))) 847 val Body = 848 rev_itlist 849 (fn Rator => fn Rand => mk_comb{Rator = Rator, Rand = Rand}) 850 Ins 851 (list_mk_comb 852 (list_mk_comb 853 (list_mk_comb (case_var,rev proj_args), 854 rev plain_vars), 855 rev abs_args)) 856 fun rev_list_mk_abs {Bvars, Body} = 857 rev_itlist 858 (fn Bvar => fn Body => mk_abs{Bvar = Bvar, Body = Body}) 859 Bvars 860 Body 861 val exists_case_fn = 862 rev_list_mk_abs 863 {Bvars = rec_vars, 864 Body = rev_list_mk_abs 865 {Bvars = plain_vars, 866 Body = rev_list_mk_abs 867 {Bvars = joint_ty_vars, 868 Body = Body}}} 869 val new_ty_const_args = rev new_ty_const_arg_vars 870 val applied_constructor = 871 list_mk_comb 872 (mk_const{Name = constructor_name, 873 Ty = rev_list_mk_fun 874 {Domain_list = new_ty_const_arg_types, 875 Range = get_type type_name}}, 876 new_ty_const_args) 877 val new_ty_induct_case = 878 list_mk_forall(new_ty_const_args, 879 mk_imp{ant = new_list_mk_conj (rev new_ty_props), 880 conseq = 881 mk_comb {Rator = (new_ty_Prop type_name), 882 Rand = applied_constructor}}) 883 val joint_cons_args = rev joint_constructor_arg_vars 884 val applied_joint_constructor = 885 list_mk_comb 886 (mk_const{Name = "JOINT_"^constructor_name, 887 Ty = rev_list_mk_fun 888 {Domain_list = joint_constructor_arg_types, 889 Range = joint_type}}, 890 joint_cons_args) 891 val joint_induction_case = 892 rev_list_mk_abs 893 {Bvars = joint_induct_rec_vars, 894 Body = rev_list_mk_abs 895 {Bvars = plain_vars, 896 Body = rev_list_mk_abs 897 {Bvars = joint_ty_vars, 898 Body = 899 mk_cond {cond = new_list_mk_conj 900 joint_induct_rec_vars, 901 larm = mk_const{Name="T",Ty = bool}, 902 rarm = 903 mk_comb{Rator = JointProp, 904 Rand = 905 applied_joint_constructor}}}}} 906 val select_exists_term = 907 list_mk_exists 908 (new_ty_const_args, 909 mk_eq {lhs = mk_comb{Rator = get_abs type_name, Rand = Joint_x}, 910 rhs = applied_constructor}) 911 in 912 {type_name = type_name, 913 case_var = case_var, 914 exists_case_fn = exists_case_fn, 915 exists_specl = rev exists_specl, 916 new_ty_const_arg_vars = new_ty_const_args, 917 joint_induction_case = joint_induction_case, 918 select_exists_term = select_exists_term, 919 applied_joint_constructor = applied_joint_constructor, 920 sym_cons_def = sym_cons_def, 921 new_ty_induct_case = new_ty_induct_case} 922 end 923 924(* 925 Case: We are looking at an argument of existing type. We need to generate 926 a variable of the existing type from var_num and add it to both plain_vars 927 and arg_vars. 928*) 929 | mk_case_aux {arg_info = (existing ty)::arg_info, 930 constructor_name, 931 type_name, 932 xy_var_num, 933 rec_var_num, 934 summand_types, 935 existing_types, 936 being_defined_types, 937 rec_vars, 938 new_ty_vars, 939 joint_ty_vars, 940 proj_args, 941 plain_vars, 942 abs_args, 943 exists_specl, 944 new_ty_const_arg_vars, 945 new_ty_const_arg_types, 946 new_ty_props, 947 joint_constructor_arg_types, 948 joint_constructor_arg_vars, 949 joint_induct_rec_vars} = 950 let 951 val xN = mk_var {Name = "x"^(int_to_string xy_var_num), 952 Ty = ty} 953 in 954 mk_case_aux {arg_info = arg_info, 955 type_name = type_name, 956 constructor_name = constructor_name, 957 xy_var_num = xy_var_num + 1, 958 rec_var_num = rec_var_num, 959 summand_types = summand_types, 960 existing_types = ty :: existing_types, 961 being_defined_types = being_defined_types, 962 rec_vars = rec_vars, 963 new_ty_vars = new_ty_vars, 964 joint_ty_vars = joint_ty_vars, 965 proj_args = proj_args, 966 plain_vars = xN :: plain_vars, 967 abs_args = abs_args, 968 exists_specl = xN :: exists_specl, 969 new_ty_const_arg_vars = xN :: new_ty_const_arg_vars, 970 new_ty_const_arg_types = 971 ty :: new_ty_const_arg_types, 972 new_ty_props = new_ty_props, 973 joint_constructor_arg_types = 974 ty :: joint_constructor_arg_types, 975 joint_constructor_arg_vars = 976 xN :: joint_constructor_arg_vars, 977 joint_induct_rec_vars = joint_induct_rec_vars} 978 end 979 980(* 981 Case: We are looking at an argument of a type being defined. We need to 982 generate a variable recN of type sum_type from rec_var_num and add it to 983 rec_vars. We need to project it onto the appropriate type_summand, add the 984 projection onto proj_args and the type_summand onto summand_types. We need 985 to generate a variable xN of the joint type from var_num and add it to the 986 arg_vars. We need to abstract it from the joint type to the type being 987 defined and add it to the abs_args. We need to add the type being defined 988 to being_defined_types. 989*) 990 | mk_case_aux {arg_info = (being_defined str)::arg_info, 991 type_name, 992 constructor_name, 993 xy_var_num, 994 rec_var_num, 995 summand_types, 996 existing_types, 997 being_defined_types, 998 rec_vars, 999 new_ty_vars, 1000 joint_ty_vars, 1001 proj_args, 1002 plain_vars, 1003 abs_args, 1004 exists_specl, 1005 new_ty_const_arg_vars, 1006 new_ty_const_arg_types, 1007 new_ty_props, 1008 joint_constructor_arg_types, 1009 joint_constructor_arg_vars, 1010 joint_induct_rec_vars} = 1011 let 1012 val M = int_to_string rec_var_num 1013 val recM = mk_var {Name = "rec"^M, Ty = sum_type} 1014 val joint_induct_recM = mk_var {Name = "rec"^M, Ty = bool} 1015 val {type_summand,Outs,...} = 1016 case find (fn entry => str = #type_name entry) Ins_Outs 1017 of SOME entry => entry 1018 | NONE => raise MUT_REC_ERR{function = "mk_case", 1019 message = "Impossible"} 1020 val proj = 1021 itlist 1022 (fn Rator => fn Rand => mk_comb{Rator = Rator, Rand = Rand}) 1023 Outs 1024 recM 1025 val {new_type = being_defined_type, abs, rep,...} = 1026 case find (fn entry => str = #type_name entry) ty_defs 1027 of SOME entry => entry 1028 | NONE => raise MUT_REC_ERR{function = "mk_case", 1029 message = "Impossible"} 1030 val N = int_to_string xy_var_num 1031 val xN = mk_var {Name = "x"^N, Ty = being_defined_type} 1032 val yN = mk_var {Name = "y"^N, Ty = joint_type} 1033 val abs_arg = mk_comb{Rator = abs, Rand = yN} 1034 val rep_arg = mk_comb{Rator = rep, Rand = xN} 1035 val new_ty_prop = mk_comb {Rator = (new_ty_Prop str), Rand = xN} 1036 in 1037 mk_case_aux {arg_info = arg_info, 1038 type_name = type_name, 1039 constructor_name = constructor_name, 1040 xy_var_num = xy_var_num + 1, 1041 rec_var_num = rec_var_num + 1, 1042 summand_types = type_summand :: summand_types, 1043 existing_types = existing_types, 1044 being_defined_types = 1045 being_defined_type :: being_defined_types, 1046 rec_vars = recM :: rec_vars, 1047 new_ty_vars = xN :: new_ty_vars, 1048 joint_ty_vars = yN :: joint_ty_vars, 1049 proj_args = proj :: proj_args, 1050 plain_vars = plain_vars, 1051 abs_args = abs_arg :: abs_args, 1052 exists_specl = rep_arg :: exists_specl, 1053 new_ty_const_arg_vars = xN :: new_ty_const_arg_vars, 1054 new_ty_const_arg_types = 1055 being_defined_type :: new_ty_const_arg_types, 1056 new_ty_props = new_ty_prop :: new_ty_props, 1057 joint_constructor_arg_types = 1058 joint_type :: joint_constructor_arg_types, 1059 joint_constructor_arg_vars = 1060 yN :: joint_constructor_arg_vars, 1061 joint_induct_rec_vars = 1062 joint_induct_recM :: joint_induct_rec_vars} 1063 end 1064 1065fun mk_case {type_name, constructor_name,arg_info} = 1066 mk_case_aux {arg_info = arg_info, 1067 type_name = type_name, 1068 constructor_name = constructor_name, 1069 xy_var_num = 1, 1070 rec_var_num = 1, 1071 summand_types = [], 1072 existing_types = [], 1073 being_defined_types = [], 1074 rec_vars = [], 1075 new_ty_vars = [], 1076 joint_ty_vars = [], 1077 proj_args = [], 1078 plain_vars = [], 1079 abs_args = [], 1080 exists_specl = [], 1081 new_ty_const_arg_vars = [], 1082 new_ty_const_arg_types = [], 1083 new_ty_props = [], 1084 joint_constructor_arg_types = [], 1085 joint_constructor_arg_vars = [], 1086 joint_induct_rec_vars = []} 1087 1088 1089val spec_cases = 1090 itlist 1091 (fn {type_name, constructors} => fn l => 1092 (itlist 1093 (fn {name,arg_info} => fn l => 1094 (mk_case {type_name = type_name, 1095 constructor_name = name, 1096 arg_info = arg_info})::l) 1097 constructors 1098 []) @ l) 1099 mut_rec_ty_spec 1100 [] 1101 1102val th1 = BETA_RULE 1103 (rev_itlist 1104 (fn {exists_case_fn,...} => (fn thm => ISPEC exists_case_fn thm)) 1105 spec_cases 1106 JointTypeAxiom) 1107 1108val (Exists, Unique) = CONJ_PAIR (EQ_MP (EXISTS_UNIQUE_CONV (concl th1)) th1) 1109 1110val P = #Rand (dest_comb(concl th1)) 1111val {Bvar = f,Body} = dest_abs P 1112 1113val mod_fns = 1114 map 1115 (fn type_name => 1116 let 1117 val {new_type = being_defined_type, rep,...} = 1118 case find (fn entry => type_name = #type_name entry) ty_defs 1119 of SOME entry => entry 1120 | NONE => raise MUT_REC_ERR{function = "", 1121 message = "Impossible"} 1122 val x = mk_var {Name = "x", Ty = being_defined_type} 1123 val {Outs,...} = 1124 case find (fn entry => type_name = #type_name entry) Ins_Outs 1125 of SOME entry => entry 1126 | NONE => raise MUT_REC_ERR{function = "", 1127 message = "Impossible"} 1128 val lambda = 1129 mk_abs{Bvar = x, 1130 Body = 1131 itlist 1132 (fn Rator => fn Rand => 1133 mk_comb{Rator = Rator, Rand = Rand}) 1134 Outs 1135 (mk_comb{Rator = f, 1136 Rand = (mk_comb{Rator = rep, Rand = x})})} 1137 val beta_thm = 1138 GEN x (SYM (BETA_CONV (mk_comb{Rator = lambda, Rand = x}))) 1139 in 1140 {lambda = lambda, beta_thm = beta_thm} 1141 end) 1142 type_names 1143 1144val rep_abs_thms = 1145 map 1146 (fn type_name => 1147 (case find (fn entry => type_name = #type_name entry) ty_defs 1148 of SOME entry => BETA_RULE (#rep_abs_thm entry) 1149 | NONE => raise MUT_REC_ERR{function = "", 1150 message = "Impossible"})) 1151 type_names 1152 1153val abs_rep_thms = map CONJUNCT1 rep_abs_thms 1154 1155val elim_cons_thms = 1156 itlist 1157 (fn {type_name, constructors} => fn l => 1158 let 1159 val cons_REP_ABS = 1160 CONJUNCT2 (definition (mk_bij_name type_name)) 1161 val {abs = cons_abs, rep = cons_rep,...} = 1162 case find (fn entry => type_name = #type_name entry) ty_defs 1163 of SOME entry => entry 1164 | NONE => raise MUT_REC_ERR{function = "", 1165 message = "Impossible"} 1166 in 1167 (itlist 1168 (fn {name,arg_info} => fn l => 1169 let 1170 val cons_def = definition (name^"_DEF") 1171 val sym_cons_def = 1172 SYM (AP_TERM cons_rep (SPEC_ALL cons_def)) 1173 val r = rand(rand(lhs(concl sym_cons_def))) 1174 val spec_REP_ABS = BETA_RULE (SPEC r cons_REP_ABS) 1175 val select_thm = 1176 TAC_PROOF(([],(lhs(concl spec_REP_ABS))), 1177 ((PURE_ONCE_REWRITE_TAC [joint_select_def]) THEN 1178 REWRITE_TAC rep_abs_thms)) 1179 val joint_elim_thm = (PURE_ONCE_REWRITE_RULE [sym_cons_def] 1180 (EQ_MP spec_REP_ABS select_thm)) 1181 val cons_elim_thm = (PURE_ONCE_REWRITE_RULE abs_rep_thms 1182 (AP_TERM cons_abs joint_elim_thm)) 1183 1184 in 1185 {type_name = type_name, 1186 joint_elim_thm = SYM joint_elim_thm, 1187 cons_elim_thm = cons_elim_thm} :: l 1188 end) 1189 constructors 1190 []) 1191 end @ l) 1192 mut_rec_ty_spec 1193 [] 1194 1195(* Do the generalization while you are at it *) 1196fun map3 f [] [] [] = [] 1197 | map3 f (x1::l1) (x2::l2) (x3::l3) = (f x1 x2 x3)::(map3 f l1 l2 l3) 1198 | map3 f _ _ _ = raise MUT_REC_ERR{function = "map3", 1199 message = "Unbalanced lists (impossible)"} 1200 1201val OUTL = sumTheory.OUTL 1202val OUTR = sumTheory.OUTR 1203val II_THM = prove((--`!x:'a. I (I x) = x`--), 1204 REWRITE_TAC[combinTheory.I_THM]); 1205 1206 1207 fun abs_every tm1 var tm2 frees = 1208 if tm1 = tm2 then var 1209 else if is_var tm2 then tm2 1210 else if is_const tm2 then tm2 1211 else if is_comb tm2 1212 then mk_comb{Rator = abs_every tm1 var (rator tm2) frees, 1213 Rand = abs_every tm1 var (rand tm2) frees} 1214 else 1215 let val {Bvar, Body} = dest_abs tm2 1216 in if mem Bvar frees then tm2 1217 else mk_abs {Bvar = Bvar, 1218 Body = abs_every tm1 var Body frees} 1219 end 1220 1221fun abstract_every tm1 v tm2 = 1222 let val var = variant (all_vars tm2) v 1223 val frees = free_vars tm1 1224 in 1225 abs_every tm1 var tm2 frees 1226 end 1227 1228 1229fun EX n [] thm = {fns = [], ext_thm = thm} 1230 | EX n (tm::tms) thm = 1231 let 1232 val f = mk_var {Name = "fn"^(int_to_string n), Ty = type_of tm} 1233 val {fns, ext_thm} = EX (n+1) tms thm 1234 val pattern = mk_exists{Bvar = f, 1235 Body = abstract_every tm f (concl ext_thm)} 1236 in 1237 {fns = f :: fns, ext_thm = EXISTS (pattern,tm) ext_thm} 1238 end 1239 1240val {ext_thm = ext_thm, fns} = 1241 EX 1 (map #lambda mod_fns) 1242 (LIST_CONJ 1243 (map3 1244 (fn {type_name, joint_elim_thm,...} => 1245 let 1246 val {Outs,...} = 1247 case find (fn entry => type_name = #type_name entry) Ins_Outs 1248 of SOME entry => entry 1249 | NONE => raise MUT_REC_ERR{function = "", 1250 message = "Impossible"} 1251 in 1252 fn {exists_specl, new_ty_const_arg_vars, ...} => fn thm => 1253 GENL new_ty_const_arg_vars 1254 (PURE_ONCE_REWRITE_RULE (map (#beta_thm) mod_fns) 1255 (PURE_REWRITE_RULE (II_THM::OUTL::OUTR::abs_rep_thms) 1256 (itlist AP_TERM Outs 1257 (PURE_ONCE_REWRITE_RULE [joint_elim_thm] 1258 (SPECL exists_specl thm))))) 1259 end) 1260 elim_cons_thms 1261 spec_cases 1262 (CONJUNCTS (ASSUME Body)))) 1263val lemma = 1264 TAC_PROOF 1265 (([], 1266 (--`!(P:'a -> bool) (Q:bool). (?x.P x) ==> ((!x.P x ==> Q) ==> Q)`--)), 1267 ((REPEAT STRIP_TAC) THEN RES_TAC)) 1268 1269val Q = concl ext_thm 1270val cases = map (#case_var) spec_cases 1271 1272val New_Ty_Existence_Thm = 1273 GENL cases 1274 (MP (MP (BETA_RULE (ISPECL [P, Q] lemma)) Exists) 1275 (GEN f (DISCH_ALL ext_thm))) 1276 1277 1278val IfThenElse_Imp = 1279 prove ((--`!A B. (B = (if A then T else B)) = (A ==> B)`--), 1280 ((REPEAT STRIP_TAC )THEN 1281 (ASM_CASES_TAC (--`A:bool`--)) THEN 1282 (ASM_REWRITE_TAC []))) 1283 1284val JointInduct = 1285let 1286 val th = 1287 CONJUNCT2 1288 (CONV_RULE EXISTS_UNIQUE_CONV 1289 (BETA_RULE 1290 (rev_itlist 1291 (fn {joint_induction_case,...} => 1292 (fn thm => ISPEC joint_induction_case thm)) 1293 spec_cases 1294 JointTypeAxiom))) 1295 val f = #Bvar (dest_forall (concl th)) 1296in 1297 GEN JointProp 1298 (REWRITE_RULE [IfThenElse_Imp] 1299 (BETA_RULE 1300 (CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) 1301 (SPECL 1302 [JointProp, 1303 (mk_abs{Bvar = Joint_x, Body = mk_const{Name = "T", Ty =bool}})] 1304 th)))) 1305end 1306 1307 1308val lemma = 1309 prove((--`!b f s:'a. ((if b then f else s) = f) = ((f = s) \/ b)`--), 1310 ((REPEAT GEN_TAC) THEN EQ_TAC THEN COND_CASES_TAC THEN 1311 (REWRITE_TAC []) THEN STRIP_TAC THEN (ASM_REWRITE_TAC[]))) 1312 1313val rep_abs_eq_simps = 1314 map 1315 (fn {type_name,applied_joint_constructor,...} => 1316 (REWRITE_RULE rep_abs_thms 1317 (CONV_RULE (DEPTH_CONV reduceLib.NEQ_CONV) 1318 (REWRITE_RULE [lemma,joint_select_def] 1319 (SYM (SPEC applied_joint_constructor 1320 (CONJUNCT2 (List.nth 1321 ((rep_abs_thms,(type_num type_name) - 1)))))))))) 1322 spec_cases 1323 1324 1325fun non_diag_map p f [] = [] 1326 | non_diag_map p f (x::xs) = 1327 if p x then non_diag_map p f xs 1328 else (f x)::(non_diag_map p f xs) 1329 1330val not_rep_abs_thms = 1331 flatten 1332 (map 1333 (fn {type_name, applied_joint_constructor, ...} => 1334 non_diag_map 1335 (fn tyn => (tyn = type_name)) 1336 (fn ty_name => 1337 prove 1338 (mk_neg(mk_eq{lhs = mk_comb{Rator = get_rep ty_name, 1339 Rand = mk_comb{Rator = get_abs ty_name, 1340 Rand = 1341 applied_joint_constructor}}, 1342 rhs = applied_joint_constructor}), 1343 ((PURE_ONCE_REWRITE_TAC 1344 (map (SYM o SPEC_ALL o CONJUNCT2) rep_abs_thms)) THEN 1345 (PURE_ONCE_REWRITE_TAC [joint_select_def]) THEN 1346 (COND_CASES_TAC ORELSE ALL_TAC) THEN (ONCE_REWRITE_TAC[]) THEN 1347 (CONV_TAC (DEPTH_CONV reduceLib.NEQ_CONV)) THEN 1348 (ONCE_REWRITE_TAC[])))) 1349 type_names) 1350 spec_cases) 1351 1352 1353 1354fun mk_case_prop type_name = 1355 let 1356 val abs = mk_comb{Rator = get_abs type_name, Rand = Joint_x} 1357 val rep_abs = mk_comb{Rator = get_rep type_name, Rand = abs} 1358 in 1359 mk_imp {ant = mk_eq{lhs = rep_abs, rhs = Joint_x}, 1360 conseq = mk_comb {Rator = new_ty_Prop type_name, 1361 Rand = abs}} 1362 end 1363 1364fun mk_rep_abs_cases_prop [] = mk_const{Name= "T",Ty=bool} 1365 | mk_rep_abs_cases_prop (type_name :: nil) = 1366 mk_case_prop type_name 1367 | mk_rep_abs_cases_prop (type_name :: type_names) = 1368 mk_conj{conj1 = mk_case_prop type_name, 1369 conj2 = mk_rep_abs_cases_prop type_names} 1370 1371val new_ty_induct_prop = mk_forall{Bvar = Joint_x, 1372 Body = mk_rep_abs_cases_prop type_names} 1373 1374 1375fun case_thm type_name num = 1376 let 1377 val var = mk_var{Name= "x"^(int_to_string num), 1378 Ty = get_type type_name} 1379 in 1380 GEN var 1381 (REWRITE_RULE 1382 rep_abs_thms 1383 (List.nth (CONJUNCTS (SPEC 1384 (mk_comb {Rator = get_rep type_name, 1385 Rand = var}) 1386 (ASSUME new_ty_induct_prop)), 1387 (num - 1)))) 1388 end 1389 1390fun case_induct_concl num [] = TRUTH 1391 | case_induct_concl num [type_name] = case_thm type_name num 1392 | case_induct_concl num (type_name::type_names) = 1393 CONJ (case_thm type_name num) (case_induct_concl (num + 1) type_names) 1394 1395val inter_case_induct_thm = (DISCH_ALL (case_induct_concl 1 type_names)) 1396 1397 1398 1399val lemma = prove ((--`!A. (T ==> A) = A`--), (REWRITE_TAC [])) 1400 1401val new_ty_induct_assum = 1402 UNDISCH (PURE_ONCE_REWRITE_RULE [lemma] (DISCH_ALL 1403 (ASSUME (new_list_mk_conj (map (#new_ty_induct_case) spec_cases))))) 1404 1405 1406val inter_case_assum = #ant(dest_imp (concl inter_case_induct_thm)) 1407 1408val pre_case_induct_thm = prove 1409((mk_imp {ant = concl new_ty_induct_assum, conseq = inter_case_assum}), 1410 ((REWRITE_TAC (map (#cons_elim_thm) elim_cons_thms)) THEN 1411 STRIP_TAC THEN 1412 (elsaUtils.MP_IMP_TAC (BETA_RULE (SPEC (rand new_ty_induct_prop) JointInduct))) THEN 1413 (ASM_REWRITE_TAC (rep_abs_eq_simps @ not_rep_abs_thms)) THEN 1414 (REPEAT CONJ_TAC) THEN (REPEAT GEN_TAC) THEN STRIP_TAC THEN 1415 (fn g as (ams,gl) => 1416 let val eqs = 1417 map (SUBST1_TAC o SYM o ASSUME) (strip_conj (#ant (dest_imp gl))) 1418 val tac = itlist (fn t1 => fn t2 => t1 THEN t2) eqs ALL_TAC 1419 in (STRIP_TAC THEN tac) g end) THEN 1420 (FIRST_ASSUM 1421 (fn th => elsaUtils.MATCH_MP_IMP_TAC (SPEC (#Bvar(dest_forall(concl th))) th))) THEN 1422 (REPEAT CONJ_TAC) THEN 1423 (FIRST_ASSUM elsaUtils.MATCH_MP_IMP_TAC) THEN (FIRST_ASSUM ACCEPT_TAC))) 1424 1425val New_Ty_Induct_Thm = itlist (fn ty_name => fn th => 1426 GEN (new_ty_Prop ty_name) th) 1427 type_names 1428 (IMP_TRANS pre_case_induct_thm 1429 inter_case_induct_thm); 1430 1431 1432 val (forall_vars,eBody) = strip_forall (concl New_Ty_Existence_Thm) 1433 val (exists_vars, New_Ty_Existence_Body) = strip_exists eBody 1434 val bad_vars = exists_vars @ forall_vars 1435 1436val New_Ty_Existence_Body = New_Ty_Existence_Body 1437 1438val {new_fns, fns_subst} = 1439 itlist 1440 (fn f => (fn {new_fns, fns_subst} => 1441 let 1442 val new_f = variant bad_vars f 1443 in 1444 {new_fns = new_f :: new_fns, 1445 fns_subst = {redex = f, residue = new_f} :: fns_subst} 1446 end)) 1447 fns 1448 {new_fns = [], fns_subst = []} 1449 1450 1451val unique_goal = 1452 mk_imp{ant = mk_conj{conj1 = New_Ty_Existence_Body, 1453 conj2 = (subst fns_subst New_Ty_Existence_Body)}, 1454 conseq = list_mk_conj (map 1455 (fn {redex, residue} => 1456 mk_eq{lhs = redex, rhs = residue}) 1457 fns_subst)} 1458 1459val pre_unique_thm = prove(unique_goal, 1460 (STRIP_TAC THEN (CONV_TAC (ONCE_DEPTH_CONV FUN_EQ_CONV)) THEN 1461 (fn g as (asm,gl) => 1462 let val eq_preds = map rand (strip_conj gl) 1463 val induct = BETA_RULE (SPECL eq_preds New_Ty_Induct_Thm) 1464 in elsaUtils.MP_IMP_TAC induct g 1465 end) THEN 1466 (REPEAT STRIP_TAC) THEN 1467 (ASM_REWRITE_TAC []))) 1468 1469val New_Ty_Uniqueness_Thm = GENL (cases @ fns @ new_fns) pre_unique_thm 1470 1471in 1472 {New_Ty_Existence_Thm = New_Ty_Existence_Thm, 1473 New_Ty_Induct_Thm = New_Ty_Induct_Thm, 1474 New_Ty_Uniqueness_Thm = New_Ty_Uniqueness_Thm} 1475end 1476 1477val _ = Parse.temp_set_grammars ambient_grammars 1478 1479end (* MutRecDef *) 1480