author blanchet Wed Jan 22 09:45:30 2014 +0100 (2014-01-22) changeset 55101 57c875e488bd parent 55100 697b41533e1a child 55102 761e40ce91bc
whitespace tuning
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Jan 21 16:56:34 2014 +0100
1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Wed Jan 22 09:45:30 2014 +0100
1.3 @@ -38,7 +38,7 @@
1.4
1.5  text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
1.6  order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
1.7 -strict order-embedding relation, @{text "<o"}), among all the well-orders on its field.  *}
1.8 +strict order-embedding relation, @{text "<o"}), among all the well-orders on its field. *}
1.9
1.10  definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
1.11  where
1.12 @@ -115,7 +115,7 @@
1.13
1.14  text{* We define the cardinal of set to be {\em some} cardinal order on that set.
1.15  We shall prove that this notion is unique up to order isomorphism, meaning
1.16 -that order isomorphism shall be the true identity of cardinals.  *}
1.17 +that order isomorphism shall be the true identity of cardinals. *}
1.18
1.19  definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
1.20  where "card_of A = (SOME r. card_order_on A r)"
1.21 @@ -827,7 +827,7 @@
1.22  theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
1.23  does not increase cardinality -- the proof of this fact adapts a standard
1.24  set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
1.25 -at page 47 in \cite{card-book}. Then everything else follows fairly easily.  *}
1.26 +at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
1.27
1.28  lemma infinite_iff_card_of_nat:
1.29  "\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
1.30 @@ -1141,13 +1141,13 @@
1.31  qed
1.32
1.33
1.34 -subsection {* The cardinal $\omega$ and the finite cardinals  *}
1.35 +subsection {* The cardinal $\omega$ and the finite cardinals *}
1.36
1.37  text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict
1.38  order relation on
1.39  @{text "nat"}, that we abbreviate by @{text "natLeq"}.  The finite cardinals
1.40  shall be the restrictions of these relations to the numbers smaller than
1.41 -fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}.  *}
1.42 +fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
1.43
1.44  abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
1.45  abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
1.46 @@ -1263,7 +1263,7 @@
1.47
1.48  text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
1.49  being a successor cardinal of @{text "r"}. Although the definition does
1.50 -not require @{text "r"} to be a cardinal, only this case will be meaningful.  *}
1.51 +not require @{text "r"} to be a cardinal, only this case will be meaningful. *}
1.52
1.53  definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
1.54  where
1.55 @@ -1314,7 +1314,7 @@
1.56  using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
1.57
1.58  text{* The minimality property of @{text "cardSuc"} originally present in its definition
1.59 -is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}:  *}
1.60 +is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *}
1.61
1.62  lemma cardSuc_least_aux:
1.63  "\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"

     2.1 --- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Tue Jan 21 16:56:34 2014 +0100
