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.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.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.41 -    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a:A & b:B"
1.43 +    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a \<in> A & b \<in> B"
1.45
1.47 -    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a':A & a:A & <a',a>:r"
1.49 +    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a':A & a \<in> A & <a',a>:r"
1.51
1.53 -    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) \<longleftrightarrow>  b':B & b:B & <b',b>:s"
1.55 +    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) \<longleftrightarrow>  b':B & b \<in> B & <b',b>:s"
1.57
1.60      "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) \<longleftrightarrow> False"
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.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.80
1.81  subsubsection{*Type checking*}
1.82
1.83 @@ -77,9 +77,9 @@
1.84
1.85  subsubsection{*Linearity*}
1.86
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.110  apply (rule wf_on_subset_A [OF _ field_radd])
1.113  done
1.114
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.139  apply (unfold ord_iso_def)
1.140  apply (safe intro!: sum_bij)
1.141 @@ -133,27 +133,27 @@
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.171 +     "(\<lambda>z\<in>(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))
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.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.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)
```