src/ZF/OrderArith.thy
changeset 13634 99a593b49b04
parent 13544 895994073bdf
child 13784 b9f6154427a4
     1.1 --- a/src/ZF/OrderArith.thy	Tue Oct 08 14:09:18 2002 +0200
     1.2 +++ b/src/ZF/OrderArith.thy	Wed Oct 09 11:07:13 2002 +0200
     1.3 @@ -398,6 +398,61 @@
     1.4  by (unfold ord_iso_def rvimage_def, blast)
     1.5  
     1.6  
     1.7 +subsection{*Every well-founded relation is a subset of some inverse image of
     1.8 +      an ordinal*}
     1.9 +
    1.10 +lemma wf_rvimage_Ord: "Ord(i) \<Longrightarrow> wf(rvimage(A, f, Memrel(i)))"
    1.11 +by (blast intro: wf_rvimage wf_Memrel)
    1.12 +
    1.13 +
    1.14 +constdefs
    1.15 +  wfrank :: "[i,i]=>i"
    1.16 +    "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
    1.17 +
    1.18 +constdefs
    1.19 +  wftype :: "i=>i"
    1.20 +    "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
    1.21 +
    1.22 +lemma wfrank: "wf(r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
    1.23 +by (subst wfrank_def [THEN def_wfrec], simp_all)
    1.24 +
    1.25 +lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))"
    1.26 +apply (rule_tac a=a in wf_induct, assumption)
    1.27 +apply (subst wfrank, assumption)
    1.28 +apply (rule Ord_succ [THEN Ord_UN], blast)
    1.29 +done
    1.30 +
    1.31 +lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
    1.32 +apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption)
    1.33 +apply (rule UN_I [THEN ltI])
    1.34 +apply (simp add: Ord_wfrank vimage_iff)+
    1.35 +done
    1.36 +
    1.37 +lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))"
    1.38 +by (simp add: wftype_def Ord_wfrank)
    1.39 +
    1.40 +lemma wftypeI: "\<lbrakk>wf(r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
    1.41 +apply (simp add: wftype_def)
    1.42 +apply (blast intro: wfrank_lt [THEN ltD])
    1.43 +done
    1.44 +
    1.45 +
    1.46 +lemma wf_imp_subset_rvimage:
    1.47 +     "[|wf(r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
    1.48 +apply (rule_tac x="wftype(r)" in exI)
    1.49 +apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI)
    1.50 +apply (simp add: Ord_wftype, clarify)
    1.51 +apply (frule subsetD, assumption, clarify)
    1.52 +apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
    1.53 +apply (blast intro: wftypeI)
    1.54 +done
    1.55 +
    1.56 +theorem wf_iff_subset_rvimage:
    1.57 +  "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r <= rvimage(A, f, Memrel(i)))"
    1.58 +by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
    1.59 +          intro: wf_rvimage_Ord [THEN wf_subset])
    1.60 +
    1.61 +
    1.62  subsection{*Other Results*}
    1.63  
    1.64  lemma wf_times: "A Int B = 0 ==> wf(A*B)"