# HG changeset patch # User paulson # Date 1029938228 -7200 # Node ID 80edb859fd2499dadd108d32b8b42e9b1df870ff # Parent e4b129eaa9c646d39bff6497d24bbef77cabeac7 tweaks and new lemmas diff -r e4b129eaa9c6 -r 80edb859fd24 src/ZF/OrderArith.thy --- 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]: " : radd(A,r,B,s) <-> a:A & b:B" @@ -53,7 +53,7 @@ " : radd(A,r,B,s) <-> False" by (unfold radd_def, blast) -(** Elimination Rule **) +subsubsection{*Elimination Rule*} lemma raddE: "[| : 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]: "<, > : 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 :(A+B)*C. case(%y. Inl(), %y. Inr(), 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 <, z>:(A*B)*C. >) : 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: " : rvimage(A,f,r) <-> : 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]: " : measure(A,f) <-> x:A & y:A & f(x)A ==> wf[B(a)](s)" + and ok: "!!a u v. [| \ s; v \ B(a); a \ A|] + ==> (\a'\A. \ r & u \ B(a')) | u \ B(a)" + shows "wf[\a\A. B(a)](s)" +apply (rule wf_onI2) +apply (erule UN_E) +apply (subgoal_tac "\z \ B(a). z \ 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";