tweaks and new lemmas
authorpaulson
Wed Aug 21 15:57:08 2002 +0200 (2002-08-21)
changeset 1351280edb859fd24
parent 13511 e4b129eaa9c6
child 13513 b9e14471629c
tweaks and new lemmas
src/ZF/OrderArith.thy
     1.1 --- a/src/ZF/OrderArith.thy	Wed Aug 21 15:56:37 2002 +0200
     1.2 +++ b/src/ZF/OrderArith.thy	Wed Aug 21 15:57:08 2002 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  subsection{*Addition of Relations -- Disjoint Sum*}
     1.6  
     1.7 -(** Rewrite rules.  Can be used to obtain introduction rules **)
     1.8 +subsubsection{*Rewrite rules.  Can be used to obtain introduction rules*}
     1.9  
    1.10  lemma radd_Inl_Inr_iff [iff]: 
    1.11      "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B"
    1.12 @@ -53,7 +53,7 @@
    1.13      "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False"
    1.14  by (unfold radd_def, blast)
    1.15  
    1.16 -(** Elimination Rule **)
    1.17 +subsubsection{*Elimination Rule*}
    1.18  
    1.19  lemma raddE:
    1.20      "[| <p',p> : radd(A,r,B,s);                  
    1.21 @@ -63,7 +63,7 @@
    1.22       |] ==> Q"
    1.23  by (unfold radd_def, blast) 
    1.24  
    1.25 -(** Type checking **)
    1.26 +subsubsection{*Type checking*}
    1.27  
    1.28  lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)"
    1.29  apply (unfold radd_def)
    1.30 @@ -72,25 +72,25 @@
    1.31  
    1.32  lemmas field_radd = radd_type [THEN field_rel_subset]
    1.33  
    1.34 -(** Linearity **)
    1.35 +subsubsection{*Linearity*}
    1.36  
    1.37  lemma linear_radd: 
    1.38      "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
    1.39  by (unfold linear_def, blast) 
    1.40  
    1.41  
    1.42 -(** Well-foundedness **)
    1.43 +subsubsection{*Well-foundedness*}
    1.44  
    1.45  lemma wf_on_radd: "[| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"
    1.46  apply (rule wf_onI2)
    1.47  apply (subgoal_tac "ALL x:A. Inl (x) : Ba")
    1.48 -(*Proving the lemma, which is needed twice!*)
    1.49 + --{*Proving the lemma, which is needed twice!*}
    1.50   prefer 2
    1.51   apply (erule_tac V = "y : A + B" in thin_rl)
    1.52   apply (rule_tac ballI)
    1.53   apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
    1.54   apply blast 
    1.55 -(*Returning to main part of proof*)
    1.56 +txt{*Returning to main part of proof*}
    1.57  apply safe
    1.58  apply blast
    1.59  apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast) 
    1.60 @@ -109,7 +109,7 @@
    1.61  apply (simp add: well_ord_def tot_ord_def linear_radd)
    1.62  done
    1.63  
    1.64 -(** An ord_iso congruence law **)
    1.65 +subsubsection{*An @{term ord_iso} congruence law*}
    1.66  
    1.67  lemma sum_bij:
    1.68       "[| f: bij(A,C);  g: bij(B,D) |]
    1.69 @@ -138,7 +138,7 @@
    1.70  apply auto
    1.71  done
    1.72  
    1.73 -(** Associativity **)
    1.74 +subsubsection{*Associativity*}
    1.75  
    1.76  lemma sum_assoc_bij:
    1.77       "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))  
    1.78 @@ -157,7 +157,7 @@
    1.79  
    1.80  subsection{*Multiplication of Relations -- Lexicographic Product*}
    1.81  
    1.82 -(** Rewrite rule.  Can be used to obtain introduction rules **)
    1.83 +subsubsection{*Rewrite rule.  Can be used to obtain introduction rules*}
    1.84  
    1.85  lemma  rmult_iff [iff]: 
    1.86      "<<a',b'>, <a,b>> : rmult(A,r,B,s) <->        
    1.87 @@ -173,20 +173,20 @@
    1.88       |] ==> Q"
    1.89  by blast 
    1.90  
    1.91 -(** Type checking **)
    1.92 +subsubsection{*Type checking*}
    1.93  
    1.94  lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)"
    1.95  by (unfold rmult_def, rule Collect_subset)
    1.96  
    1.97  lemmas field_rmult = rmult_type [THEN field_rel_subset]
    1.98  
    1.99 -(** Linearity **)
   1.100 +subsubsection{*Linearity*}
   1.101  
   1.102  lemma linear_rmult:
   1.103      "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
   1.104  by (simp add: linear_def, blast) 
   1.105  
   1.106 -(** Well-foundedness **)
   1.107 +subsubsection{*Well-foundedness*}
   1.108  
   1.109  lemma wf_on_rmult: "[| wf[A](r);  wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))"
   1.110  apply (rule wf_onI2)
   1.111 @@ -214,7 +214,7 @@
   1.112  done
   1.113  
   1.114  
   1.115 -(** An ord_iso congruence law **)
   1.116 +subsubsection{*An @{term ord_iso} congruence law*}
   1.117  
   1.118  lemma prod_bij:
   1.119       "[| f: bij(A,C);  g: bij(B,D) |] 
   1.120 @@ -274,7 +274,7 @@
   1.121  apply (auto elim!: well_ord_is_wf [THEN wf_on_asym] predE)
   1.122  done
   1.123  
   1.124 -(** Distributive law **)
   1.125 +subsubsection{*Distributive law*}
   1.126  
   1.127  lemma sum_prod_distrib_bij:
   1.128       "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
   1.129 @@ -288,7 +288,7 @@
   1.130              (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
   1.131  by (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
   1.132  
   1.133 -(** Associativity **)
   1.134 +subsubsection{*Associativity*}
   1.135  
   1.136  lemma prod_assoc_bij:
   1.137       "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
   1.138 @@ -302,12 +302,12 @@
   1.139  
   1.140  subsection{*Inverse Image of a Relation*}
   1.141  
   1.142 -(** Rewrite rule **)
   1.143 +subsubsection{*Rewrite rule*}
   1.144  
   1.145  lemma rvimage_iff: "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A"
   1.146  by (unfold rvimage_def, blast)
   1.147  
   1.148 -(** Type checking **)
   1.149 +subsubsection{*Type checking*}
   1.150  
   1.151  lemma rvimage_type: "rvimage(A,f,r) <= A*A"
   1.152  apply (unfold rvimage_def, rule Collect_subset)
   1.153 @@ -319,7 +319,7 @@
   1.154  by (unfold rvimage_def, blast)
   1.155  
   1.156  
   1.157 -(** Partial Ordering Properties **)
   1.158 +subsubsection{*Partial Ordering Properties*}
   1.159  
   1.160  lemma irrefl_rvimage: 
   1.161      "[| f: inj(A,B);  irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"
   1.162 @@ -339,7 +339,7 @@
   1.163  apply (blast intro!: irrefl_rvimage trans_on_rvimage)
   1.164  done
   1.165  
   1.166 -(** Linearity **)
   1.167 +subsubsection{*Linearity*}
   1.168  
   1.169  lemma linear_rvimage:
   1.170      "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
   1.171 @@ -354,7 +354,7 @@
   1.172  done
   1.173  
   1.174  
   1.175 -(** Well-foundedness **)
   1.176 +subsubsection{*Well-foundedness*}
   1.177  
   1.178  (*Not sure if wf_on_rvimage could be proved from this!*)
   1.179  lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))"
   1.180 @@ -397,7 +397,9 @@
   1.181  by (unfold ord_iso_def rvimage_def, blast)
   1.182  
   1.183  
   1.184 -(** The "measure" relation is useful with wfrec **)
   1.185 +subsubsection{*Other Results*}
   1.186 +
   1.187 +subsubsection{*The "measure" relation is useful with wfrec*}
   1.188  
   1.189  lemma measure_eq_rvimage_Memrel:
   1.190       "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))"
   1.191 @@ -412,6 +414,28 @@
   1.192  lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
   1.193  by (simp (no_asm) add: measure_def)
   1.194  
   1.195 +subsubsection{*Well-foundedness of Unions*}
   1.196 +
   1.197 +lemma wf_on_Union:
   1.198 + assumes wfA: "wf[A](r)"
   1.199 +     and wfB: "!!a. a\<in>A ==> wf[B(a)](s)"
   1.200 +     and ok: "!!a u v. [|<u,v> \<in> s; v \<in> B(a); a \<in> A|] 
   1.201 +                       ==> (\<exists>a'\<in>A. <a',a> \<in> r & u \<in> B(a')) | u \<in> B(a)"
   1.202 + shows "wf[\<Union>a\<in>A. B(a)](s)"
   1.203 +apply (rule wf_onI2)
   1.204 +apply (erule UN_E)
   1.205 +apply (subgoal_tac "\<forall>z \<in> B(a). z \<in> Ba", blast)
   1.206 +apply (rule_tac a = a in wf_on_induct [OF wfA], assumption)
   1.207 +apply (rule ballI)
   1.208 +apply (rule_tac a = z in wf_on_induct [OF wfB], assumption, assumption)
   1.209 +apply (rename_tac u) 
   1.210 +apply (drule_tac x=u in bspec, blast) 
   1.211 +apply (erule mp, clarify)
   1.212 +apply (frule ok, assumption+); 
   1.213 +apply blast 
   1.214 +done
   1.215 +
   1.216 +
   1.217  ML {*
   1.218  val measure_def = thm "measure_def";
   1.219  val radd_Inl_Inr_iff = thm "radd_Inl_Inr_iff";