2.2 +++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Wed Jan 22 09:45:30 2014 +0100
2.3 @@ -11,7 +11,6 @@
2.4  imports BNF_Wellorder_Embedding
2.5  begin
2.6
2.7 -
2.8  text {* In this section, we study basic constructions on well-orders, such as restriction to
2.9  a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders,
2.10  and bounded square.  We also define between well-orders
2.11 @@ -19,59 +18,48 @@
2.12  @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}), and
2.13  @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).  We study the
2.14  connections between these relations, order filters, and the aforementioned constructions.
2.15 -A main result of this section is that @{text "<o"} is well-founded.  *}
2.16 +A main result of this section is that @{text "<o"} is well-founded. *}
2.17
2.18
2.19 -subsection {* Restriction to a set  *}
2.20 -
2.21 +subsection {* Restriction to a set *}
2.22
2.23  abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel"
2.24  where "Restr r A \<equiv> r Int (A \<times> A)"
2.25
2.26 -
2.27  lemma Restr_subset:
2.28  "A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A"
2.29  by blast
2.30
2.31 -
2.32  lemma Restr_Field: "Restr r (Field r) = r"
2.33  unfolding Field_def by auto
2.34
2.35 -
2.36  lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
2.37  unfolding refl_on_def Field_def by auto
2.38
2.39 -
2.40  lemma antisym_Restr:
2.41  "antisym r \<Longrightarrow> antisym(Restr r A)"
2.42  unfolding antisym_def Field_def by auto
2.43
2.44 -
2.45  lemma Total_Restr:
2.46  "Total r \<Longrightarrow> Total(Restr r A)"
2.47  unfolding total_on_def Field_def by auto
2.48
2.49 -
2.50  lemma trans_Restr:
2.51  "trans r \<Longrightarrow> trans(Restr r A)"
2.52  unfolding trans_def Field_def by blast
2.53
2.54 -
2.55  lemma Preorder_Restr:
2.56  "Preorder r \<Longrightarrow> Preorder(Restr r A)"
2.57  unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)
2.58
2.59 -
2.60  lemma Partial_order_Restr:
2.61  "Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
2.62  unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)
2.63
2.64 -
2.65  lemma Linear_order_Restr:
2.66  "Linear_order r \<Longrightarrow> Linear_order(Restr r A)"
2.67  unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)
2.68
2.69 -
2.70  lemma Well_order_Restr:
2.71  assumes "Well_order r"
2.72  shows "Well_order(Restr r A)"
2.73 @@ -83,21 +71,17 @@
2.75  qed
2.76
2.77 -
2.78  lemma Field_Restr_subset: "Field(Restr r A) \<le> A"
2.79  by (auto simp add: Field_def)
2.80
2.81 -
2.82  lemma Refl_Field_Restr:
2.83  "Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"
2.84  unfolding refl_on_def Field_def by blast
2.85
2.86 -
2.87  lemma Refl_Field_Restr2:
2.88  "\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
2.89  by (auto simp add: Refl_Field_Restr)
2.90
2.91 -
2.92  lemma well_order_on_Restr:
2.93  assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
2.94  shows "well_order_on A (Restr r A)"
2.95 @@ -106,14 +90,12 @@
2.96       order_on_defs[of "Field r" r] by auto
2.97
2.98
2.99 -subsection {* Order filters versus restrictions and embeddings  *}
2.100 -
2.101 +subsection {* Order filters versus restrictions and embeddings *}
2.102
2.103  lemma Field_Restr_ofilter:
2.104  "\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
2.105  by (auto simp add: wo_rel_def wo_rel.ofilter_def wo_rel.REFL Refl_Field_Restr2)
2.106
2.107 -
2.108  lemma ofilter_Restr_under:
2.109  assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
2.110  shows "under (Restr r A) a = under r a"
2.111 @@ -125,7 +107,6 @@
2.112    thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
2.113  qed
2.114
2.115 -
2.116  lemma ofilter_embed:
2.117  assumes "Well_order r"
2.118  shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)"
2.119 @@ -159,7 +140,6 @@
2.120    thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def)
2.121  qed
2.122
2.123 -
2.124  lemma ofilter_Restr_Int:
2.125  assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A"
2.126  shows "wo_rel.ofilter (Restr r B) (A Int B)"
2.127 @@ -183,7 +163,6 @@
2.128    qed
2.129  qed
2.130
2.131 -
2.132  lemma ofilter_Restr_subset:
2.133  assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" and SUB: "A \<le> B"
2.134  shows "wo_rel.ofilter (Restr r B) A"
2.135 @@ -192,7 +171,6 @@
2.136    thus ?thesis using assms ofilter_Restr_Int[of r A B] by auto
2.137  qed
2.138
2.139 -
2.140  lemma ofilter_subset_embed:
2.141  assumes WELL: "Well_order r" and
2.142          OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
2.143 @@ -231,7 +209,6 @@
2.144    qed
2.145  qed
2.146
2.147 -
2.148  lemma ofilter_subset_embedS_iso:
2.149  assumes WELL: "Well_order r" and
2.150          OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
2.151 @@ -255,14 +232,12 @@
2.152          FieldA FieldB bij_betw_id_iff[of A B] by auto
2.153  qed
2.154
2.155 -
2.156  lemma ofilter_subset_embedS:
2.157  assumes WELL: "Well_order r" and
2.158          OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
2.159  shows "(A < B) = embedS (Restr r A) (Restr r B) id"
2.160  using assms by (simp add: ofilter_subset_embedS_iso)
2.161
2.162 -
2.163  lemma embed_implies_iso_Restr:
2.164  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
2.165          EMB: "embed r' r f"
2.166 @@ -288,13 +263,11 @@
2.167
2.168  subsection {* The strict inclusion on proper ofilters is well-founded *}
2.169
2.170 -
2.171  definition ofilterIncl :: "'a rel \<Rightarrow> 'a set rel"
2.172  where
2.173  "ofilterIncl r \<equiv> {(A,B). wo_rel.ofilter r A \<and> A \<noteq> Field r \<and>
2.174                           wo_rel.ofilter r B \<and> B \<noteq> Field r \<and> A < B}"
2.175
2.176 -
2.177  lemma wf_ofilterIncl:
2.178  assumes WELL: "Well_order r"
2.179  shows "wf(ofilterIncl r)"
2.180 @@ -329,10 +302,8 @@
2.181  qed
2.182
2.183
2.184 -
2.185  subsection {* Ordering the well-orders by existence of embeddings *}
2.186
2.187 -
2.188  text {* We define three relations between well-orders:
2.189  \begin{itemize}
2.190  \item @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"});
2.191 @@ -345,20 +316,16 @@
2.192  @{text "\<le>"}, @{text "<"}, @{text "="} associated to a total order on a set.
2.193  *}
2.194
2.195 -
2.196  definition ordLeq :: "('a rel * 'a' rel) set"
2.197  where
2.198  "ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}"
2.199
2.200 -
2.201  abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50)
2.202  where "r <=o r' \<equiv> (r,r') \<in> ordLeq"
2.203
2.204 -
2.205  abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50)
2.206  where "r \<le>o r' \<equiv> r <=o r'"
2.207
2.208 -
2.209  definition ordLess :: "('a rel * 'a' rel) set"
2.210  where
2.211  "ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"
2.212 @@ -366,7 +333,6 @@
2.213  abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)
2.214  where "r <o r' \<equiv> (r,r') \<in> ordLess"
2.215
2.216 -
2.217  definition ordIso :: "('a rel * 'a' rel) set"
2.218  where
2.219  "ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"
2.220 @@ -374,7 +340,6 @@
2.221  abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)
2.222  where "r =o r' \<equiv> (r,r') \<in> ordIso"
2.223
2.224 -
2.225  lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def
2.226
2.227  lemma ordLeq_Well_order_simp:
2.228 @@ -382,18 +347,15 @@
2.229  shows "Well_order r \<and> Well_order r'"
2.230  using assms unfolding ordLeq_def by simp
2.231
2.232 -
2.233  text{* Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders
2.234  on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
2.235  restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,
2.236 -to @{text "'a rel rel"}.  *}
2.237 -
2.238 +to @{text "'a rel rel"}. *}
2.239
2.240  lemma ordLeq_reflexive:
2.241  "Well_order r \<Longrightarrow> r \<le>o r"
2.242  unfolding ordLeq_def using id_embed[of r] by blast
2.243
2.244 -
2.245  lemma ordLeq_transitive[trans]:
2.246  assumes *: "r \<le>o r'" and **: "r' \<le>o r''"
2.247  shows "r \<le>o r''"
2.248 @@ -407,17 +369,14 @@
2.249    thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto
2.250  qed
2.251
2.252 -
2.253  lemma ordLeq_total:
2.254  "\<lbrakk>Well_order r; Well_order r'\<rbrakk> \<Longrightarrow> r \<le>o r' \<or> r' \<le>o r"
2.255  unfolding ordLeq_def using wellorders_totally_ordered by blast
2.256
2.257 -
2.258  lemma ordIso_reflexive:
2.259  "Well_order r \<Longrightarrow> r =o r"
2.260  unfolding ordIso_def using id_iso[of r] by blast
2.261
2.262 -
2.263  lemma ordIso_transitive[trans]:
2.264  assumes *: "r =o r'" and **: "r' =o r''"
2.265  shows "r =o r''"
2.266 @@ -431,7 +390,6 @@
2.267    thus "r =o r''" unfolding ordIso_def using 1 by auto
2.268  qed
2.269
2.270 -
2.271  lemma ordIso_symmetric:
2.272  assumes *: "r =o r'"
2.273  shows "r' =o r"
2.274 @@ -445,7 +403,6 @@
2.275    thus "r' =o r" unfolding ordIso_def using 1 by (auto simp add: iso_def)
2.276  qed
2.277
2.278 -
2.279  lemma ordLeq_ordLess_trans[trans]:
2.280  assumes "r \<le>o r'" and " r' <o r''"
2.281  shows "r <o r''"
2.282 @@ -456,7 +413,6 @@
2.283    using embed_comp_embedS by blast
2.284  qed
2.285
2.286 -
2.287  lemma ordLess_ordLeq_trans[trans]:
2.288  assumes "r <o r'" and " r' \<le>o r''"
2.289  shows "r <o r''"
2.290 @@ -467,7 +423,6 @@
2.291    using embedS_comp_embed by blast
2.292  qed
2.293
2.294 -
2.295  lemma ordLeq_ordIso_trans[trans]:
2.296  assumes "r \<le>o r'" and " r' =o r''"
2.297  shows "r \<le>o r''"
2.298 @@ -478,7 +433,6 @@
2.299    using embed_comp_iso by blast
2.300  qed
2.301
2.302 -
2.303  lemma ordIso_ordLeq_trans[trans]:
2.304  assumes "r =o r'" and " r' \<le>o r''"
2.305  shows "r \<le>o r''"
2.306 @@ -489,7 +443,6 @@
2.307    using iso_comp_embed by blast
2.308  qed
2.309
2.310 -
2.311  lemma ordLess_ordIso_trans[trans]:
2.312  assumes "r <o r'" and " r' =o r''"
2.313  shows "r <o r''"
2.314 @@ -500,7 +453,6 @@
2.315    using embedS_comp_iso by blast
2.316  qed
2.317
2.318 -
2.319  lemma ordIso_ordLess_trans[trans]:
2.320  assumes "r =o r'" and " r' <o r''"
2.321  shows "r <o r''"
2.322 @@ -511,7 +463,6 @@
2.323    using iso_comp_embedS by blast
2.324  qed
2.325
2.326 -
2.327  lemma ordLess_not_embed:
2.328  assumes "r <o r'"
2.329  shows "\<not>(\<exists>f'. embed r' r f')"
2.330 @@ -527,7 +478,6 @@
2.331    thus ?thesis by blast
2.332  qed
2.333
2.334 -
2.335  lemma ordLess_Field:
2.336  assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f"
2.337  shows "\<not> (f(Field r1) = Field r2)"
2.338 @@ -546,7 +496,6 @@
2.339    ultimately show ?thesis by (simp add: bij_betw_def)
2.340  qed
2.341
2.342 -
2.343  lemma ordLess_iff:
2.344  "r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))"
2.345  proof
2.346 @@ -568,7 +517,6 @@
2.347    unfolding ordLess_def using * by (fastforce simp add: embedS_def)
2.348  qed
2.349
2.350 -
2.351  lemma ordLess_irreflexive: "\<not> r <o r"
2.352  proof
2.353    assume "r <o r"
2.354 @@ -578,12 +526,10 @@
2.355    ultimately show False by blast
2.356  qed
2.357
2.358 -
2.359  lemma ordLeq_iff_ordLess_or_ordIso:
2.360  "r \<le>o r' = (r <o r' \<or> r =o r')"
2.361  unfolding ordRels_def embedS_defs iso_defs by blast
2.362
2.363 -
2.364  lemma ordIso_iff_ordLeq:
2.365  "(r =o r') = (r \<le>o r' \<and> r' \<le>o r)"
2.366  proof
2.367 @@ -604,12 +550,10 @@
2.368    thus "r =o r'" unfolding ordIso_def using 1 by auto
2.369  qed
2.370
2.371 -
2.372  lemma not_ordLess_ordLeq:
2.373  "r <o r' \<Longrightarrow> \<not> r' \<le>o r"
2.374  using ordLess_ordLeq_trans ordLess_irreflexive by blast
2.375
2.376 -
2.377  lemma ordLess_or_ordLeq:
2.378  assumes WELL: "Well_order r" and WELL': "Well_order r'"
2.379  shows "r <o r' \<or> r' \<le>o r"
2.380 @@ -624,46 +568,37 @@
2.381    ultimately show ?thesis by blast
2.382  qed
2.383
2.384 -
2.385  lemma not_ordLess_ordIso:
2.386  "r <o r' \<Longrightarrow> \<not> r =o r'"
2.387  using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
2.388
2.389 -
2.390  lemma not_ordLeq_iff_ordLess:
2.391  assumes WELL: "Well_order r" and WELL': "Well_order r'"
2.392  shows "(\<not> r' \<le>o r) = (r <o r')"
2.393  using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
2.394
2.395 -
2.396  lemma not_ordLess_iff_ordLeq:
2.397  assumes WELL: "Well_order r" and WELL': "Well_order r'"
2.398  shows "(\<not> r' <o r) = (r \<le>o r')"
2.399  using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
2.400
2.401 -
2.402  lemma ordLess_transitive[trans]:
2.403  "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
2.404  using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
2.405
2.406 -
2.407  corollary ordLess_trans: "trans ordLess"
2.408  unfolding trans_def using ordLess_transitive by blast
2.409
2.410 -
2.411  lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric
2.412
2.413 -
2.414  lemma ordIso_imp_ordLeq:
2.415  "r =o r' \<Longrightarrow> r \<le>o r'"
2.416  using ordIso_iff_ordLeq by blast
2.417
2.418 -
2.419  lemma ordLess_imp_ordLeq:
2.420  "r <o r' \<Longrightarrow> r \<le>o r'"
2.421  using ordLeq_iff_ordLess_or_ordIso by blast
2.422
2.423 -
2.424  lemma ofilter_subset_ordLeq:
2.425  assumes WELL: "Well_order r" and
2.426          OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
2.427 @@ -687,7 +622,6 @@
2.428    wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast
2.429  qed
2.430
2.431 -
2.432  lemma ofilter_subset_ordLess:
2.433  assumes WELL: "Well_order r" and
2.434          OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
2.435 @@ -705,13 +639,11 @@
2.436    finally show ?thesis .
2.437  qed
2.438
2.439 -
2.440  lemma ofilter_ordLess:
2.441  "\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> (A < Field r) = (Restr r A <o r)"
2.442  by (simp add: ofilter_subset_ordLess wo_rel.Field_ofilter
2.443      wo_rel_def Restr_Field)
2.444
2.445 -
2.446  corollary underS_Restr_ordLess:
2.447  assumes "Well_order r" and "Field r \<noteq> {}"
2.448  shows "Restr r (underS r a) <o r"
2.449 @@ -722,7 +654,6 @@
2.450    by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
2.451  qed
2.452
2.453 -
2.454  lemma embed_ordLess_ofilterIncl:
2.455  assumes
2.456    OL12: "r1 <o r2" and OL23: "r2 <o r3" and
2.457 @@ -769,7 +700,6 @@
2.458    unfolding ofilterIncl_def by auto
2.459  qed
2.460
2.461 -
2.462  lemma ordLess_iff_ordIso_Restr:
2.463  assumes WELL: "Well_order r" and WELL': "Well_order r'"
2.464  shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"
2.465 @@ -795,7 +725,6 @@
2.466    thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto
2.467  qed
2.468
2.469 -
2.470  lemma internalize_ordLess:
2.471  "(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)"
2.472  proof
2.473 @@ -816,7 +745,6 @@
2.474    thus "r' <o r" using ordIso_ordLess_trans by blast
2.475  qed
2.476
2.477 -
2.478  lemma internalize_ordLeq:
2.479  "(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)"
2.480  proof
2.481 @@ -837,7 +765,6 @@
2.482    thus "r' \<le>o r" using ordIso_ordLeq_trans by blast
2.483  qed
2.484
2.485 -
2.486  lemma ordLeq_iff_ordLess_Restr:
2.487  assumes WELL: "Well_order r" and WELL': "Well_order r'"
2.488  shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"
2.489 @@ -858,7 +785,6 @@
2.490    thus "r \<le>o r'" using ordLess_or_ordLeq assms by blast
2.491  qed
2.492
2.493 -
2.494  lemma finite_ordLess_infinite:
2.495  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
2.496          FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
2.497 @@ -872,7 +798,6 @@
2.498    thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
2.499  qed
2.500
2.501 -
2.502  lemma finite_well_order_on_ordIso:
2.503  assumes FIN: "finite A" and
2.504          WELL: "well_order_on A r" and WELL': "well_order_on A r'"
2.505 @@ -897,21 +822,17 @@
2.506    ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis
2.507  qed
2.508
2.509 -
2.510  subsection{* @{text "<o"} is well-founded *}
2.511
2.512 -
2.513  text {* Of course, it only makes sense to state that the @{text "<o"} is well-founded
2.514  on the restricted type @{text "'a rel rel"}.  We prove this by first showing that, for any set
2.515  of well-orders all embedded in a fixed well-order, the function mapping each well-order
2.516  in the set to an order filter of the fixed well-order is compatible w.r.t. to @{text "<o"} versus
2.517  {\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded. *}
2.518
2.519 -
2.520  definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set"
2.521  where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f)  (Field r)"
2.522
2.523 -
2.524  lemma ord_to_filter_compat:
2.525  "compat (ordLess Int (ordLess^-1{r0} \<times> ordLess^-1{r0}))
2.526          (ofilterIncl r0)
2.527 @@ -929,7 +850,6 @@
2.528    using * ** by (simp add: embed_ordLess_ofilterIncl)
2.529  qed
2.530
2.531 -
2.532  theorem wf_ordLess: "wf ordLess"
2.533  proof-
2.534    {fix r0 :: "('a \<times> 'a) set"
2.535 @@ -963,30 +883,24 @@
2.536  qed
2.537
2.538
2.539 -
2.540 -subsection {* Copy via direct images  *}
2.541 -
2.542 +subsection {* Copy via direct images *}
2.543
2.544  text{* The direct image operator is the dual of the inverse image operator @{text "inv_image"}
2.545  from @{text "Relation.thy"}.  It is useful for transporting a well-order between
2.546  different types. *}
2.547
2.548 -
2.549  definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel"
2.550  where
2.551  "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
2.552
2.553 -
2.554  lemma dir_image_Field:
2.555  "Field(dir_image r f) \<le> f  (Field r)"
2.556  unfolding dir_image_def Field_def by auto
2.557
2.558 -
2.559  lemma dir_image_minus_Id:
2.560  "inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
2.561  unfolding inj_on_def Field_def dir_image_def by auto
2.562
2.563 -
2.564  lemma Refl_dir_image:
2.565  assumes "Refl r"
2.566  shows "Refl(dir_image r f)"
2.567 @@ -1004,7 +918,6 @@
2.568    by(unfold refl_on_def Field_def Domain_def Range_def, auto)
2.569  qed
2.570
2.571 -
2.572  lemma trans_dir_image:
2.573  assumes TRANS: "trans r" and INJ: "inj_on f (Field r)"
2.574  shows "trans(dir_image r f)"
2.575 @@ -1022,12 +935,10 @@
2.576    unfolding dir_image_def using 1 by auto
2.577  qed
2.578
2.579 -
2.580  lemma Preorder_dir_image:
2.581  "\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)"
2.582  by (simp add: preorder_on_def Refl_dir_image trans_dir_image)
2.583
2.584 -
2.585  lemma antisym_dir_image:
2.586  assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
2.587  shows "antisym(dir_image r f)"
2.588 @@ -1043,12 +954,10 @@
2.589    thus "a' = b'" using 1 by auto
2.590  qed
2.591
2.592 -
2.593  lemma Partial_order_dir_image:
2.594  "\<lbrakk>Partial_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Partial_order (dir_image r f)"
2.595  by (simp add: partial_order_on_def Preorder_dir_image antisym_dir_image)
2.596
2.597 -
2.598  lemma Total_dir_image:
2.599  assumes TOT: "Total r" and INJ: "inj_on f (Field r)"
2.600  shows "Total(dir_image r f)"
2.601 @@ -1064,12 +973,10 @@
2.602    using 1 unfolding dir_image_def by auto
2.603  qed
2.604
2.605 -
2.606  lemma Linear_order_dir_image:
2.607  "\<lbrakk>Linear_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Linear_order (dir_image r f)"
2.608  by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image)
2.609
2.610 -
2.611  lemma wf_dir_image:
2.612  assumes WF: "wf r" and INJ: "inj_on f (Field r)"
2.613  shows "wf(dir_image r f)"
2.614 @@ -1095,7 +1002,6 @@
2.615    using A_def 1 by blast
2.616  qed
2.617
2.618 -
2.619  lemma Well_order_dir_image:
2.620  "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
2.621  using assms unfolding well_order_on_def
2.622 @@ -1104,33 +1010,27 @@
2.623    subset_inj_on[of f "Field r" "Field(r - Id)"]
2.624    mono_Field[of "r - Id" r] by auto
2.625
2.626 -
2.627  lemma dir_image_Field2:
2.628  "Refl r \<Longrightarrow> Field(dir_image r f) = f  (Field r)"
2.629  unfolding Field_def dir_image_def refl_on_def Domain_def Range_def by blast
2.630
2.631 -
2.632  lemma dir_image_bij_betw:
2.633  "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
2.634  unfolding bij_betw_def
2.635  by (simp add: dir_image_Field2 order_on_defs)
2.636
2.637 -
2.638  lemma dir_image_compat:
2.639  "compat r (dir_image r f) f"
2.640  unfolding compat_def dir_image_def by auto
2.641
2.642 -
2.643  lemma dir_image_iso:
2.644  "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> iso r (dir_image r f) f"
2.645  using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast
2.646
2.647 -
2.648  lemma dir_image_ordIso:
2.649  "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> r =o dir_image r f"
2.650  unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast
2.651
2.652 -
2.653  lemma Well_order_iso_copy:
2.654  assumes WELL: "well_order_on A r" and BIJ: "bij_betw f A A'"
2.655  shows "\<exists>r'. well_order_on A' r' \<and> r =o r'"
2.656 @@ -1149,9 +1049,7 @@
2.657  qed
2.658
2.659
2.660 -
2.661 -subsection {* Bounded square  *}
2.662 -
2.663 +subsection {* Bounded square *}
2.664
2.665  text{* This construction essentially defines, for an order relation @{text "r"}, a lexicographic
2.666  order @{text "bsqr r"} on @{text "(Field r) \<times> (Field r)"}, applying the
2.667 @@ -1168,7 +1066,6 @@
2.668  construction) is that any proper order filter of the product order is included in a rectangle, i.e.,
2.669  in a product of proper filters on the original relation (assumed to be a well-order). *}
2.670
2.671 -
2.672  definition bsqr :: "'a rel => ('a * 'a)rel"
2.673  where
2.674  "bsqr r = {((a1,a2),(b1,b2)).
2.675 @@ -1179,7 +1076,6 @@
2.676              wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1  \<and> (a2,b2) \<in> r - Id
2.677             )}"
2.678
2.679 -
2.680  lemma Field_bsqr:
2.681  "Field (bsqr r) = Field r \<times> Field r"
2.682  proof
2.683 @@ -1202,11 +1098,9 @@
2.684    qed
2.685  qed
2.686
2.687 -
2.688  lemma bsqr_Refl: "Refl(bsqr r)"
2.689  by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
2.690
2.691 -
2.692  lemma bsqr_Trans:
2.693  assumes "Well_order r"
2.694  shows "trans (bsqr r)"
2.695 @@ -1296,7 +1190,6 @@
2.696    qed
2.697  qed
2.698
2.699 -
2.700  lemma bsqr_antisym:
2.701  assumes "Well_order r"
2.702  shows "antisym (bsqr r)"
2.703 @@ -1367,7 +1260,6 @@
2.704    qed
2.705  qed
2.706
2.707 -
2.708  lemma bsqr_Total:
2.709  assumes "Well_order r"
2.710  shows "Total(bsqr r)"
2.711 @@ -1485,14 +1377,12 @@
2.712    thus ?thesis unfolding total_on_def by fast
2.713  qed
2.714
2.715 -
2.716  lemma bsqr_Linear_order:
2.717  assumes "Well_order r"
2.718  shows "Linear_order(bsqr r)"
2.719  unfolding order_on_defs
2.720  using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast
2.721
2.722 -
2.723  lemma bsqr_Well_order:
2.724  assumes "Well_order r"
2.725  shows "Well_order(bsqr r)"
2.726 @@ -1557,7 +1447,6 @@
2.727    ultimately show "\<exists>d \<in> D. \<forall>d' \<in> D. (d,d') \<in> bsqr r" by fastforce
2.728  qed
2.729
2.730 -
2.731  lemma bsqr_max2:
2.732  assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \<in> bsqr r"
2.733  shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
2.734 @@ -1572,7 +1461,6 @@
2.735    ultimately show ?thesis using WELL unfolding order_on_defs refl_on_def by auto
2.736  qed
2.737
2.738 -
2.739  lemma bsqr_ofilter:
2.740  assumes WELL: "Well_order r" and
2.741          OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and

     3.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Tue Jan 21 16:56:34 2014 +0100
