1169691Skan(* ========================================================================= *) 2169691Skan(* *) 3169691Skan(* Inductive Definitions (John Harrison) *) 4169691Skan(* *) 5169691Skan(* ========================================================================= *) 6169691Skan 7169691Skanstructure InductiveDefinition :> InductiveDefinition = 8169691Skanstruct 9169691Skan 10169691Skanopen HolKernel boolLib liteLib refuteLib AC Ho_Rewrite; 11169691Skan 12169691Skan(* Fix the grammar used by this file *) 13169691Skanstructure Parse = 14169691Skanstruct 15169691Skan open Parse 16169691Skan val (Type,Term) = Parse.parse_from_grammars boolTheory.bool_grammars 17169691Skan fun == q x = Type q 18169691Skanend 19169691Skanopen Parse 20169691Skan 21169691Skan(*--------------------------------------------------------------------------- 22169691Skan Variants. We re-define the kernel "variant" function here because 23169691Skan of a subtle difference between Hol98 variant and Hol88/light 24169691Skan variant functions: the former only looks at strings, while the 25169691Skan latter look at variables. For example 26169691Skan 27169691Skan variant [`x:bool`] `x:'a` 28169691Skan 29169691Skan yields x' in Hol98, but `x` in the latter (I think). The following 30169691Skan version of variant also does not vary away from constants with the 31169691Skan same name, maybe it should. 32169691Skan ---------------------------------------------------------------------------*) 33169691Skan 34169691Skanlocal fun prime v = let val (n,ty) = dest_var v in mk_var(n^"'",ty) end 35169691Skanin 36169691Skanfun vary V v = if op_mem aconv v V then vary V (prime v) else v 37169691Skanend 38169691Skan 39169691Skan(* ------------------------------------------------------------------------- *) 40169691Skan(* Produces a sequence of variants, considering previous inventions. *) 41169691Skan(* ------------------------------------------------------------------------- *) 42169691Skan 43169691Skanfun variants av [] = [] 44169691Skan | variants av (h::t) = 45169691Skan let val vh = vary av h 46169691Skan in vh::variants (vh::av) t 47169691Skan end; 48169691Skan 49169691Skan(* ------------------------------------------------------------------------- *) 50169691Skan(* Apply a destructor as many times as elements in list. *) 51169691Skan(* ------------------------------------------------------------------------- *) 52169691Skan 53169691Skanfun nsplit dest clist x = 54169691Skan if null clist then ([],x) else 55169691Skan let val (l,r) = dest x 56169691Skan val (ll,y) = nsplit dest (tl clist) r 57169691Skan in (l::ll,y) 58169691Skan end;; 59169691Skan 60169691Skan(* ------------------------------------------------------------------------- *) 61169691Skan(* Strip off exactly n arguments from combination. *) 62169691Skan(* ------------------------------------------------------------------------- *) 63169691Skan 64169691Skanval strip_ncomb = 65169691Skan let fun strip(n,tm,acc) = 66169691Skan if n < 1 then (tm,acc) else 67169691Skan let val (l,r) = dest_comb tm 68169691Skan in strip(n - 1,l,r::acc) 69169691Skan end 70169691Skan in fn n => fn tm => strip(n,tm,[]) 71169691Skan end;; 72169691Skan 73169691Skan(* ------------------------------------------------------------------------- *) 74169691Skan(* Share out list according to pattern in list-of-lists. *) 75169691Skan(* ------------------------------------------------------------------------- *) 76169691Skan 77169691Skanfun shareout [] _ = [] 78169691Skan | shareout (h::t) all = 79169691Skan let val (l,r) = split_after (length h) all 80169691Skan in l::shareout t r 81169691Skan end; 82169691Skan 83169691Skan(* ------------------------------------------------------------------------- *) 84169691Skan(* Produce a set of reasonably readable arguments, using variants if needed. *) 85169691Skan(* ------------------------------------------------------------------------- *) 86169691Skan 87169691Skanval make_args = 88169691Skan let fun margs n avoid tys = 89169691Skan if null tys then [] else 90169691Skan let val v = variant avoid (mk_var("a"^(int_to_string n),hd tys)) 91169691Skan in v::margs (n + 1) (v::avoid) (tl tys) 92169691Skan end 93169691Skan in margs 0 end;; 94169691Skan 95169691Skan(* ------------------------------------------------------------------------- *) 96169691Skan(* Grabs conclusion of rule, whether or not it has an antecedant. *) 97169691Skan(* ------------------------------------------------------------------------- *) 98169691Skan 99169691Skanfun getconcl tm = 100169691Skan let val bod = repeat (snd o dest_forall) tm 101169691Skan in snd(dest_imp bod) handle HOL_ERR _ => bod 102169691Skan end;; 103169691Skan 104169691Skan(* ------------------------------------------------------------------------- *) 105169691Skan(* Likewise, but quantify afterwards. *) 106169691Skan(* ------------------------------------------------------------------------- *) 107169691Skan 108169691Skanfun HALF_BETA_EXPAND args th = GENL args (RIGHT_BETAS args th);; 109169691Skan 110169691Skan(* ------------------------------------------------------------------------- *) 111169691Skan(* Converse of SIMPLE_DISJ_CASES, i.e. P \/ Q |- R => P |- R, Q |- R *) 112169691Skan(* ------------------------------------------------------------------------- *) 113169691Skan 114169691Skanfun SIMPLE_DISJ_PAIR th = 115169691Skan let val (l,r) = dest_disj(hd(hyp th)) 116169691Skan in (PROVE_HYP (DISJ1 (ASSUME l) r) th,PROVE_HYP (DISJ2 l (ASSUME r)) th) 117169691Skan end;; 118169691Skan 119169691Skan(* ------------------------------------------------------------------------- *) 120169691Skan(* Iterated FORALL_IMP_CONV: (!x1..xn. P[xs] ==> Q) => (?x1..xn. P[xs]) ==> Q*) 121169691Skan(* ------------------------------------------------------------------------- *) 122169691Skan 123169691Skanval lhand = rand o rator;; 124169691Skan 125169691Skanfun FORALL_IMPS_CONV tm = 126169691Skan let val (avs,bod) = strip_forall tm 127169691Skan val th1 = DISCH tm (UNDISCH(SPEC_ALL(ASSUME tm))) 128169691Skan val th2 = itlist SIMPLE_CHOOSE avs th1 129169691Skan val tm2 = hd(hyp th2) 130169691Skan val th3 = DISCH tm2 (UNDISCH th2) 131169691Skan val th4 = ASSUME (concl th3) 132169691Skan val ant = lhand bod 133169691Skan val th5 = itlist SIMPLE_EXISTS avs (ASSUME ant) 134169691Skan val th6 = GENL avs (DISCH ant (MP th4 th5)) 135169691Skan in IMP_ANTISYM_RULE (DISCH_ALL th3) (DISCH_ALL th6) end;; 136169691Skan 137169691Skan(* ------------------------------------------------------------------------- *) 138169691Skan(* (!x1..xn. P1[xs] ==> Q[xs]) /\ ... /\ (!x1..xn. Pm[xs] ==> Q[xs]) *) 139169691Skan(* => (!x1..xn. P1[xs] \/ ... \/ Pm[xs] ==> Q[xs]) *) 140169691Skan(* ------------------------------------------------------------------------- *) 141169691Skan 142169691Skanfun AND_IMPS_CONV tm = 143169691Skan let val ths = CONJUNCTS(ASSUME tm) 144169691Skan val avs = fst(strip_forall(concl(hd ths))) 145169691Skan val thl = map (DISCH tm o UNDISCH o SPEC_ALL) ths 146169691Skan val th1 = end_itlist SIMPLE_DISJ_CASES thl 147169691Skan val tm1 = hd(hyp th1) 148169691Skan val th2 = GENL avs (DISCH tm1 (UNDISCH th1)) 149169691Skan val tm2 = concl th2 150169691Skan val th3 = DISCH tm2 (UNDISCH (SPEC_ALL (ASSUME tm2))) 151169691Skan val (thts,tht) = nsplit SIMPLE_DISJ_PAIR (tl ths) th3 152169691Skan fun proc_fn th = 153169691Skan let val t = hd(hyp th) in GENL avs (DISCH t (UNDISCH th)) 154169691Skan end 155169691Skan val th4 = itlist (CONJ o proc_fn) thts (proc_fn tht) 156169691Skan in IMP_ANTISYM_RULE (DISCH_ALL th2) (DISCH_ALL th4) end;; 157169691Skan 158169691Skan(* ------------------------------------------------------------------------- *) 159169691Skan(* A, x = t |- P[x] *) 160169691Skan(* ------------------ EXISTS_EQUATION *) 161169691Skan(* A |- ?x. P[x] *) 162169691Skan(* ------------------------------------------------------------------------- *) 163169691Skan 164169691Skanval EXISTS_EQUATION = Prim_rec.EXISTS_EQUATION 165169691Skan 166169691Skan(* ========================================================================= *) 167169691Skan(* Part 1: The main part of the inductive definitions package. *) 168169691Skan(* ========================================================================= *) 169169691Skan 170169691Skan(* ------------------------------------------------------------------------- *) 171169691Skan(* Translates a single clause to have variable arguments, simplifying. *) 172169691Skan(* ------------------------------------------------------------------------- *) 173169691Skan 174169691Skan(* ------------------------------------------------------------------------- *) 175169691Skan(* [JRH] Removed "Fail" constructor from handle trap. *) 176169691Skan(* ------------------------------------------------------------------------- *) 177169691Skan 178169691Skanlocal 179169691Skan fun redres_eq {redex=x1,residue=e1} {redex=x2,residue=e2} = 180169691Skan aconv x1 x2 andalso aconv e1 e2 181169691Skan fun getequs(avs,[]) = [] 182169691Skan | getequs(avs,(h as {redex=r,residue})::t) = 183169691Skan if op_mem aconv r avs then 184169691Skan h::getequs(avs,filter (fn{redex,...} => not(aconv r redex)) t) 185169691Skan else getequs(avs,t) 186169691Skan fun calculate_simp_sequence avs plis = 187169691Skan let val oks = getequs(avs,plis) 188169691Skan in (oks,op_set_diff redres_eq plis oks) 189169691Skan end 190169691Skan fun mk_eq_of_bind{redex,residue} = mk_eq(residue,redex) 191169691Skanin 192169691Skanfun canonicalize_clause clause carg = 193169691Skan let val (avs,bimp) = strip_forall clause 194169691Skan val (ant,con) = dest_imp bimp handle HOL_ERR _ => (T,bimp) 195169691Skan val (rel,xargs) = strip_comb con 196169691Skan val plis = map2 (curry op |->) xargs carg 197169691Skan val (yes,no) = calculate_simp_sequence avs plis 198169691Skan val nvs = filter (not o C (op_mem aconv) (map #redex yes)) avs 199169691Skan val eth = 200169691Skan if is_imp bimp then 201169691Skan let val atm = itlist (curry mk_conj o mk_eq_of_bind) (yes@no) ant 202169691Skan val (ths,tth) = nsplit CONJ_PAIR plis (ASSUME atm) 203169691Skan val thl = map 204169691Skan (fn t => first(fn th => aconv (lhs(concl th)) t) ths) 205169691Skan carg 206169691Skan val th0 = MP (SPECL avs (ASSUME clause)) tth 207169691Skan val th1 = rev_itlist (C (curry MK_COMB)) thl (REFL rel) 208169691Skan val th2 = EQ_MP (SYM th1) th0 209169691Skan val th3 = INST yes (DISCH atm th2) 210169691Skan val tm4 = funpow (length yes) rand (lhand(concl th3)) 211169691Skan val th4 = itlist (CONJ o REFL o #residue) yes (ASSUME tm4) 212169691Skan val th5 = GENL carg (GENL nvs (DISCH tm4 (MP th3 th4))) 213169691Skan val th6 = SPECL nvs (SPECL (map #redex plis) (ASSUME(concl th5))) 214169691Skan val th7 = itlist (CONJ o REFL o #redex) no (ASSUME ant) 215169691Skan val th8 = GENL avs (DISCH ant (MP th6 th7)) 216169691Skan in IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th8) 217169691Skan end 218169691Skan else 219169691Skan let val _ = not (null no) orelse 220169691Skan raise mk_HOL_ERR "InductiveDefinition" 221169691Skan "canonicalize_clause" 222169691Skan "Vacuous clause trivialises whole definition" 223169691Skan val atm = list_mk_conj(map mk_eq_of_bind (yes@no)) 224169691Skan val ths = CONJUNCTS (ASSUME atm) 225 val thl = map 226 (fn t => first(fn th => aconv (lhs(concl th)) t) ths) 227 carg 228 val th0 = SPECL avs (ASSUME clause) 229 val th1 = rev_itlist (C (curry MK_COMB)) thl (REFL rel) 230 val th2 = EQ_MP (SYM th1) th0 231 val th3 = INST yes (DISCH atm th2) 232 val tm4 = funpow (length yes) rand (lhand(concl th3)) 233 val th4 = itlist (CONJ o REFL o #residue) yes (ASSUME tm4) 234 val th5 = GENL carg (GENL nvs (DISCH tm4 (MP th3 th4))) 235 val th6 = SPECL nvs (SPECL (map #redex plis) (ASSUME(concl th5))) 236 val th7 = end_itlist CONJ (map (REFL o #redex) no) 237 val th8 = GENL avs (MP th6 th7) 238 in IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th8) 239 end 240 val ftm = funpow (length carg) (body o rand) (rand(concl eth)) 241 in TRANS eth (itlist MK_FORALL carg (FORALL_IMPS_CONV ftm)) 242 end 243 handle e => raise (wrap_exn "InductiveDefinition" "canonicalize_clause" e) 244end; 245 246(* ------------------------------------------------------------------------- *) 247(* Canonicalizes the set of clauses, disjoining compatible antecedants. *) 248(* ------------------------------------------------------------------------- *) 249 250local fun assoc2 x (h1::t1,h2::t2) = if aconv x h1 then h2 else assoc2 x (t1,t2) 251 | assoc2 x _ = fail() 252in 253fun canonicalize_clauses clauses = 254 let val concls = map getconcl clauses 255 val uncs = map strip_comb concls 256 val rels = itlist (op_insert aconv o fst) uncs [] 257 val xargs = map (C (op_assoc aconv) uncs) rels 258 val closed = list_mk_conj clauses 259 val avoids = all_vars closed 260 val flargs = make_args avoids (map type_of (end_foldr (op @) xargs)) 261 val vargs = shareout xargs flargs 262 val cargs = map (C assoc2 (rels,vargs) o fst) uncs 263 val cthms = map2 canonicalize_clause clauses cargs 264 val pclauses = map (rand o concl) cthms 265 fun collectclauses tm = 266 mapfilter (fn t => if aconv (fst t) tm then snd t else fail()) 267 (zip (map fst uncs) pclauses) 268 val clausell = map collectclauses rels 269 val cclausel = map list_mk_conj clausell 270 val cclauses = list_mk_conj cclausel 271 and oclauses = list_mk_conj pclauses 272 val pth = TRANS (end_itlist MK_CONJ cthms) 273 (CONJ_ACI(mk_eq(oclauses,cclauses))) 274 in TRANS pth (end_itlist MK_CONJ (map AND_IMPS_CONV cclausel)) 275 end 276 handle e => raise (wrap_exn "InductiveDefinition" "canonicalize_clauses" e) 277end; 278 279 280(* ------------------------------------------------------------------------- *) 281(* Prove definitions work for non-schematic relations with canonical rules. *) 282(* ------------------------------------------------------------------------- *) 283 284fun derive_canon_inductive_relations pclauses = 285 let val closed = list_mk_conj pclauses 286 val pclauses = strip_conj closed 287 val (vargs,bodies) = split(map strip_forall pclauses) 288 val (ants,concs) = split(map dest_imp bodies) 289 val rels = map (repeat rator) concs 290 val avoids = all_vars closed 291 val rels' = variants avoids rels 292 val prime_fn = subst (map2 (curry op |->) rels rels' ) 293 val closed' = prime_fn closed 294 fun mk_def arg con = 295 mk_eq(repeat rator con, 296 list_mk_abs(arg,list_mk_forall(rels', 297 mk_imp(closed',prime_fn con)))) 298 val deftms = map2 mk_def vargs concs 299 val defthms = map2 HALF_BETA_EXPAND vargs (map ASSUME deftms) 300 fun mk_ind args th = 301 let val th1 = fst(EQ_IMP_RULE(SPEC_ALL th)) 302 val ant = lhand(concl th1) 303 val th2 = SPECL rels' (UNDISCH th1) 304 in GENL args (DISCH ant (UNDISCH th2)) 305 end 306 val indthms = map2 mk_ind vargs defthms 307 val indthmr = end_itlist CONJ indthms 308 val indthm = GENL rels' (DISCH closed' indthmr) 309 val mconcs = map2 (fn a => fn t => 310 list_mk_forall(a,mk_imp(t,prime_fn t))) vargs ants 311 val monotm = mk_imp(concl indthmr,list_mk_conj mconcs) 312 val monothm = ASSUME(list_mk_forall(rels,list_mk_forall(rels',monotm))) 313 val closthm = ASSUME closed' 314 val monothms = CONJUNCTS 315 (MP (SPEC_ALL monothm) (MP (SPECL rels' indthm) closthm)) 316 val closthms = CONJUNCTS closthm 317 fun prove_rule mth (cth,dth) = 318 let val (avs,bod) = strip_forall(concl mth) 319 val th1 = IMP_TRANS (SPECL avs mth) (SPECL avs cth) 320 val th2 = GENL rels' (DISCH closed' (UNDISCH th1)) 321 val th3 = EQ_MP (SYM (SPECL avs dth)) th2 322 in GENL avs (DISCH (lhand bod) th3) 323 end 324 val ruvalhms = map2 prove_rule monothms (zip closthms defthms) 325 val ruvalhm = end_itlist CONJ ruvalhms 326 val dtms = map2 (curry list_mk_abs) vargs ants 327 val double_fn = subst (map2 (curry op |->) rels dtms) 328 fun mk_unbetas tm dtm = 329 let val (avs,bod) = strip_forall tm 330 val (il,r) = dest_comb bod 331 val (i,l) = dest_comb il 332 val bth = RIGHT_BETAS avs (REFL dtm) 333 val munb = AP_THM (AP_TERM i bth) r 334 val iunb = AP_TERM (mk_comb(i,double_fn l)) bth 335 val junb = AP_TERM (mk_comb(i,r)) bth 336 val quantify = itlist MK_FORALL avs 337 in (quantify munb,(quantify iunb,quantify junb)) 338 end 339 val unths = map2 mk_unbetas pclauses dtms 340 val irthm = EQ_MP (SYM(end_itlist MK_CONJ (map fst unths))) ruvalhm 341 val mrthm = MP (SPECL rels (SPECL dtms monothm)) irthm 342 val imrth = EQ_MP 343 (SYM(end_itlist MK_CONJ (map (fst o snd) unths))) mrthm 344 val ifthm = MP (SPECL dtms indthm) imrth 345 val fthm = EQ_MP (end_itlist MK_CONJ (map (snd o snd) unths)) ifthm 346 fun mk_case th1 th2 = 347 let val avs = fst(strip_forall(concl th1)) 348 in GENL avs (IMP_ANTISYM_RULE (SPEC_ALL th1) (SPEC_ALL th2)) 349 end 350 val casethm = end_itlist CONJ 351 (map2 mk_case (CONJUNCTS fthm) (CONJUNCTS ruvalhm)) 352 in CONJ ruvalhm (CONJ indthm casethm) 353 end 354 handle e => raise (wrap_exn "InductiveDefinition" 355 "derive_canon_inductive_relations"e); 356 357(* ------------------------------------------------------------------------- *) 358(* General case for nonschematic relations; monotonicity & defn hyps. *) 359(* ------------------------------------------------------------------------- *) 360 361fun derive_nonschematic_inductive_relations tm = 362 let val clauses = strip_conj tm 363 val canonthm = canonicalize_clauses clauses 364 val canonthm' = SYM canonthm 365 val pclosed = rand(concl canonthm) 366 val pclauses = strip_conj pclosed 367 val rawthm = derive_canon_inductive_relations pclauses 368 val (ruvalhm,otherthms) = CONJ_PAIR rawthm 369 val (indthm,casethm) = CONJ_PAIR otherthms 370 val ruvalhm' = EQ_MP canonthm' ruvalhm 371 and indthm' = CONV_RULE (ONCE_DEPTH_CONV (REWR_CONV canonthm')) indthm 372 in CONJ ruvalhm' (CONJ indthm' casethm) 373 end 374 handle e => raise (wrap_exn "InductiveDefinition" 375 "derive_nonschematic_inductive_relations" e); 376 377 378(* ========================================================================= *) 379(* Part 2: Tactic-integrated tools for proving monotonicity automatically. *) 380(* ========================================================================= *) 381 382 383(* ---------------------------------------------------------------------- 384 MONO_ABS_TAC 385 386 ?- (\x. P[x]) x1 .. xn ==> (\y. Q[y]) x1 .. xn 387 ================================================== 388 ?- P[x1] x2 .. xn ==> Q[x1] x2 .. xn 389 390 ---------------------------------------------------------------------- *) 391 392fun MONO_ABS_TAC (asl,w) = 393 let val (ant,con) = dest_imp w 394 val vars = snd(strip_comb con) 395 val rnum = length vars - 1 396 val (hd1,args1) = strip_ncomb rnum ant 397 and (hd2,args2) = strip_ncomb rnum con 398 val th1 = rev_itlist (C AP_THM) args1 (BETA_CONV hd1) 399 and th2 = rev_itlist (C AP_THM) args1 (BETA_CONV hd2) 400 val th3 = MK_COMB(AP_TERM boolSyntax.implication th1,th2) 401 in CONV_TAC(REWR_CONV th3) (asl,w) 402 end;; 403 404(* ---------------------------------------------------------------------- 405 MONO_UNCURRY_TAC 406 407 ?- UNCURRY f x1 .. xn ==> UNCURRY f' x1 .. xn 408 ================================================== 409 ?- f y1 y2 .. xn ==> f' y1 y2 .. xn 410 411 ---------------------------------------------------------------------- *) 412 413fun MONO_UNCURRY_TAC (asl, w) = let 414 val U = DB.fetch "pair" "UNCURRY" 415 val (ant, con) = dest_imp w 416 val vars = snd (strip_comb con) 417 val rnum = length vars - 2 418 val (hd1, args1) = strip_ncomb rnum ant 419 val (hd2, args2) = strip_ncomb rnum con 420 val th1 = rev_itlist (C AP_THM) args1 (ISPECL (#2 (strip_comb hd1)) U) 421 val th2 = rev_itlist (C AP_THM) args2 (ISPECL (#2 (strip_comb hd2)) U) 422 val th3 = MK_COMB(AP_TERM boolSyntax.implication th1, th2) 423in 424 CONV_TAC (REWR_CONV th3) (asl, w) 425end 426 427 428(* ------------------------------------------------------------------------- *) 429(* Collection, so users can add their own rules. *) 430(* *) 431(* As a simple speedup, the tactics are indexed by head operator in the *) 432(* relevant expression. If there isn't a head constant, use the empty string.*) 433(* ------------------------------------------------------------------------- *) 434(* ------------------------------------------------------------------------- *) 435(* Simplified version of MATCH_MP_TAC to avoid quantifier troubles. *) 436(* ------------------------------------------------------------------------- *) 437 438fun BACKCHAIN_TAC th = 439 let val match_fn = HO_PART_MATCH (snd o dest_imp) th 440 in fn (asl,w) => 441 let val th1 = match_fn w 442 val (ant,con) = dest_imp(concl th1) 443 in ([(asl,ant)],fn [t] => HO_MATCH_MP th1 t | _ => raise Match) 444 end 445 end;; 446 447type monoset = (string * thm) list; 448 449(*--------------------------------------------------------------------------- 450 * MONO_AND = |- (A ==> B) /\ (C ==> D) ==> (A /\ C ==> B /\ D) 451 * MONO_OR = |- (A ==> B) /\ (C ==> D) ==> (A \/ C ==> B \/ D) 452 * MONO_IMP = |- (B ==> A) /\ (C ==> D) ==> ((A ==> C) ==> (B ==> D)) 453 * MONO_NOT = |- (B ==> A) ==> (~A ==> ~B) 454 * MONO_COND = |- (w ==> x) /\ (y ==> z) ==> (COND b w y) ==> (COND b x z) 455 * MONO_ALL = |- (!x. P x ==> Q x) ==> ((!x. P x) ==> (!x. Q x)) 456 * MONO_EXISTS = |- (!x. P x ==> Q x) ==> ((?x. P x) ==> (?x. Q x)) 457 *---------------------------------------------------------------------------*) 458 459 460val MONO_EXISTS = prove ( 461 ``(!x:'a. P x ==> Q x) ==> ($? P ==> $? Q)``, 462 DISCH_THEN(MP_TAC o HO_MATCH_MP MONO_EXISTS) THEN 463 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[]) 464 465val MONO_FORALL = prove ( 466 ``(!x:'a. P x ==> Q x) ==> ($! P ==> $! Q)``, 467 DISCH_THEN(MP_TAC o HO_MATCH_MP MONO_ALL) THEN 468 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[]) 469 470val MONO_RESFORALL = prove( 471 ``(!x:'a. P' x ==> P x) /\ (!x. Q x ==> Q' x) ==> 472 (RES_FORALL P Q ==> RES_FORALL P' Q')``, 473 REWRITE_TAC [RES_FORALL_THM, IN_DEF] THEN BETA_TAC THEN REPEAT STRIP_TAC THEN 474 REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC []) 475 476val MONO_RESEXISTS = prove( 477 ``(!x:'a. P x ==> P' x) /\ (!x. Q x ==> Q' x) ==> 478 (RES_EXISTS P Q ==> RES_EXISTS P' Q')``, 479 REWRITE_TAC [RES_EXISTS_THM, IN_DEF] THEN BETA_TAC THEN REPEAT STRIP_TAC THEN 480 EXISTS_TAC ``x:'a`` THEN RES_TAC THEN ASM_REWRITE_TAC []) 481 482val MONO_COND = let open Rewrite boolTheory in 483 ONCE_REWRITE_RULE[AND_IMP_INTRO]MONO_COND 484end 485 486val bool_monoset = 487 [("/\\", MONO_AND), 488 ("\\/", MONO_OR), 489 ("?", MONO_EXISTS), 490 ("!", MONO_FORALL), 491 ("==>", MONO_IMP), 492 ("~", MONO_NOT), 493 ("COND",MONO_COND), 494 ("RES_FORALL", MONO_RESFORALL), 495 ("RES_EXISTS", MONO_RESEXISTS)] 496 497 498val IMP_REFL = let val p = mk_var("p", bool) in ASSUME p |> DISCH p |> GEN p end 499 500fun APPLY_MONOTAC monoset (asl, w) = let 501 val (a,c) = dest_imp w 502in 503 if aconv a c then ACCEPT_TAC (SPEC a IMP_REFL) (asl,w) 504 else let 505 val {Thy,Name,...} = dest_thy_const(repeat rator c) 506 handle HOL_ERR _ => {Thy = "", Name = "", 507 Ty = Type.alpha} 508 in 509 case (Thy,Name) of 510 ("","") => MONO_ABS_TAC (asl, w) 511 | ("pair", "UNCURRY") => MONO_UNCURRY_TAC (asl, w) 512 | _ => tryfind (fn (k,t) => if k = Name then BACKCHAIN_TAC t (asl,w) 513 else fail()) 514 monoset 515 end 516end 517 518(* ------------------------------------------------------------------------- *) 519(* Tactics to prove monotonicity automatically. *) 520(* ------------------------------------------------------------------------- *) 521 522fun MONO_STEP_TAC finisher monoset = 523 REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN 524 (APPLY_MONOTAC monoset ORELSE finisher) 525 526fun MONO_TAC monoset = let 527 (* first case is for monotonicity proving in making the definition, where 528 there will be an assumption of the form 529 !vs. P vs ==> P' vs 530 to hand. 531 The second case (after the ORELSE) is for proving strong induction, where 532 there won't be any assumptions, but the goal will have reduced to 533 con vs /\ con' vs ==> con vs 534 *) 535 val finisher = FIRST_ASSUM MATCH_ACCEPT_TAC ORELSE 536 (REPEAT STRIP_TAC THEN FIRST_ASSUM ACCEPT_TAC) 537in 538 REPEAT (MONO_STEP_TAC finisher monoset) 539end 540 541(* =========================================================================*) 542(* Part 3: Utility functions to modify the basic theorems in various ways. *) 543(* *) 544(* There are various fnctions that can be applied to a theorem: *) 545(* *) 546(* (1) Attempt to prove the monotonicity hypotheses *) 547(* *) 548(* (2) Generalize it over schematic variables *) 549(* *) 550(* (3) Derive a raw existence assertion *) 551(* *) 552(* (4) Actually make definitions of the inductive relations. *) 553(* *) 554(* Generally one applies either or both of (1) and (2), then does (4). *) 555(* =========================================================================*) 556 557(* ------------------------------------------------------------------------- *) 558(* Attempt to dispose of the non-equational assumption(s) of a theorem. *) 559(* ------------------------------------------------------------------------- *) 560 561fun prove_monotonicity_hyps monoset = 562 let val tac = REPEAT GEN_TAC THEN 563 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN 564 REPEAT CONJ_TAC THEN (MONO_TAC monoset) 565 fun prove_mth t = TAC_PROOF(([],t),tac) 566 in fn th => 567 let val mths = mapfilter prove_mth (filter (not o is_eq) (hyp th)) 568 in itlist PROVE_HYP mths th 569 end 570 end 571 handle e => raise (wrap_exn "InductiveDefinition" 572 "prove_monotonicity_hyps" e); 573 574(* ------------------------------------------------------------------------- *) 575(* Generalize definitions and theorem over given variables (all the same!) *) 576(* ------------------------------------------------------------------------- *) 577 578fun generalize_schematic_variables vs = 579 let fun generalize_def tm th = 580 let val (l,r) = dest_eq tm 581 val (lname,lty) = dest_var l 582 val l' = mk_var(lname,itlist (curry (op -->) o type_of) vs lty) 583 val r' = list_mk_abs(vs,r) 584 val tm' = mk_eq(l',r') 585 val th0 = RIGHT_BETAS vs (ASSUME tm') 586 val th1 = INST [l |-> lhs(concl th0)] (DISCH tm th) 587 in MP th1 th0 588 end 589 in fn th => 590 let val (defs,others) = partition is_eq (hyp th) 591 val others' = 592 map (fn t => let val fvs = free_vars t 593 in SPECL fvs (ASSUME (list_mk_forall(fvs,t))) 594 end) 595 others 596 val th1 = itlist generalize_def defs th 597 in GENL vs (itlist PROVE_HYP others' th1) 598 end 599 end; 600 601(* ------------------------------------------------------------------------- *) 602(* Derive existence. *) 603(* ------------------------------------------------------------------------- *) 604 605fun derive_existence th = itlist EXISTS_EQUATION (filter is_eq (hyp th)) th 606 607(* ------------------------------------------------------------------------- *) 608(* Make definitions. *) 609(* ------------------------------------------------------------------------- *) 610 611fun make_definitions stem th = let 612 val defs = filter is_eq (hyp th) 613 fun mkdef i tm = 614 new_definition(stem ^ Int.toString i ^ !boolLib.def_suffix, tm) 615 val dths = if length defs = 1 then 616 [new_definition(stem ^ !boolLib.def_suffix, hd defs)] 617 else 618 mapi mkdef defs 619 val insts = map2 (curry op |->) (map lhs defs) (map (lhs o concl) dths) 620in 621 rev_itlist (C MP) dths (INST insts (itlist DISCH defs th)) 622end 623 624(* ------------------------------------------------------------------------- *) 625(* "Unschematize" a set of clauses. *) 626(* ------------------------------------------------------------------------- *) 627 628val inddef_strict = ref false; 629val _ = Feedback.register_btrace ("inddef strict", inddef_strict); 630 631fun indented_term_to_string n tm = let 632 val nspaces = CharVector.tabulate(n, K #" ") 633 fun pper tm = let 634 open smpp 635 in 636 add_string nspaces >> 637 block PP.CONSISTENT n ( 638 Lib.with_flag (Parse.current_backend, PPBackEnd.raw_terminal) 639 (lift Parse.pp_term) 640 tm 641 ) 642 end 643in 644 PP.pp_to_string (!Globals.linewidth) (Parse.mlower o pper) tm 645end 646 647 648local 649 fun pare_comb qvs tm = 650 if null (op_intersect aconv (free_vars tm) qvs) 651 andalso all is_var (snd(strip_comb tm)) 652 then tm 653 else pare_comb qvs (rator tm) 654 fun schem_head cls = 655 let val (avs,bod) = strip_forall cls 656 in pare_comb avs (snd(dest_imp bod) handle HOL_ERR _ => bod) 657 end 658 fun common_prefix0 acc l1 l2 = 659 case (l1, l2) of 660 ([], _) => acc 661 | (_, []) => acc 662 | (h1::t1, h2::t2) => if aconv h1 h2 then common_prefix0 (h1::acc) t1 t2 663 else acc 664 fun common_prefix l1 l2 = List.rev (common_prefix0 [] l1 l2) 665 fun lcommon_prefix0 acc l = 666 case l of 667 [] => acc 668 | (h::t) => let 669 val newprefix = common_prefix acc h 670 in 671 if null newprefix then [] 672 else lcommon_prefix0 newprefix t 673 end 674 fun lcommon_prefix [] = [] 675 | lcommon_prefix (h::t) = lcommon_prefix0 h t 676 677in 678fun unschematize_clauses clauses = let 679 val schem = map schem_head clauses 680 val schems = op_mk_set aconv schem 681 fun insert_list l s = foldl (fn (t,s) => HOLset.add(s,t)) s l 682 val hdops = op_mk_set aconv (map (#1 o strip_comb) schems) 683 val schemv_extent = length (#2 (strip_comb (hd schems))) 684 fun is_hdop_instance t = let 685 val (f,args) = strip_comb t 686 in 687 op_mem aconv f hdops andalso length args = schemv_extent 688 end 689 val all_instances = 690 foldl (fn (t, s) => insert_list (find_terms is_hdop_instance t) s) 691 empty_tmset clauses 692 fun do_substitution schems = let 693 val avoids = all_vars (list_mk_conj clauses) 694 fun hack_fn tm = mk_var(fst(dest_var(repeat rator tm)),type_of tm) 695 val grels = variants avoids (map hack_fn schems) 696 val crels = map2 (curry op |->) schems grels 697 val clauses' = map (subst crels) clauses 698 in 699 (clauses',snd(strip_comb(hd schems))) 700 end 701in 702 if is_var(hd schem) then (clauses,[]) 703 else if !inddef_strict then 704 if not (HOLset.numItems all_instances = 1) then let 705 val instlist = HOLset.listItems all_instances 706 val t1_s = trace("types", 1) (indented_term_to_string 2) (hd instlist) 707 val t2_s = 708 trace("types", 1) (indented_term_to_string 2) (hd (tl instlist)) 709 in 710 failwith ("Schematic variable(s) not used consistently - witness\n"^ 711 t1_s^"\nand\n"^t2_s) 712 end 713 else 714 do_substitution schems 715 else (* liberal definitions *) let 716 val prefix_vars = HOLset.foldr (fn (t,l) => #2 (strip_comb t)::l) 717 [] all_instances 718 val prefix = lcommon_prefix prefix_vars 719 in 720 if null prefix then (clauses, []) 721 else let 722 val plist = String.concat (Lib.commafy 723 (map (quote o #1 o dest_var) prefix)) 724 val _ = HOL_MESG ("Treating "^plist^" as schematic variable"^ 725 (if length prefix > 1 then "s" else "")) 726 in 727 do_substitution (map (fn t => list_mk_comb(t, prefix)) hdops) 728 end 729 end 730 end 731end; 732 733(* ========================================================================= *) 734(* Part 4: The final user wrapper. *) 735(* ========================================================================= *) 736 737 738fun check_definition schemevars clocs tm = let 739 (* check that tm has no extra type variables or free variables other than *) 740 (* the heads of clauses *) 741 val clauses = strip_conj tm 742 fun ind_concl tm = #2 (dest_imp tm) handle HOL_ERR _ => tm 743 val relvars = 744 HOLset.addList(empty_tmset, 745 map (#1 o strip_comb o ind_concl o #2 o strip_forall) 746 clauses) 747 val okvars = foldl (fn (v,s) => HOLset.add(s,v)) relvars schemevars 748 val empty_tyset = HOLset.empty Type.compare 749 val reltyvars = HOLset.foldl (fn (tm,tyvset) => 750 HOLset.addList(tyvset, 751 type_vars_in_term tm)) 752 empty_tyset relvars 753 val reltyvars = List.foldl (fn (tm,tyvset) => 754 HOLset.addList(tyvset, 755 type_vars_in_term tm)) 756 reltyvars schemevars 757 758 (* check that there aren't duplicate names in the forall chain *) 759 fun check_clause_foralls n c = let 760 val (vs, body) = strip_forall c 761 val loc = List.nth(clocs, n) handle Subscript => locn.Loc_None 762 fun foldthis (v, acc) = let 763 val (nm, _) = dest_var v 764 in 765 if HOLset.member(acc, nm) then 766 raise mk_HOL_ERRloc "InductiveDefinition" 767 "check_clause" 768 loc 769 ("Clause #"^Int.toString (n + 1)^ 770 " contains duplicate name "^nm^ 771 " in outermost universal quantification") 772 else HOLset.add(acc, nm) 773 end 774 in 775 ignore (List.foldl foldthis (HOLset.empty String.compare) vs) 776 end 777 val _ = appi check_clause_foralls clauses 778 779 780 fun check_tyvars n c = let 781 val tyvs = HOLset.addList(empty_tyset, type_vars_in_term c) 782 in 783 if not (HOLset.isSubset(tyvs, reltyvars)) then let 784 val really_free = HOLset.difference(tyvs, reltyvars) 785 val free_list0 = HOLset.foldr (fn (v,sl) => dest_vartype v :: sl) 786 [] really_free 787 val free_list = Lib.commafy free_list0 788 val tmstring = trace ("types", 1) (indented_term_to_string 2) c 789 val loc = List.nth (clocs, n) handle Subscript => locn.Loc_None 790 in 791 raise mk_HOL_ERRloc 792 "InductiveDefinition" "check_clause" loc 793 (String.concat ("Clause #" :: Int.toString (n + 1):: 794 ":\n" :: tmstring :: 795 "\ncontains free type variable"^ 796 (if length free_list > 1 then "s" else "")^ 797 ": " :: free_list)) 798 end 799 else 800 () 801 end 802 val _ = appi check_tyvars clauses 803 804 805 806 (* here, generalise on the extra free variables if we're not being strict *) 807 fun check_clause n c = let 808 val fvs = FVL [c] empty_tmset 809 in 810 if not (HOLset.isSubset(fvs, okvars)) then let 811 val really_free = HOLset.difference(fvs, okvars) 812 val free_list0 = 813 HOLset.foldr (fn (v,sl) => Lib.quote (#1 (dest_var v)) :: sl) 814 [] really_free 815 val free_list = Lib.commafy free_list0 816 val loc = List.nth(clocs, n) handle Subscript => locn.Loc_None 817 in 818 if !inddef_strict then let 819 val tmstring = trace ("types", 1) (indented_term_to_string 2) c 820 in 821 raise mk_HOL_ERRloc 822 "InductiveDefinition" 823 "check_clause" 824 loc 825 (String.concat ("Clause #" :: Int.toString n :: 826 ",\n" :: tmstring :: 827 "\ncontains free variables: " :: 828 free_list)) 829 end 830 else 831 (HOL_MESG ("Generalising variable" ^ 832 (if length free_list > 1 then "s " else " ")^ 833 String.concat free_list ^ 834 " in clause #"^Int.toString n ^ 835 (if loc = locn.Loc_None then "" 836 else " ("^locn.toShortString loc^")")); 837 list_mk_forall (HOLset.listItems really_free, c)) 838 end 839 else c 840 end 841in 842 list_mk_conj (mapi check_clause clauses) 843end 844 845 846 847fun prove_nonschematic_inductive_relations_exist monoset tm = let 848 val th0 = derive_nonschematic_inductive_relations tm 849 val th1 = prove_monotonicity_hyps monoset th0 850in 851 derive_existence th1 852end 853 handle e => 854 raise (wrap_exn "InductiveDefinition" 855 "prove_nonschematic_inductive_relations_exist" e); 856 857(* ------------------------------------------------------------------------- *) 858(* The schematic case. *) 859(* *) 860(* All relations in a given call must have the same schematic args (if they *) 861(* aren't mutually inductive, use separate definitions), which must occur as *) 862(* the first arguments to each relation, in the same order(!) *) 863(* ------------------------------------------------------------------------- *) 864 865fun prove_inductive_relations_exist monoset tm = 866 let val clauses = strip_conj tm 867 val (clauses',fvs) = unschematize_clauses clauses 868 val th0 = derive_nonschematic_inductive_relations 869 (check_definition fvs [] (list_mk_conj clauses')) 870 val th1 = prove_monotonicity_hyps monoset th0 871 val th2 = generalize_schematic_variables fvs th1 872 in derive_existence th2 873 end 874 handle e => raise (wrap_exn "InductiveDefinition" 875 "prove_inductive_relations_exist" e); 876 877 878fun new_inductive_definition monoset stem (tm,clocs) = 879 let val clauses = strip_conj tm 880 val (clauses',fvs) = unschematize_clauses clauses 881 val th0 = derive_nonschematic_inductive_relations 882 (check_definition fvs clocs (list_mk_conj clauses')) 883 val th1 = prove_monotonicity_hyps monoset th0 884 val th2 = generalize_schematic_variables fvs th1 885 val th3 = make_definitions stem th2 886 val avs = fst(strip_forall(concl th3)) 887 val (r,ic) = CONJ_PAIR(SPECL avs th3) 888 val (i,c) = CONJ_PAIR ic 889 in (GENL avs r, GENL avs i, GENL avs c) 890 end 891 handle e => raise wrap_exn "InductiveDefinition" "new_inductive_definition" e; 892 893end (* InductiveDefinition *) 894