1(* ========================================================================= *) 2(* *) 3(* Inductive Definitions (John Harrison) *) 4(* *) 5(* ========================================================================= *) 6 7structure InductiveDefinition :> InductiveDefinition = 8struct 9 10open HolKernel boolLib liteLib refuteLib AC Ho_Rewrite; 11 12(* Fix the grammar used by this file *) 13structure Parse = 14struct 15 open Parse 16 val (Type,Term) = Parse.parse_from_grammars boolTheory.bool_grammars 17 fun == q x = Type q 18end 19open Parse 20 21(*--------------------------------------------------------------------------- 22 Variants. We re-define the kernel "variant" function here because 23 of a subtle difference between Hol98 variant and Hol88/light 24 variant functions: the former only looks at strings, while the 25 latter look at variables. For example 26 27 variant [`x:bool`] `x:'a` 28 29 yields x' in Hol98, but `x` in the latter (I think). The following 30 version of variant also does not vary away from constants with the 31 same name, maybe it should. 32 ---------------------------------------------------------------------------*) 33 34local fun prime v = let val (n,ty) = dest_var v in mk_var(n^"'",ty) end 35in 36fun vary V v = if mem v V then vary V (prime v) else v 37end 38 39(* ------------------------------------------------------------------------- *) 40(* Produces a sequence of variants, considering previous inventions. *) 41(* ------------------------------------------------------------------------- *) 42 43fun variants av [] = [] 44 | variants av (h::t) = 45 let val vh = vary av h 46 in vh::variants (vh::av) t 47 end; 48 49(* ------------------------------------------------------------------------- *) 50(* Apply a destructor as many times as elements in list. *) 51(* ------------------------------------------------------------------------- *) 52 53fun nsplit dest clist x = 54 if null clist then ([],x) else 55 let val (l,r) = dest x 56 val (ll,y) = nsplit dest (tl clist) r 57 in (l::ll,y) 58 end;; 59 60(* ------------------------------------------------------------------------- *) 61(* Strip off exactly n arguments from combination. *) 62(* ------------------------------------------------------------------------- *) 63 64val strip_ncomb = 65 let fun strip(n,tm,acc) = 66 if n < 1 then (tm,acc) else 67 let val (l,r) = dest_comb tm 68 in strip(n - 1,l,r::acc) 69 end 70 in fn n => fn tm => strip(n,tm,[]) 71 end;; 72 73(* ------------------------------------------------------------------------- *) 74(* Share out list according to pattern in list-of-lists. *) 75(* ------------------------------------------------------------------------- *) 76 77fun shareout [] _ = [] 78 | shareout (h::t) all = 79 let val (l,r) = split_after (length h) all 80 in l::shareout t r 81 end; 82 83(* ------------------------------------------------------------------------- *) 84(* Produce a set of reasonably readable arguments, using variants if needed. *) 85(* ------------------------------------------------------------------------- *) 86 87val make_args = 88 let fun margs n avoid tys = 89 if null tys then [] else 90 let val v = variant avoid (mk_var("a"^(int_to_string n),hd tys)) 91 in v::margs (n + 1) (v::avoid) (tl tys) 92 end 93 in margs 0 end;; 94 95(* ------------------------------------------------------------------------- *) 96(* Grabs conclusion of rule, whether or not it has an antecedant. *) 97(* ------------------------------------------------------------------------- *) 98 99fun getconcl tm = 100 let val bod = repeat (snd o dest_forall) tm 101 in snd(dest_imp bod) handle HOL_ERR _ => bod 102 end;; 103 104(* ------------------------------------------------------------------------- *) 105(* Likewise, but quantify afterwards. *) 106(* ------------------------------------------------------------------------- *) 107 108fun HALF_BETA_EXPAND args th = GENL args (RIGHT_BETAS args th);; 109 110(* ------------------------------------------------------------------------- *) 111(* Converse of SIMPLE_DISJ_CASES, i.e. P \/ Q |- R => P |- R, Q |- R *) 112(* ------------------------------------------------------------------------- *) 113 114fun SIMPLE_DISJ_PAIR th = 115 let val (l,r) = dest_disj(hd(hyp th)) 116 in (PROVE_HYP (DISJ1 (ASSUME l) r) th,PROVE_HYP (DISJ2 l (ASSUME r)) th) 117 end;; 118 119(* ------------------------------------------------------------------------- *) 120(* Iterated FORALL_IMP_CONV: (!x1..xn. P[xs] ==> Q) => (?x1..xn. P[xs]) ==> Q*) 121(* ------------------------------------------------------------------------- *) 122 123val lhand = rand o rator;; 124 125fun FORALL_IMPS_CONV tm = 126 let val (avs,bod) = strip_forall tm 127 val th1 = DISCH tm (UNDISCH(SPEC_ALL(ASSUME tm))) 128 val th2 = itlist SIMPLE_CHOOSE avs th1 129 val tm2 = hd(hyp th2) 130 val th3 = DISCH tm2 (UNDISCH th2) 131 val th4 = ASSUME (concl th3) 132 val ant = lhand bod 133 val th5 = itlist SIMPLE_EXISTS avs (ASSUME ant) 134 val th6 = GENL avs (DISCH ant (MP th4 th5)) 135 in IMP_ANTISYM_RULE (DISCH_ALL th3) (DISCH_ALL th6) end;; 136 137(* ------------------------------------------------------------------------- *) 138(* (!x1..xn. P1[xs] ==> Q[xs]) /\ ... /\ (!x1..xn. Pm[xs] ==> Q[xs]) *) 139(* => (!x1..xn. P1[xs] \/ ... \/ Pm[xs] ==> Q[xs]) *) 140(* ------------------------------------------------------------------------- *) 141 142fun AND_IMPS_CONV tm = 143 let val ths = CONJUNCTS(ASSUME tm) 144 val avs = fst(strip_forall(concl(hd ths))) 145 val thl = map (DISCH tm o UNDISCH o SPEC_ALL) ths 146 val th1 = end_itlist SIMPLE_DISJ_CASES thl 147 val tm1 = hd(hyp th1) 148 val th2 = GENL avs (DISCH tm1 (UNDISCH th1)) 149 val tm2 = concl th2 150 val th3 = DISCH tm2 (UNDISCH (SPEC_ALL (ASSUME tm2))) 151 val (thts,tht) = nsplit SIMPLE_DISJ_PAIR (tl ths) th3 152 fun proc_fn th = 153 let val t = hd(hyp th) in GENL avs (DISCH t (UNDISCH th)) 154 end 155 val th4 = itlist (CONJ o proc_fn) thts (proc_fn tht) 156 in IMP_ANTISYM_RULE (DISCH_ALL th2) (DISCH_ALL th4) end;; 157 158(* ------------------------------------------------------------------------- *) 159(* A, x = t |- P[x] *) 160(* ------------------ EXISTS_EQUATION *) 161(* A |- ?x. P[x] *) 162(* ------------------------------------------------------------------------- *) 163 164val EXISTS_EQUATION = Prim_rec.EXISTS_EQUATION 165 166(* ========================================================================= *) 167(* Part 1: The main part of the inductive definitions package. *) 168(* ========================================================================= *) 169 170(* ------------------------------------------------------------------------- *) 171(* Translates a single clause to have variable arguments, simplifying. *) 172(* ------------------------------------------------------------------------- *) 173 174(* ------------------------------------------------------------------------- *) 175(* [JRH] Removed "Fail" constructor from handle trap. *) 176(* ------------------------------------------------------------------------- *) 177 178local fun getequs(avs,[]) = [] 179 | getequs(avs,(h as {redex=r,residue})::t) = 180 if mem r avs 181 then h::getequs(avs,filter (fn{redex,...} => not(r=redex)) t) 182 else getequs(avs,t) 183 fun calculate_simp_sequence avs plis = 184 let val oks = getequs(avs,plis) 185 in (oks,subtract plis oks) 186 end 187 fun mk_eq_of_bind{redex,residue} = mk_eq(residue,redex) 188in 189fun canonicalize_clause clause carg = 190 let val (avs,bimp) = strip_forall clause 191 val (ant,con) = dest_imp bimp handle HOL_ERR _ => (T,bimp) 192 val (rel,xargs) = strip_comb con 193 val plis = map2 (curry op |->) xargs carg 194 val (yes,no) = calculate_simp_sequence avs plis 195 val nvs = filter (not o C mem (map #redex yes)) avs 196 val eth = 197 if is_imp bimp then 198 let val atm = itlist (curry mk_conj o mk_eq_of_bind) (yes@no) ant 199 val (ths,tth) = nsplit CONJ_PAIR plis (ASSUME atm) 200 val thl = map(fn t => first(fn th => lhs(concl th) = t)ths) carg 201 val th0 = MP (SPECL avs (ASSUME clause)) tth 202 val th1 = rev_itlist (C (curry MK_COMB)) thl (REFL rel) 203 val th2 = EQ_MP (SYM th1) th0 204 val th3 = INST yes (DISCH atm th2) 205 val tm4 = funpow (length yes) rand (lhand(concl th3)) 206 val th4 = itlist (CONJ o REFL o #residue) yes (ASSUME tm4) 207 val th5 = GENL carg (GENL nvs (DISCH tm4 (MP th3 th4))) 208 val th6 = SPECL nvs (SPECL (map #redex plis) (ASSUME(concl th5))) 209 val th7 = itlist (CONJ o REFL o #redex) no (ASSUME ant) 210 val th8 = GENL avs (DISCH ant (MP th6 th7)) 211 in IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th8) 212 end 213 else 214 let val _ = not (null no) orelse 215 raise mk_HOL_ERR "InductiveDefinition" 216 "canonicalize_clause" 217 "Vacuous clause trivialises whole definition" 218 val atm = list_mk_conj(map mk_eq_of_bind (yes@no)) 219 val ths = CONJUNCTS (ASSUME atm) 220 val thl = map(fn t => first(fn th => lhs(concl th) = t) ths) carg 221 val th0 = SPECL avs (ASSUME clause) 222 val th1 = rev_itlist (C (curry MK_COMB)) thl (REFL rel) 223 val th2 = EQ_MP (SYM th1) th0 224 val th3 = INST yes (DISCH atm th2) 225 val tm4 = funpow (length yes) rand (lhand(concl th3)) 226 val th4 = itlist (CONJ o REFL o #residue) yes (ASSUME tm4) 227 val th5 = GENL carg (GENL nvs (DISCH tm4 (MP th3 th4))) 228 val th6 = SPECL nvs (SPECL (map #redex plis) (ASSUME(concl th5))) 229 val th7 = end_itlist CONJ (map (REFL o #redex) no) 230 val th8 = GENL avs (MP th6 th7) 231 in IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th8) 232 end 233 val ftm = funpow (length carg) (body o rand) (rand(concl eth)) 234 in TRANS eth (itlist MK_FORALL carg (FORALL_IMPS_CONV ftm)) 235 end 236 handle e => raise (wrap_exn "InductiveDefinition" "canonicalize_clause" e) 237end; 238 239(* ------------------------------------------------------------------------- *) 240(* Canonicalizes the set of clauses, disjoining compatible antecedants. *) 241(* ------------------------------------------------------------------------- *) 242 243local fun assoc2 x (h1::t1,h2::t2) = if x = h1 then h2 else assoc2 x (t1,t2) 244 | assoc2 x _ = fail() 245in 246fun canonicalize_clauses clauses = 247 let val concls = map getconcl clauses 248 val uncs = map strip_comb concls 249 val rels = itlist (insert o fst) uncs [] 250 val xargs = map (C assoc uncs) rels 251 val closed = list_mk_conj clauses 252 val avoids = all_vars closed 253 val flargs = make_args avoids (map type_of (end_foldr (op @) xargs)) 254 val vargs = shareout xargs flargs 255 val cargs = map (C assoc2 (rels,vargs) o fst) uncs 256 val cthms = map2 canonicalize_clause clauses cargs 257 val pclauses = map (rand o concl) cthms 258 fun collectclauses tm = 259 mapfilter (fn t => if fst t = tm then snd t else fail()) 260 (zip (map fst uncs) pclauses) 261 val clausell = map collectclauses rels 262 val cclausel = map list_mk_conj clausell 263 val cclauses = list_mk_conj cclausel 264 and oclauses = list_mk_conj pclauses 265 val pth = TRANS (end_itlist MK_CONJ cthms) 266 (CONJ_ACI(mk_eq(oclauses,cclauses))) 267 in TRANS pth (end_itlist MK_CONJ (map AND_IMPS_CONV cclausel)) 268 end 269 handle e => raise (wrap_exn "InductiveDefinition" "canonicalize_clauses" e) 270end; 271 272 273(* ------------------------------------------------------------------------- *) 274(* Prove definitions work for non-schematic relations with canonical rules. *) 275(* ------------------------------------------------------------------------- *) 276 277fun derive_canon_inductive_relations pclauses = 278 let val closed = list_mk_conj pclauses 279 val pclauses = strip_conj closed 280 val (vargs,bodies) = split(map strip_forall pclauses) 281 val (ants,concs) = split(map dest_imp bodies) 282 val rels = map (repeat rator) concs 283 val avoids = all_vars closed 284 val rels' = variants avoids rels 285 val prime_fn = subst (map2 (curry op |->) rels rels' ) 286 val closed' = prime_fn closed 287 fun mk_def arg con = 288 mk_eq(repeat rator con, 289 list_mk_abs(arg,list_mk_forall(rels', 290 mk_imp(closed',prime_fn con)))) 291 val deftms = map2 mk_def vargs concs 292 val defthms = map2 HALF_BETA_EXPAND vargs (map ASSUME deftms) 293 fun mk_ind args th = 294 let val th1 = fst(EQ_IMP_RULE(SPEC_ALL th)) 295 val ant = lhand(concl th1) 296 val th2 = SPECL rels' (UNDISCH th1) 297 in GENL args (DISCH ant (UNDISCH th2)) 298 end 299 val indthms = map2 mk_ind vargs defthms 300 val indthmr = end_itlist CONJ indthms 301 val indthm = GENL rels' (DISCH closed' indthmr) 302 val mconcs = map2 (fn a => fn t => 303 list_mk_forall(a,mk_imp(t,prime_fn t))) vargs ants 304 val monotm = mk_imp(concl indthmr,list_mk_conj mconcs) 305 val monothm = ASSUME(list_mk_forall(rels,list_mk_forall(rels',monotm))) 306 val closthm = ASSUME closed' 307 val monothms = CONJUNCTS 308 (MP (SPEC_ALL monothm) (MP (SPECL rels' indthm) closthm)) 309 val closthms = CONJUNCTS closthm 310 fun prove_rule mth (cth,dth) = 311 let val (avs,bod) = strip_forall(concl mth) 312 val th1 = IMP_TRANS (SPECL avs mth) (SPECL avs cth) 313 val th2 = GENL rels' (DISCH closed' (UNDISCH th1)) 314 val th3 = EQ_MP (SYM (SPECL avs dth)) th2 315 in GENL avs (DISCH (lhand bod) th3) 316 end 317 val ruvalhms = map2 prove_rule monothms (zip closthms defthms) 318 val ruvalhm = end_itlist CONJ ruvalhms 319 val dtms = map2 (curry list_mk_abs) vargs ants 320 val double_fn = subst (map2 (curry op |->) rels dtms) 321 fun mk_unbetas tm dtm = 322 let val (avs,bod) = strip_forall tm 323 val (il,r) = dest_comb bod 324 val (i,l) = dest_comb il 325 val bth = RIGHT_BETAS avs (REFL dtm) 326 val munb = AP_THM (AP_TERM i bth) r 327 val iunb = AP_TERM (mk_comb(i,double_fn l)) bth 328 val junb = AP_TERM (mk_comb(i,r)) bth 329 val quantify = itlist MK_FORALL avs 330 in (quantify munb,(quantify iunb,quantify junb)) 331 end 332 val unths = map2 mk_unbetas pclauses dtms 333 val irthm = EQ_MP (SYM(end_itlist MK_CONJ (map fst unths))) ruvalhm 334 val mrthm = MP (SPECL rels (SPECL dtms monothm)) irthm 335 val imrth = EQ_MP 336 (SYM(end_itlist MK_CONJ (map (fst o snd) unths))) mrthm 337 val ifthm = MP (SPECL dtms indthm) imrth 338 val fthm = EQ_MP (end_itlist MK_CONJ (map (snd o snd) unths)) ifthm 339 fun mk_case th1 th2 = 340 let val avs = fst(strip_forall(concl th1)) 341 in GENL avs (IMP_ANTISYM_RULE (SPEC_ALL th1) (SPEC_ALL th2)) 342 end 343 val casethm = end_itlist CONJ 344 (map2 mk_case (CONJUNCTS fthm) (CONJUNCTS ruvalhm)) 345 in CONJ ruvalhm (CONJ indthm casethm) 346 end 347 handle e => raise (wrap_exn "InductiveDefinition" 348 "derive_canon_inductive_relations"e); 349 350(* ------------------------------------------------------------------------- *) 351(* General case for nonschematic relations; monotonicity & defn hyps. *) 352(* ------------------------------------------------------------------------- *) 353 354fun derive_nonschematic_inductive_relations tm = 355 let val clauses = strip_conj tm 356 val canonthm = canonicalize_clauses clauses 357 val canonthm' = SYM canonthm 358 val pclosed = rand(concl canonthm) 359 val pclauses = strip_conj pclosed 360 val rawthm = derive_canon_inductive_relations pclauses 361 val (ruvalhm,otherthms) = CONJ_PAIR rawthm 362 val (indthm,casethm) = CONJ_PAIR otherthms 363 val ruvalhm' = EQ_MP canonthm' ruvalhm 364 and indthm' = CONV_RULE (ONCE_DEPTH_CONV (REWR_CONV canonthm')) indthm 365 in CONJ ruvalhm' (CONJ indthm' casethm) 366 end 367 handle e => raise (wrap_exn "InductiveDefinition" 368 "derive_nonschematic_inductive_relations" e); 369 370 371(* ========================================================================= *) 372(* Part 2: Tactic-integrated tools for proving monotonicity automatically. *) 373(* ========================================================================= *) 374 375 376(* ---------------------------------------------------------------------- 377 MONO_ABS_TAC 378 379 ?- (\x. P[x]) x1 .. xn ==> (\y. Q[y]) x1 .. xn 380 ================================================== 381 ?- P[x1] x2 .. xn ==> Q[x1] x2 .. xn 382 383 ---------------------------------------------------------------------- *) 384 385fun MONO_ABS_TAC (asl,w) = 386 let val (ant,con) = dest_imp w 387 val vars = snd(strip_comb con) 388 val rnum = length vars - 1 389 val (hd1,args1) = strip_ncomb rnum ant 390 and (hd2,args2) = strip_ncomb rnum con 391 val th1 = rev_itlist (C AP_THM) args1 (BETA_CONV hd1) 392 and th2 = rev_itlist (C AP_THM) args1 (BETA_CONV hd2) 393 val th3 = MK_COMB(AP_TERM boolSyntax.implication th1,th2) 394 in CONV_TAC(REWR_CONV th3) (asl,w) 395 end;; 396 397(* ---------------------------------------------------------------------- 398 MONO_UNCURRY_TAC 399 400 ?- UNCURRY f x1 .. xn ==> UNCURRY f' x1 .. xn 401 ================================================== 402 ?- f y1 y2 .. xn ==> f' y1 y2 .. xn 403 404 ---------------------------------------------------------------------- *) 405 406fun MONO_UNCURRY_TAC (asl, w) = let 407 val U = DB.fetch "pair" "UNCURRY" 408 val (ant, con) = dest_imp w 409 val vars = snd (strip_comb con) 410 val rnum = length vars - 2 411 val (hd1, args1) = strip_ncomb rnum ant 412 val (hd2, args2) = strip_ncomb rnum con 413 val th1 = rev_itlist (C AP_THM) args1 (ISPECL (#2 (strip_comb hd1)) U) 414 val th2 = rev_itlist (C AP_THM) args2 (ISPECL (#2 (strip_comb hd2)) U) 415 val th3 = MK_COMB(AP_TERM boolSyntax.implication th1, th2) 416in 417 CONV_TAC (REWR_CONV th3) (asl, w) 418end 419 420 421(* ------------------------------------------------------------------------- *) 422(* Collection, so users can add their own rules. *) 423(* *) 424(* As a simple speedup, the tactics are indexed by head operator in the *) 425(* relevant expression. If there isn't a head constant, use the empty string.*) 426(* ------------------------------------------------------------------------- *) 427(* ------------------------------------------------------------------------- *) 428(* Simplified version of MATCH_MP_TAC to avoid quantifier troubles. *) 429(* ------------------------------------------------------------------------- *) 430 431fun BACKCHAIN_TAC th = 432 let val match_fn = HO_PART_MATCH (snd o dest_imp) th 433 in fn (asl,w) => 434 let val th1 = match_fn w 435 val (ant,con) = dest_imp(concl th1) 436 in ([(asl,ant)],fn [t] => HO_MATCH_MP th1 t | _ => raise Match) 437 end 438 end;; 439 440type monoset = (string * thm) list; 441 442(*--------------------------------------------------------------------------- 443 * MONO_AND = |- (A ==> B) /\ (C ==> D) ==> (A /\ C ==> B /\ D) 444 * MONO_OR = |- (A ==> B) /\ (C ==> D) ==> (A \/ C ==> B \/ D) 445 * MONO_IMP = |- (B ==> A) /\ (C ==> D) ==> ((A ==> C) ==> (B ==> D)) 446 * MONO_NOT = |- (B ==> A) ==> (~A ==> ~B) 447 * MONO_COND = |- (w ==> x) /\ (y ==> z) ==> (COND b w y) ==> (COND b x z) 448 * MONO_ALL = |- (!x. P x ==> Q x) ==> ((!x. P x) ==> (!x. Q x)) 449 * MONO_EXISTS = |- (!x. P x ==> Q x) ==> ((?x. P x) ==> (?x. Q x)) 450 *---------------------------------------------------------------------------*) 451 452 453val MONO_EXISTS = prove ( 454 ``(!x:'a. P x ==> Q x) ==> ($? P ==> $? Q)``, 455 DISCH_THEN(MP_TAC o HO_MATCH_MP MONO_EXISTS) THEN 456 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[]) 457 458val MONO_FORALL = prove ( 459 ``(!x:'a. P x ==> Q x) ==> ($! P ==> $! Q)``, 460 DISCH_THEN(MP_TAC o HO_MATCH_MP MONO_ALL) THEN 461 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[]) 462 463val MONO_RESFORALL = prove( 464 ``(!x:'a. P' x ==> P x) /\ (!x. Q x ==> Q' x) ==> 465 (RES_FORALL P Q ==> RES_FORALL P' Q')``, 466 REWRITE_TAC [RES_FORALL_THM, IN_DEF] THEN BETA_TAC THEN REPEAT STRIP_TAC THEN 467 REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC []) 468 469val MONO_RESEXISTS = prove( 470 ``(!x:'a. P x ==> P' x) /\ (!x. Q x ==> Q' x) ==> 471 (RES_EXISTS P Q ==> RES_EXISTS P' Q')``, 472 REWRITE_TAC [RES_EXISTS_THM, IN_DEF] THEN BETA_TAC THEN REPEAT STRIP_TAC THEN 473 EXISTS_TAC ``x:'a`` THEN RES_TAC THEN ASM_REWRITE_TAC []) 474 475val MONO_COND = let open Rewrite boolTheory in 476 ONCE_REWRITE_RULE[AND_IMP_INTRO]MONO_COND 477end 478 479val bool_monoset = 480 [("/\\", MONO_AND), 481 ("\\/", MONO_OR), 482 ("?", MONO_EXISTS), 483 ("!", MONO_FORALL), 484 ("==>", MONO_IMP), 485 ("~", MONO_NOT), 486 ("COND",MONO_COND), 487 ("RES_FORALL", MONO_RESFORALL), 488 ("RES_EXISTS", MONO_RESEXISTS)] 489 490 491val IMP_REFL = let val p = mk_var("p", bool) in ASSUME p |> DISCH p |> GEN p end 492 493fun APPLY_MONOTAC monoset (asl, w) = let 494 val (a,c) = dest_imp w 495in 496 if aconv a c then ACCEPT_TAC (SPEC a IMP_REFL) (asl,w) 497 else let 498 val {Thy,Name,...} = dest_thy_const(repeat rator c) 499 handle HOL_ERR _ => {Thy = "", Name = "", 500 Ty = Type.alpha} 501 in 502 case (Thy,Name) of 503 ("","") => MONO_ABS_TAC (asl, w) 504 | ("pair", "UNCURRY") => MONO_UNCURRY_TAC (asl, w) 505 | _ => tryfind (fn (k,t) => if k = Name then BACKCHAIN_TAC t (asl,w) 506 else fail()) 507 monoset 508 end 509end 510 511(* ------------------------------------------------------------------------- *) 512(* Tactics to prove monotonicity automatically. *) 513(* ------------------------------------------------------------------------- *) 514 515fun MONO_STEP_TAC finisher monoset = 516 REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN 517 (APPLY_MONOTAC monoset ORELSE finisher) 518 519fun MONO_TAC monoset = let 520 (* first case is for monotonicity proving in making the definition, where 521 there will be an assumption of the form 522 !vs. P vs ==> P' vs 523 to hand. 524 The second case (after the ORELSE) is for proving strong induction, where 525 there won't be any assumptions, but the goal will have reduced to 526 con vs /\ con' vs ==> con vs 527 *) 528 val finisher = FIRST_ASSUM MATCH_ACCEPT_TAC ORELSE 529 (REPEAT STRIP_TAC THEN FIRST_ASSUM ACCEPT_TAC) 530in 531 REPEAT (MONO_STEP_TAC finisher monoset) 532end 533 534(* =========================================================================*) 535(* Part 3: Utility functions to modify the basic theorems in various ways. *) 536(* *) 537(* There are various fnctions that can be applied to a theorem: *) 538(* *) 539(* (1) Attempt to prove the monotonicity hypotheses *) 540(* *) 541(* (2) Generalize it over schematic variables *) 542(* *) 543(* (3) Derive a raw existence assertion *) 544(* *) 545(* (4) Actually make definitions of the inductive relations. *) 546(* *) 547(* Generally one applies either or both of (1) and (2), then does (4). *) 548(* =========================================================================*) 549 550(* ------------------------------------------------------------------------- *) 551(* Attempt to dispose of the non-equational assumption(s) of a theorem. *) 552(* ------------------------------------------------------------------------- *) 553 554fun prove_monotonicity_hyps monoset = 555 let val tac = REPEAT GEN_TAC THEN 556 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN 557 REPEAT CONJ_TAC THEN (MONO_TAC monoset) 558 fun prove_mth t = TAC_PROOF(([],t),tac) 559 in fn th => 560 let val mths = mapfilter prove_mth (filter (not o is_eq) (hyp th)) 561 in itlist PROVE_HYP mths th 562 end 563 end 564 handle e => raise (wrap_exn "InductiveDefinition" 565 "prove_monotonicity_hyps" e); 566 567(* ------------------------------------------------------------------------- *) 568(* Generalize definitions and theorem over given variables (all the same!) *) 569(* ------------------------------------------------------------------------- *) 570 571fun generalize_schematic_variables vs = 572 let fun generalize_def tm th = 573 let val (l,r) = dest_eq tm 574 val (lname,lty) = dest_var l 575 val l' = mk_var(lname,itlist (curry (op -->) o type_of) vs lty) 576 val r' = list_mk_abs(vs,r) 577 val tm' = mk_eq(l',r') 578 val th0 = RIGHT_BETAS vs (ASSUME tm') 579 val th1 = INST [l |-> lhs(concl th0)] (DISCH tm th) 580 in MP th1 th0 581 end 582 in fn th => 583 let val (defs,others) = partition is_eq (hyp th) 584 val others' = 585 map (fn t => let val fvs = free_vars t 586 in SPECL fvs (ASSUME (list_mk_forall(fvs,t))) 587 end) 588 others 589 val th1 = itlist generalize_def defs th 590 in GENL vs (itlist PROVE_HYP others' th1) 591 end 592 end; 593 594(* ------------------------------------------------------------------------- *) 595(* Derive existence. *) 596(* ------------------------------------------------------------------------- *) 597 598fun derive_existence th = itlist EXISTS_EQUATION (filter is_eq (hyp th)) th 599 600(* ------------------------------------------------------------------------- *) 601(* Make definitions. *) 602(* ------------------------------------------------------------------------- *) 603 604fun make_definitions stem th = let 605 val defs = filter is_eq (hyp th) 606 fun mkdef i tm = 607 new_definition(stem ^ Int.toString i ^ !boolLib.def_suffix, tm) 608 val dths = if length defs = 1 then 609 [new_definition(stem ^ !boolLib.def_suffix, hd defs)] 610 else 611 mapi mkdef defs 612 val insts = map2 (curry op |->) (map lhs defs) (map (lhs o concl) dths) 613in 614 rev_itlist (C MP) dths (INST insts (itlist DISCH defs th)) 615end 616 617(* ------------------------------------------------------------------------- *) 618(* "Unschematize" a set of clauses. *) 619(* ------------------------------------------------------------------------- *) 620 621val inddef_strict = ref false; 622val _ = Feedback.register_btrace ("inddef strict", inddef_strict); 623 624fun indented_term_to_string n tm = let 625 val nspaces = CharVector.tabulate(n, K #" ") 626 fun pper tm = let 627 open smpp 628 in 629 add_string nspaces >> 630 block PP.CONSISTENT n ( 631 Lib.with_flag (Parse.current_backend, PPBackEnd.raw_terminal) 632 (lift Parse.pp_term) 633 tm 634 ) 635 end 636in 637 PP.pp_to_string (!Globals.linewidth) (Parse.mlower o pper) tm 638end 639 640 641local 642 fun pare_comb qvs tm = 643 if null (intersect (free_vars tm) qvs) 644 andalso all is_var (snd(strip_comb tm)) 645 then tm 646 else pare_comb qvs (rator tm) 647 fun schem_head cls = 648 let val (avs,bod) = strip_forall cls 649 in pare_comb avs (snd(dest_imp bod) handle HOL_ERR _ => bod) 650 end 651 fun common_prefix0 acc l1 l2 = 652 case (l1, l2) of 653 ([], _) => acc 654 | (_, []) => acc 655 | (h1::t1, h2::t2) => if h1 = h2 then common_prefix0 (h1::acc) t1 t2 656 else acc 657 fun common_prefix l1 l2 = List.rev (common_prefix0 [] l1 l2) 658 fun lcommon_prefix0 acc l = 659 case l of 660 [] => acc 661 | (h::t) => let 662 val newprefix = common_prefix acc h 663 in 664 if null newprefix then [] 665 else lcommon_prefix0 newprefix t 666 end 667 fun lcommon_prefix [] = [] 668 | lcommon_prefix (h::t) = lcommon_prefix0 h t 669 670in 671fun unschematize_clauses clauses = let 672 val schem = map schem_head clauses 673 val schems = mk_set schem 674 fun insert_list l s = foldl (fn (t,s) => HOLset.add(s,t)) s l 675 val hdops = mk_set (map (#1 o strip_comb) schems) 676 val schemv_extent = length (#2 (strip_comb (hd schems))) 677 fun is_hdop_instance t = let 678 val (f,args) = strip_comb t 679 in 680 mem f hdops andalso length args = schemv_extent 681 end 682 val all_instances = 683 foldl (fn (t, s) => insert_list (find_terms is_hdop_instance t) s) 684 empty_tmset clauses 685 fun do_substitution schems = let 686 val avoids = all_vars (list_mk_conj clauses) 687 fun hack_fn tm = mk_var(fst(dest_var(repeat rator tm)),type_of tm) 688 val grels = variants avoids (map hack_fn schems) 689 val crels = map2 (curry op |->) schems grels 690 val clauses' = map (subst crels) clauses 691 in 692 (clauses',snd(strip_comb(hd schems))) 693 end 694in 695 if is_var(hd schem) then (clauses,[]) 696 else if !inddef_strict then 697 if not (HOLset.numItems all_instances = 1) then let 698 val instlist = HOLset.listItems all_instances 699 val t1_s = trace("types", 1) (indented_term_to_string 2) (hd instlist) 700 val t2_s = 701 trace("types", 1) (indented_term_to_string 2) (hd (tl instlist)) 702 in 703 failwith ("Schematic variable(s) not used consistently - witness\n"^ 704 t1_s^"\nand\n"^t2_s) 705 end 706 else 707 do_substitution schems 708 else (* liberal definitions *) let 709 val prefix_vars = HOLset.foldr (fn (t,l) => #2 (strip_comb t)::l) 710 [] all_instances 711 val prefix = lcommon_prefix prefix_vars 712 in 713 if null prefix then (clauses, []) 714 else let 715 val plist = String.concat (Lib.commafy 716 (map (quote o #1 o dest_var) prefix)) 717 val _ = HOL_MESG ("Treating "^plist^" as schematic variable"^ 718 (if length prefix > 1 then "s" else "")) 719 in 720 do_substitution (map (fn t => list_mk_comb(t, prefix)) hdops) 721 end 722 end 723 end 724end; 725 726(* ========================================================================= *) 727(* Part 4: The final user wrapper. *) 728(* ========================================================================= *) 729 730 731fun check_definition schemevars clocs tm = let 732 (* check that tm has no extra type variables or free variables other than *) 733 (* the heads of clauses *) 734 val clauses = strip_conj tm 735 fun ind_concl tm = #2 (dest_imp tm) handle HOL_ERR _ => tm 736 val relvars = 737 HOLset.addList(empty_tmset, 738 map (#1 o strip_comb o ind_concl o #2 o strip_forall) 739 clauses) 740 val okvars = foldl (fn (v,s) => HOLset.add(s,v)) relvars schemevars 741 val empty_tyset = HOLset.empty Type.compare 742 val reltyvars = HOLset.foldl (fn (tm,tyvset) => 743 HOLset.addList(tyvset, 744 type_vars_in_term tm)) 745 empty_tyset relvars 746 val reltyvars = List.foldl (fn (tm,tyvset) => 747 HOLset.addList(tyvset, 748 type_vars_in_term tm)) 749 reltyvars schemevars 750 751 (* check that there aren't duplicate names in the forall chain *) 752 fun check_clause_foralls n c = let 753 val (vs, body) = strip_forall c 754 val loc = List.nth(clocs, n) handle Subscript => locn.Loc_None 755 fun foldthis (v, acc) = let 756 val (nm, _) = dest_var v 757 in 758 if HOLset.member(acc, nm) then 759 raise mk_HOL_ERRloc "InductiveDefinition" 760 "check_clause" 761 loc 762 ("Clause #"^Int.toString (n + 1)^ 763 " contains duplicate name "^nm^ 764 " in outermost universal quantification") 765 else HOLset.add(acc, nm) 766 end 767 in 768 ignore (List.foldl foldthis (HOLset.empty String.compare) vs) 769 end 770 val _ = appi check_clause_foralls clauses 771 772 773 fun check_tyvars n c = let 774 val tyvs = HOLset.addList(empty_tyset, type_vars_in_term c) 775 in 776 if not (HOLset.isSubset(tyvs, reltyvars)) then let 777 val really_free = HOLset.difference(tyvs, reltyvars) 778 val free_list0 = HOLset.foldr (fn (v,sl) => dest_vartype v :: sl) 779 [] really_free 780 val free_list = Lib.commafy free_list0 781 val tmstring = trace ("types", 1) (indented_term_to_string 2) c 782 val loc = List.nth (clocs, n) handle Subscript => locn.Loc_None 783 in 784 raise mk_HOL_ERRloc 785 "InductiveDefinition" "check_clause" loc 786 (String.concat ("Clause #" :: Int.toString (n + 1):: 787 ":\n" :: tmstring :: 788 "\ncontains free type variable"^ 789 (if length free_list > 1 then "s" else "")^ 790 ": " :: free_list)) 791 end 792 else 793 () 794 end 795 val _ = appi check_tyvars clauses 796 797 798 799 (* here, generalise on the extra free variables if we're not being strict *) 800 fun check_clause n c = let 801 val fvs = FVL [c] empty_tmset 802 in 803 if not (HOLset.isSubset(fvs, okvars)) then let 804 val really_free = HOLset.difference(fvs, okvars) 805 val free_list0 = 806 HOLset.foldr (fn (v,sl) => Lib.quote (#1 (dest_var v)) :: sl) 807 [] really_free 808 val free_list = Lib.commafy free_list0 809 val loc = List.nth(clocs, n) handle Subscript => locn.Loc_None 810 in 811 if !inddef_strict then let 812 val tmstring = trace ("types", 1) (indented_term_to_string 2) c 813 in 814 raise mk_HOL_ERRloc 815 "InductiveDefinition" 816 "check_clause" 817 loc 818 (String.concat ("Clause #" :: Int.toString n :: 819 ",\n" :: tmstring :: 820 "\ncontains free variables: " :: 821 free_list)) 822 end 823 else 824 (HOL_MESG ("Generalising variable" ^ 825 (if length free_list > 1 then "s " else " ")^ 826 String.concat free_list ^ 827 " in clause #"^Int.toString n ^ 828 (if loc = locn.Loc_None then "" 829 else " ("^locn.toShortString loc^")")); 830 list_mk_forall (HOLset.listItems really_free, c)) 831 end 832 else c 833 end 834in 835 list_mk_conj (mapi check_clause clauses) 836end 837 838 839 840fun prove_nonschematic_inductive_relations_exist monoset tm = let 841 val th0 = derive_nonschematic_inductive_relations tm 842 val th1 = prove_monotonicity_hyps monoset th0 843in 844 derive_existence th1 845end 846 handle e => 847 raise (wrap_exn "InductiveDefinition" 848 "prove_nonschematic_inductive_relations_exist" e); 849 850(* ------------------------------------------------------------------------- *) 851(* The schematic case. *) 852(* *) 853(* All relations in a given call must have the same schematic args (if they *) 854(* aren't mutually inductive, use separate definitions), which must occur as *) 855(* the first arguments to each relation, in the same order(!) *) 856(* ------------------------------------------------------------------------- *) 857 858fun prove_inductive_relations_exist monoset tm = 859 let val clauses = strip_conj tm 860 val (clauses',fvs) = unschematize_clauses clauses 861 val th0 = derive_nonschematic_inductive_relations 862 (check_definition fvs [] (list_mk_conj clauses')) 863 val th1 = prove_monotonicity_hyps monoset th0 864 val th2 = generalize_schematic_variables fvs th1 865 in derive_existence th2 866 end 867 handle e => raise (wrap_exn "InductiveDefinition" 868 "prove_inductive_relations_exist" e); 869 870 871fun new_inductive_definition monoset stem (tm,clocs) = 872 let val clauses = strip_conj tm 873 val (clauses',fvs) = unschematize_clauses clauses 874 val th0 = derive_nonschematic_inductive_relations 875 (check_definition fvs clocs (list_mk_conj clauses')) 876 val th1 = prove_monotonicity_hyps monoset th0 877 val th2 = generalize_schematic_variables fvs th1 878 val th3 = make_definitions stem th2 879 val avs = fst(strip_forall(concl th3)) 880 val (r,ic) = CONJ_PAIR(SPECL avs th3) 881 val (i,c) = CONJ_PAIR ic 882 in (GENL avs r, GENL avs i, GENL avs c) 883 end 884 handle e => raise wrap_exn "InductiveDefinition" "new_inductive_definition" e; 885 886end (* InductiveDefinition *) 887