(* Title: ZF/WF.thy ID: $Id: WF.thy,v 1.25 2005/06/17 14:15:09 haftmann Exp $ Author: Tobias Nipkow and Lawrence C Paulson Copyright 1994 University of Cambridge 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. *) header{*Well-Founded Recursion*} theory WF imports Trancl begin constdefs wf :: "i=>o" (*r is a well-founded relation*) "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)" wf_on :: "[i,i]=>o" ("wf[_]'(_')") (*r is well-founded on A*) "wf_on(A,r) == wf(r Int A*A)" is_recfun :: "[i, i, [i,i]=>i, i] =>o" "is_recfun(r,a,H,f) == (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))" the_recfun :: "[i, i, [i,i]=>i] =>i" "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))" wftrec :: "[i, i, [i,i]=>i] =>i" "wftrec(r,a,H) == H(a, the_recfun(r,a,H))" wfrec :: "[i, i, [i,i]=>i] =>i" (*public version. Does not require r to be transitive*) "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))" wfrec_on :: "[i, i, i, [i,i]=>i] =>i" ("wfrec[_]'(_,_,_')") "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)" subsection{*Well-Founded Relations*} subsubsection{*Equivalences between @{term wf} and @{term wf_on}*} lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)" by (unfold wf_def wf_on_def, force) lemma wf_on_imp_wf: "[|wf[A](r); r <= A*A|] ==> wf(r)"; by (simp add: wf_on_def subset_Int_iff) lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)" by (unfold wf_def wf_on_def, fast) lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)" by (blast intro: wf_imp_wf_on wf_on_field_imp_wf) lemma wf_on_subset_A: "[| wf[A](r); B<=A |] ==> wf[B](r)" by (unfold wf_on_def wf_def, fast) lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)" by (unfold wf_on_def wf_def, fast) lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)" by (simp add: wf_def, fast) subsubsection{*Introduction Rules for @{term wf_on}*} text{*If every non-empty subset of @{term A} has an @{term r}-minimal element then we have @{term "wf[A](r)"}.*} lemma wf_onI: assumes prem: "!!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r |] ==> False" shows "wf[A](r)" apply (unfold wf_on_def wf_def) apply (rule equals0I [THEN disjCI, THEN allI]) apply (rule_tac Z = Z in prem, blast+) done text{*If @{term r} allows well-founded induction over @{term A} then we have @{term "wf[A](r)"}. Premise is equivalent to @{term "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *} lemma wf_onI2: assumes prem: "!!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A |] ==> y:B" shows "wf[A](r)" apply (rule wf_onI) apply (rule_tac c=u in prem [THEN DiffE]) prefer 3 apply blast apply fast+ done subsubsection{*Well-founded Induction*} text{*Consider the least @{term z} in @{term "domain(r)"} such that @{term "P(z)"} does not hold...*} lemma wf_induct [induct set: wf]: "[| wf(r); !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) |] ==> P(a)" apply (unfold wf_def) apply (erule_tac x = "{z : domain(r). ~ P(z)}" in allE) apply blast done lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf] text{*The form of this rule is designed to match @{text wfI}*} lemma wf_induct2: "[| wf(r); a:A; field(r)<=A; !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x) |] ==> P(a)" apply (erule_tac P="a:A" in rev_mp) apply (erule_tac a=a in wf_induct, blast) done lemma field_Int_square: "field(r Int A*A) <= A" by blast lemma wf_on_induct [consumes 2, induct set: wf_on]: "[| wf[A](r); a:A; !!x.[| x: A; ALL y:A. <y,x>: r --> P(y) |] ==> P(x) |] ==> P(a)" apply (unfold wf_on_def) apply (erule wf_induct2, assumption) apply (rule field_Int_square, blast) done lemmas wf_on_induct_rule = wf_on_induct [rule_format, consumes 2, induct set: wf_on] text{*If @{term r} allows well-founded induction then we have @{term "wf(r)"}.*} lemma wfI: "[| field(r)<=A; !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A|] ==> y:B |] ==> wf(r)" apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf]) apply (rule wf_onI2) prefer 2 apply blast apply blast done subsection{*Basic Properties of Well-Founded Relations*} lemma wf_not_refl: "wf(r) ==> <a,a> ~: r" by (erule_tac a=a in wf_induct, blast) lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. <a,x>:r --> <x,a> ~: r" by (erule_tac a=a in wf_induct, blast) (* [| wf(r); <a,x> : r; ~P ==> <x,a> : r |] ==> P *) lemmas wf_asym = wf_not_sym [THEN swap, standard] lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r" by (erule_tac a=a in wf_on_induct, assumption, blast) lemma wf_on_not_sym [rule_format]: "[| wf[A](r); a:A |] ==> ALL b:A. <a,b>:r --> <b,a>~:r" apply (erule_tac a=a in wf_on_induct, assumption, blast) done lemma wf_on_asym: "[| wf[A](r); ~Z ==> <a,b> : r; <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z" by (blast dest: wf_on_not_sym) (*Needed to prove well_ordI. Could also reason that wf[A](r) means wf(r Int A*A); thus wf( (r Int A*A)^+ ) and use wf_not_refl *) lemma wf_on_chain3: "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P" apply (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P", blast) apply (erule_tac a=a in wf_on_induct, assumption, blast) done text{*transitive closure of a WF relation is WF provided @{term A} is downward closed*} lemma wf_on_trancl: "[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)" apply (rule wf_onI2) apply (frule bspec [THEN mp], assumption+) apply (erule_tac a = y in wf_on_induct, assumption) apply (blast elim: tranclE, blast) done lemma wf_trancl: "wf(r) ==> wf(r^+)" apply (simp add: wf_iff_wf_on_field) apply (rule wf_on_subset_A) apply (erule wf_on_trancl) apply blast apply (rule trancl_type [THEN field_rel_subset]) done text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*} lemmas underI = vimage_singleton_iff [THEN iffD2, standard] lemmas underD = vimage_singleton_iff [THEN iffD1, standard] subsection{*The Predicate @{term is_recfun}*} lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)" apply (unfold is_recfun_def) apply (erule ssubst) apply (rule lamI [THEN rangeI, THEN lam_type], assumption) done lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function] lemma apply_recfun: "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))" apply (unfold is_recfun_def) txt{*replace f only on the left-hand side*} apply (erule_tac P = "%x.?t(x) = ?u" in ssubst) apply (simp add: underI) done lemma is_recfun_equal [rule_format]: "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> <x,a>:r --> <x,b>:r --> f`x=g`x" apply (frule_tac f = f in is_recfun_type) apply (frule_tac f = g in is_recfun_type) apply (simp add: is_recfun_def) apply (erule_tac a=x in wf_induct) apply (intro impI) apply (elim ssubst) apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) apply (rule_tac t = "%z. H (?x,z) " in subst_context) apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:f <-> <y,z>:g") apply (blast dest: transD) apply (simp add: apply_iff) apply (blast dest: transD intro: sym) done lemma is_recfun_cut: "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r |] ==> restrict(f, r-``{b}) = g" apply (frule_tac f = f in is_recfun_type) apply (rule fun_extension) apply (blast dest: transD intro: restrict_type2) apply (erule is_recfun_type, simp) apply (blast dest: transD intro: is_recfun_equal) done subsection{*Recursion: Main Existence Lemma*} lemma is_recfun_functional: "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g" by (blast intro: fun_extension is_recfun_type is_recfun_equal) lemma the_recfun_eq: "[| is_recfun(r,a,H,f); wf(r); trans(r) |] ==> the_recfun(r,a,H) = f" apply (unfold the_recfun_def) apply (blast intro: is_recfun_functional) done (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *) lemma is_the_recfun: "[| is_recfun(r,a,H,f); wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))" by (simp add: the_recfun_eq) lemma unfold_the_recfun: "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))" apply (rule_tac a=a in wf_induct, assumption) apply (rename_tac a1) apply (rule_tac f = "lam y: r-``{a1}. wftrec (r,y,H)" in is_the_recfun) apply typecheck apply (unfold is_recfun_def wftrec_def) --{*Applying the substitution: must keep the quantified assumption!*} apply (rule lam_cong [OF refl]) apply (drule underD) apply (fold is_recfun_def) apply (rule_tac t = "%z. H(?x,z)" in subst_context) apply (rule fun_extension) apply (blast intro: is_recfun_type) apply (rule lam_type [THEN restrict_type2]) apply blast apply (blast dest: transD) apply (frule spec [THEN mp], assumption) apply (subgoal_tac "<xa,a1> : r") apply (drule_tac x1 = xa in spec [THEN mp], assumption) apply (simp add: vimage_singleton_iff apply_recfun is_recfun_cut) apply (blast dest: transD) done subsection{*Unfolding @{term "wftrec(r,a,H)"}*} lemma the_recfun_cut: "[| wf(r); trans(r); <b,a>:r |] ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)" by (blast intro: is_recfun_cut unfold_the_recfun) (*NOT SUITABLE FOR REWRITING: it is recursive!*) lemma wftrec: "[| wf(r); trans(r) |] ==> wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))" apply (unfold wftrec_def) apply (subst unfold_the_recfun [unfolded is_recfun_def]) apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut) done subsubsection{*Removal of the Premise @{term "trans(r)"}*} (*NOT SUITABLE FOR REWRITING: it is recursive!*) lemma wfrec: "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))" apply (unfold wfrec_def) apply (erule wf_trancl [THEN wftrec, THEN ssubst]) apply (rule trans_trancl) apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context]) apply (erule r_into_trancl) apply (rule subset_refl) done (*This form avoids giant explosions in proofs. NOTE USE OF == *) lemma def_wfrec: "[| !!x. h(x)==wfrec(r,x,H); wf(r) |] ==> h(a) = H(a, lam x: r-``{a}. h(x))" apply simp apply (elim wfrec) done lemma wfrec_type: "[| 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)" apply (rule_tac a = a in wf_induct2, assumption+) apply (subst wfrec, assumption) apply (simp add: lam_type underD) done lemma wfrec_on: "[| wf[A](r); a: A |] ==> wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))" apply (unfold wf_on_def wfrec_on_def) apply (erule wfrec [THEN trans]) apply (simp add: vimage_Int_square cons_subset_iff) done text{*Minimal-element characterization of well-foundedness*} lemma wf_eq_minimal: "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))" by (unfold wf_def, blast) ML {* val wf_def = thm "wf_def"; val wf_on_def = thm "wf_on_def"; val wf_imp_wf_on = thm "wf_imp_wf_on"; val wf_on_field_imp_wf = thm "wf_on_field_imp_wf"; val wf_iff_wf_on_field = thm "wf_iff_wf_on_field"; val wf_on_subset_A = thm "wf_on_subset_A"; val wf_on_subset_r = thm "wf_on_subset_r"; val wf_onI = thm "wf_onI"; val wf_onI2 = thm "wf_onI2"; val wf_induct = thm "wf_induct"; val wf_induct2 = thm "wf_induct2"; val field_Int_square = thm "field_Int_square"; val wf_on_induct = thm "wf_on_induct"; val wfI = thm "wfI"; val wf_not_refl = thm "wf_not_refl"; val wf_not_sym = thm "wf_not_sym"; val wf_asym = thm "wf_asym"; val wf_on_not_refl = thm "wf_on_not_refl"; val wf_on_not_sym = thm "wf_on_not_sym"; val wf_on_asym = thm "wf_on_asym"; val wf_on_chain3 = thm "wf_on_chain3"; val wf_on_trancl = thm "wf_on_trancl"; val wf_trancl = thm "wf_trancl"; val underI = thm "underI"; val underD = thm "underD"; val is_recfun_type = thm "is_recfun_type"; val apply_recfun = thm "apply_recfun"; val is_recfun_equal = thm "is_recfun_equal"; val is_recfun_cut = thm "is_recfun_cut"; val is_recfun_functional = thm "is_recfun_functional"; val is_the_recfun = thm "is_the_recfun"; val unfold_the_recfun = thm "unfold_the_recfun"; val the_recfun_cut = thm "the_recfun_cut"; val wftrec = thm "wftrec"; val wfrec = thm "wfrec"; val def_wfrec = thm "def_wfrec"; val wfrec_type = thm "wfrec_type"; val wfrec_on = thm "wfrec_on"; val wf_eq_minimal = thm "wf_eq_minimal"; *} end
lemma wf_imp_wf_on:
wf(r) ==> wf[A](r)
lemma wf_on_imp_wf:
[| wf[A](r); r ⊆ A × A |] ==> wf(r)
lemma wf_on_field_imp_wf:
wf[field(r)](r) ==> wf(r)
lemma wf_iff_wf_on_field:
wf(r) <-> wf[field(r)](r)
lemma wf_on_subset_A:
[| wf[A](r); B ⊆ A |] ==> wf[B](r)
lemma wf_on_subset_r:
[| wf[A](r); s ⊆ r |] ==> wf[A](s)
lemma wf_subset:
[| wf(s); r ⊆ s |] ==> wf(r)
lemma wf_onI:
(!!Z u. [| Z ⊆ A; u ∈ Z; ∀x∈Z. ∃y∈Z. 〈y, x〉 ∈ r |] ==> False) ==> wf[A](r)
lemma wf_onI2:
(!!y B. [| ∀x∈A. (∀y∈A. 〈y, x〉 ∈ r --> y ∈ B) --> x ∈ B; y ∈ A |] ==> y ∈ B) ==> wf[A](r)
lemma wf_induct:
[| wf(r); !!x. ∀y. 〈y, x〉 ∈ r --> P(y) ==> P(x) |] ==> P(a)
lemmas wf_induct_rule:
[| wf(r); !!x. (!!y. 〈y, x〉 ∈ r ==> P(y)) ==> P(x) |] ==> P(a)
lemmas wf_induct_rule:
[| wf(r); !!x. (!!y. 〈y, x〉 ∈ r ==> P(y)) ==> P(x) |] ==> P(a)
lemma wf_induct2:
[| wf(r); a ∈ A; field(r) ⊆ A; !!x. [| x ∈ A; ∀y. 〈y, x〉 ∈ r --> P(y) |] ==> P(x) |] ==> P(a)
lemma field_Int_square:
field(r ∩ A × A) ⊆ A
lemma wf_on_induct:
[| wf[A](r); a ∈ A; !!x. [| x ∈ A; ∀y∈A. 〈y, x〉 ∈ r --> P(y) |] ==> P(x) |] ==> P(a)
lemmas wf_on_induct_rule:
[| wf[A](r); a ∈ A; !!x. [| x ∈ A; !!y. [| y ∈ A; 〈y, x〉 ∈ r |] ==> P(y) |] ==> P(x) |] ==> P(a)
lemmas wf_on_induct_rule:
[| wf[A](r); a ∈ A; !!x. [| x ∈ A; !!y. [| y ∈ A; 〈y, x〉 ∈ r |] ==> P(y) |] ==> P(x) |] ==> P(a)
lemma wfI:
[| field(r) ⊆ A; !!y B. [| ∀x∈A. (∀y∈A. 〈y, x〉 ∈ r --> y ∈ B) --> x ∈ B; y ∈ A |] ==> y ∈ B |] ==> wf(r)
lemma wf_not_refl:
wf(r) ==> 〈a, a〉 ∉ r
lemma wf_not_sym:
[| wf(r); 〈a, x〉 ∈ r |] ==> 〈x, a〉 ∉ r
lemmas wf_asym:
[| wf(r); 〈a, x〉 ∈ r; ¬ P ==> 〈x, a〉 ∈ r |] ==> P
lemmas wf_asym:
[| wf(r); 〈a, x〉 ∈ r; ¬ P ==> 〈x, a〉 ∈ r |] ==> P
lemma wf_on_not_refl:
[| wf[A](r); a ∈ A |] ==> 〈a, a〉 ∉ r
lemma wf_on_not_sym:
[| wf[A](r); a ∈ A; b ∈ A; 〈a, b〉 ∈ r |] ==> 〈b, a〉 ∉ r
lemma wf_on_asym:
[| wf[A](r); ¬ Z ==> 〈a, b〉 ∈ r; 〈b, a〉 ∉ r ==> Z; ¬ Z ==> a ∈ A; ¬ Z ==> b ∈ A |] ==> Z
lemma wf_on_chain3:
[| wf[A](r); 〈a, b〉 ∈ r; 〈b, c〉 ∈ r; 〈c, a〉 ∈ r; a ∈ A; b ∈ A; c ∈ A |] ==> P
lemma wf_on_trancl:
[| wf[A](r); r -`` A ⊆ A |] ==> wf[A](r^+)
lemma wf_trancl:
wf(r) ==> wf(r^+)
lemmas underI:
〈a, b〉 ∈ r ==> a ∈ r -`` {b}
lemmas underI:
〈a, b〉 ∈ r ==> a ∈ r -`` {b}
lemmas underD:
a ∈ r -`` {b} ==> 〈a, b〉 ∈ r
lemmas underD:
a ∈ r -`` {b} ==> 〈a, b〉 ∈ r
lemma is_recfun_type:
is_recfun(r, a, H, f) ==> f ∈ r -`` {a} -> range(f)
lemmas is_recfun_imp_function:
is_recfun(r1, a1, H1, f) ==> function(f)
lemmas is_recfun_imp_function:
is_recfun(r1, a1, H1, f) ==> function(f)
lemma apply_recfun:
[| is_recfun(r, a, H, f); 〈x, a〉 ∈ r |] ==> f ` x = H(x, restrict(f, r -`` {x}))
lemma is_recfun_equal:
[| wf(r); trans(r); is_recfun(r, a, H, f); is_recfun(r, b, H, g); 〈x, a〉 ∈ r; 〈x, b〉 ∈ r |] ==> f ` x = g ` x
lemma is_recfun_cut:
[| wf(r); trans(r); is_recfun(r, a, H, f); is_recfun(r, b, H, g); 〈b, a〉 ∈ r |] ==> restrict(f, r -`` {b}) = g
lemma is_recfun_functional:
[| wf(r); trans(r); is_recfun(r, a, H, f); is_recfun(r, a, H, g) |] ==> f = g
lemma the_recfun_eq:
[| is_recfun(r, a, H, f); wf(r); trans(r) |] ==> the_recfun(r, a, H) = f
lemma is_the_recfun:
[| is_recfun(r, a, H, f); wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r, a, H))
lemma unfold_the_recfun:
[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r, a, H))
lemma the_recfun_cut:
[| wf(r); trans(r); 〈b, a〉 ∈ r |] ==> restrict(the_recfun(r, a, H), r -`` {b}) = the_recfun(r, b, H)
lemma wftrec:
[| wf(r); trans(r) |] ==> wftrec(r, a, H) = H(a, λx∈r -`` {a}. wftrec(r, x, H))
lemma wfrec:
wf(r) ==> wfrec(r, a, H) = H(a, λx∈r -`` {a}. wfrec(r, x, H))
lemma def_wfrec:
[| !!x. h(x) == wfrec(r, x, H); wf(r) |] ==> h(a) = H(a, λx∈r -`` {a}. h(x))
lemma wfrec_type:
[| 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)
lemma wfrec_on:
[| wf[A](r); a ∈ A |] ==> wfrec[A](r,a,H) = H(a, λx∈r -`` {a} ∩ A. wfrec[A](r,x,H))
lemma wf_eq_minimal:
wf(r) <-> (∀Q x. x ∈ Q --> (∃z∈Q. ∀y. 〈y, z〉 ∈ r --> y ∉ Q))