3.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Wed Jan 22 09:45:30 2014 +0100
3.3 @@ -11,7 +11,6 @@
3.4  imports Zorn BNF_Wellorder_Relation
3.5  begin
3.6
3.7 -
3.8  text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and
3.9  prove their basic properties.  The notion of embedding is considered from the point
3.10  of view of the theory of ordinals, and therefore requires the source to be injected
3.11 @@ -36,7 +35,6 @@
3.12    by (auto simp add: inj_on_UNION_chain)
3.13  qed
3.14
3.15 -
3.16  lemma under_underS_bij_betw:
3.17  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.18          IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
3.19 @@ -57,10 +55,8 @@
3.20  qed
3.21
3.22
3.23 -
3.24  subsection {* (Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
3.25 -functions  *}
3.26 -
3.27 +functions *}
3.28
3.29  text{* Standardly, a function is an embedding of a well-order in another if it injectively and
3.30  order-compatibly maps the former into an order filter of the latter.
3.31 @@ -70,40 +66,32 @@
3.32  and the set of strict lower bounds of its image.  (Later we prove equivalence with
3.33  the standard definition -- lemma @{text "embed_iff_compat_inj_on_ofilter"}.)
3.34  A {\em strict embedding} (operator @{text "embedS"})  is a non-bijective embedding
3.35 -and an isomorphism (operator @{text "iso"}) is a bijective embedding.   *}
3.36 -
3.37 +and an isomorphism (operator @{text "iso"}) is a bijective embedding. *}
3.38
3.39  definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
3.40  where
3.41  "embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
3.42
3.43 -
3.44  lemmas embed_defs = embed_def embed_def[abs_def]
3.45
3.46 -
3.47  text {* Strict embeddings: *}
3.48
3.49  definition embedS :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
3.50  where
3.51  "embedS r r' f \<equiv> embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')"
3.52
3.53 -
3.54  lemmas embedS_defs = embedS_def embedS_def[abs_def]
3.55
3.56 -
3.57  definition iso :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
3.58  where
3.59  "iso r r' f \<equiv> embed r r' f \<and> bij_betw f (Field r) (Field r')"
3.60
3.61 -
3.62  lemmas iso_defs = iso_def iso_def[abs_def]
3.63
3.64 -
3.65  definition compat :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
3.66  where
3.67  "compat r r' f \<equiv> \<forall>a b. (a,b) \<in> r \<longrightarrow> (f a, f b) \<in> r'"
3.68
3.69 -
3.70  lemma compat_wf:
3.71  assumes CMP: "compat r r' f" and WF: "wf r'"
3.72  shows "wf r"
3.73 @@ -115,15 +103,12 @@
3.74    using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto
3.75  qed
3.76
3.77 -
3.78  lemma id_embed: "embed r r id"
3.79  by(auto simp add: id_def embed_def bij_betw_def)
3.80
3.81 -
3.82  lemma id_iso: "iso r r id"
3.83  by(auto simp add: id_def embed_def iso_def bij_betw_def)
3.84
3.85 -
3.86  lemma embed_in_Field:
3.87  assumes WELL: "Well_order r" and
3.88          EMB: "embed r r' f" and IN: "a \<in> Field r"
3.89 @@ -140,7 +125,6 @@
3.90    by (auto simp: under_def)
3.91  qed
3.92
3.93 -
3.94  lemma comp_embed:
3.95  assumes WELL: "Well_order r" and
3.96          EMB: "embed r r' f" and EMB': "embed r' r'' f'"
3.97 @@ -160,7 +144,6 @@
3.99  qed
3.100
3.101 -
3.102  lemma comp_iso:
3.103  assumes WELL: "Well_order r" and
3.104          EMB: "iso r r' f" and EMB': "iso r' r'' f'"
3.105 @@ -168,15 +151,12 @@
3.106  using assms unfolding iso_def
3.107  by (auto simp add: comp_embed bij_betw_trans)
3.108
3.109 -
3.110 -text{* That @{text "embedS"} is also preserved by function composition shall be proved only later.  *}
3.111 -
3.112 +text{* That @{text "embedS"} is also preserved by function composition shall be proved only later. *}
3.113
3.114  lemma embed_Field:
3.115  "\<lbrakk>Well_order r; embed r r' f\<rbrakk> \<Longrightarrow> f(Field r) \<le> Field r'"
3.116  by (auto simp add: embed_in_Field)
3.117
3.118 -
3.119  lemma embed_preserves_ofilter:
3.120  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.121          EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"
3.122 @@ -204,7 +184,6 @@
3.123    qed
3.124  qed
3.125
3.126 -
3.127  lemma embed_Field_ofilter:
3.128  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.129          EMB: "embed r r' f"
3.130 @@ -216,7 +195,6 @@
3.131    show ?thesis by (auto simp add: embed_preserves_ofilter)
3.132  qed
3.133
3.134 -
3.135  lemma embed_compat:
3.136  assumes EMB: "embed r r' f"
3.137  shows "compat r r' f"
3.138 @@ -234,7 +212,6 @@
3.139    by (auto simp add: under_def)
3.140  qed
3.141
3.142 -
3.143  lemma embed_inj_on:
3.144  assumes WELL: "Well_order r" and EMB: "embed r r' f"
3.145  shows "inj_on f (Field r)"
3.146 @@ -271,7 +248,6 @@
3.147    by (auto simp add: total_on_def)
3.148  qed
3.149
3.150 -
3.151  lemma embed_underS:
3.152  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.153          EMB: "embed r r' f" and IN: "a \<in> Field r"
3.154 @@ -293,7 +269,6 @@
3.155    by (auto simp add: notIn_Un_bij_betw3)
3.156  qed
3.157
3.158 -
3.159  lemma embed_iff_compat_inj_on_ofilter:
3.160  assumes WELL: "Well_order r" and WELL': "Well_order r'"
3.161  shows "embed r r' f = (compat r r' f \<and> inj_on f (Field r) \<and> wo_rel.ofilter r' (f(Field r)))"
3.162 @@ -366,7 +341,6 @@
3.163    qed
3.164  qed
3.165
3.166 -
3.167  lemma inv_into_ofilter_embed:
3.168  assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
3.169          BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and
3.170 @@ -442,7 +416,6 @@
3.171    thus ?thesis unfolding embed_def .
3.172  qed
3.173
3.174 -
3.175  lemma inv_into_underS_embed:
3.176  assumes WELL: "Well_order r" and
3.177          BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
3.178 @@ -452,7 +425,6 @@
3.179  using assms
3.180  by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
3.181
3.182 -
3.183  lemma inv_into_Field_embed:
3.184  assumes WELL: "Well_order r" and EMB: "embed r r' f" and
3.185          IMAGE: "Field r' \<le> f  (Field r)"
3.186 @@ -468,7 +440,6 @@
3.187    by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
3.188  qed
3.189
3.190 -
3.191  lemma inv_into_Field_embed_bij_betw:
3.192  assumes WELL: "Well_order r" and
3.193          EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')"
3.194 @@ -481,12 +452,8 @@
3.195  qed
3.196
3.197
3.198 -
3.199 -
3.200 -
3.201  subsection {* Given any two well-orders, one can be embedded in the other *}
3.202
3.203 -
3.204  text{* Here is an overview of the proof of of this fact, stated in theorem
3.205  @{text "wellorders_totally_ordered"}:
3.206
3.207 @@ -506,7 +473,6 @@
3.208     (lemma @{text "wellorders_totally_ordered_aux2"}).
3.209  *}
3.210
3.211 -
3.212  lemma wellorders_totally_ordered_aux:
3.213  fixes r ::"'a rel"  and r'::"'a' rel" and
3.214        f :: "'a \<Rightarrow> 'a'" and a::'a
3.215 @@ -616,7 +582,6 @@
3.216    using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto
3.217  qed
3.218
3.219 -
3.220  lemma wellorders_totally_ordered_aux2:
3.221  fixes r ::"'a rel"  and r'::"'a' rel" and
3.222        f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool"  and a::'a
3.223 @@ -696,7 +661,6 @@
3.224    unfolding embed_def by blast
3.225  qed
3.226
3.227 -
3.228  theorem wellorders_totally_ordered:
3.229  fixes r ::"'a rel"  and r'::"'a' rel"
3.230  assumes WELL: "Well_order r" and WELL': "Well_order r'"
3.231 @@ -805,15 +769,13 @@
3.232  qed
3.233
3.234
3.235 -subsection {* Uniqueness of embeddings  *}
3.236 -
3.237 +subsection {* Uniqueness of embeddings *}
3.238
3.239  text{* Here we show a fact complementary to the one from the previous subsection -- namely,
3.240  that between any two well-orders there is {\em at most} one embedding, and is the one
3.241  definable by the expected well-order recursive equation.  As a consequence, any two
3.242  embeddings of opposite directions are mutually inverse. *}
3.243
3.244 -
3.245  lemma embed_determined:
3.246  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.247          EMB: "embed r r' f" and IN: "a \<in> Field r"
3.248 @@ -832,7 +794,6 @@
3.249    ultimately show ?thesis by simp
3.250  qed
3.251
3.252 -
3.253  lemma embed_unique:
3.254  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.255          EMBf: "embed r r' f" and EMBg: "embed r r' g"
3.256 @@ -848,7 +809,6 @@
3.257    using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
3.258  qed
3.259
3.260 -
3.261  lemma embed_bothWays_inverse:
3.262  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.263          EMB: "embed r r' f" and EMB': "embed r' r f'"
3.264 @@ -871,7 +831,6 @@
3.265    ultimately show ?thesis by blast
3.266  qed
3.267
3.268 -
3.269  lemma embed_bothWays_bij_betw:
3.270  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.271          EMB: "embed r r' f" and EMB': "embed r' r g"
3.272 @@ -899,7 +858,6 @@
3.273    qed
3.274  qed
3.275
3.276 -
3.277  lemma embed_bothWays_iso:
3.278  assumes WELL: "Well_order r"  and WELL': "Well_order r'" and
3.279          EMB: "embed r r' f" and EMB': "embed r' r g"
3.280 @@ -907,8 +865,7 @@
3.281  unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)
3.282
3.283
3.284 -subsection {* More properties of embeddings, strict embeddings and isomorphisms  *}
3.285 -
3.286 +subsection {* More properties of embeddings, strict embeddings and isomorphisms *}
3.287
3.288  lemma embed_bothWays_Field_bij_betw:
3.289  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.290 @@ -924,7 +881,6 @@
3.291    show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto
3.292  qed
3.293
3.294 -
3.295  lemma embedS_comp_embed:
3.296  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
3.297          and  EMB: "embedS r r' f" and EMB': "embed r' r'' f'"
3.298 @@ -948,7 +904,6 @@
3.299    ultimately show ?thesis unfolding embedS_def by auto
3.300  qed
3.301
3.302 -
3.303  lemma embed_comp_embedS:
3.304  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
3.305          and  EMB: "embed r r' f" and EMB': "embedS r' r'' f'"
3.306 @@ -972,7 +927,6 @@
3.307    ultimately show ?thesis unfolding embedS_def by auto
3.308  qed
3.309
3.310 -
3.311  lemma embed_comp_iso:
3.312  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
3.313          and  EMB: "embed r r' f" and EMB': "iso r' r'' f'"
3.314 @@ -980,7 +934,6 @@
3.315  using assms unfolding iso_def
3.316  by (auto simp add: comp_embed)
3.317
3.318 -
3.319  lemma iso_comp_embed:
3.320  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
3.321          and  EMB: "iso r r' f" and EMB': "embed r' r'' f'"
3.322 @@ -988,7 +941,6 @@
3.323  using assms unfolding iso_def
3.324  by (auto simp add: comp_embed)
3.325
3.326 -
3.327  lemma embedS_comp_iso:
3.328  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
3.329          and  EMB: "embedS r r' f" and EMB': "iso r' r'' f'"
3.330 @@ -996,7 +948,6 @@
3.331  using assms unfolding iso_def
3.332  by (auto simp add: embedS_comp_embed)
3.333
3.334 -
3.335  lemma iso_comp_embedS:
3.336  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
3.337          and  EMB: "iso r r' f" and EMB': "embedS r' r'' f'"
3.338 @@ -1004,7 +955,6 @@
3.339  using assms unfolding iso_def  using embed_comp_embedS
3.340  by (auto simp add: embed_comp_embedS)
3.341
3.342 -
3.343  lemma embedS_Field:
3.344  assumes WELL: "Well_order r" and EMB: "embedS r r' f"
3.345  shows "f  (Field r) < Field r'"
3.346 @@ -1020,7 +970,6 @@
3.347    ultimately show ?thesis by blast
3.348  qed
3.349
3.350 -
3.351  lemma embedS_iff:
3.352  assumes WELL: "Well_order r" and ISO: "embed r r' f"
3.353  shows "embedS r r' f = (f  (Field r) < Field r')"
3.354 @@ -1036,12 +985,10 @@
3.355    using ISO by auto
3.356  qed
3.357
3.358 -
3.359  lemma iso_Field:
3.360  "iso r r' f \<Longrightarrow> f  (Field r) = Field r'"
3.361  using assms by (auto simp add: iso_def bij_betw_def)
3.362
3.363 -
3.364  lemma iso_iff:
3.365  assumes "Well_order r"
3.366  shows "iso r r' f = (embed r r' f \<and> f  (Field r) = Field r')"
3.367 @@ -1057,7 +1004,6 @@
3.368    with * show "iso r r' f" unfolding iso_def by auto
3.369  qed
3.370
3.371 -
3.372  lemma iso_iff2:
3.373  assumes "Well_order r"
3.374  shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>
3.375 @@ -1110,7 +1056,6 @@
3.376    thus "embed r r' f" unfolding embed_def using * by auto
3.377  qed
3.378
3.379 -
3.380  lemma iso_iff3:
3.381  assumes WELL: "Well_order r" and WELL': "Well_order r'"
3.382  shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)"
3.383 @@ -1140,6 +1085,4 @@
3.384    qed
3.385  qed
3.386
3.387 -
3.388 -
3.389  end

     4.1 --- a/src/HOL/BNF_Wellorder_Relation.thy	Tue Jan 21 16:56:34 2014 +0100
