--- a/src/ZF/OrderArith.thy Wed Aug 21 15:56:37 2002 +0200
+++ b/src/ZF/OrderArith.thy Wed Aug 21 15:57:08 2002 +0200
@@ -35,7 +35,7 @@
subsection{*Addition of Relations -- Disjoint Sum*}
-(** Rewrite rules. Can be used to obtain introduction rules **)
+subsubsection{*Rewrite rules. Can be used to obtain introduction rules*}
lemma radd_Inl_Inr_iff [iff]:
"<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B"
@@ -53,7 +53,7 @@
"<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"
by (unfold radd_def, blast)
-(** Elimination Rule **)
+subsubsection{*Elimination Rule*}
lemma raddE:
"[| <p',p> : radd(A,r,B,s);
@@ -63,7 +63,7 @@
|] ==> Q"
by (unfold radd_def, blast)
-(** Type checking **)
+subsubsection{*Type checking*}
lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)"
apply (unfold radd_def)
@@ -72,25 +72,25 @@
lemmas field_radd = radd_type [THEN field_rel_subset]
-(** Linearity **)
+subsubsection{*Linearity*}
lemma linear_radd:
"[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
by (unfold linear_def, blast)
-(** Well-foundedness **)
+subsubsection{*Well-foundedness*}
lemma wf_on_radd: "[| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"
apply (rule wf_onI2)
apply (subgoal_tac "ALL x:A. Inl (x) : Ba")
-(*Proving the lemma, which is needed twice!*)
+ --{*Proving the lemma, which is needed twice!*}
prefer 2
apply (erule_tac V = "y : A + B" in thin_rl)
apply (rule_tac ballI)
apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
apply blast
-(*Returning to main part of proof*)
+txt{*Returning to main part of proof*}
apply safe
apply blast
apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast)
@@ -109,7 +109,7 @@
apply (simp add: well_ord_def tot_ord_def linear_radd)
done
-(** An ord_iso congruence law **)
+subsubsection{*An @{term ord_iso} congruence law*}
lemma sum_bij:
"[| f: bij(A,C); g: bij(B,D) |]
@@ -138,7 +138,7 @@
apply auto
done
-(** Associativity **)
+subsubsection{*Associativity*}
lemma sum_assoc_bij:
"(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))
@@ -157,7 +157,7 @@
subsection{*Multiplication of Relations -- Lexicographic Product*}
-(** Rewrite rule. Can be used to obtain introduction rules **)
+subsubsection{*Rewrite rule. Can be used to obtain introduction rules*}
lemma rmult_iff [iff]:
"<<a',b'>, <a,b>> : rmult(A,r,B,s) <->
@@ -173,20 +173,20 @@
|] ==> Q"
by blast
-(** Type checking **)
+subsubsection{*Type checking*}
lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)"
by (unfold rmult_def, rule Collect_subset)
lemmas field_rmult = rmult_type [THEN field_rel_subset]
-(** Linearity **)
+subsubsection{*Linearity*}
lemma linear_rmult:
"[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
by (simp add: linear_def, blast)
-(** Well-foundedness **)
+subsubsection{*Well-foundedness*}
lemma wf_on_rmult: "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))"
apply (rule wf_onI2)
@@ -214,7 +214,7 @@
done
-(** An ord_iso congruence law **)
+subsubsection{*An @{term ord_iso} congruence law*}
lemma prod_bij:
"[| f: bij(A,C); g: bij(B,D) |]
@@ -274,7 +274,7 @@
apply (auto elim!: well_ord_is_wf [THEN wf_on_asym] predE)
done
-(** Distributive law **)
+subsubsection{*Distributive law*}
lemma sum_prod_distrib_bij:
"(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
@@ -288,7 +288,7 @@
(A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
by (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
-(** Associativity **)
+subsubsection{*Associativity*}
lemma prod_assoc_bij:
"(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
@@ -302,12 +302,12 @@
subsection{*Inverse Image of a Relation*}
-(** Rewrite rule **)
+subsubsection{*Rewrite rule*}
lemma rvimage_iff: "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A"
by (unfold rvimage_def, blast)
-(** Type checking **)
+subsubsection{*Type checking*}
lemma rvimage_type: "rvimage(A,f,r) <= A*A"
apply (unfold rvimage_def, rule Collect_subset)
@@ -319,7 +319,7 @@
by (unfold rvimage_def, blast)
-(** Partial Ordering Properties **)
+subsubsection{*Partial Ordering Properties*}
lemma irrefl_rvimage:
"[| f: inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"
@@ -339,7 +339,7 @@
apply (blast intro!: irrefl_rvimage trans_on_rvimage)
done
-(** Linearity **)
+subsubsection{*Linearity*}
lemma linear_rvimage:
"[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
@@ -354,7 +354,7 @@
done
-(** Well-foundedness **)
+subsubsection{*Well-foundedness*}
(*Not sure if wf_on_rvimage could be proved from this!*)
lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))"
@@ -397,7 +397,9 @@
by (unfold ord_iso_def rvimage_def, blast)
-(** The "measure" relation is useful with wfrec **)
+subsubsection{*Other Results*}
+
+subsubsection{*The "measure" relation is useful with wfrec*}
lemma measure_eq_rvimage_Memrel:
"measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))"
@@ -412,6 +414,28 @@
lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
by (simp (no_asm) add: measure_def)
+subsubsection{*Well-foundedness of Unions*}
+
+lemma wf_on_Union:
+ assumes wfA: "wf[A](r)"
+ and wfB: "!!a. a\<in>A ==> wf[B(a)](s)"
+ and ok: "!!a u v. [|<u,v> \<in> s; v \<in> B(a); a \<in> A|]
+ ==> (\<exists>a'\<in>A. <a',a> \<in> r & u \<in> B(a')) | u \<in> B(a)"
+ shows "wf[\<Union>a\<in>A. B(a)](s)"
+apply (rule wf_onI2)
+apply (erule UN_E)
+apply (subgoal_tac "\<forall>z \<in> B(a). z \<in> Ba", blast)
+apply (rule_tac a = a in wf_on_induct [OF wfA], assumption)
+apply (rule ballI)
+apply (rule_tac a = z in wf_on_induct [OF wfB], assumption, assumption)
+apply (rename_tac u)
+apply (drule_tac x=u in bspec, blast)
+apply (erule mp, clarify)
+apply (frule ok, assumption+);
+apply blast
+done
+
+
ML {*
val measure_def = thm "measure_def";
val radd_Inl_Inr_iff = thm "radd_Inl_Inr_iff";