1(* In order to use our recursive theorem on mutually recursive types to 2 define functions on these types, we need to be able to extract from a 3 description of how the function should behave the values of the 4 "return functions": the things that are universally quantified on 5 the outside of the recursive theorem, which are functions and 6 constants, one for each constructor of the mutually recursive types, 7 that compute the return value of the function from the arguments 8 of the constructor and the return values of applications of (possibly 9 other) mutually recursive functions to the constructor args. We then 10 instantiate our recursive function with them, define the functions, 11 and prove that the definitions satisfy the desired properties. *) 12 13(* 14 In any term that defines a set of mutually recursive functions, 15 there must be at most one function defined for each type (there need 16 not be a function defined for every type). If a function is being 17 defined on a type, the term must provide, in a sepate conjunct, a 18 value for each constructor for the type, except as descibed below in 19 the text reguarding the examples. 20 21 Both examples define the same functions, a set of functions that 22 count the number of variables and constructors used in a pattern. The 23 first term gives explictly the values of the function on all 24 constructors for each type for which a function is defined, and the 25 second one uses the variable "allelse" to give the values for some of 26 the constructors. The "allelse" works like this: Say a function is 27 being defined on a type (call it TY, in the second example this is 28 atpat) and the case for a constructor is missing (for example, 29 SCONatpat). If, following the clauses for the constructors for which 30 explicit values are given (in the second example, VARatpat, CONatpat, 31 EXCONatpat, RECORD2atpat, and PARatpat), there is a conjunct where the 32 constructor applied to appropriate arguments (here, (SCONatpat sc)) is 33 replaced by the variable "allelse" with type TY, then the value to the 34 right of the = sign is used as the value of the function on terms 35 constructed with that constructor. If there is a variable "arg" with 36 type TY as one of the subterms of this value (the one to the right of 37 the =), this will be replaced by the constructor applied to arguments 38 (again, (SCONatpat sc)). There may be at most one "allelse" clause per 39 function being defined, but there is no limit to the number of 40 "allelse" clauses used in the term (they will be destinguished by the 41 type of the variable). As noted above, the "allelse" clause must 42 follow the clauses giving values for specific constructors (there need 43 not be any of these). 44 45--`(varcon_pat (ATPATpat ap) = varcon_atpat ap) /\ 46 (varcon_pat (CONpat c ap) = 1 + (varcon_atpat ap)) /\ 47 (varcon_pat (EXCONpat e a) = 1 + (varcon_atpat a)) /\ 48 (varcon_atpat WILDCARDatpat = 0) /\ 49 (varcon_atpat (SCONatpat sc) = 0) /\ 50 (varcon_atpat (VARatpat v) = 1) /\ 51 (varcon_atpat (CONatpat c) = 1) /\ 52 (varcon_atpat (EXCONatpat e) = 1) /\ 53 (varcon_atpat RECORD1atpat = 0) /\ 54 (varcon_atpat (RECORD2atpat pr) = varcon_patrow pr) /\ 55 (varcon_atpat (PARatpat p) = varcon_pat p) /\ 56 (varcon_patrow DOTDOTDOT = 0) /\ 57 (varcon_patrow (PATROW1 l p) = varcon_pat p) /\ 58 (varcon_patrow (PATROW2 l p pr) = (varcon_pat p) + (varcon_patrow pr))`-- 59 60--`(varcon_pat (ATPATpat ap) = varcon_atpat ap) /\ 61 (varcon_pat (CONpat c ap) = 1 + (varcon_atpat ap)) /\ 62 (varcon_pat (EXCONpat e a) = 1 + (varcon_atpat a)) /\ 63 (varcon_atpat (VARatpat v) = 1) /\ 64 (varcon_atpat (CONatpat c) = 1) /\ 65 (varcon_atpat (EXCONatpat e) = 1) /\ 66 (varcon_atpat (RECORD2atpat pr) = varcon_patrow pr) /\ 67 (varcon_atpat (PARatpat p) = varcon_pat p) /\ 68 (varcon_atpat allelse = 0) /\ 69 (varcon_patrow DOTDOTDOT = 0) /\ 70 (varcon_patrow (PATROW1 l p) = varcon_pat p) /\ 71 (varcon_patrow (PATROW2 l p pr) = (varcon_pat p) + (varcon_patrow pr))`-- 72 73*) 74 75structure Recftn :> Recftn = 76struct 77 78open HolKernel Parse basicHol90Lib; 79 80type term = Term.term 81type fixity = Parse.fixity 82type thm = Thm.thm; 83 84 85val ambient_grammars = Parse.current_grammars(); 86val _ = Parse.temp_set_grammars boolTheory.bool_grammars 87 88 89(* define_mutual_functions takes the term def (one such as the one above) 90 and warps it into a state where it can be combined with rec_axiom to 91 produce definitions for the mutually recursive functions the user 92 has given information enough to define. It returns a proof that 93 the functions defined really do satisfy the conditions 94 imposed by the term *) 95 96fun define_mutual_functions {rec_axiom, name = specification_name, 97 fixities, def} = 98let 99open Rsyntax (* use records *) 100(* (* We coerce the type so that rec_axiom and def agree *) 101 local 102 val rec_type_args = 103 #Args(dest_type(hd(#Args(dest_type(type_of 104 (hd(#1(strip_exists(#2(strip_forall (concl rec_axiom))))))))))) 105 val def_type_args = 106 #Args(dest_type(type_of (rand(lhs(hd(strip_conj def)))))) 107 val ty_subst = 108 Lib.map2 109 (fn redex => fn residue => {redex = redex,residue=residue}) 110 rec_type_args 111 def_type_args 112 in 113 val rec_axiom = if rec_type_args = def_type_args then rec_axiom 114 else INST_TYPE ty_subst rec_axiom 115 end 116*) 117 (* first need to deconstruct rec_axiom so we know what to look for *) 118 119 (* term_name and type_name are used for making error messages *) 120 fun term_name tm = 121 if is_var tm then 122 #Name (dest_var tm) 123 else if is_const tm then 124 #Name (dest_const tm) 125 else raise HOL_ERR {origin_structure = "define_mutual_functions", 126 origin_function = "term_name", 127 message = "term is not constant or var"} 128 129 fun type_name ty = #Tyop (dest_type ty) 130 131 (* decompose takes as arguments a term that is a constructor applied 132 to some args and the list of args stripped off so far; it strips 133 off the rest of the args, returning the constructor by itself 134 and the complete list of args *) 135 fun decompose (tm, args_so_far) = 136 if is_comb tm then 137 let val {Rator, Rand} = dest_comb tm in 138 decompose (Rator, Rand :: args_so_far) 139 end 140 else 141 (tm, args_so_far) 142 143 (* extract_cons gets, for a conjunct in the main body of rec_axiom, 144 the constructor associated with it, the arguments of the constructor, 145 and the type the constructor will construct *) 146 fun extract_cons conj = 147 let val (cons_args, body) = strip_forall conj 148 val applied_cons = #Rand (dest_comb (#lhs (dest_eq body))) 149 in 150 {result_type = type_of applied_cons, 151 cons = fst (decompose (applied_cons, [])), 152 cons_args = cons_args} 153 end 154 155 (* now we want to break up our defining term as a preliminary step 156 to defining what's there *) 157 158 (* get_def_info returns a record that looks like this 159 {ftn = <fun_being_defined>, 160 ftn_dom = <domain type of function>, 161 constructor = <constructor this case covers>, 162 args = <constructor args>, 163 def = <term defining this case for function>} *) 164 fun get_def_info conj = 165 let val {lhs, rhs} = dest_eq conj 166 val {Rator = ftn_term, Rand = applied_cons} = dest_comb lhs 167 val ftn_dom = type_of applied_cons 168 val (con, args) = decompose (applied_cons, []) 169 in 170 {ftn = ftn_term, ftn_dom = ftn_dom, 171 constructor = con, args = args, def = rhs} 172 end 173 174 val def_data = map get_def_info (strip_conj def) 175 176 local 177 val stripped_rec = 178 #2(strip_exists (#2(strip_forall (concl rec_axiom)))) 179 val gen_cons_data = map extract_cons (strip_conj stripped_rec) 180 181 fun same_cons constructor {cons,cons_args,result_type}= 182 (#Name(dest_const constructor) = #Name(dest_const cons)) 183 fun find_ty_subst {constructor,args,def,ftn,ftn_dom} = 184 #2(Term.match_term 185 (#cons(Lib.first (same_cons constructor) gen_cons_data)) 186 constructor) 187 handle HOL_ERR _ => [] 188 189(********* backwards args to match_term ************************************ 190 * fun find_ty_subst {constructor,args,def,ftn,ftn_dom} = 191 * #2(Match.match_term constructor 192 * (#cons(Lib.first (same_cons constructor) gen_cons_data))) 193 * handle HOL_ERR _ => [] 194 **************************************************************************) 195 val subst = 196 foldr (fn (data,subs) => ((find_ty_subst data) @ subs)) [] def_data 197 in 198 val rec_axiom = 199 (case subst of [] => rec_axiom | _ => INST_TYPE subst rec_axiom) 200 val cons_data = 201 (case subst of [] => gen_cons_data 202 | _ => map extract_cons 203 (strip_conj(#2(strip_exists 204 (#2(strip_forall (concl rec_axiom))))))) 205 end 206 207 (* get_type_info just gets a list of the types involved in the 208 mutually recursive type definition creating them *) 209 fun get_types ({result_type, cons, cons_args}::cons_data, 210 ty_last_seen, tys) = 211 if result_type <> ty_last_seen then 212 (* this is the first time we've seen this type *) 213 get_types (cons_data, result_type, result_type::tys) 214 else 215 get_types (cons_data, ty_last_seen, tys) 216 | get_types ([], _, tys) = rev tys 217 (* we pass ==:`num`== as ty_last_seen as it for sure will not be the 218 return type of any of the constructors for our mutually 219 recursive types *) 220 val types = get_types (cons_data, Type`:num`, []) 221 222 (* now we need to looks thru' def_data and figure out exactly 223 what is there and what isn't *) 224 225 (* get_def_for_con looks thru' def_data to see if it can find a 226 definition for this constructor. If finds exactly one, returns 227 SOME <datum>, if finds none, returns NONE, if finds more than 228 one, raises an exception *) 229 fun get_def_for_con {result_type, cons, cons_args} = 230 let fun apply_all ftn (arg::args) = 231 apply_all (mk_comb {Rator = ftn, Rand = arg}) args 232 | apply_all ftn [] = ftn 233 (* lookup_con looks for an item with information on cons in def_info, 234 returns NONE if didn't find it, and if some sort of match was 235 found returns a flag indicating whether an exact match was 236 found (ie, we matched against a constructor rather than an 237 "allelse"), and the corresponding item from def_info if it 238 found the constructor, or the information from an "allelse" 239 clause if it found that, as well as the rest of the def_info 240 (for error checking). If the argument exact_match_found is true, 241 then we will not match with "allelse" clauses. This is to avoid 242 matching with an "allelse" clause after already matching 243 getting an exact constructor match. *) 244 fun lookup_cons (exact_match_found, 245 (def_datum as {ftn, ftn_dom, constructor, 246 args, def})::more_data) = 247 (* return the info if we've found it *) 248 if constructor = cons then 249 SOME (true, def_datum, more_data) 250 (* check if there's an "allelse" clause for this type; 251 if so, the constructor is the one we're looking for 252 and the body is the definition provided by the user 253 with the applied constructor substituted for the 254 variable "arg" in order to allow the uxser to do something 255 with the argument of the function. *) 256 else if not exact_match_found andalso (result_type = ftn_dom) 257 andalso (is_var constructor) 258 andalso (#Name (dest_var constructor) = "allelse") then 259 let val arg_var = mk_var {Name = "arg", Ty = ftn_dom} 260 val app_cons = apply_all cons cons_args 261 val subst_def = subst [{redex = arg_var, 262 residue = app_cons}] def 263 in 264 SOME (false, 265 {ftn = ftn, ftn_dom = ftn_dom, 266 constructor = cons, args = cons_args, 267 def = subst_def}, more_data) 268 end 269 else 270 lookup_cons (exact_match_found, more_data) 271 | lookup_cons (_, []) = NONE 272 val lookup_info = lookup_cons (false, def_data) 273 in 274 case lookup_info 275 (* if there was no info, there's no case for this 276 constructor for our type *) 277 of NONE => NONE 278 (* if it was in here, check to make sure it wasn't in there 279 more than once *) 280 | SOME (exact_match_found, def_datum, more_data) => 281 (case lookup_cons (exact_match_found, more_data) 282 (* that constructor only appeared once *) 283 of NONE => SOME def_datum 284 (* constructor appeared more than once in def *) 285 | SOME (_, _, _) => raise HOL_ERR 286 {origin_structure = "define_mutual_functions", 287 origin_function = "get_def_for_con", 288 message = ("constructor " ^ (term_name cons) ^ 289 " appears more than once in definition")}) 290 end 291 val def_cases = map get_def_for_con cons_data 292 293 (* get_result_typevar destructs function types until it finds that 294 the range type is a typevar, and then returns that typevar *) 295 fun get_result_typevar ftn_ty = 296 if is_vartype ftn_ty then 297 ftn_ty 298 else 299 get_result_typevar (hd (tl (#Args (dest_type ftn_ty)))) 300 301 (* we want to make sure that if the person is trying to define a 302 function for a type, then s/he gives a value for each of the 303 constructors for that type, and that only one function is being 304 defined. Also, we return a list telling, for each type, which (if any) 305 functions is being defined for that type *) 306 fun check_error ftn = 307 raise HOL_ERR {origin_structure = "define_mutual_functions", 308 origin_function = "check_def", 309 message = ("only some cases provided for function " ^ 310 (term_name ftn))} 311 val one_ty = Type`:one` 312 val one_tm = Term`one` 313 314 fun get_ftn_info ({cons, cons_args, result_type}::cons_data, 315 def_datum::def_data, 316 ftn_dom_ty, 317 ftn_being_defined) = 318 if result_type <> ftn_dom_ty then 319 (* we have a new type to report info and check functions for *) 320 case def_datum 321 of NONE => 322 (* we set range type to be one because we will create 323 a dummy function returning one. The domain of the 324 function we're defining is the result type of the 325 constructor it's operating on *) 326 {ftn_op = NONE, dom_ty = result_type, rng_ty = one_ty}:: 327 get_ftn_info (cons_data, def_data, result_type, NONE) 328 | SOME {args, constructor, def, ftn, ftn_dom} => 329 {ftn_op = SOME ftn, dom_ty = result_type, 330 rng_ty = type_of def}:: 331 get_ftn_info (cons_data, def_data, result_type, SOME ftn) 332 else 333 (* we need to make sure the functions match *) 334 (case def_datum 335 of NONE => 336 (case ftn_being_defined 337 of NONE => 338 get_ftn_info (cons_data, def_data, ftn_dom_ty, NONE) 339 | SOME ftn => check_error ftn) 340 | SOME {args, constructor, def, ftn, ftn_dom} => 341 (case ftn_being_defined 342 of NONE => check_error ftn 343 | SOME other_ftn => 344 if ftn <> other_ftn then raise HOL_ERR 345 {origin_structure = "define_mutual_functions", 346 origin_function = "get_ftn_info", 347 message = ("two different functions " ^ 348 (term_name ftn) ^ 349 " and " ^ (term_name other_ftn) ^ 350 " defined for type " ^ (type_name result_type))} 351 else 352 get_ftn_info (cons_data, def_data, 353 ftn_dom_ty, ftn_being_defined))) 354 | get_ftn_info (_, _, _, _) = [] 355 356 (* again, pass ==`:num`== as a type that shouldn't be among the 357 recursive types *) 358 val ftn_type_data = get_ftn_info (cons_data, def_cases, Type`:num`, NONE) 359 360 (* now we need to construct the return functions from the data given *) 361 362 (* Now I want to get the definitions of the functions and constants 363 that compute return values for each constructor, ie, the a-nn in 364 the definition of syntax_rec. To do this, we munge the def field 365 in each element of term_parts. Using the example above, consider the 366 phrase 367 (varcon_pat (CONpat c ap) = 1 + (varcon_atpat ap)) 368 We want to create nn, the function that will return a value for 369 items constructed using CONpat. nn should have type 370 'j->id->atpat->'m, where 'j and 'm, the return values of varcon_atpat 371 and varcon_pat, resp, are both num. So nn will have the form 372 \r:num. \c:con. \ap:atpat. <body> 373 We have to munge (1 + (varcon_atpat ap)) around to be <body>. The main 374 thing we have to do is replace recursive calls with the arguments 375 provided for that purpose. We know that ap must have 376 type atpat (since it's the second arg to constructor CONpat), and 377 so the only recursive function that can be applied to it is 378 varcon_atpat, the function being defined for that type. So we replace 379 (varcon_atpat ap) with r to get the body. Thus nn will be 380 \r. \c. \ap. 1 + r 381 If no function is defined for a type, I will create a dummy function 382 that returns one for all inputs. *) 383 384 (* lookup_ftn will tell me, for each type, if it is one of the recursive 385 types we're defining funtions on, and if so, whether the person is 386 defining a function on it and what the domain and range types of 387 such a function would be. lookup_return is the datatype returned by 388 lookup_ftn *) 389 datatype lookup_return = not_rec_type | 390 rec_ftn_info of {dom_ty:hol_type, ftn_op:term option, rng_ty:hol_type} 391 392 fun lookup_ftn (dom, (datum as {ftn_op, dom_ty, rng_ty})::ftn_type_data) = 393 if dom = dom_ty then 394 rec_ftn_info datum 395 else 396 lookup_ftn (dom, ftn_type_data) 397 | lookup_ftn (_, []) = not_rec_type 398 399 (* get_rec_vars is used when no function is being defined for this type, 400 figures out what vars to abstract over to make a constant function, 401 returns them is reverse order. all_vars initially contains the args 402 (which are variables) of the constructors; the recursive variables 403 are added on as they are computed *) 404 fun get_rec_vars (all_vars, arg::more_args, rev_rec_vars) = 405 let val ftn_info = lookup_ftn (type_of arg, ftn_type_data) 406 in 407 case ftn_info 408 of not_rec_type => 409 (* can't recurse on this arg, so add no more vars *) 410 get_rec_vars (all_vars, more_args, rev_rec_vars) 411 | rec_ftn_info {ftn_op, dom_ty, rng_ty} => 412 (* we'll have to create a recursive var for it *) 413 let val new_var = variant all_vars 414 (mk_var {Name = "r", Ty = rng_ty}) 415 in 416 get_rec_vars (new_var::all_vars, more_args, 417 new_var::rev_rec_vars) 418 end 419 end 420 | get_rec_vars (all_vars, [], rev_rec_vars) = rev_rec_vars 421 422 (* sort_cons_args is used to sort the constructor args into 423 recursive (one of the types defined in the recursive type def) 424 and nonrecursive (an existing type). This is done because the 425 return functions have the non-recursive args before the 426 recursive args, even if they were interspersed in the definition 427 of the constructor. Within those sorts, however, earlier 428 constructor args are earlier in the lists. The list returned is 429 in reverse order (i.e. rev_rec_args @ rev_nonrec_args) since 430 abstract_over_vars takes them in reverse order *) 431 fun sort_cons_args (arg::cons_args, rev_rec_args, rev_nonrec_args) = 432 let val ftn_info = lookup_ftn (type_of arg, ftn_type_data) 433 in 434 case ftn_info 435 of not_rec_type => sort_cons_args 436 (cons_args, rev_rec_args, arg::rev_nonrec_args) 437 | rec_ftn_info _ => sort_cons_args 438 (cons_args, arg::rev_rec_args, rev_nonrec_args) 439 end 440 | sort_cons_args ([], rev_rec_args, rev_nonrec_args) = 441 rev_rec_args @ rev_nonrec_args 442 443 (* replace_recursion actually does the job of replacing recursive calls 444 (like (varcon_atpat ap)) with variables (like r) in definition 445 given in order to make body of return function. It returns 446 the modified term (which will be the body of our function) and 447 the variables representing the recursions (in reverse order). The arg 448 all_vars initially contains the args (which are variables) of the 449 constructors; the recursive variables are added on as they 450 are computed *) 451 fun replace_recursion (tm, all_vars, [], rev_rec_vars) = 452 (tm, rev_rec_vars) 453 | replace_recursion (tm, all_vars, arg::args, rev_rec_vars) = 454 let val ftn_info = lookup_ftn (type_of arg, ftn_type_data) 455 in 456 case ftn_info 457 of not_rec_type => 458 (* this is a base type, no need to do recursion *) 459 replace_recursion (tm, all_vars, args, rev_rec_vars) 460 | rec_ftn_info {ftn_op = NONE, dom_ty, rng_ty} => 461 (* this is a recursive type, but there will be no 462 recursive calls on this arg since no recursive function 463 is being defined on it. Still, we need to abstract 464 over it *) 465 let val new_var = variant all_vars 466 (mk_var {Name = "r", Ty = rng_ty}) 467 in 468 replace_recursion (tm, new_var::all_vars, 469 args, new_var::rev_rec_vars) 470 end 471 | rec_ftn_info {ftn_op = SOME ftn, dom_ty, rng_ty} => 472 (* this is a recursive type and we will have to replace 473 recursive calls on it *) 474 let val term_to_replace = mk_comb {Rator = ftn, Rand = arg} 475 val new_var = variant all_vars 476 (mk_var {Name = "r", Ty = rng_ty}) 477 val sub1 = [{redex = term_to_replace, residue = new_var}] 478 in 479 replace_recursion (subst sub1 tm, new_var::all_vars, 480 args, new_var::rev_rec_vars) 481 end 482 end 483 484 (* abstract_over_vars takes as arguments the body of the function 485 we are creating and the variables we want to abstract over (in 486 reverse order), and returns the body abstracted over the vars *) 487 fun abstract_over_vars (tm, []) = tm 488 | abstract_over_vars (tm, arg::rev_args) = 489 abstract_over_vars (mk_abs {Bvar = arg, Body = tm}, 490 rev_args) 491 492 (* create_return_fun munges the RHS of an equation given in the term 493 into the function or constant (one of a - nn) needed by syntax_rec *) 494 fun create_return_fun (NONE, 495 {cons, cons_args, result_type}) = 496 (* no function defined for this type, make the function be 497 \<rec vars> <cons args -- nonrecursive ones first>. one *) 498 let val rev_sorted_args = sort_cons_args (cons_args, [], []) 499 val rev_rec_vars = get_rec_vars (cons_args, cons_args, []) 500 in 501 abstract_over_vars (abstract_over_vars (one_tm, rev_sorted_args), 502 rev_rec_vars) 503 end 504 | create_return_fun (SOME {ftn, ftn_dom, constructor, args, def}, 505 {cons, cons_args, result_type}) = 506 let val (body, rev_rec_vars) = replace_recursion (def, args, args, []) 507 val rev_sorted_args = sort_cons_args (args, [], []) 508 in 509 abstract_over_vars (abstract_over_vars (body, rev_sorted_args), 510 rev_rec_vars) 511 end 512 513 (* create list of functions and constants that create return values for 514 our mutually recursive functions *) 515 val return_functions = map create_return_fun 516 (combine (def_cases, cons_data)) 517 518 (* Now we can define our mutually recursive functions. If we specialize 519 rec_axiom to our return functions, we get a theorem that says that 520 the functions that we want to exist do exist. Actually the form 521 of the theorem is 522 ? fn1 ... fnN. (fn1 satisfies property1) /\ ... 523 (fnN satisfies propertyN) 524 where N is the number of mutually recursive types, fI is the 525 function defined for type I (using the order in which the types 526 are given in rec_axiom), and propertyI is, if a function is 527 defined for type I, definition the user gave, otherwise 528 propertyI says that the function returns one on all inputs. *) 529 val exists_thm = BETA_RULE (ISPECL return_functions rec_axiom) 530 531 (* We will need to prove a theorem something like 532 ? fn1 fn2 ... fnM. <user's definition with fnI in place of 533 functions user wants to define> 534 (where M <= N is the number of functions the user actually defined) 535 in order to do a new_specification to define the functions. 536 537 Our first step will be to get rid of all the unwanted conjuncts 538 (those that refer to types the user isn't defining a function for), 539 thus obtaining a theorem like 540 ? fn1 fn2 ... fnN. <user's definition with fnI in place of 541 functions user wants to define> 542 and later we will get rid of the undesired fnI's that we're 543 quantifying over. 544 To get this theorem we will prove a lemma (called lemma1 below) saying 545 !P Q. ((?fn1 ... fnN. P fn1 ... fnN) /\ 546 (!fn1 ... fnN. P fn1 ... fnN ==> Q fn1 ... fnN)) ==> 547 ?fn1 ... fnN. Q fn1 ... fnN 548 The idea is that P will be instantiated to 549 \fn1 fn2 ... fnN. (fn1 satisfies property1) /\ ... 550 (fnN satisfies propertyN) 551 mentioned above, and Q will be instantiated to 552 \fn1 fn2 ... fnN. <user's definition with fnI in place of 553 functions user wants to define> 554 from above. *) 555 556 (* To prove this lemma we will use TAC_PROOF. Our first task is to 557 concoct the term that is the conclusion *) 558 val (rec_ftn_vars, base_P) = strip_exists (concl exists_thm) 559 (* Let's make Ptm, which is what the P variable in our lemma will 560 eventually be instantiated to *) 561 val Ptm = list_mk_abs (rec_ftn_vars, base_P) 562 (* Pvar and Qvar will be the generic properties we'll use in the lemma *) 563 val Pvar = mk_var {Name = "P", Ty = type_of Ptm} 564 val Qvar = mk_var {Name = "Q", Ty = type_of Ptm} 565 (* make applied versions of P and Q *) 566 val Papp = list_mk_comb (Pvar, rec_ftn_vars) 567 val Qapp = list_mk_comb (Qvar, rec_ftn_vars) 568 (* make the antecedant *) 569 val conj1 = list_mk_exists (rec_ftn_vars, Papp) 570 val conj2 = list_mk_forall (rec_ftn_vars, 571 mk_imp {ant = Papp, conseq = Qapp}) 572 val ant = mk_conj {conj1 = conj1, conj2 = conj2} 573 (* make the consequent *) 574 val conseq = list_mk_exists (rec_ftn_vars, Qapp) 575 (* and now for our goal *) 576 val goal = list_mk_forall ([Pvar, Qvar], 577 mk_imp {ant = ant, conseq = conseq}) 578 (* Make a tactic for instantiating all our existential variables *) 579 fun mk_multi_exists_tac [] = ALL_TAC 580 | mk_multi_exists_tac [ftn_var] = EXISTS_TAC ftn_var 581 | mk_multi_exists_tac (ftn_var::rec_ftn_vars) = 582 (EXISTS_TAC ftn_var) THEN (mk_multi_exists_tac rec_ftn_vars) 583 val multi_exists_tac = mk_multi_exists_tac rec_ftn_vars 584 (* Prove it! *) 585 val lemma1 = TAC_PROOF 586 (([], goal), 587 (REPEAT GEN_TAC) THEN STRIP_TAC THEN multi_exists_tac THEN 588 (MP_TAC (ASSUME Papp)) THEN (ASM_REWRITE_TAC [])) 589 590 (* Specialize lemma1 to Ptm *) 591 val specP_lemma1 = BETA_RULE (SPEC Ptm lemma1) 592 593 (* we need to get some info about exists_thm: for each conjunct 594 I want the conjunct itself, the constructor and the conjunct 595 refers to, and the type of the constructor *) 596 fun get_exists_info conjunct = 597 let val (_, temp_tm) = strip_forall conjunct 598 val cons_and_args = rand (lhs temp_tm) 599 val return_type = type_of cons_and_args 600 val (constructor, _) = decompose (cons_and_args, []) 601 in 602 {cons = constructor, cons_range = return_type, conj = conjunct} 603 end 604 val exists_data = map get_exists_info 605 (strip_conj (snd (strip_exists (concl exists_thm)))) 606 607 (* addlist performs the functions, essentially, of (rev l1)@l2 *) 608 fun addlist (item::rev_list, old_list) = 609 addlist (rev_list, item::old_list) 610 | addlist ([], old_list) = old_list 611 612 (* get_conj_for_cons looks through exists_data to find the conjunct 613 associated with the constructor field of an item in def_data, 614 returns the conj found as well as exists_data with that conj 615 removed *) 616 fun get_conj_for_cons ({constructor, ftn, ftn_dom, args, def}, 617 exists_data) = 618 let fun helper (seen_data, 619 (datum as {cons, conj, cons_range})::exists_data) = 620 if constructor = cons then 621 (conj, addlist (seen_data, exists_data)) 622 else 623 helper (datum::seen_data, exists_data) 624 | helper (seen_data, []) = raise HOL_ERR 625 {origin_structure = "define_mutual_functions", 626 origin_function = "get_conj_for_cons", 627 message = ("illegal constructor " ^ (term_name constructor) ^ 628 " in definition")} 629 in 630 helper ([], exists_data) 631 end 632 (* get_conjs_for_allelse returns a list of the conjunts that apply 633 to an allelse clause, returns the list of conjs found as well 634 as exists_data with those conjs removed *) 635 fun get_conjs_for_allelse ({constructor, ftn, ftn_dom, args, def}, 636 exists_data) = 637 let fun helper (seen_data, conjs, 638 (datum as {cons, conj, cons_range})::exists_data) = 639 if ftn_dom = cons_range then 640 helper (seen_data, conj::conjs, exists_data) 641 else 642 helper (datum::seen_data, conjs, exists_data) 643 | helper (seen_data, conjs, []) = (rev conjs, rev seen_data) 644 in 645 helper ([], [], exists_data) 646 end 647 648 (* this function goes through the list, picking out the conjunc(s) 649 that go with each conjunct in def. There might be more than one 650 conjunct since the conjunct in def might be an "allelse" one. 651 As we find the conjuncts the functions get_conjs_for_allelse and 652 get_conj_for_cons eliminate them from the version of exists_data 653 that they return so that when we come across an "allelse" clause 654 we will know which clauses have already been used for the non 655 "allelse" conjuncts *) 656 fun mk_Qtm_body ((datum as {ftn, ftn_dom, constructor, args, def}) 657 ::def_data, 658 exists_data) = 659 if is_var constructor then 660 if #Name (dest_var constructor) = "allelse" then 661 let val (conjs, exists_data2) = 662 get_conjs_for_allelse (datum, exists_data) 663 in 664 conjs@(mk_Qtm_body (def_data, exists_data2)) 665 end 666 else 667 raise HOL_ERR {origin_structure = "define_mutual_functions", 668 origin_function = "mk_Qtm_body", 669 message = ("illegal variable " ^ 670 (term_name constructor) ^ 671 " in definition")} 672 else 673 let val (conj, exists_data2) = 674 get_conj_for_cons (datum, exists_data) 675 in 676 conj::(mk_Qtm_body (def_data, exists_data2)) 677 end 678 | mk_Qtm_body ([], exists_data) = [] 679 680 (* Make Qtm, the term Q will be instantiated to *) 681 val Qtm = list_mk_abs (rec_ftn_vars, 682 list_mk_conj (mk_Qtm_body (def_data, exists_data))) 683 val specPQ_lemma1 = BETA_RULE(SPEC Qtm specP_lemma1) 684 685 (* Now want to prove !fn1 ... fnN. P fn1 ... fnN ==> Q fn1 ... fnN *) 686 val goal = #conj2 (dest_conj (#ant (dest_imp (concl specPQ_lemma1)))) 687 (* this goal is pretty easy to prove for the variables fn1 thru' 688 fnN, since all the conjuncts in Qtm are present in Ptm, but would take 689 a long time to verify for the particular functions that make Ptn true. 690 This is why we are using lemma1 in the first place *) 691 val lemma2 = TAC_PROOF 692 (([],goal), 693 (REPEAT GEN_TAC) THEN STRIP_TAC THEN (REPEAT CONJ_TAC) THEN 694 (FIRST_ASSUM ACCEPT_TAC)) 695 696 (* now that we have both ?fn1 ... fnN. Ptm fn1 ... fnN (in exists_thm) 697 and !fn1 ... fnN. Ptm fn1 ... fnN ==> Qtm fn1 ... fnN) (in lemma2) we 698 now conclude that ?fn1 ... fnN. Qtm fn1 ... fnN (which is existsQ) *) 699 val existsQ = MP specPQ_lemma1 (CONJ exists_thm lemma2) 700 701 (* Now we need to eliminate from the f1 ... fN 702 the functions the user didn't want to define (we defined them 703 as functions returning one). We do this using a rewrite. *) 704 val sat_thm = REWRITE_RULE [] existsQ 705 706 (* Now we want to use sat_thm in a new_specification. 707 To do this we need the names of the functions we are defining, 708 in the order in which the constructors for it are presented in 709 rec_axiom. ftn_type_data will give us this info *) 710 val new_ftn_names = 711 foldr (fn ({ftn_op = NONE, dom_ty, rng_ty}, namelist) => 712 namelist 713 | ({ftn_op = SOME ftn, dom_ty, rng_ty}, namelist) => 714 (#Name (dest_var ftn))::namelist) 715 [] 716 ftn_type_data 717 718 val consts = 719 case fixities 720 of SOME fixes => (map2 721 (fn name => fn fixity => {const_name = name, 722 fixity = fixity}) 723 new_ftn_names 724 fixes 725 handle (HOL_ERR _) => raise 726 HOL_ERR {origin_structure = "top", 727 origin_function = 728 "define_mutual_functions", 729 message = 730 "term is not constant or var"}) 731 | NONE => map (fn name => {const_name = name, fixity = Prefix}) 732 new_ftn_names 733 734 (* Now we do our definition. *) 735 val final = new_specification 736 {name = specification_name, 737 consts = consts, 738 sat_thm = sat_thm} 739 740 in 741 final 742 end 743 744val _ = Parse.temp_set_grammars ambient_grammars 745end; 746 747(* Tests: 748 749(* The following is an example of a term used to define mutually 750 recursive functions operating on the syntax classes. It defines a 751 function that counts the number of variables and constructors used 752 in a pattern. *) 753 754val def = 755--`(varcon_pat (ATPATpat ap) = varcon_atpat ap) /\ 756 (varcon_pat (CONpat c ap) = 1 + (varcon_atpat ap)) /\ 757 (varcon_pat (EXCONpat e a) = 1 + (varcon_atpat a)) /\ 758 (varcon_atpat WILDCARDatpat = 0) /\ 759 (varcon_atpat (SCONatpat sc) = 0) /\ 760 (varcon_atpat (VARatpat v) = 1) /\ 761 (varcon_atpat (CONatpat c) = 1) /\ 762 (varcon_atpat (EXCONatpat e) = 1) /\ 763 (varcon_atpat RECORD1atpat = 0) /\ 764 (varcon_atpat (RECORD2atpat pr) = varcon_patrow pr) /\ 765 (varcon_atpat (PARatpat p) = varcon_pat p) /\ 766 (varcon_patrow DOTDOTDOT = 0) /\ 767 (varcon_patrow (PATROW1 l p) = varcon_pat p) /\ 768 (varcon_patrow (PATROW2 l p pr) = (varcon_pat p) + (varcon_patrow pr))`-- 769 770val def = 771--`(varcon_pat (ATPATpat ap) = varcon_atpat ap) /\ 772 (varcon_pat (CONpat c ap) = 1 + (varcon_atpat ap)) /\ 773 (varcon_pat (EXCONpat e a) = 1 + (varcon_atpat a)) /\ 774 (varcon_atpat (VARatpat v) = 1) /\ 775 (varcon_atpat (CONatpat c) = 1) /\ 776 (varcon_atpat (EXCONatpat e) = 1) /\ 777 (varcon_atpat (RECORD2atpat pr) = varcon_patrow pr) /\ 778 (varcon_atpat (PARatpat p) = varcon_pat p) /\ 779 (varcon_atpat allelse = 0) /\ 780 (varcon_patrow DOTDOTDOT = 0) /\ 781 (varcon_patrow (PATROW1 l p) = varcon_pat p) /\ 782 (varcon_patrow (PATROW2 l p pr) = (varcon_pat p) + (varcon_patrow pr))`-- 783 784val def = 785--`(varcon_pat (ATPATpat ap) = varcon_atpat ap) /\ 786 (varcon_pat (CONpat c ap) = 1 + (varcon_atpat ap)) /\ 787 (varcon_pat (EXCONpat e a) = 1 + (varcon_atpat a)) /\ 788 (varcon_atpat (VARatpat v) = 1) /\ 789 (varcon_atpat (CONatpat c) = 1) /\ 790 (varcon_atpat (EXCONatpat e) = 1) /\ 791 (varcon_atpat (RECORD2atpat pr) = varcon_patrow pr) /\ 792 (varcon_atpat (PARatpat p) = varcon_pat p) /\ 793 (varcon_atpat allelse = 0) /\ 794 (varcon_patrow DOTDOTDOT = 0) /\ 795 (varcon_patrow (PATROW1 l p) = varcon_pat p) /\ 796 (varcon_patrow (PATROW2 l p pr) = (varcon_pat p) + (varcon_patrow pr))`-- 797 798val def = 799--`(foo33 (ATEXPexp ae) = T) /\ 800 (foo33 allelse = 801 eval_exp arg ^initial_state ^initial_env ^initial_state 802 (PACKvp ^Bind_pack))`-- 803 804end tests 805 *) 806