1(* 2set_trace "Unicode" 0; 3set_trace "pp_annotations" 0; 4*) 5 6use (HOLDIR^"/src/pfl/defchoose"); 7 8(* quietdec := true; *) 9open numSyntax optionSyntax pairSyntax optionTheory; 10(* quietdec := false; *) 11 12 13val suc_zero = ``SUC 0``; 14 15(*---------------------------------------------------------------------------*) 16(* Examples *) 17(*---------------------------------------------------------------------------*) 18 19val ack_tm = 20 ``ack m n = 21 if m=0 then n + 1 else 22 if n=0 then ack (m-1) 1 else 23 ack (m-1) (ack m (n-1))``; 24 25val ack1_tm = 26 ``(ack 0 n = n+1) /\ 27 (ack m 0 = ack (m-1) 1) /\ 28 (ack (SUC m) (SUC n) = ack m (ack (SUC m) n))``; 29 30val ack2_tm = 31 ``(!n. ack 0 n = n+1) /\ 32 (!m. ack m 0 = ack (m-1) 1) /\ 33 (!m n. ack (SUC m) (SUC n) = ack m (ack (SUC m) n))``; 34 35val fact_tm = ``fact n = if n=0 then 1 else n * fact (n-1)``; 36 37val fact1_tm = ``fact n = if n=0 then 1 else (n + n) * (13 * fact (n-1) + n)``; 38 39val fact2_tm = ``fact n = if n=0 then 1 else 40 (n + fact (n-1)) * (13 * fact (n-1) + n)``; 41 42val fact3_tm = ``fact n = if n=0 then 1 else 43 let x = n + n 44 in x * fact (n-1)``; 45 46val fact4_tm = ``fact n = if n=0 then 1 else 47 let x = fact (n-1) 48 in x + n * x``; 49 50val fact5_tm = ``fact n = if n=0 then 1 else 51 let x = fact (n-1) 52 and y = n + n 53 in y + n * x``; 54 55val map_tm = ``(map f [] = []) /\ (map f (h::t) = f h :: map f t)``; 56val f91_tm = ``f91 n = if n>100 then n-10 else f91(f91(n+11))``; 57val f91a_tm = ``f91 n = if n>100 then n-10 else n + f91(f91(n+11))``; 58 59val Z_tm = ``Z n = if n=0 then 0 else Z(Z(Z(n-1)))``; 60val Z1_tm = ``Z1 n = if n=0 then 0 else SUC(SUC(Z(n-1))) + Z1 (n-1)``; 61val Z2_tm = ``Z1 n = if n=0 then 0 else SUC(SUC(Z1(n-1))) + Z1 (n-1)``; 62 63val partle_tm = 64 ``(part x [] = ([],[])) /\ 65 (part x (h::t) = 66 let (l1,l2) = part x t 67 in if h <= x then (h::l1, l2) else (l1,h::l2))``; 68 69val part_tm = 70 ``(part P [] = ([],[])) /\ 71 (part P (h::t) = 72 let (l1,l2) = part P t 73 in if P h then (h::l1, l2) else (l1,h::l2))``; 74 75val qsort0_tm = 76 ``(qsort [] = []) /\ 77 (qsort (h::t) = 78 let l1 = FILTER (\x. x <= h) t in 79 let l2 = FILTER (\x. x > h) t 80 in qsort l1 ++ [h] ++ qsort l2)``; 81 82val qsort1_tm = 83 ``(qsort [] = []) /\ 84 (qsort (h::t) = 85 let l1 = FILTER (\x. x <= h) t in 86 let l2 = FILTER (\x. x > h) t 87 in qsort l1 ++ [h] ++ qsort l2)``; 88 89val qsort2_tm = 90 ``(qsort [] = []) /\ 91 (qsort (h::t) = 92 let l1 = FILTER (\x. x <= h) t 93 and l2 = FILTER (\x. x > h) t 94 in qsort l1 ++ [h] ++ qsort l2)``; 95 96val qsort3_tm = 97 ``(qsort [] = []) /\ 98 (qsort (h::t) = 99 let (l1,l2) = part (\x. x <= h) t 100 in qsort l1 ++ [h] ++ qsort l2)``; 101 102val qsort4_tm = 103 ``(qsort R [] = []) /\ 104 (qsort R (h::t) = 105 let (l1,l2) = part (\x. R x h) t 106 in qsort R l1 ++ [h] ++ qsort R l2)``; 107 108(*---------------------------------------------------------------------------*) 109(* Code *) 110(*---------------------------------------------------------------------------*) 111(* 112val pair_case_tm = prim_mk_const{Name="pair_case",Thy="pair"}; 113 114fun mk_pair_case (f,a) = 115 let val theta = match_type (type_of pair_case_tm) (type_of f) 116 in list_mk_comb(inst theta pair_case_tm,[f,a]) 117 end; 118*) 119 120fun list_mk_option_cases u d ty = 121 itlist (fn (a,v) => fn c => 122 mk_option_case (mk_none ty, mk_abs(v, c), a)) 123 u d; 124 125(*---------------------------------------------------------------------------*) 126(* Splits tmlist into a triple (u,d,vs) in which u is a list of pairs of *) 127(* form (term,var), d is a list of terms, and vs is a list of used variables *) 128(* The intent is that tmlist represents a list of terms, some of which are *) 129(* statically known to be defined, i.e. are of the form "SOME t". The other *) 130(* terms are not statically known to be defined. It is possible that they *) 131(* might statically be known to be undefined, i.e. NONE, but that is not *) 132(* catered for at the moment. If a term is not of the form SOME t, then, we *) 133(* have to put the definedness test into the term structure. This is done *) 134(* by making case analysis on an option. So ... d is the transformed tmlist *) 135(* and u contains the elements of tmlist that can't be trivially shown to *) 136(* be defined. *) 137(*---------------------------------------------------------------------------*) 138 139fun split_args tmlist fvs = 140 itlist (fn t => fn (u,d,vs) => 141 if is_some t then (u,dest_some t::d,vs) 142 else let val ty = dest_option(type_of t) 143 val v = variant vs (mk_var("v",ty)) 144 in ((t,v)::u, v::d, (v::vs)) 145 end) tmlist ([],[],fvs); 146 147(*---------------------------------------------------------------------------*) 148(* Partiality transformation. Note that it is, at present, really only *) 149(* applicable to first-order terms. Explicit lambdas are handled, but not *) 150(* other terms of functional type. *) 151(*---------------------------------------------------------------------------*) 152 153fun partialize env tm = 154 if is_var tm orelse is_const tm then mk_some tm else 155 if is_abs tm then 156 let val (v,M) = dest_abs tm 157 in mk_abs(v,partialize env M) 158 end else 159 if is_cond tm then 160 let val (b,t1,t2) = dest_cond tm 161 val b' = partialize env b 162 val t1' = partialize env t1 163 val t2' = partialize env t2 164 in 165 if is_some b' andalso is_some t1' andalso is_some t2' 166 then mk_some (mk_cond(dest_some b', dest_some t1', dest_some t2')) 167 else 168 if is_some b' then mk_cond (dest_some(b'), t1', t2') 169 else 170 let val rty = type_of tm 171 val v = variant (free_vars tm) (mk_var("v",bool)) 172 in mk_option_case (mk_none rty, mk_abs(v, mk_cond(v,t1',t2')), b') 173 end 174 end else 175 if TypeBase.is_case tm then 176 let val (case_tm,ob,clauses) = TypeBase.dest_case tm 177 val ob' = partialize env ob 178 val clauses' = map (I ## partialize env) clauses 179 in 180 if is_some ob' andalso Lib.all (is_some o snd) clauses' 181 then mk_some (TypeBase.mk_case 182 (dest_some ob',map (I##dest_some) clauses')) 183 else 184 if is_some ob' then TypeBase.mk_case (dest_some(ob'), clauses') 185 else let val rty = type_of tm 186 val v = variant (free_vars tm) (mk_var("v",type_of ob)) 187 in mk_option_case 188 (mk_none rty, mk_abs(v, TypeBase.mk_case(v,clauses')), ob') 189 end 190 end else 191 if is_let tm then 192 let val (bindings,M) = dest_anylet tm 193 val bindings' = zip (map fst bindings) 194 (map (partialize env o snd) bindings) 195 val M' = partialize env M 196 in itlist (fn (v,t) => fn body => 197 if is_some t 198 then mk_anylet ([(v,dest_some t)],body) 199 else mk_option_case 200 (mk_none (dest_option(type_of t)),mk_pabs(v,body), t)) 201 bindings' M' 202 end 203 else (* is_comb tm *) 204 let val (f,args) = strip_comb tm 205 val args' = map (partialize env) args 206 val (u,d,vs) = split_args args' (free_vars tm) 207 val fapp = case subst_assoc (equal f) env 208 of NONE => mk_some(list_mk_comb(f,d)) 209 | SOME g => list_mk_comb(g,d) 210 in 211 list_mk_option_cases u fapp (type_of tm) 212 end; 213 214fun optional fvar = 215 let val (fname,ty) = dest_var fvar 216 val pfname = "p"^fname 217 val (src,target) = strip_fun ty 218 val ty' = list_mk_fun (src, mk_option target) 219 in 220 fvar |-> mk_var(pfname, ty') 221 end; 222 223fun indexed d fvar = 224 let val (fname,ty) = dest_var fvar 225 val ifname = "i"^fname 226 val (src,target) = strip_fun ty 227 val ty' = list_mk_fun (num::src, mk_option target) 228 in 229 fvar |-> mk_comb(mk_var(ifname, ty'),d) 230 end; 231 232fun mysubst theta v = Option.valOf(subst_assoc (equal v) theta); 233 234fun mk_typed_vars name vlist tylist = 235 let fun vary (away,[],vars) = rev vars 236 | vary (away,ty::tyl,vars) = 237 let val v = variant away (mk_var(name,ty)) 238 in vary (v::away,tyl,v::vars) 239 end 240 in Lib.with_flag 241 (Globals.priming, SOME"") vary (vlist,tylist,[]) 242 end; 243 244fun single x = [x]; 245 246fun new_base_cases eqns vars = 247 let fun munge fns [] vars bcases = ([],bcases) 248 | munge fns (h::t) vars bcases = 249 let val (f,args) = strip_comb(lhs (snd(strip_forall h))) in 250 if mem f fns 251 then (append(single h) ## I) (munge fns t vars bcases) 252 else let val h0_vars = mk_typed_vars "v" vars (tl (map type_of args)) 253 val h0 = mk_eq(list_mk_comb(f,zero_tm::h0_vars), 254 mk_none(dest_option(type_of(rhs h)))) 255 in (append [h0,h]##I) 256 (munge (f::fns) t (h0_vars@vars) (h0::bcases)) 257 end 258 end 259 in munge [] eqns vars [] 260 end; 261 262val option_case_rewrite = Q.prove 263(`option_case a g (option_case NONE f ob) = 264 option_case a (\v. option_case a g (f v)) ob`, 265 Cases_on `ob` THEN RW_TAC std_ss []); 266 267val linearize_case = QCONV (SIMP_CONV std_ss [option_case_rewrite]); 268 269fun mk_peqns ufns L R = 270 let val thetaP = map optional ufns 271 val L' = map (partialize thetaP) L 272 val R' = map (partialize thetaP) R 273 val eqns = map mk_eq (zip L' R') 274 in 275 map (rhs o concl o linearize_case) eqns 276 end; 277 278(*---------------------------------------------------------------------------*) 279(* Run term through the partiality transformation and build the partial and *) 280(* indexed versions of the equations. *) 281(*---------------------------------------------------------------------------*) 282 283fun alt_eqns tm = 284 let val eqns = map (snd o strip_forall) (strip_conj tm) 285 val (L,R) = unzip(map dest_eq eqns) 286 val (fns,args) = unzip(map strip_comb L) 287 val ufns = mk_set fns (* unique fns, should all be variables *) 288 val peqns = mk_peqns ufns L R 289 (* now make ieqns *) 290 val vars = all_vars tm 291 val d = variant vars (mk_var("d",num)) 292 val thetaL = map (indexed (mk_suc d)) ufns 293 val thetaR = map (indexed d) ufns 294 val fns' = map (mysubst thetaL) fns 295 val L' = map2 (curry list_mk_comb) fns' args 296 val R' = map (partialize thetaR) R 297 val ieqns1 = map mk_eq (zip L' R') 298 val (ieqns2,base_cases) = new_base_cases ieqns1 (d::vars) 299 val ieqns = map (rhs o concl o linearize_case) ieqns2 300 in 301 (peqns, ieqns, ufns, base_cases) 302 end; 303 304(*---------------------------------------------------------------------------*) 305(* Input: ifn 0 v0 ... vn = NONE *) 306(*---------------------------------------------------------------------------*) 307 308fun limit_spec_def base_case = 309 let val (fvar,args) = strip_comb(lhs base_case) 310 val args' = tl args 311 val (fname,ty) = dest_var fvar 312 val fconst = mk_const (fname,ty) 313 val lim_name = fname^"Lim" 314 val limvar = Lib.with_flag(Globals.priming,SOME"_") 315 (variant (all_vars base_case)) (mk_var(lim_name,num)) 316 val fapp = mk_is_some(list_mk_comb(fconst, limvar::args')) 317 val tm' = list_mk_forall(args',mk_exists(limvar,fapp)) 318 in 319 DEFCHOOSE (lim_name^"_spec", lim_name, tm') 320 end 321 handle e => raise wrap_exn "Index" "limit_spec_def" e; 322 323fun pfn_def fname limspec_thm = 324 let val tm = snd(dest_imp(snd(strip_forall(concl limspec_thm)))) 325 val ifn_app = dest_is_some tm 326 val (const,args) = strip_comb ifn_app 327 val args' = tl args 328 val ty = list_mk_fun(map type_of args',type_of ifn_app) 329 val pfn_name = "p"^fname 330 val pfn_var = mk_var(pfn_name,ty) 331 val deftm = mk_eq(list_mk_comb(pfn_var,args'),ifn_app) 332 in 333 new_definition (pfn_name^"_def",deftm) 334 end 335 handle e => raise wrap_exn "Index" "pfn_def" e; 336 337fun fn_def name pfn_def = 338 let val pfn_app = lhs(snd(strip_forall(concl pfn_def))) 339 val (pfn,args) = strip_comb pfn_app 340 val (dtys,rty) = strip_fun (type_of pfn) 341 val fn_var = mk_var(name,list_mk_fun(dtys,dest_option rty)) 342 val lapp = list_mk_comb(fn_var,args) 343 val deftm = mk_eq(lapp,mk_the pfn_app) 344 in 345 new_definition (name^"_def",deftm) 346 end 347 handle e => raise wrap_exn "Index" "fn_def" e; 348 349fun in_dom_def name fn_def = 350 let val (lapp,rapp) = dest_eq(snd(strip_forall(concl fn_def))) 351 val (lfn,args) = strip_comb lapp 352 val right = mk_is_some(dest_the rapp) 353 val dname = "in_dom_"^name 354 val dom_var = mk_var(dname,list_mk_fun(map type_of args,bool)) 355 val deftm = mk_eq(list_mk_comb(dom_var, args),right) 356 in 357 new_definition (dname^"_def",deftm) 358 end 359 handle e => raise wrap_exn "Index" "in_dom_def" e; 360 361fun mk_defs tm = 362 let open TotalDefn 363 val (peqns, ieqns, vfns, base_cases) = alt_eqns tm 364 val ivar = fst(strip_comb(lhs(snd(strip_forall(hd ieqns))))) 365 val iname = fst(dest_var ivar) 366 val idef = tDefine iname `^(list_mk_conj ieqns)` (WF_REL_TAC`measure FST`) 367 val limspec_thms = map limit_spec_def base_cases 368 val names = map (fst o dest_var) vfns 369 val pfn_defs = map2 pfn_def names limspec_thms 370 val fn_defs = map2 fn_def names pfn_defs 371 val dom_defs = map2 in_dom_def names fn_defs 372 in 373 (peqns,idef,limspec_thms,pfn_defs,fn_defs,dom_defs) 374 end; 375 376fun cross_prod [] l2 = [] 377 | cross_prod (h::t) l2 = map (pair h) l2 @ cross_prod t l2; 378 379fun merge pn ((alist,b),(blist,e)) = (alist@[if pn then b else mk_neg b]@blist,e); 380 381fun merge_paths bpaths pospaths negpaths = 382 map (merge true) (cross_prod bpaths pospaths) @ 383 map (merge false) (cross_prod bpaths negpaths); 384 385(*---------------------------------------------------------------------------*) 386(* Collect maximal non-if terms on rhs, plus accumulate recursive calls. *) 387(*---------------------------------------------------------------------------*) 388 389fun paths vfns tm = 390 if is_cond tm 391 then let val (b,t1,t2) = dest_cond tm 392 in merge_paths (paths vfns b) (paths vfns t1) (paths vfns t2) 393 end else 394 if TypeBase.is_case tm 395 then let val (cconst,ob,clauses) = TypeBase.dest_case tm 396 val (pats,rhsl) = unzip clauses 397 val plists = map (paths vfns) rhsl 398 fun patch pat plist = map (fn (ctxt,e) => (mk_eq(ob,pat)::ctxt,e)) plist 399 val patched = map2 patch pats plists 400 in flatten patched 401 end else 402 if is_let tm 403 then let val (binds, body) = dest_anylet tm 404 val plist = paths vfns body 405 fun patch (x,M) (ctxt,e) = (mk_eq(x,M)::ctxt, body) 406 in map (fn path => itlist patch binds path) plist 407 end else 408 if is_comb tm 409 then let val (f,_) = strip_comb tm 410 in if mem f vfns 411 then [([mk_is_some tm],tm)] 412 else [([],tm)] 413 end 414 else [([],tm)]; 415 416fun list_mk_conj_imp ([],b) = b 417 | list_mk_conj_imp (blist,b) = mk_imp(list_mk_conj blist,b); 418 419(*---------------------------------------------------------------------------*) 420(* Adding index pattern (0,SUC) may duplicate clauses, which is unfortunate, *) 421(* because I can't then just use peqns to generate my proof obligations. *) 422(* Instead, I have to use the post-pattern match translation arising from *) 423(* idef and then change those into corresponding pfn equations. That will *) 424(* ensure that the idef will always be able to be applied as a rewrite in *) 425(* proofs. Example : ack 0 n = SOME(n+1), but pattern-match translation with *) 426(* depth added results in this turning into two equations *) 427(* *) 428(* iack (SUC d) 0 0 = SOME(0+1) and iack (SUC d) 0 (SUC n) = SOME(SUC n + 1) *) 429(* *) 430(* so if we generated a pack 0 n = SOME (n+1) goal that wouldn't work because*) 431(* the rewrite rules for iack are too specific to rewrite that. *) 432(*---------------------------------------------------------------------------*) 433 434fun pgoals peqns idef = 435 let fun fn_of clause = fst(strip_comb(lhs(snd(strip_forall clause)))) 436 val vpfns = mk_set(map fn_of peqns) 437 val cpfns = map (mk_const o dest_var) vpfns 438 val idefs = strip_conj(snd(strip_forall(concl idef))) 439 val idefs' = map (snd o strip_forall) (tl idefs) 440 val ifns = mk_set(map fn_of idefs') 441 val _ = assert (fn () => length ifns = length cpfns) () 442 fun mk_rule ifn pfn = mk_thm([],``^ifn ^(mk_var("n",num)) = ^pfn``) 443 val rules = map2 mk_rule ifns cpfns 444 fun transform ieqn = rhs(concl(QCONV(REWRITE_CONV rules) ieqn)) 445 val peqns' = map transform idefs' 446 val plists = map (fn eqn => (lhs eqn, paths vpfns (rhs eqn))) peqns' 447 fun mk_goal left (ctxt,e) = list_mk_conj_imp(ctxt,mk_eq(left,e)) 448 fun mk_goals (left,list) = map (mk_goal left) list 449 val raw_goals = flatten (map mk_goals plists) 450 in 451 raw_goals 452 end; 453 454fun test tm = 455 let val (peqns,idef,limspec_thms,pfn_defs,fn_defs,dom_defs) = mk_defs tm 456 val goals = pgoals peqns idef 457 in 458 app (fn tm => ignore(set_goal([],tm))) (rev goals); 459 (peqns,idef,limspec_thms,pfn_defs,fn_defs,dom_defs) 460 end; 461 462STOP; 463 464 465 466fun BASE_DEFINED_TAC idef limspec ifn_def_pos (asl,goal) = 467 let val (ifn,args) = strip_comb(lhs goal) 468 val args' = tl args 469 val subgoal = mk_is_some(list_mk_comb(ifn,suc_zero::args')) 470 val fact = EQT_ELIM 471 (REWRITE_CONV ([idef,IS_SOME_DEF]@map ASSUME asl) subgoal) 472 in 473 CHOOSE_THEN SUBST_ALL_TAC 474 (MATCH_MP ifn_def_pos (MATCH_MP limspec fact)) 475 end (asl,goal) 476 handle e => raise wrap_exn "Index" "BASE_DEFINED_TAC" e; 477 478fun pbase_clause pfn_def idef limspec ifn_def_pos = 479 REPEAT STRIP_TAC THEN REPEAT BasicProvers.VAR_EQ_TAC THEN 480 PURE_REWRITE_TAC [pfn_def] THEN 481 BASE_DEFINED_TAC idef limspec ifn_def_pos THEN 482 ASM_REWRITE_TAC [idef] 483 484fun precursive_clause pfn_def idef limspec = ... 485 486val (peqns,idef,limspec_thms,pfn_defs,fn_defs,dom_defs) = test ack_tm; 487 488(* Base case *) 489val [pfn_def] = pfn_defs; 490val [limspec] = limspec_thms; 491val ifn_def_pos = Q.prove 492(`!d m n. IS_SOME(iack d m n) ==> ?e. d = SUC e`, 493 Cases THEN RW_TAC std_ss [idef]); 494 495e (pbase_clause pfn_def idef limspec ifn_def_pos); 496 497(* Recursive case *) 498(* Recursive case *) 499 500dropn 12; 501 502(* factorial *) 503val (peqns,idef,limspec_thms,pfn_defs,fn_defs,dom_defs) = test fact_tm; 504 505val [pfn_def] = pfn_defs; 506val [limspec] = limspec_thms; 507val ifn_def_pos = Q.prove 508(`!d n. IS_SOME(ifact d n) ==> ?e. d = SUC e`, 509 Cases THEN RW_TAC std_ss [idef]); 510 511(* Base case *) 512e (pbase_clause pfn_def idef limspec ifn_def_pos); 513 514(*Recursive case *) 515 516(* 91 *) 517val (peqns,idef,limspec_thms,pfn_defs,fn_defs,dom_defs) = test f91_tm; 518 519val [pfn_def] = pfn_defs; 520val [limspec] = limspec_thms; 521val ifn_def_pos = Q.prove 522(`!d n. IS_SOME(if91 d n) ==> ?e. d = SUC e`, 523 Cases THEN RW_TAC std_ss [idef]); 524 525(* Base case *) 526e (pbase_clause pfn_def idef limspec ifn_def_pos); 527 528(* Ack by complex patterns ... fails because of pattern expansion. *) 529val (peqns,idef,limspec_thms,pfn_defs,fn_defs,dom_defs) = test ack1_tm; 530 531(* Base case *) 532val [pfn_def] = pfn_defs; 533val [limspec] = limspec_thms; 534val ifn_def_pos = Q.prove 535(`!d m n. IS_SOME(iack d m n) ==> ?e. d = SUC e`, 536 Cases THEN RW_TAC std_ss [idef]); 537 538e (pbase_clause pfn_def idef limspec ifn_def_pos); 539drop(); 540e (pbase_clause pfn_def idef limspec ifn_def_pos); 541 542(* Recursive case *) 543(* Recursive case *) 544