src/ZF/OrderArith.thy
 changeset 60770 240563fbf41d parent 58871 c399ae4b836f child 61798 27f3c10b0b50
```     1.1 --- a/src/ZF/OrderArith.thy	Thu Jul 23 14:20:51 2015 +0200
1.2 +++ b/src/ZF/OrderArith.thy	Thu Jul 23 14:25:05 2015 +0200
1.3 @@ -3,7 +3,7 @@
1.4      Copyright   1994  University of Cambridge
1.5  *)
1.6
1.7 -section{*Combining Orderings: Foundations of Ordinal Arithmetic*}
1.8 +section\<open>Combining Orderings: Foundations of Ordinal Arithmetic\<close>
1.9
1.10  theory OrderArith imports Order Sum Ordinal begin
1.11
1.12 @@ -34,9 +34,9 @@
1.13      "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
1.14
1.15
1.16 -subsection{*Addition of Relations -- Disjoint Sum*}
1.17 +subsection\<open>Addition of Relations -- Disjoint Sum\<close>
1.18
1.19 -subsubsection{*Rewrite rules.  Can be used to obtain introduction rules*}
1.20 +subsubsection\<open>Rewrite rules.  Can be used to obtain introduction rules\<close>
1.21
1.23      "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a \<in> A & b \<in> B"
1.24 @@ -56,7 +56,7 @@
1.25
1.26  declare radd_Inr_Inl_iff [THEN iffD1, dest!]
1.27
1.28 -subsubsection{*Elimination Rule*}
1.29 +subsubsection\<open>Elimination Rule\<close>
1.30
1.33 @@ -66,7 +66,7 @@
1.34       |] ==> Q"
1.36
1.37 -subsubsection{*Type checking*}
1.38 +subsubsection\<open>Type checking\<close>
1.39
1.42 @@ -75,25 +75,25 @@
1.43
1.45
1.46 -subsubsection{*Linearity*}
1.47 +subsubsection\<open>Linearity\<close>
1.48
1.50      "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
1.51  by (unfold linear_def, blast)
1.52
1.53
1.54 -subsubsection{*Well-foundedness*}
1.55 +subsubsection\<open>Well-foundedness\<close>
1.56
1.58  apply (rule wf_onI2)
1.59  apply (subgoal_tac "\<forall>x\<in>A. Inl (x) \<in> Ba")
1.60 - --{*Proving the lemma, which is needed twice!*}
1.61 + --\<open>Proving the lemma, which is needed twice!\<close>
1.62   prefer 2
1.63   apply (erule_tac V = "y \<in> A + B" in thin_rl)
1.64   apply (rule_tac ballI)
1.65   apply (erule_tac r = r and a = x in wf_on_induct, assumption)
1.66   apply blast
1.67 -txt{*Returning to main part of proof*}
1.68 +txt\<open>Returning to main part of proof\<close>
1.69  apply safe
1.70  apply blast
1.71  apply (erule_tac r = s and a = ya in wf_on_induct, assumption, blast)
1.72 @@ -112,7 +112,7 @@
1.74  done
1.75
1.76 -subsubsection{*An @{term ord_iso} congruence law*}
1.77 +subsubsection\<open>An @{term ord_iso} congruence law\<close>
1.78
1.79  lemma sum_bij:
1.80       "[| f \<in> bij(A,C);  g \<in> bij(B,D) |]
1.81 @@ -141,7 +141,7 @@
1.82  apply auto
1.83  done
1.84
1.85 -subsubsection{*Associativity*}
1.86 +subsubsection\<open>Associativity\<close>
1.87
1.88  lemma sum_assoc_bij:
1.89       "(\<lambda>z\<in>(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))
1.90 @@ -158,9 +158,9 @@
1.91  by (rule sum_assoc_bij [THEN ord_isoI], auto)
1.92
1.93
1.94 -subsection{*Multiplication of Relations -- Lexicographic Product*}
1.95 +subsection\<open>Multiplication of Relations -- Lexicographic Product\<close>
1.96
1.97 -subsubsection{*Rewrite rule.  Can be used to obtain introduction rules*}
1.98 +subsubsection\<open>Rewrite rule.  Can be used to obtain introduction rules\<close>
1.99
1.100  lemma  rmult_iff [iff]:
1.101      "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) \<longleftrightarrow>
1.102 @@ -176,20 +176,20 @@
1.103       |] ==> Q"
1.104  by blast
1.105
1.106 -subsubsection{*Type checking*}
1.107 +subsubsection\<open>Type checking\<close>
1.108
1.109  lemma rmult_type: "rmult(A,r,B,s) \<subseteq> (A*B) * (A*B)"
1.110  by (unfold rmult_def, rule Collect_subset)
1.111
1.112  lemmas field_rmult = rmult_type [THEN field_rel_subset]
1.113
1.114 -subsubsection{*Linearity*}
1.115 +subsubsection\<open>Linearity\<close>
1.116
1.117  lemma linear_rmult:
1.118      "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
1.119  by (simp add: linear_def, blast)
1.120
1.121 -subsubsection{*Well-foundedness*}
1.122 +subsubsection\<open>Well-foundedness\<close>
1.123
1.124  lemma wf_on_rmult: "[| wf[A](r);  wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))"
1.125  apply (rule wf_onI2)
1.126 @@ -217,7 +217,7 @@
1.127  done
1.128
1.129
1.130 -subsubsection{*An @{term ord_iso} congruence law*}
1.131 +subsubsection\<open>An @{term ord_iso} congruence law\<close>
1.132
1.133  lemma prod_bij:
1.134       "[| f \<in> bij(A,C);  g \<in> bij(B,D) |]
1.135 @@ -277,7 +277,7 @@
1.136  apply (auto elim!: well_ord_is_wf [THEN wf_on_asym] predE)
1.137  done
1.138
1.139 -subsubsection{*Distributive law*}
1.140 +subsubsection\<open>Distributive law\<close>
1.141
1.142  lemma sum_prod_distrib_bij:
1.143       "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
1.144 @@ -291,7 +291,7 @@
1.145              (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
1.146  by (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
1.147
1.148 -subsubsection{*Associativity*}
1.149 +subsubsection\<open>Associativity\<close>
1.150
1.151  lemma prod_assoc_bij:
1.152       "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) \<in> bij((A*B)*C, A*(B*C))"
1.153 @@ -303,14 +303,14 @@
1.154              A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"
1.155  by (rule prod_assoc_bij [THEN ord_isoI], auto)
1.156
1.157 -subsection{*Inverse Image of a Relation*}
1.158 +subsection\<open>Inverse Image of a Relation\<close>
1.159
1.160 -subsubsection{*Rewrite rule*}
1.161 +subsubsection\<open>Rewrite rule\<close>
1.162
1.163  lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r)  \<longleftrightarrow>  <f`a,f`b>: r & a \<in> A & b \<in> A"
1.164  by (unfold rvimage_def, blast)
1.165
1.166 -subsubsection{*Type checking*}
1.167 +subsubsection\<open>Type checking\<close>
1.168
1.169  lemma rvimage_type: "rvimage(A,f,r) \<subseteq> A*A"
1.170  by (unfold rvimage_def, rule Collect_subset)
1.171 @@ -321,7 +321,7 @@
1.172  by (unfold rvimage_def, blast)
1.173
1.174
1.175 -subsubsection{*Partial Ordering Properties*}
1.176 +subsubsection\<open>Partial Ordering Properties\<close>
1.177
1.178  lemma irrefl_rvimage:
1.179      "[| f \<in> inj(A,B);  irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"
1.180 @@ -341,7 +341,7 @@
1.181  apply (blast intro!: irrefl_rvimage trans_on_rvimage)
1.182  done
1.183
1.184 -subsubsection{*Linearity*}
1.185 +subsubsection\<open>Linearity\<close>
1.186
1.187  lemma linear_rvimage:
1.188      "[| f \<in> inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
1.189 @@ -356,7 +356,7 @@
1.190  done
1.191
1.192
1.193 -subsubsection{*Well-foundedness*}
1.194 +subsubsection\<open>Well-foundedness\<close>
1.195
1.196  lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))"
1.197  apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal)
1.198 @@ -369,8 +369,8 @@
1.199  apply blast
1.200  done
1.201
1.202 -text{*But note that the combination of @{text wf_imp_wf_on} and
1.203 - @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
1.204 +text\<open>But note that the combination of @{text wf_imp_wf_on} and
1.205 + @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}\<close>
1.206  lemma wf_on_rvimage: "[| f \<in> A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
1.207  apply (rule wf_onI2)
1.208  apply (subgoal_tac "\<forall>z\<in>A. f`z=f`y \<longrightarrow> z \<in> Ba")
1.209 @@ -400,8 +400,8 @@
1.210  by (unfold ord_iso_def rvimage_def, blast)
1.211
1.212
1.213 -subsection{*Every well-founded relation is a subset of some inverse image of
1.214 -      an ordinal*}
1.215 +subsection\<open>Every well-founded relation is a subset of some inverse image of
1.216 +      an ordinal\<close>
1.217
1.218  lemma wf_rvimage_Ord: "Ord(i) \<Longrightarrow> wf(rvimage(A, f, Memrel(i)))"
1.219  by (blast intro: wf_rvimage wf_Memrel)
1.220 @@ -455,12 +455,12 @@
1.221            intro: wf_rvimage_Ord [THEN wf_subset])
1.222
1.223
1.224 -subsection{*Other Results*}
1.225 +subsection\<open>Other Results\<close>
1.226
1.227  lemma wf_times: "A \<inter> B = 0 ==> wf(A*B)"
1.228  by (simp add: wf_def, blast)
1.229
1.230 -text{*Could also be used to prove @{text wf_radd}*}
1.231 +text\<open>Could also be used to prove @{text wf_radd}\<close>
1.232  lemma wf_Un:
1.233       "[| range(r) \<inter> domain(s) = 0; wf(r);  wf(s) |] ==> wf(r \<union> s)"
1.234  apply (simp add: wf_def, clarify)
1.235 @@ -473,7 +473,7 @@
1.236  apply (blast intro: elim: equalityE)
1.237  done
1.238
1.239 -subsubsection{*The Empty Relation*}
1.240 +subsubsection\<open>The Empty Relation\<close>
1.241
1.242  lemma wf0: "wf(0)"
1.243  by (simp add: wf_def, blast)
1.244 @@ -484,7 +484,7 @@
1.245  lemma well_ord0: "well_ord(0,0)"
1.246  by (blast intro: wf_imp_wf_on well_ordI wf0 linear0)
1.247
1.248 -subsubsection{*The "measure" relation is useful with wfrec*}
1.249 +subsubsection\<open>The "measure" relation is useful with wfrec\<close>
1.250
1.251  lemma measure_eq_rvimage_Memrel:
1.252       "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))"
1.253 @@ -524,7 +524,7 @@
1.254  lemma measure_type: "measure(A,f) \<subseteq> A*A"
1.255  by (auto simp add: measure_def)
1.256
1.257 -subsubsection{*Well-foundedness of Unions*}
1.258 +subsubsection\<open>Well-foundedness of Unions\<close>
1.259
1.260  lemma wf_on_Union:
1.261   assumes wfA: "wf[A](r)"
1.262 @@ -544,7 +544,7 @@
1.263  apply (frule ok, assumption+, blast)
1.264  done
1.265
1.266 -subsubsection{*Bijections involving Powersets*}
1.267 +subsubsection\<open>Bijections involving Powersets\<close>
1.268
1.269  lemma Pow_sum_bij:
1.270      "(\<lambda>Z \<in> Pow(A+B). <{x \<in> A. Inl(x) \<in> Z}, {y \<in> B. Inr(y) \<in> Z}>)
1.271 @@ -554,7 +554,7 @@
1.272  apply force+
1.273  done
1.274
1.275 -text{*As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"} *}
1.276 +text\<open>As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"}\<close>
1.277  lemma Pow_Sigma_bij:
1.278      "(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})
1.279       \<in> bij(Pow(Sigma(A,B)), \<Pi> x \<in> A. Pow(B(x)))"
```