src/ZF/OrderArith.thy
changeset 13544 895994073bdf
parent 13512 80edb859fd24
child 13634 99a593b49b04
     1.1 --- a/src/ZF/OrderArith.thy	Wed Aug 28 13:08:34 2002 +0200
     1.2 +++ b/src/ZF/OrderArith.thy	Wed Aug 28 13:08:50 2002 +0200
     1.3 @@ -356,7 +356,6 @@
     1.4  
     1.5  subsubsection{*Well-foundedness*}
     1.6  
     1.7 -(*Not sure if wf_on_rvimage could be proved from this!*)
     1.8  lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))"
     1.9  apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal)
    1.10  apply clarify
    1.11 @@ -368,6 +367,8 @@
    1.12  apply blast 
    1.13  done
    1.14  
    1.15 +text{*But note that the combination of @{text wf_imp_wf_on} and
    1.16 + @{text wf_rvimage} gives @{term "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
    1.17  lemma wf_on_rvimage: "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
    1.18  apply (rule wf_onI2)
    1.19  apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba")
    1.20 @@ -397,7 +398,34 @@
    1.21  by (unfold ord_iso_def rvimage_def, blast)
    1.22  
    1.23  
    1.24 -subsubsection{*Other Results*}
    1.25 +subsection{*Other Results*}
    1.26 +
    1.27 +lemma wf_times: "A Int B = 0 ==> wf(A*B)"
    1.28 +by (simp add: wf_def, blast)
    1.29 +
    1.30 +text{*Could also be used to prove @{text wf_radd}*}
    1.31 +lemma wf_Un:
    1.32 +     "[| range(r) Int domain(s) = 0; wf(r);  wf(s) |] ==> wf(r Un s)"
    1.33 +apply (simp add: wf_def, clarify) 
    1.34 +apply (rule equalityI) 
    1.35 + prefer 2 apply blast 
    1.36 +apply clarify 
    1.37 +apply (drule_tac x=Z in spec)
    1.38 +apply (drule_tac x="Z Int domain(s)" in spec)
    1.39 +apply simp 
    1.40 +apply (blast intro: elim: equalityE) 
    1.41 +done
    1.42 +
    1.43 +subsubsection{*The Empty Relation*}
    1.44 +
    1.45 +lemma wf0: "wf(0)"
    1.46 +by (simp add: wf_def, blast)
    1.47 +
    1.48 +lemma linear0: "linear(0,0)"
    1.49 +by (simp add: linear_def)
    1.50 +
    1.51 +lemma well_ord0: "well_ord(0,0)"
    1.52 +by (blast intro: wf_imp_wf_on well_ordI wf0 linear0)
    1.53  
    1.54  subsubsection{*The "measure" relation is useful with wfrec*}
    1.55  
    1.56 @@ -414,6 +442,31 @@
    1.57  lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
    1.58  by (simp (no_asm) add: measure_def)
    1.59  
    1.60 +lemma linear_measure: 
    1.61 + assumes Ordf: "!!x. x \<in> A ==> Ord(f(x))"
    1.62 +     and inj:  "!!x y. [|x \<in> A; y \<in> A; f(x) = f(y) |] ==> x=y"
    1.63 + shows "linear(A, measure(A,f))"
    1.64 +apply (auto simp add: linear_def) 
    1.65 +apply (rule_tac i="f(x)" and j="f(y)" in Ord_linear_lt) 
    1.66 +    apply (simp_all add: Ordf) 
    1.67 +apply (blast intro: inj) 
    1.68 +done
    1.69 +
    1.70 +lemma wf_on_measure: "wf[B](measure(A,f))"
    1.71 +by (rule wf_imp_wf_on [OF wf_measure])
    1.72 +
    1.73 +lemma well_ord_measure: 
    1.74 + assumes Ordf: "!!x. x \<in> A ==> Ord(f(x))"
    1.75 +     and inj:  "!!x y. [|x \<in> A; y \<in> A; f(x) = f(y) |] ==> x=y"
    1.76 + shows "well_ord(A, measure(A,f))"
    1.77 +apply (rule well_ordI)
    1.78 +apply (rule wf_on_measure) 
    1.79 +apply (blast intro: linear_measure Ordf inj) 
    1.80 +done
    1.81 +
    1.82 +lemma measure_type: "measure(A,f) <= A*A"
    1.83 +by (auto simp add: measure_def)
    1.84 +
    1.85  subsubsection{*Well-foundedness of Unions*}
    1.86  
    1.87  lemma wf_on_Union: