src/ZF/OrderArith.thy
changeset 46953 2b6e55924af3
parent 46821 ff6b0c1087f2
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/OrderArith.thy	Thu Mar 15 15:54:22 2012 +0000
     1.2 +++ b/src/ZF/OrderArith.thy	Thu Mar 15 16:35:02 2012 +0000
     1.3 @@ -10,24 +10,24 @@
     1.4  definition
     1.5    (*disjoint sum of two relations; underlies ordinal addition*)
     1.6    radd    :: "[i,i,i,i]=>i"  where
     1.7 -    "radd(A,r,B,s) == 
     1.8 -                {z: (A+B) * (A+B).  
     1.9 -                    (\<exists>x y. z = <Inl(x), Inr(y)>)   |   
    1.10 -                    (\<exists>x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |      
    1.11 +    "radd(A,r,B,s) ==
    1.12 +                {z: (A+B) * (A+B).
    1.13 +                    (\<exists>x y. z = <Inl(x), Inr(y)>)   |
    1.14 +                    (\<exists>x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |
    1.15                      (\<exists>y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
    1.16  
    1.17  definition
    1.18    (*lexicographic product of two relations; underlies ordinal multiplication*)
    1.19    rmult   :: "[i,i,i,i]=>i"  where
    1.20 -    "rmult(A,r,B,s) == 
    1.21 -                {z: (A*B) * (A*B).  
    1.22 -                    \<exists>x' y' x y. z = <<x',y'>, <x,y>> &         
    1.23 +    "rmult(A,r,B,s) ==
    1.24 +                {z: (A*B) * (A*B).
    1.25 +                    \<exists>x' y' x y. z = <<x',y'>, <x,y>> &
    1.26                         (<x',x>: r | (x'=x & <y',y>: s))}"
    1.27  
    1.28  definition
    1.29    (*inverse image of a relation*)
    1.30    rvimage :: "[i,i,i]=>i"  where
    1.31 -    "rvimage(A,f,r) == {z: A*A. \<exists>x y. z = <x,y> & <f`x,f`y>: r}"
    1.32 +    "rvimage(A,f,r) == {z \<in> A*A. \<exists>x y. z = <x,y> & <f`x,f`y>: r}"
    1.33  
    1.34  definition
    1.35    measure :: "[i, i\<Rightarrow>i] \<Rightarrow> i"  where
    1.36 @@ -38,33 +38,33 @@
    1.37  
    1.38  subsubsection{*Rewrite rules.  Can be used to obtain introduction rules*}
    1.39  
    1.40 -lemma radd_Inl_Inr_iff [iff]: 
    1.41 -    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a:A & b:B"
    1.42 +lemma radd_Inl_Inr_iff [iff]:
    1.43 +    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a \<in> A & b \<in> B"
    1.44  by (unfold radd_def, blast)
    1.45  
    1.46 -lemma radd_Inl_iff [iff]: 
    1.47 -    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a':A & a:A & <a',a>:r"
    1.48 +lemma radd_Inl_iff [iff]:
    1.49 +    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a':A & a \<in> A & <a',a>:r"
    1.50  by (unfold radd_def, blast)
    1.51  
    1.52 -lemma radd_Inr_iff [iff]: 
    1.53 -    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) \<longleftrightarrow>  b':B & b:B & <b',b>:s"
    1.54 +lemma radd_Inr_iff [iff]:
    1.55 +    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) \<longleftrightarrow>  b':B & b \<in> B & <b',b>:s"
    1.56  by (unfold radd_def, blast)
    1.57  
    1.58 -lemma radd_Inr_Inl_iff [simp]: 
    1.59 +lemma radd_Inr_Inl_iff [simp]:
    1.60      "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) \<longleftrightarrow> False"
    1.61  by (unfold radd_def, blast)
    1.62  
    1.63 -declare radd_Inr_Inl_iff [THEN iffD1, dest!] 
    1.64 +declare radd_Inr_Inl_iff [THEN iffD1, dest!]
    1.65  
    1.66  subsubsection{*Elimination Rule*}
    1.67  
    1.68  lemma raddE:
    1.69 -    "[| <p',p> \<in> radd(A,r,B,s);                  
    1.70 -        !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q;        
    1.71 -        !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q;  
    1.72 -        !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q   
    1.73 +    "[| <p',p> \<in> radd(A,r,B,s);
    1.74 +        !!x y. [| p'=Inl(x); x \<in> A; p=Inr(y); y \<in> B |] ==> Q;
    1.75 +        !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x \<in> A |] ==> Q;
    1.76 +        !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y \<in> B |] ==> Q
    1.77       |] ==> Q"
    1.78 -by (unfold radd_def, blast) 
    1.79 +by (unfold radd_def, blast)
    1.80  
    1.81  subsubsection{*Type checking*}
    1.82  
    1.83 @@ -77,9 +77,9 @@
    1.84  
    1.85  subsubsection{*Linearity*}
    1.86  
    1.87 -lemma linear_radd: 
    1.88 +lemma linear_radd:
    1.89      "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
    1.90 -by (unfold linear_def, blast) 
    1.91 +by (unfold linear_def, blast)
    1.92  
    1.93  
    1.94  subsubsection{*Well-foundedness*}
    1.95 @@ -92,17 +92,17 @@
    1.96   apply (erule_tac V = "y \<in> A + B" in thin_rl)
    1.97   apply (rule_tac ballI)
    1.98   apply (erule_tac r = r and a = x in wf_on_induct, assumption)
    1.99 - apply blast 
   1.100 + apply blast
   1.101  txt{*Returning to main part of proof*}
   1.102  apply safe
   1.103  apply blast
   1.104 -apply (erule_tac r = s and a = ya in wf_on_induct, assumption, blast) 
   1.105 +apply (erule_tac r = s and a = ya in wf_on_induct, assumption, blast)
   1.106  done
   1.107  
   1.108  lemma wf_radd: "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
   1.109  apply (simp add: wf_iff_wf_on_field)
   1.110  apply (rule wf_on_subset_A [OF _ field_radd])
   1.111 -apply (blast intro: wf_on_radd) 
   1.112 +apply (blast intro: wf_on_radd)
   1.113  done
   1.114  
   1.115  lemma well_ord_radd:
   1.116 @@ -115,17 +115,17 @@
   1.117  subsubsection{*An @{term ord_iso} congruence law*}
   1.118  
   1.119  lemma sum_bij:
   1.120 -     "[| f: bij(A,C);  g: bij(B,D) |]
   1.121 +     "[| f \<in> bij(A,C);  g \<in> bij(B,D) |]
   1.122        ==> (\<lambda>z\<in>A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) \<in> bij(A+B, C+D)"
   1.123 -apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))" 
   1.124 +apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))"
   1.125         in lam_bijective)
   1.126 -apply (typecheck add: bij_is_inj inj_is_fun) 
   1.127 -apply (auto simp add: left_inverse_bij right_inverse_bij) 
   1.128 +apply (typecheck add: bij_is_inj inj_is_fun)
   1.129 +apply (auto simp add: left_inverse_bij right_inverse_bij)
   1.130  done
   1.131  
   1.132 -lemma sum_ord_iso_cong: 
   1.133 -    "[| f: ord_iso(A,r,A',r');  g: ord_iso(B,s,B',s') |] ==>      
   1.134 -            (\<lambda>z\<in>A+B. case(%x. Inl(f`x), %y. Inr(g`y), z))             
   1.135 +lemma sum_ord_iso_cong:
   1.136 +    "[| f \<in> ord_iso(A,r,A',r');  g \<in> ord_iso(B,s,B',s') |] ==>
   1.137 +            (\<lambda>z\<in>A+B. case(%x. Inl(f`x), %y. Inr(g`y), z))
   1.138              \<in> ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))"
   1.139  apply (unfold ord_iso_def)
   1.140  apply (safe intro!: sum_bij)
   1.141 @@ -133,27 +133,27 @@
   1.142  apply (auto cong add: conj_cong simp add: bij_is_fun [THEN apply_type])
   1.143  done
   1.144  
   1.145 -(*Could we prove an ord_iso result?  Perhaps 
   1.146 +(*Could we prove an ord_iso result?  Perhaps
   1.147       ord_iso(A+B, radd(A,r,B,s), A \<union> B, r \<union> s) *)
   1.148 -lemma sum_disjoint_bij: "A \<inter> B = 0 ==>      
   1.149 +lemma sum_disjoint_bij: "A \<inter> B = 0 ==>
   1.150              (\<lambda>z\<in>A+B. case(%x. x, %y. y, z)) \<in> bij(A+B, A \<union> B)"
   1.151 -apply (rule_tac d = "%z. if z:A then Inl (z) else Inr (z) " in lam_bijective)
   1.152 +apply (rule_tac d = "%z. if z \<in> A then Inl (z) else Inr (z) " in lam_bijective)
   1.153  apply auto
   1.154  done
   1.155  
   1.156  subsubsection{*Associativity*}
   1.157  
   1.158  lemma sum_assoc_bij:
   1.159 -     "(\<lambda>z\<in>(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))  
   1.160 +     "(\<lambda>z\<in>(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))
   1.161        \<in> bij((A+B)+C, A+(B+C))"
   1.162 -apply (rule_tac d = "case (%x. Inl (Inl (x)), case (%x. Inl (Inr (x)), Inr))" 
   1.163 +apply (rule_tac d = "case (%x. Inl (Inl (x)), case (%x. Inl (Inr (x)), Inr))"
   1.164         in lam_bijective)
   1.165  apply auto
   1.166  done
   1.167  
   1.168  lemma sum_assoc_ord_iso:
   1.169 -     "(\<lambda>z\<in>(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))  
   1.170 -      \<in> ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),     
   1.171 +     "(\<lambda>z\<in>(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))
   1.172 +      \<in> ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),
   1.173                  A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"
   1.174  by (rule sum_assoc_bij [THEN ord_isoI], auto)
   1.175  
   1.176 @@ -162,19 +162,19 @@
   1.177  
   1.178  subsubsection{*Rewrite rule.  Can be used to obtain introduction rules*}
   1.179  
   1.180 -lemma  rmult_iff [iff]: 
   1.181 -    "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) \<longleftrightarrow>        
   1.182 -            (<a',a>: r  & a':A & a:A & b': B & b: B) |   
   1.183 -            (<b',b>: s  & a'=a & a:A & b': B & b: B)"
   1.184 +lemma  rmult_iff [iff]:
   1.185 +    "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) \<longleftrightarrow>
   1.186 +            (<a',a>: r  & a':A & a \<in> A & b': B & b \<in> B) |
   1.187 +            (<b',b>: s  & a'=a & a \<in> A & b': B & b \<in> B)"
   1.188  
   1.189  by (unfold rmult_def, blast)
   1.190  
   1.191 -lemma rmultE: 
   1.192 -    "[| <<a',b'>, <a,b>> \<in> rmult(A,r,B,s);               
   1.193 -        [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;         
   1.194 -        [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q  
   1.195 +lemma rmultE:
   1.196 +    "[| <<a',b'>, <a,b>> \<in> rmult(A,r,B,s);
   1.197 +        [| <a',a>: r;  a':A;  a \<in> A;  b':B;  b \<in> B |] ==> Q;
   1.198 +        [| <b',b>: s;  a \<in> A;  a'=a;  b':B;  b \<in> B |] ==> Q
   1.199       |] ==> Q"
   1.200 -by blast 
   1.201 +by blast
   1.202  
   1.203  subsubsection{*Type checking*}
   1.204  
   1.205 @@ -187,7 +187,7 @@
   1.206  
   1.207  lemma linear_rmult:
   1.208      "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
   1.209 -by (simp add: linear_def, blast) 
   1.210 +by (simp add: linear_def, blast)
   1.211  
   1.212  subsubsection{*Well-foundedness*}
   1.213  
   1.214 @@ -206,7 +206,7 @@
   1.215  lemma wf_rmult: "[| wf(r);  wf(s) |] ==> wf(rmult(field(r),r,field(s),s))"
   1.216  apply (simp add: wf_iff_wf_on_field)
   1.217  apply (rule wf_on_subset_A [OF _ field_rmult])
   1.218 -apply (blast intro: wf_on_rmult) 
   1.219 +apply (blast intro: wf_on_rmult)
   1.220  done
   1.221  
   1.222  lemma well_ord_rmult:
   1.223 @@ -220,17 +220,17 @@
   1.224  subsubsection{*An @{term ord_iso} congruence law*}
   1.225  
   1.226  lemma prod_bij:
   1.227 -     "[| f: bij(A,C);  g: bij(B,D) |] 
   1.228 +     "[| f \<in> bij(A,C);  g \<in> bij(B,D) |]
   1.229        ==> (lam <x,y>:A*B. <f`x, g`y>) \<in> bij(A*B, C*D)"
   1.230 -apply (rule_tac d = "%<x,y>. <converse (f) `x, converse (g) `y>" 
   1.231 +apply (rule_tac d = "%<x,y>. <converse (f) `x, converse (g) `y>"
   1.232         in lam_bijective)
   1.233 -apply (typecheck add: bij_is_inj inj_is_fun) 
   1.234 -apply (auto simp add: left_inverse_bij right_inverse_bij) 
   1.235 +apply (typecheck add: bij_is_inj inj_is_fun)
   1.236 +apply (auto simp add: left_inverse_bij right_inverse_bij)
   1.237  done
   1.238  
   1.239 -lemma prod_ord_iso_cong: 
   1.240 -    "[| f: ord_iso(A,r,A',r');  g: ord_iso(B,s,B',s') |]      
   1.241 -     ==> (lam <x,y>:A*B. <f`x, g`y>)                                  
   1.242 +lemma prod_ord_iso_cong:
   1.243 +    "[| f \<in> ord_iso(A,r,A',r');  g \<in> ord_iso(B,s,B',s') |]
   1.244 +     ==> (lam <x,y>:A*B. <f`x, g`y>)
   1.245           \<in> ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))"
   1.246  apply (unfold ord_iso_def)
   1.247  apply (safe intro!: prod_bij)
   1.248 @@ -243,7 +243,7 @@
   1.249  
   1.250  (*Used??*)
   1.251  lemma singleton_prod_ord_iso:
   1.252 -     "well_ord({x},xr) ==>   
   1.253 +     "well_ord({x},xr) ==>
   1.254            (\<lambda>z\<in>A. <x,z>) \<in> ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))"
   1.255  apply (rule singleton_prod_bij [THEN ord_isoI])
   1.256  apply (simp (no_asm_simp))
   1.257 @@ -253,8 +253,8 @@
   1.258  (*Here we build a complicated function term, then simplify it using
   1.259    case_cong, id_conv, comp_lam, case_case.*)
   1.260  lemma prod_sum_singleton_bij:
   1.261 -     "a\<notin>C ==>  
   1.262 -       (\<lambda>x\<in>C*B + D. case(%x. x, %y.<a,y>, x))  
   1.263 +     "a\<notin>C ==>
   1.264 +       (\<lambda>x\<in>C*B + D. case(%x. x, %y.<a,y>, x))
   1.265         \<in> bij(C*B + D, C*B \<union> {a}*D)"
   1.266  apply (rule subst_elem)
   1.267  apply (rule id_bij [THEN sum_bij, THEN comp_bij])
   1.268 @@ -267,10 +267,10 @@
   1.269  done
   1.270  
   1.271  lemma prod_sum_singleton_ord_iso:
   1.272 - "[| a:A;  well_ord(A,r) |] ==>  
   1.273 -    (\<lambda>x\<in>pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x))  
   1.274 -    \<in> ord_iso(pred(A,a,r)*B + pred(B,b,s),               
   1.275 -                  radd(A*B, rmult(A,r,B,s), B, s),       
   1.276 + "[| a \<in> A;  well_ord(A,r) |] ==>
   1.277 +    (\<lambda>x\<in>pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x))
   1.278 +    \<in> ord_iso(pred(A,a,r)*B + pred(B,b,s),
   1.279 +                  radd(A*B, rmult(A,r,B,s), B, s),
   1.280                pred(A,a,r)*B \<union> {a}*pred(B,b,s), rmult(A,r,B,s))"
   1.281  apply (rule prod_sum_singleton_bij [THEN ord_isoI])
   1.282  apply (simp (no_asm_simp) add: pred_iff well_ord_is_wf [THEN wf_on_not_refl])
   1.283 @@ -280,14 +280,14 @@
   1.284  subsubsection{*Distributive law*}
   1.285  
   1.286  lemma sum_prod_distrib_bij:
   1.287 -     "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
   1.288 +     "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
   1.289        \<in> bij((A+B)*C, (A*C)+(B*C))"
   1.290 -by (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) " 
   1.291 +by (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) "
   1.292      in lam_bijective, auto)
   1.293  
   1.294  lemma sum_prod_distrib_ord_iso:
   1.295 - "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
   1.296 -  \<in> ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t),  
   1.297 + "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
   1.298 +  \<in> ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t),
   1.299              (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
   1.300  by (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
   1.301  
   1.302 @@ -298,8 +298,8 @@
   1.303  by (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
   1.304  
   1.305  lemma prod_assoc_ord_iso:
   1.306 - "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                    
   1.307 -  \<in> ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),   
   1.308 + "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)
   1.309 +  \<in> ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),
   1.310              A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"
   1.311  by (rule prod_assoc_bij [THEN ord_isoI], auto)
   1.312  
   1.313 @@ -307,7 +307,7 @@
   1.314  
   1.315  subsubsection{*Rewrite rule*}
   1.316  
   1.317 -lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r)  \<longleftrightarrow>  <f`a,f`b>: r & a:A & b:A"
   1.318 +lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r)  \<longleftrightarrow>  <f`a,f`b>: r & a \<in> A & b \<in> A"
   1.319  by (unfold rvimage_def, blast)
   1.320  
   1.321  subsubsection{*Type checking*}
   1.322 @@ -323,20 +323,20 @@
   1.323  
   1.324  subsubsection{*Partial Ordering Properties*}
   1.325  
   1.326 -lemma irrefl_rvimage: 
   1.327 -    "[| f: inj(A,B);  irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"
   1.328 +lemma irrefl_rvimage:
   1.329 +    "[| f \<in> inj(A,B);  irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"
   1.330  apply (unfold irrefl_def rvimage_def)
   1.331  apply (blast intro: inj_is_fun [THEN apply_type])
   1.332  done
   1.333  
   1.334 -lemma trans_on_rvimage: 
   1.335 -    "[| f: inj(A,B);  trans[B](r) |] ==> trans[A](rvimage(A,f,r))"
   1.336 +lemma trans_on_rvimage:
   1.337 +    "[| f \<in> inj(A,B);  trans[B](r) |] ==> trans[A](rvimage(A,f,r))"
   1.338  apply (unfold trans_on_def rvimage_def)
   1.339  apply (blast intro: inj_is_fun [THEN apply_type])
   1.340  done
   1.341  
   1.342 -lemma part_ord_rvimage: 
   1.343 -    "[| f: inj(A,B);  part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))"
   1.344 +lemma part_ord_rvimage:
   1.345 +    "[| f \<in> inj(A,B);  part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))"
   1.346  apply (unfold part_ord_def)
   1.347  apply (blast intro!: irrefl_rvimage trans_on_rvimage)
   1.348  done
   1.349 @@ -344,13 +344,13 @@
   1.350  subsubsection{*Linearity*}
   1.351  
   1.352  lemma linear_rvimage:
   1.353 -    "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
   1.354 -apply (simp add: inj_def linear_def rvimage_iff) 
   1.355 -apply (blast intro: apply_funtype) 
   1.356 +    "[| f \<in> inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
   1.357 +apply (simp add: inj_def linear_def rvimage_iff)
   1.358 +apply (blast intro: apply_funtype)
   1.359  done
   1.360  
   1.361 -lemma tot_ord_rvimage: 
   1.362 -    "[| f: inj(A,B);  tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))"
   1.363 +lemma tot_ord_rvimage:
   1.364 +    "[| f \<in> inj(A,B);  tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))"
   1.365  apply (unfold tot_ord_def)
   1.366  apply (blast intro!: part_ord_rvimage linear_rvimage)
   1.367  done
   1.368 @@ -361,19 +361,19 @@
   1.369  lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))"
   1.370  apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal)
   1.371  apply clarify
   1.372 -apply (subgoal_tac "\<exists>w. w \<in> {w: {f`x. x:Q}. \<exists>x. x: Q & (f`x = w) }")
   1.373 +apply (subgoal_tac "\<exists>w. w \<in> {w: {f`x. x \<in> Q}. \<exists>x. x \<in> Q & (f`x = w) }")
   1.374   apply (erule allE)
   1.375   apply (erule impE)
   1.376   apply assumption
   1.377   apply blast
   1.378 -apply blast 
   1.379 +apply blast
   1.380  done
   1.381  
   1.382  text{*But note that the combination of @{text wf_imp_wf_on} and
   1.383   @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
   1.384 -lemma wf_on_rvimage: "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
   1.385 +lemma wf_on_rvimage: "[| f \<in> A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
   1.386  apply (rule wf_onI2)
   1.387 -apply (subgoal_tac "\<forall>z\<in>A. f`z=f`y \<longrightarrow> z: Ba")
   1.388 +apply (subgoal_tac "\<forall>z\<in>A. f`z=f`y \<longrightarrow> z \<in> Ba")
   1.389   apply blast
   1.390  apply (erule_tac a = "f`y" in wf_on_induct)
   1.391   apply (blast intro!: apply_funtype)
   1.392 @@ -382,21 +382,21 @@
   1.393  
   1.394  (*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
   1.395  lemma well_ord_rvimage:
   1.396 -     "[| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))"
   1.397 +     "[| f \<in> inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))"
   1.398  apply (rule well_ordI)
   1.399  apply (unfold well_ord_def tot_ord_def)
   1.400  apply (blast intro!: wf_on_rvimage inj_is_fun)
   1.401  apply (blast intro!: linear_rvimage)
   1.402  done
   1.403  
   1.404 -lemma ord_iso_rvimage: 
   1.405 -    "f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)"
   1.406 +lemma ord_iso_rvimage:
   1.407 +    "f \<in> bij(A,B) ==> f \<in> ord_iso(A, rvimage(A,f,s), B, s)"
   1.408  apply (unfold ord_iso_def)
   1.409  apply (simp add: rvimage_iff)
   1.410  done
   1.411  
   1.412 -lemma ord_iso_rvimage_eq: 
   1.413 -    "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r \<inter> A*A"
   1.414 +lemma ord_iso_rvimage_eq:
   1.415 +    "f \<in> ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r \<inter> A*A"
   1.416  by (unfold ord_iso_def rvimage_def, blast)
   1.417  
   1.418  
   1.419 @@ -463,14 +463,14 @@
   1.420  text{*Could also be used to prove @{text wf_radd}*}
   1.421  lemma wf_Un:
   1.422       "[| range(r) \<inter> domain(s) = 0; wf(r);  wf(s) |] ==> wf(r \<union> s)"
   1.423 -apply (simp add: wf_def, clarify) 
   1.424 -apply (rule equalityI) 
   1.425 - prefer 2 apply blast 
   1.426 -apply clarify 
   1.427 +apply (simp add: wf_def, clarify)
   1.428 +apply (rule equalityI)
   1.429 + prefer 2 apply blast
   1.430 +apply clarify
   1.431  apply (drule_tac x=Z in spec)
   1.432  apply (drule_tac x="Z \<inter> domain(s)" in spec)
   1.433 -apply simp 
   1.434 -apply (blast intro: elim: equalityE) 
   1.435 +apply simp
   1.436 +apply (blast intro: elim: equalityE)
   1.437  done
   1.438  
   1.439  subsubsection{*The Empty Relation*}
   1.440 @@ -496,29 +496,29 @@
   1.441  lemma wf_measure [iff]: "wf(measure(A,f))"
   1.442  by (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
   1.443  
   1.444 -lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) \<longleftrightarrow> x:A & y:A & f(x)<f(y)"
   1.445 +lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) \<longleftrightarrow> x \<in> A & y \<in> A & f(x)<f(y)"
   1.446  by (simp (no_asm) add: measure_def)
   1.447  
   1.448 -lemma linear_measure: 
   1.449 +lemma linear_measure:
   1.450   assumes Ordf: "!!x. x \<in> A ==> Ord(f(x))"
   1.451       and inj:  "!!x y. [|x \<in> A; y \<in> A; f(x) = f(y) |] ==> x=y"
   1.452   shows "linear(A, measure(A,f))"
   1.453 -apply (auto simp add: linear_def) 
   1.454 -apply (rule_tac i="f(x)" and j="f(y)" in Ord_linear_lt) 
   1.455 -    apply (simp_all add: Ordf) 
   1.456 -apply (blast intro: inj) 
   1.457 +apply (auto simp add: linear_def)
   1.458 +apply (rule_tac i="f(x)" and j="f(y)" in Ord_linear_lt)
   1.459 +    apply (simp_all add: Ordf)
   1.460 +apply (blast intro: inj)
   1.461  done
   1.462  
   1.463  lemma wf_on_measure: "wf[B](measure(A,f))"
   1.464  by (rule wf_imp_wf_on [OF wf_measure])
   1.465  
   1.466 -lemma well_ord_measure: 
   1.467 +lemma well_ord_measure:
   1.468   assumes Ordf: "!!x. x \<in> A ==> Ord(f(x))"
   1.469       and inj:  "!!x y. [|x \<in> A; y \<in> A; f(x) = f(y) |] ==> x=y"
   1.470   shows "well_ord(A, measure(A,f))"
   1.471  apply (rule well_ordI)
   1.472 -apply (rule wf_on_measure) 
   1.473 -apply (blast intro: linear_measure Ordf inj) 
   1.474 +apply (rule wf_on_measure)
   1.475 +apply (blast intro: linear_measure Ordf inj)
   1.476  done
   1.477  
   1.478  lemma measure_type: "measure(A,f) \<subseteq> A*A"
   1.479 @@ -529,7 +529,7 @@
   1.480  lemma wf_on_Union:
   1.481   assumes wfA: "wf[A](r)"
   1.482       and wfB: "!!a. a\<in>A ==> wf[B(a)](s)"
   1.483 -     and ok: "!!a u v. [|<u,v> \<in> s; v \<in> B(a); a \<in> A|] 
   1.484 +     and ok: "!!a u v. [|<u,v> \<in> s; v \<in> B(a); a \<in> A|]
   1.485                         ==> (\<exists>a'\<in>A. <a',a> \<in> r & u \<in> B(a')) | u \<in> B(a)"
   1.486   shows "wf[\<Union>a\<in>A. B(a)](s)"
   1.487  apply (rule wf_onI2)
   1.488 @@ -538,25 +538,25 @@
   1.489  apply (rule_tac a = a in wf_on_induct [OF wfA], assumption)
   1.490  apply (rule ballI)
   1.491  apply (rule_tac a = z in wf_on_induct [OF wfB], assumption, assumption)
   1.492 -apply (rename_tac u) 
   1.493 -apply (drule_tac x=u in bspec, blast) 
   1.494 +apply (rename_tac u)
   1.495 +apply (drule_tac x=u in bspec, blast)
   1.496  apply (erule mp, clarify)
   1.497 -apply (frule ok, assumption+, blast) 
   1.498 +apply (frule ok, assumption+, blast)
   1.499  done
   1.500  
   1.501  subsubsection{*Bijections involving Powersets*}
   1.502  
   1.503  lemma Pow_sum_bij:
   1.504 -    "(\<lambda>Z \<in> Pow(A+B). <{x \<in> A. Inl(x) \<in> Z}, {y \<in> B. Inr(y) \<in> Z}>)  
   1.505 +    "(\<lambda>Z \<in> Pow(A+B). <{x \<in> A. Inl(x) \<in> Z}, {y \<in> B. Inr(y) \<in> Z}>)
   1.506       \<in> bij(Pow(A+B), Pow(A)*Pow(B))"
   1.507 -apply (rule_tac d = "%<X,Y>. {Inl (x). x \<in> X} \<union> {Inr (y). y \<in> Y}" 
   1.508 +apply (rule_tac d = "%<X,Y>. {Inl (x). x \<in> X} \<union> {Inr (y). y \<in> Y}"
   1.509         in lam_bijective)
   1.510  apply force+
   1.511  done
   1.512  
   1.513  text{*As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"} *}
   1.514  lemma Pow_Sigma_bij:
   1.515 -    "(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})  
   1.516 +    "(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})
   1.517       \<in> bij(Pow(Sigma(A,B)), \<Pi> x \<in> A. Pow(B(x)))"
   1.518  apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
   1.519  apply (blast intro: lam_type)