diff -r 000000000000 -r a5a9c433f639 src/ZF/WF.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/WF.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,262 @@ +(* Title: ZF/wf.ML + ID: $Id$ + Author: Tobias Nipkow and Lawrence C Paulson + Copyright 1992 University of Cambridge + +For wf.thy. Well-founded Recursion + +Derived first for transitive relations, and finally for arbitrary WF relations +via wf_trancl and trans_trancl. + +It is difficult to derive this general case directly, using r^+ instead of +r. In is_recfun, the two occurrences of the relation must have the same +form. Inserting r^+ in the_recfun or wftrec yields a recursion rule with +r^+ -`` {a} instead of r-``{a}. This recursion rule is stronger in +principle, but harder to use, especially to prove wfrec_eclose_eq in +epsilon.ML. Expanding out the definition of wftrec in wfrec would yield +a mess. +*) + +open WF; + +val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")]; + +val wf_ss = ZF_ss addcongs [H_cong]; + + +(*** Well-founded relations ***) + +(*Are these two theorems at all useful??*) + +(*If every subset of field(r) possesses an r-minimal element then wf(r). + Seems impossible to prove this for domain(r) or range(r) instead... + Consider in particular finite wf relations!*) +val [prem1,prem2] = goalw WF.thy [wf_def] + "[| field(r)<=A; \ +\ !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. :r |] ==> False |] \ +\ ==> wf(r)"; +by (rtac (equals0I RS disjCI RS allI) 1); +by (rtac prem2 1); +by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1); +by (fast_tac ZF_cs 1); +by (fast_tac ZF_cs 1); +val wfI = result(); + +(*If r allows well-founded induction then wf(r)*) +val [prem1,prem2] = goal WF.thy + "[| field(r)<=A; \ +\ !!B. ALL x:A. (ALL y. : r --> y:B) --> x:B ==> A<=B |] \ +\ ==> wf(r)"; +by (rtac (prem1 RS wfI) 1); +by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1); +by (fast_tac ZF_cs 3); +by (fast_tac ZF_cs 2); +by (fast_tac ZF_cs 1); +val wfI2 = result(); + + +(** Well-founded Induction **) + +(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*) +val major::prems = goalw WF.thy [wf_def] + "[| wf(r); \ +\ !!x.[| ALL y. : r --> P(y) |] ==> P(x) \ +\ |] ==> P(a)"; +by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ] (major RS allE) 1); +by (etac disjE 1); +by (rtac classical 1); +by (etac equals0D 1); +by (etac (singletonI RS UnI2 RS CollectI) 1); +by (etac bexE 1); +by (etac CollectE 1); +by (etac swap 1); +by (resolve_tac prems 1); +by (fast_tac ZF_cs 1); +val wf_induct = result(); + +(*Perform induction on i, then prove the wf(r) subgoal using prems. *) +fun wf_ind_tac a prems i = + EVERY [res_inst_tac [("a",a)] wf_induct i, + rename_last_tac a ["1"] (i+1), + ares_tac prems i]; + +(*The form of this rule is designed to match wfI2*) +val wfr::amem::prems = goal WF.thy + "[| wf(r); a:A; field(r)<=A; \ +\ !!x.[| x: A; ALL y. : r --> P(y) |] ==> P(x) \ +\ |] ==> P(a)"; +by (rtac (amem RS rev_mp) 1); +by (wf_ind_tac "a" [wfr] 1); +by (rtac impI 1); +by (eresolve_tac prems 1); +by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1); +val wf_induct2 = result(); + +val prems = goal WF.thy "[| wf(r); :r; :r |] ==> False"; +by (subgoal_tac "ALL x. :r --> :r --> False" 1); +by (wf_ind_tac "a" prems 2); +by (fast_tac ZF_cs 2); +by (fast_tac (FOL_cs addIs prems) 1); +val wf_anti_sym = result(); + +(*transitive closure of a WF relation is WF!*) +val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; +by (rtac (trancl_type RS field_rel_subset RS wfI2) 1); +by (rtac subsetI 1); +(*must retain the universal formula for later use!*) +by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1); +by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1); +by (rtac subset_refl 1); +by (rtac (impI RS allI) 1); +by (etac tranclE 1); +by (etac (bspec RS mp) 1); +by (etac fieldI1 1); +by (fast_tac ZF_cs 1); +by (fast_tac ZF_cs 1); +val wf_trancl = result(); + +(** r-``{a} is the set of everything under a in r **) + +val underI = standard (vimage_singleton_iff RS iffD2); +val underD = standard (vimage_singleton_iff RS iffD1); + +(** is_recfun **) + +val [major] = goalw WF.thy [is_recfun_def] + "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"; +by (rtac (major RS ssubst) 1); +by (rtac (lamI RS rangeI RS lam_type) 1); +by (assume_tac 1); +val is_recfun_type = result(); + +val [isrec,rel] = goalw WF.thy [is_recfun_def] + "[| is_recfun(r,a,H,f); :r |] ==> f`x = H(x, restrict(f,r-``{x}))"; +by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1); +by (rtac (rel RS underI RS beta) 1); +val apply_recfun = result(); + +(*eresolve_tac transD solves :r using transitivity AT MOST ONCE + spec RS mp instantiates induction hypotheses*) +fun indhyp_tac hyps = + ares_tac (TrueI::hyps) ORELSE' + (cut_facts_tac hyps THEN' + DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE' + eresolve_tac [underD, transD, spec RS mp])); + +(*** NOTE! some simplifications need a different auto_tac!! ***) +val wf_super_ss = wf_ss setauto indhyp_tac; + +val prems = goalw WF.thy [is_recfun_def] + "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \ +\ :r --> :r --> f`x=g`x"; +by (cut_facts_tac prems 1); +by (wf_ind_tac "x" prems 1); +by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); +by (rewtac restrict_def); +by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1); +val is_recfun_equal_lemma = result(); +val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp); + +val prems as [wfr,transr,recf,recg,_] = goal WF.thy + "[| wf(r); trans(r); \ +\ is_recfun(r,a,H,f); is_recfun(r,b,H,g); :r |] ==> \ +\ restrict(f, r-``{b}) = g"; +by (cut_facts_tac prems 1); +by (rtac (consI1 RS restrict_type RS fun_extension) 1); +by (etac is_recfun_type 1); +by (ALLGOALS + (ASM_SIMP_TAC (wf_super_ss addrews + [ [wfr,transr,recf,recg] MRS is_recfun_equal ]))); +val is_recfun_cut = result(); + +(*** Main Existence Lemma ***) + +val prems = goal WF.thy + "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g"; +by (cut_facts_tac prems 1); +by (rtac fun_extension 1); +by (REPEAT (ares_tac [is_recfun_equal] 1 + ORELSE eresolve_tac [is_recfun_type,underD] 1)); +val is_recfun_functional = result(); + +(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *) +val prems = goalw WF.thy [the_recfun_def] + "[| is_recfun(r,a,H,f); wf(r); trans(r) |] \ +\ ==> is_recfun(r, a, H, the_recfun(r,a,H))"; +by (rtac (ex1I RS theI) 1); +by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1)); +val is_the_recfun = result(); + +val prems = goal WF.thy + "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"; +by (cut_facts_tac prems 1); +by (wf_ind_tac "a" prems 1); +by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1); +by (REPEAT (assume_tac 2)); +by (rewrite_goals_tac [is_recfun_def, wftrec_def]); +(*Applying the substitution: must keep the quantified assumption!!*) +by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1)); +by (fold_tac [is_recfun_def]); +by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1); +by (rtac is_recfun_type 1); +by (ALLGOALS + (ASM_SIMP_TAC + (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut]))); +val unfold_the_recfun = result(); + + +(*** Unfolding wftrec ***) + +val prems = goal WF.thy + "[| wf(r); trans(r); :r |] ==> \ +\ restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"; +by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1)); +val the_recfun_cut = result(); + +(*NOT SUITABLE FOR REWRITING since it is recursive!*) +val prems = goalw WF.thy [wftrec_def] + "[| wf(r); trans(r) |] ==> \ +\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"; +by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1); +by (ALLGOALS (ASM_SIMP_TAC + (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym, + the_recfun_cut])))); +val wftrec = result(); + +(** Removal of the premise trans(r) **) + +(*NOT SUITABLE FOR REWRITING since it is recursive!*) +val [wfr] = goalw WF.thy [wfrec_def] + "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))"; +by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1); +by (rtac trans_trancl 1); +by (rtac (refl RS H_cong) 1); +by (rtac (vimage_pair_mono RS restrict_lam_eq) 1); +by (etac r_into_trancl 1); +by (rtac subset_refl 1); +val wfrec = result(); + +(*This form avoids giant explosions in proofs. NOTE USE OF == *) +val rew::prems = goal WF.thy + "[| !!x. h(x)==wfrec(r,x,H); wf(r) |] ==> \ +\ h(a) = H(a, lam x: r-``{a}. h(x))"; +by (rewtac rew); +by (REPEAT (resolve_tac (prems@[wfrec]) 1)); +val def_wfrec = result(); + +val prems = goal WF.thy + "[| wf(r); a:A; field(r)<=A; \ +\ !!x u. [| x: A; u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x) \ +\ |] ==> wfrec(r,a,H) : B(a)"; +by (res_inst_tac [("a","a")] wf_induct2 1); +by (rtac (wfrec RS ssubst) 4); +by (REPEAT (ares_tac (prems@[lam_type]) 1 + ORELSE eresolve_tac [spec RS mp, underD] 1)); +val wfrec_type = result(); + +val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def] + "[| r=r'; !!x u. H(x,u)=H'(x,u); a=a' |] \ +\ ==> wfrec(r,a,H)=wfrec(r',a',H')"; +by (EVERY1 (map rtac (prems RL [subst]))); +by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1); +val wfrec_cong = result();