4.2 +++ b/src/HOL/BNF_Wellorder_Relation.thy	Wed Jan 22 09:45:30 2014 +0100
4.3 @@ -11,13 +11,11 @@
4.4  imports Order_Relation
4.5  begin
4.6
4.7 -
4.8  text{* In this section, we develop basic concepts and results pertaining
4.9  to well-order relations.  Note that we consider well-order relations
4.10  as {\em non-strict relations},
4.11  i.e., as containing the diagonals of their fields. *}
4.12
4.13 -
4.14  locale wo_rel =
4.15    fixes r :: "'a rel"
4.16    assumes WELL: "Well_order r"
4.17 @@ -40,49 +38,39 @@
4.18
4.19  subsection {* Auxiliaries *}
4.20
4.21 -
4.22  lemma REFL: "Refl r"
4.23  using WELL order_on_defs[of _ r] by auto
4.24
4.25 -
4.26  lemma TRANS: "trans r"
4.27  using WELL order_on_defs[of _ r] by auto
4.28
4.29 -
4.30  lemma ANTISYM: "antisym r"
4.31  using WELL order_on_defs[of _ r] by auto
4.32
4.33 -
4.34  lemma TOTAL: "Total r"
4.35  using WELL order_on_defs[of _ r] by auto
4.36
4.37 -
4.38  lemma TOTALS: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
4.39  using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force
4.40
4.41 -
4.42  lemma LIN: "Linear_order r"
4.43  using WELL well_order_on_def[of _ r] by auto
4.44
4.45 -
4.46  lemma WF: "wf (r - Id)"
4.47  using WELL well_order_on_def[of _ r] by auto
4.48
4.49 -
4.50  lemma cases_Total:
4.51  "\<And> phi a b. \<lbrakk>{a,b} <= Field r; ((a,b) \<in> r \<Longrightarrow> phi a b); ((b,a) \<in> r \<Longrightarrow> phi a b)\<rbrakk>
4.52               \<Longrightarrow> phi a b"
4.53  using TOTALS by auto
4.54
4.55 -
4.56  lemma cases_Total3:
4.57  "\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<or> (b,a) \<in> r - Id \<Longrightarrow> phi a b);
4.58                (a = b \<Longrightarrow> phi a b)\<rbrakk>  \<Longrightarrow> phi a b"
4.59  using TOTALS by auto
4.60
4.61
4.62 -subsection {* Well-founded induction and recursion adapted to non-strict well-order relations  *}
4.63 -
4.64 +subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
4.65
4.66  text{* Here we provide induction and recursion principles specific to {\em non-strict}
4.67  well-order relations.
4.68 @@ -90,7 +78,6 @@
4.69  for doing away with the tediousness of
4.70  having to take out the diagonal each time in order to switch to a well-founded relation. *}
4.71
4.72 -
4.73  lemma well_order_induct:
4.74  assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
4.75  shows "P a"
4.76 @@ -100,19 +87,16 @@
4.77    thus "P a" using WF wf_induct[of "r - Id" P a] by blast
4.78  qed
4.79
4.80 -
4.81  definition
4.82  worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
4.83  where
4.84  "worec F \<equiv> wfrec (r - Id) F"
4.85
4.86 -
4.87  definition
4.88  adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
4.89  where
4.90  "adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x"
4.91
4.92 -
4.93  lemma worec_fixpoint:
4.95  shows "worec H = H (worec H)"
4.96 @@ -127,8 +111,7 @@
4.97  qed
4.98
4.99
4.100 -subsection {* The notions of maximum, minimum, supremum, successor and order filter  *}
4.101 -
4.102 +subsection {* The notions of maximum, minimum, supremum, successor and order filter *}
4.103
4.104  text{*
4.105  We define the successor {\em of a set}, and not of an element (the latter is of course
4.106 @@ -141,18 +124,15 @@
4.107  meaningful for sets for which strict upper bounds exist.
4.108  Order filters for well-orders are also known as initial segments". *}
4.109
4.110 -
4.111  definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
4.112  where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
4.113
4.114 -
4.115  definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
4.116  where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
4.117
4.118  definition minim :: "'a set \<Rightarrow> 'a"
4.119  where "minim A \<equiv> THE b. isMinim A b"
4.120
4.121 -
4.122  definition supr :: "'a set \<Rightarrow> 'a"
4.123  where "supr A \<equiv> minim (Above A)"
4.124
4.125 @@ -166,7 +146,6 @@
4.126
4.127  subsubsection {* Properties of max2 *}
4.128
4.129 -
4.130  lemma max2_greater_among:
4.131  assumes "a \<in> Field r" and "b \<in> Field r"
4.132  shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
4.133 @@ -191,26 +170,22 @@
4.134    total_on_def[of "Field r" r] by blast
4.135  qed
4.136
4.137 -
4.138  lemma max2_greater:
4.139  assumes "a \<in> Field r" and "b \<in> Field r"
4.140  shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
4.141  using assms by (auto simp add: max2_greater_among)
4.142
4.143 -
4.144  lemma max2_among:
4.145  assumes "a \<in> Field r" and "b \<in> Field r"
4.146  shows "max2 a b \<in> {a, b}"
4.147  using assms max2_greater_among[of a b] by simp
4.148
4.149 -
4.150  lemma max2_equals1:
4.151  assumes "a \<in> Field r" and "b \<in> Field r"
4.152  shows "(max2 a b = a) = ((b,a) \<in> r)"
4.153  using assms ANTISYM unfolding antisym_def using TOTALS
4.154  by(auto simp add: max2_def max2_among)
4.155
4.156 -
4.157  lemma max2_equals2:
4.158  assumes "a \<in> Field r" and "b \<in> Field r"
4.159  shows "(max2 a b = b) = ((a,b) \<in> r)"
4.160 @@ -220,7 +195,6 @@
4.161
4.162  subsubsection {* Existence and uniqueness for isMinim and well-definedness of minim *}
4.163
4.164 -
4.165  lemma isMinim_unique:
4.166  assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
4.167  shows "a = a'"
4.168 @@ -240,7 +214,6 @@
4.169    show ?thesis using ANTISYM antisym_def[of r] by blast
4.170  qed
4.171
4.172 -
4.173  lemma Well_order_isMinim_exists:
4.174  assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
4.175  shows "\<exists>b. isMinim B b"
4.176 @@ -269,7 +242,6 @@
4.177    qed
4.178  qed
4.179
4.180 -
4.181  lemma minim_isMinim:
4.182  assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
4.183  shows "isMinim B (minim B)"
4.184 @@ -284,10 +256,8 @@
4.185    unfolding minim_def using theI[of ?phi b] by blast
4.186  qed
4.187
4.188 -
4.189  subsubsection{* Properties of minim *}
4.190
4.191 -
4.192  lemma minim_in:
4.193  assumes "B \<le> Field r" and "B \<noteq> {}"
4.194  shows "minim B \<in> B"
4.195 @@ -297,7 +267,6 @@
4.196    thus ?thesis by (simp add: isMinim_def)
4.197  qed
4.198
4.199 -
4.200  lemma minim_inField:
4.201  assumes "B \<le> Field r" and "B \<noteq> {}"
4.202  shows "minim B \<in> Field r"
4.203 @@ -306,7 +275,6 @@
4.204    thus ?thesis using assms by blast
4.205  qed
4.206
4.207 -
4.208  lemma minim_least:
4.209  assumes  SUB: "B \<le> Field r" and IN: "b \<in> B"
4.210  shows "(minim B, b) \<in> r"
4.211 @@ -316,7 +284,6 @@
4.212    thus ?thesis by (auto simp add: isMinim_def IN)
4.213  qed
4.214
4.215 -
4.216  lemma equals_minim:
4.217  assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
4.218          LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
4.219 @@ -329,10 +296,8 @@
4.220    using isMinim_unique by auto
4.221  qed
4.222
4.223 -
4.224  subsubsection{* Properties of successor *}
4.225
4.226 -
4.227  lemma suc_AboveS:
4.228  assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
4.229  shows "suc B \<in> AboveS B"
4.230 @@ -343,7 +308,6 @@
4.231    using assms by (simp add: minim_in)
4.232  qed
4.233
4.234 -
4.235  lemma suc_greater:
4.236  assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
4.237          IN: "b \<in> B"
4.238 @@ -354,7 +318,6 @@
4.239    with IN AboveS_def[of r] show ?thesis by simp
4.240  qed
4.241
4.242 -
4.243  lemma suc_least_AboveS:
4.244  assumes ABOVES: "a \<in> AboveS B"
4.245  shows "(suc B,a) \<in> r"
4.246 @@ -365,7 +328,6 @@
4.247    using assms minim_least by simp
4.248  qed
4.249
4.250 -
4.251  lemma suc_inField:
4.252  assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
4.253  shows "suc B \<in> Field r"
4.254 @@ -375,7 +337,6 @@
4.255    using assms AboveS_Field[of r] by auto
4.256  qed
4.257
4.258 -
4.259  lemma equals_suc_AboveS:
4.260  assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
4.261          MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
4.262 @@ -388,7 +349,6 @@
4.263    by simp
4.264  qed
4.265
4.266 -
4.267  lemma suc_underS:
4.268  assumes IN: "a \<in> Field r"
4.269  shows "a = suc (underS a)"
4.270 @@ -432,7 +392,6 @@
4.271
4.272  subsubsection {* Properties of order filters *}
4.273
4.274 -
4.275  lemma under_ofilter:
4.276  "ofilter (under a)"
4.277  proof(unfold ofilter_def under_def, auto simp add: Field_def)
4.278 @@ -442,7 +401,6 @@
4.279    using TRANS trans_def[of r] by blast
4.280  qed
4.281
4.282 -
4.283  lemma underS_ofilter:
4.284  "ofilter (underS a)"
4.285  proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
4.286 @@ -456,12 +414,10 @@
4.287    using TRANS trans_def[of r] by blast
4.288  qed
4.289
4.290 -
4.291  lemma Field_ofilter:
4.292  "ofilter (Field r)"
4.293  by(unfold ofilter_def under_def, auto simp add: Field_def)
4.294
4.295 -
4.296  lemma ofilter_underS_Field:
4.297  "ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
4.298  proof
4.299 @@ -523,12 +479,10 @@
4.300    qed
4.301  qed
4.302
4.303 -
4.304  lemma ofilter_UNION:
4.305  "(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
4.306  unfolding ofilter_def by blast
4.307
4.308 -
4.309  lemma ofilter_under_UNION:
4.310  assumes "ofilter A"
4.311  shows "A = (\<Union> a \<in> A. under a)"
4.312 @@ -542,10 +496,8 @@
4.313    thus "A \<le> (\<Union> a \<in> A. under a)" by blast
4.314  qed
4.315
4.316 -
4.317  subsubsection{* Other properties *}
4.318
4.319 -
4.320  lemma ofilter_linord:
4.321  assumes OF1: "ofilter A" and OF2: "ofilter B"
4.322  shows "A \<le> B \<or> B \<le> A"
4.323 @@ -587,7 +539,6 @@
4.324    qed
4.325  qed
4.326
4.327 -
4.328  lemma ofilter_AboveS_Field:
4.329  assumes "ofilter A"
4.330  shows "A \<union> (AboveS A) = Field r"
4.331 @@ -614,7 +565,6 @@
4.332    thus "Field r \<le> A \<union> (AboveS A)" by blast
4.333  qed
4.334
4.335 -
4.336  lemma suc_ofilter_in:
4.337  assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
4.338          REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
4.339 @@ -633,10 +583,6 @@
4.340    thus ?thesis by blast
4.341  qed
4.342
4.343 -
4.344 -
4.345  end (* context wo_rel *)
4.346
4.347 -
4.348 -
4.349  end
`