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.22  lemma radd_Inl_Inr_iff [iff]:
    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.31  lemma raddE:
    1.32      "[| <p',p> \<in> radd(A,r,B,s);
    1.33 @@ -66,7 +66,7 @@
    1.34       |] ==> Q"
    1.35  by (unfold radd_def, blast)
    1.36  
    1.37 -subsubsection{*Type checking*}
    1.38 +subsubsection\<open>Type checking\<close>
    1.39  
    1.40  lemma radd_type: "radd(A,r,B,s) \<subseteq> (A+B) * (A+B)"
    1.41  apply (unfold radd_def)
    1.42 @@ -75,25 +75,25 @@
    1.43  
    1.44  lemmas field_radd = radd_type [THEN field_rel_subset]
    1.45  
    1.46 -subsubsection{*Linearity*}
    1.47 +subsubsection\<open>Linearity\<close>
    1.48  
    1.49  lemma linear_radd:
    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.57  lemma wf_on_radd: "[| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"
    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.73  apply (simp add: well_ord_def tot_ord_def linear_radd)
    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)))"