src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy
author blanchet
Thu Jan 16 20:52:54 2014 +0100 (2014-01-16)
changeset 55023 38db7814481d
parent 54980 7e0573a490ee
permissions -rw-r--r--
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet@54481
     1
(*  Title:      HOL/Cardinals/Constructions_on_Wellorders_FP.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@54481
     5
Constructions on wellorders (FP).
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@54481
     8
header {* Constructions on Wellorders (FP) *}
blanchet@48975
     9
blanchet@54481
    10
theory Constructions_on_Wellorders_FP
blanchet@54481
    11
imports Wellorder_Embedding_FP
blanchet@48975
    12
begin
blanchet@48975
    13
blanchet@48975
    14
blanchet@48975
    15
text {* In this section, we study basic constructions on well-orders, such as restriction to
blanchet@48975
    16
a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders,
blanchet@48975
    17
and bounded square.  We also define between well-orders
blanchet@48975
    18
the relations @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"}),
blanchet@48975
    19
@{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}), and
blanchet@48975
    20
@{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).  We study the
blanchet@48975
    21
connections between these relations, order filters, and the aforementioned constructions.
blanchet@48975
    22
A main result of this section is that @{text "<o"} is well-founded.  *}
blanchet@48975
    23
blanchet@48975
    24
blanchet@48975
    25
subsection {* Restriction to a set  *}
blanchet@48975
    26
blanchet@48975
    27
blanchet@48975
    28
abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel"
blanchet@48975
    29
where "Restr r A \<equiv> r Int (A \<times> A)"
blanchet@48975
    30
blanchet@48975
    31
blanchet@48975
    32
lemma Restr_subset:
blanchet@48975
    33
"A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A"
blanchet@48975
    34
by blast
blanchet@48975
    35
blanchet@48975
    36
blanchet@48975
    37
lemma Restr_Field: "Restr r (Field r) = r"
blanchet@48975
    38
unfolding Field_def by auto
blanchet@48975
    39
blanchet@48975
    40
blanchet@48975
    41
lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
blanchet@48975
    42
unfolding refl_on_def Field_def by auto
blanchet@48975
    43
blanchet@48975
    44
blanchet@48975
    45
lemma antisym_Restr:
blanchet@48975
    46
"antisym r \<Longrightarrow> antisym(Restr r A)"
blanchet@48975
    47
unfolding antisym_def Field_def by auto
blanchet@48975
    48
blanchet@48975
    49
blanchet@48975
    50
lemma Total_Restr:
blanchet@48975
    51
"Total r \<Longrightarrow> Total(Restr r A)"
blanchet@48975
    52
unfolding total_on_def Field_def by auto
blanchet@48975
    53
blanchet@48975
    54
blanchet@48975
    55
lemma trans_Restr:
blanchet@48975
    56
"trans r \<Longrightarrow> trans(Restr r A)"
blanchet@48975
    57
unfolding trans_def Field_def by blast
blanchet@48975
    58
blanchet@48975
    59
blanchet@48975
    60
lemma Preorder_Restr:
blanchet@48975
    61
"Preorder r \<Longrightarrow> Preorder(Restr r A)"
blanchet@48975
    62
unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)
blanchet@48975
    63
blanchet@48975
    64
blanchet@48975
    65
lemma Partial_order_Restr:
blanchet@48975
    66
"Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
blanchet@48975
    67
unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)
blanchet@48975
    68
blanchet@48975
    69
blanchet@48975
    70
lemma Linear_order_Restr:
blanchet@48975
    71
"Linear_order r \<Longrightarrow> Linear_order(Restr r A)"
blanchet@48975
    72
unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)
blanchet@48975
    73
blanchet@48975
    74
blanchet@48975
    75
lemma Well_order_Restr:
blanchet@48975
    76
assumes "Well_order r"
blanchet@48975
    77
shows "Well_order(Restr r A)"
blanchet@48975
    78
proof-
blanchet@48975
    79
  have "Restr r A - Id \<le> r - Id" using Restr_subset by blast
blanchet@48975
    80
  hence "wf(Restr r A - Id)" using assms
blanchet@48975
    81
  using well_order_on_def wf_subset by blast
blanchet@48975
    82
  thus ?thesis using assms unfolding well_order_on_def
blanchet@48975
    83
  by (simp add: Linear_order_Restr)
blanchet@48975
    84
qed
blanchet@48975
    85
blanchet@48975
    86
blanchet@48975
    87
lemma Field_Restr_subset: "Field(Restr r A) \<le> A"
blanchet@48975
    88
by (auto simp add: Field_def)
blanchet@48975
    89
blanchet@48975
    90
blanchet@48975
    91
lemma Refl_Field_Restr:
blanchet@48975
    92
"Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"
blanchet@54482
    93
unfolding refl_on_def Field_def by blast
blanchet@48975
    94
blanchet@48975
    95
blanchet@48975
    96
lemma Refl_Field_Restr2:
blanchet@48975
    97
"\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
blanchet@48975
    98
by (auto simp add: Refl_Field_Restr)
blanchet@48975
    99
blanchet@48975
   100
blanchet@48975
   101
lemma well_order_on_Restr:
blanchet@48975
   102
assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
blanchet@48975
   103
shows "well_order_on A (Restr r A)"
blanchet@48975
   104
using assms
blanchet@48975
   105
using Well_order_Restr[of r A] Refl_Field_Restr2[of r A]
blanchet@48975
   106
     order_on_defs[of "Field r" r] by auto
blanchet@48975
   107
blanchet@48975
   108
blanchet@48975
   109
subsection {* Order filters versus restrictions and embeddings  *}
blanchet@48975
   110
blanchet@48975
   111
blanchet@48975
   112
lemma Field_Restr_ofilter:
blanchet@48975
   113
"\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
blanchet@48975
   114
by (auto simp add: wo_rel_def wo_rel.ofilter_def wo_rel.REFL Refl_Field_Restr2)
blanchet@48975
   115
blanchet@48975
   116
blanchet@48975
   117
lemma ofilter_Restr_under:
blanchet@48975
   118
assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
blanchet@55023
   119
shows "under (Restr r A) a = under r a"
blanchet@48975
   120
using assms wo_rel_def
blanchet@55023
   121
proof(auto simp add: wo_rel.ofilter_def under_def)
blanchet@48975
   122
  fix b assume *: "a \<in> A" and "(b,a) \<in> r"
blanchet@55023
   123
  hence "b \<in> under r a \<and> a \<in> Field r"
blanchet@55023
   124
  unfolding under_def using Field_def by fastforce
blanchet@48975
   125
  thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
blanchet@48975
   126
qed
blanchet@48975
   127
blanchet@48975
   128
blanchet@48975
   129
lemma ofilter_embed:
blanchet@48975
   130
assumes "Well_order r"
blanchet@48975
   131
shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)"
blanchet@48975
   132
proof
blanchet@48975
   133
  assume *: "wo_rel.ofilter r A"
blanchet@48975
   134
  show "A \<le> Field r \<and> embed (Restr r A) r id"
blanchet@48975
   135
  proof(unfold embed_def, auto)
blanchet@48975
   136
    fix a assume "a \<in> A" thus "a \<in> Field r" using assms *
blanchet@48975
   137
    by (auto simp add: wo_rel_def wo_rel.ofilter_def)
blanchet@48975
   138
  next
blanchet@48975
   139
    fix a assume "a \<in> Field (Restr r A)"
blanchet@55023
   140
    thus "bij_betw id (under (Restr r A) a) (under r a)" using assms *
blanchet@48975
   141
    by (simp add: ofilter_Restr_under Field_Restr_ofilter)
blanchet@48975
   142
  qed
blanchet@48975
   143
next
blanchet@48975
   144
  assume *: "A \<le> Field r \<and> embed (Restr r A) r id"
blanchet@48975
   145
  hence "Field(Restr r A) \<le> Field r"
blanchet@48975
   146
  using assms  embed_Field[of "Restr r A" r id] id_def
blanchet@48975
   147
        Well_order_Restr[of r] by auto
blanchet@48975
   148
  {fix a assume "a \<in> A"
blanchet@48975
   149
   hence "a \<in> Field(Restr r A)" using * assms
blanchet@48975
   150
   by (simp add: order_on_defs Refl_Field_Restr2)
blanchet@55023
   151
   hence "bij_betw id (under (Restr r A) a) (under r a)"
blanchet@48975
   152
   using * unfolding embed_def by auto
blanchet@55023
   153
   hence "under r a \<le> under (Restr r A) a"
blanchet@48975
   154
   unfolding bij_betw_def by auto
blanchet@55023
   155
   also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)
blanchet@48975
   156
   also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)
blanchet@55023
   157
   finally have "under r a \<le> A" .
blanchet@48975
   158
  }
blanchet@48975
   159
  thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def)
blanchet@48975
   160
qed
blanchet@48975
   161
blanchet@48975
   162
blanchet@48975
   163
lemma ofilter_Restr_Int:
blanchet@48975
   164
assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A"
blanchet@48975
   165
shows "wo_rel.ofilter (Restr r B) (A Int B)"
blanchet@48975
   166
proof-
blanchet@48975
   167
  let ?rB = "Restr r B"
blanchet@48975
   168
  have Well: "wo_rel r" unfolding wo_rel_def using WELL .
blanchet@48975
   169
  hence Refl: "Refl r" by (simp add: wo_rel.REFL)
blanchet@48975
   170
  hence Field: "Field ?rB = Field r Int B"
blanchet@48975
   171
  using Refl_Field_Restr by blast
blanchet@48975
   172
  have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
blanchet@48975
   173
  by (simp add: Well_order_Restr wo_rel_def)
blanchet@48975
   174
  (* Main proof *)
blanchet@48975
   175
  show ?thesis using WellB assms
blanchet@55023
   176
  proof(auto simp add: wo_rel.ofilter_def under_def)
blanchet@48975
   177
    fix a assume "a \<in> A" and *: "a \<in> B"
blanchet@48975
   178
    hence "a \<in> Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def)
blanchet@48975
   179
    with * show "a \<in> Field ?rB" using Field by auto
blanchet@48975
   180
  next
blanchet@48975
   181
    fix a b assume "a \<in> A" and "(b,a) \<in> r"
blanchet@55023
   182
    thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def)
blanchet@48975
   183
  qed
blanchet@48975
   184
qed
blanchet@48975
   185
blanchet@48975
   186
blanchet@48975
   187
lemma ofilter_Restr_subset:
blanchet@48975
   188
assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" and SUB: "A \<le> B"
blanchet@48975
   189
shows "wo_rel.ofilter (Restr r B) A"
blanchet@48975
   190
proof-
blanchet@48975
   191
  have "A Int B = A" using SUB by blast
blanchet@48975
   192
  thus ?thesis using assms ofilter_Restr_Int[of r A B] by auto
blanchet@48975
   193
qed
blanchet@48975
   194
blanchet@48975
   195
blanchet@48975
   196
lemma ofilter_subset_embed:
blanchet@48975
   197
assumes WELL: "Well_order r" and
blanchet@48975
   198
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
blanchet@48975
   199
shows "(A \<le> B) = (embed (Restr r A) (Restr r B) id)"
blanchet@48975
   200
proof-
blanchet@48975
   201
  let ?rA = "Restr r A"  let ?rB = "Restr r B"
blanchet@48975
   202
  have Well: "wo_rel r" unfolding wo_rel_def using WELL .
blanchet@48975
   203
  hence Refl: "Refl r" by (simp add: wo_rel.REFL)
blanchet@48975
   204
  hence FieldA: "Field ?rA = Field r Int A"
blanchet@48975
   205
  using Refl_Field_Restr by blast
blanchet@48975
   206
  have FieldB: "Field ?rB = Field r Int B"
blanchet@48975
   207
  using Refl Refl_Field_Restr by blast
blanchet@48975
   208
  have WellA: "wo_rel ?rA \<and> Well_order ?rA" using WELL
blanchet@48975
   209
  by (simp add: Well_order_Restr wo_rel_def)
blanchet@48975
   210
  have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
blanchet@48975
   211
  by (simp add: Well_order_Restr wo_rel_def)
blanchet@48975
   212
  (* Main proof *)
blanchet@48975
   213
  show ?thesis
blanchet@48975
   214
  proof
blanchet@48975
   215
    assume *: "A \<le> B"
blanchet@48975
   216
    hence "wo_rel.ofilter (Restr r B) A" using assms
blanchet@48975
   217
    by (simp add: ofilter_Restr_subset)
blanchet@48975
   218
    hence "embed (Restr ?rB A) (Restr r B) id"
blanchet@48975
   219
    using WellB ofilter_embed[of "?rB" A] by auto
blanchet@48975
   220
    thus "embed (Restr r A) (Restr r B) id"
blanchet@48975
   221
    using * by (simp add: Restr_subset)
blanchet@48975
   222
  next
blanchet@48975
   223
    assume *: "embed (Restr r A) (Restr r B) id"
blanchet@48975
   224
    {fix a assume **: "a \<in> A"
blanchet@48975
   225
     hence "a \<in> Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def)
blanchet@48975
   226
     with ** FieldA have "a \<in> Field ?rA" by auto
blanchet@48975
   227
     hence "a \<in> Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto
blanchet@48975
   228
     hence "a \<in> B" using FieldB by auto
blanchet@48975
   229
    }
blanchet@48975
   230
    thus "A \<le> B" by blast
blanchet@48975
   231
  qed
blanchet@48975
   232
qed
blanchet@48975
   233
blanchet@48975
   234
blanchet@48975
   235
lemma ofilter_subset_embedS_iso:
blanchet@48975
   236
assumes WELL: "Well_order r" and
blanchet@48975
   237
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
blanchet@48975
   238
shows "((A < B) = (embedS (Restr r A) (Restr r B) id)) \<and>
blanchet@48975
   239
       ((A = B) = (iso (Restr r A) (Restr r B) id))"
blanchet@48975
   240
proof-
blanchet@48975
   241
  let ?rA = "Restr r A"  let ?rB = "Restr r B"
blanchet@48975
   242
  have Well: "wo_rel r" unfolding wo_rel_def using WELL .
blanchet@48975
   243
  hence Refl: "Refl r" by (simp add: wo_rel.REFL)
blanchet@48975
   244
  hence "Field ?rA = Field r Int A"
blanchet@48975
   245
  using Refl_Field_Restr by blast
blanchet@48975
   246
  hence FieldA: "Field ?rA = A" using OFA Well
blanchet@48975
   247
  by (auto simp add: wo_rel.ofilter_def)
blanchet@48975
   248
  have "Field ?rB = Field r Int B"
blanchet@48975
   249
  using Refl Refl_Field_Restr by blast
blanchet@48975
   250
  hence FieldB: "Field ?rB = B" using OFB Well
blanchet@48975
   251
  by (auto simp add: wo_rel.ofilter_def)
blanchet@48975
   252
  (* Main proof *)
blanchet@48975
   253
  show ?thesis unfolding embedS_def iso_def
blanchet@48975
   254
  using assms ofilter_subset_embed[of r A B]
blanchet@48975
   255
        FieldA FieldB bij_betw_id_iff[of A B] by auto
blanchet@48975
   256
qed
blanchet@48975
   257
blanchet@48975
   258
blanchet@48975
   259
lemma ofilter_subset_embedS:
blanchet@48975
   260
assumes WELL: "Well_order r" and
blanchet@48975
   261
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
blanchet@48975
   262
shows "(A < B) = embedS (Restr r A) (Restr r B) id"
blanchet@48975
   263
using assms by (simp add: ofilter_subset_embedS_iso)
blanchet@48975
   264
blanchet@48975
   265
blanchet@48975
   266
lemma embed_implies_iso_Restr:
blanchet@48975
   267
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
blanchet@48975
   268
        EMB: "embed r' r f"
blanchet@48975
   269
shows "iso r' (Restr r (f ` (Field r'))) f"
blanchet@48975
   270
proof-
blanchet@48975
   271
  let ?A' = "Field r'"
blanchet@48975
   272
  let ?r'' = "Restr r (f ` ?A')"
blanchet@48975
   273
  have 0: "Well_order ?r''" using WELL Well_order_Restr by blast
blanchet@48975
   274
  have 1: "wo_rel.ofilter r (f ` ?A')" using assms embed_Field_ofilter  by blast
blanchet@48975
   275
  hence "Field ?r'' = f ` (Field r')" using WELL Field_Restr_ofilter by blast
blanchet@48975
   276
  hence "bij_betw f ?A' (Field ?r'')"
blanchet@48975
   277
  using EMB embed_inj_on WELL' unfolding bij_betw_def by blast
blanchet@48975
   278
  moreover
blanchet@48975
   279
  {have "\<forall>a b. (a,b) \<in> r' \<longrightarrow> a \<in> Field r' \<and> b \<in> Field r'"
blanchet@48975
   280
   unfolding Field_def by auto
blanchet@48975
   281
   hence "compat r' ?r'' f"
blanchet@48975
   282
   using assms embed_iff_compat_inj_on_ofilter
blanchet@48975
   283
   unfolding compat_def by blast
blanchet@48975
   284
  }
blanchet@48975
   285
  ultimately show ?thesis using WELL' 0 iso_iff3 by blast
blanchet@48975
   286
qed
blanchet@48975
   287
blanchet@48975
   288
blanchet@48975
   289
subsection {* The strict inclusion on proper ofilters is well-founded *}
blanchet@48975
   290
blanchet@48975
   291
blanchet@48975
   292
definition ofilterIncl :: "'a rel \<Rightarrow> 'a set rel"
blanchet@48975
   293
where
blanchet@48975
   294
"ofilterIncl r \<equiv> {(A,B). wo_rel.ofilter r A \<and> A \<noteq> Field r \<and>
blanchet@48975
   295
                         wo_rel.ofilter r B \<and> B \<noteq> Field r \<and> A < B}"
blanchet@48975
   296
blanchet@48975
   297
blanchet@48975
   298
lemma wf_ofilterIncl:
blanchet@48975
   299
assumes WELL: "Well_order r"
blanchet@48975
   300
shows "wf(ofilterIncl r)"
blanchet@48975
   301
proof-
blanchet@48975
   302
  have Well: "wo_rel r" using WELL by (simp add: wo_rel_def)
blanchet@48975
   303
  hence Lo: "Linear_order r" by (simp add: wo_rel.LIN)
blanchet@48975
   304
  let ?h = "(\<lambda> A. wo_rel.suc r A)"
blanchet@48975
   305
  let ?rS = "r - Id"
blanchet@48975
   306
  have "wf ?rS" using WELL by (simp add: order_on_defs)
blanchet@48975
   307
  moreover
blanchet@48975
   308
  have "compat (ofilterIncl r) ?rS ?h"
blanchet@48975
   309
  proof(unfold compat_def ofilterIncl_def,
blanchet@48975
   310
        intro allI impI, simp, elim conjE)
blanchet@48975
   311
    fix A B
blanchet@48975
   312
    assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and
blanchet@48975
   313
           **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"
blanchet@48975
   314
    then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and
blanchet@55023
   315
                         1: "A = underS r a \<and> B = underS r b"
blanchet@48975
   316
    using Well by (auto simp add: wo_rel.ofilter_underS_Field)
blanchet@48975
   317
    hence "a \<noteq> b" using *** by auto
blanchet@48975
   318
    moreover
blanchet@48975
   319
    have "(a,b) \<in> r" using 0 1 Lo ***
blanchet@55023
   320
    by (auto simp add: underS_incl_iff)
blanchet@48975
   321
    moreover
blanchet@48975
   322
    have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B"
blanchet@48975
   323
    using Well 0 1 by (simp add: wo_rel.suc_underS)
blanchet@48975
   324
    ultimately
blanchet@48975
   325
    show "(wo_rel.suc r A, wo_rel.suc r B) \<in> r \<and> wo_rel.suc r A \<noteq> wo_rel.suc r B"
blanchet@48975
   326
    by simp
blanchet@48975
   327
  qed
blanchet@48975
   328
  ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf)
blanchet@48975
   329
qed
blanchet@48975
   330
blanchet@48975
   331
blanchet@48975
   332
blanchet@54476
   333
subsection {* Ordering the well-orders by existence of embeddings *}
blanchet@48975
   334
blanchet@48975
   335
blanchet@48975
   336
text {* We define three relations between well-orders:
blanchet@48975
   337
\begin{itemize}
blanchet@48975
   338
\item @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"});
blanchet@48975
   339
\item @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"});
blanchet@48975
   340
\item @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).
blanchet@48975
   341
\end{itemize}
blanchet@48975
   342
%
blanchet@48975
   343
The prefix "ord" and the index "o" in these names stand for "ordinal-like".
blanchet@48975
   344
These relations shall be proved to be inter-connected in a similar fashion as the trio
blanchet@48975
   345
@{text "\<le>"}, @{text "<"}, @{text "="} associated to a total order on a set.
blanchet@48975
   346
*}
blanchet@48975
   347
blanchet@48975
   348
blanchet@48975
   349
definition ordLeq :: "('a rel * 'a' rel) set"
blanchet@48975
   350
where
blanchet@48975
   351
"ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}"
blanchet@48975
   352
blanchet@48975
   353
blanchet@48975
   354
abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50)
blanchet@48975
   355
where "r <=o r' \<equiv> (r,r') \<in> ordLeq"
blanchet@48975
   356
blanchet@48975
   357
blanchet@48975
   358
abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50)
blanchet@48975
   359
where "r \<le>o r' \<equiv> r <=o r'"
blanchet@48975
   360
blanchet@48975
   361
blanchet@48975
   362
definition ordLess :: "('a rel * 'a' rel) set"
blanchet@48975
   363
where
blanchet@48975
   364
"ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"
blanchet@48975
   365
blanchet@48975
   366
abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)
blanchet@48975
   367
where "r <o r' \<equiv> (r,r') \<in> ordLess"
blanchet@48975
   368
blanchet@48975
   369
blanchet@48975
   370
definition ordIso :: "('a rel * 'a' rel) set"
blanchet@48975
   371
where
blanchet@48975
   372
"ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"
blanchet@48975
   373
blanchet@48975
   374
abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)
blanchet@48975
   375
where "r =o r' \<equiv> (r,r') \<in> ordIso"
blanchet@48975
   376
blanchet@48975
   377
blanchet@48975
   378
lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def
blanchet@48975
   379
blanchet@48975
   380
lemma ordLeq_Well_order_simp:
blanchet@48975
   381
assumes "r \<le>o r'"
blanchet@48975
   382
shows "Well_order r \<and> Well_order r'"
blanchet@48975
   383
using assms unfolding ordLeq_def by simp
blanchet@48975
   384
blanchet@48975
   385
blanchet@48975
   386
text{* Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders
blanchet@48975
   387
on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
blanchet@48975
   388
restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,
blanchet@48975
   389
to @{text "'a rel rel"}.  *}
blanchet@48975
   390
blanchet@48975
   391
blanchet@48975
   392
lemma ordLeq_reflexive:
blanchet@48975
   393
"Well_order r \<Longrightarrow> r \<le>o r"
blanchet@48975
   394
unfolding ordLeq_def using id_embed[of r] by blast
blanchet@48975
   395
blanchet@48975
   396
blanchet@48975
   397
lemma ordLeq_transitive[trans]:
blanchet@48975
   398
assumes *: "r \<le>o r'" and **: "r' \<le>o r''"
blanchet@48975
   399
shows "r \<le>o r''"
blanchet@48975
   400
proof-
blanchet@48975
   401
  obtain f and f'
blanchet@48975
   402
  where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
blanchet@48975
   403
        "embed r r' f" and "embed r' r'' f'"
blanchet@48975
   404
  using * ** unfolding ordLeq_def by blast
blanchet@48975
   405
  hence "embed r r'' (f' o f)"
blanchet@48975
   406
  using comp_embed[of r r' f r'' f'] by auto
blanchet@48975
   407
  thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto
blanchet@48975
   408
qed
blanchet@48975
   409
blanchet@48975
   410
blanchet@48975
   411
lemma ordLeq_total:
blanchet@48975
   412
"\<lbrakk>Well_order r; Well_order r'\<rbrakk> \<Longrightarrow> r \<le>o r' \<or> r' \<le>o r"
blanchet@48975
   413
unfolding ordLeq_def using wellorders_totally_ordered by blast
blanchet@48975
   414
blanchet@48975
   415
blanchet@48975
   416
lemma ordIso_reflexive:
blanchet@48975
   417
"Well_order r \<Longrightarrow> r =o r"
blanchet@48975
   418
unfolding ordIso_def using id_iso[of r] by blast
blanchet@48975
   419
blanchet@48975
   420
blanchet@48975
   421
lemma ordIso_transitive[trans]:
blanchet@48975
   422
assumes *: "r =o r'" and **: "r' =o r''"
blanchet@48975
   423
shows "r =o r''"
blanchet@48975
   424
proof-
blanchet@48975
   425
  obtain f and f'
blanchet@48975
   426
  where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
blanchet@48975
   427
        "iso r r' f" and 3: "iso r' r'' f'"
blanchet@48975
   428
  using * ** unfolding ordIso_def by auto
blanchet@48975
   429
  hence "iso r r'' (f' o f)"
blanchet@48975
   430
  using comp_iso[of r r' f r'' f'] by auto
blanchet@48975
   431
  thus "r =o r''" unfolding ordIso_def using 1 by auto
blanchet@48975
   432
qed
blanchet@48975
   433
blanchet@48975
   434
blanchet@48975
   435
lemma ordIso_symmetric:
blanchet@48975
   436
assumes *: "r =o r'"
blanchet@48975
   437
shows "r' =o r"
blanchet@48975
   438
proof-
blanchet@48975
   439
  obtain f where 1: "Well_order r \<and> Well_order r'" and
blanchet@48975
   440
                 2: "embed r r' f \<and> bij_betw f (Field r) (Field r')"
blanchet@48975
   441
  using * by (auto simp add: ordIso_def iso_def)
blanchet@48975
   442
  let ?f' = "inv_into (Field r) f"
blanchet@48975
   443
  have "embed r' r ?f' \<and> bij_betw ?f' (Field r') (Field r)"
blanchet@48975
   444
  using 1 2 by (simp add: bij_betw_inv_into inv_into_Field_embed_bij_betw)
blanchet@48975
   445
  thus "r' =o r" unfolding ordIso_def using 1 by (auto simp add: iso_def)
blanchet@48975
   446
qed
blanchet@48975
   447
blanchet@48975
   448
blanchet@48975
   449
lemma ordLeq_ordLess_trans[trans]:
blanchet@48975
   450
assumes "r \<le>o r'" and " r' <o r''"
blanchet@48975
   451
shows "r <o r''"
blanchet@48975
   452
proof-
blanchet@48975
   453
  have "Well_order r \<and> Well_order r''"
blanchet@48975
   454
  using assms unfolding ordLeq_def ordLess_def by auto
blanchet@48975
   455
  thus ?thesis using assms unfolding ordLeq_def ordLess_def
blanchet@48975
   456
  using embed_comp_embedS by blast
blanchet@48975
   457
qed
blanchet@48975
   458
blanchet@48975
   459
blanchet@48975
   460
lemma ordLess_ordLeq_trans[trans]:
blanchet@48975
   461
assumes "r <o r'" and " r' \<le>o r''"
blanchet@48975
   462
shows "r <o r''"
blanchet@48975
   463
proof-
blanchet@48975
   464
  have "Well_order r \<and> Well_order r''"
blanchet@48975
   465
  using assms unfolding ordLeq_def ordLess_def by auto
blanchet@48975
   466
  thus ?thesis using assms unfolding ordLeq_def ordLess_def
blanchet@48975
   467
  using embedS_comp_embed by blast
blanchet@48975
   468
qed
blanchet@48975
   469
blanchet@48975
   470
blanchet@48975
   471
lemma ordLeq_ordIso_trans[trans]:
blanchet@48975
   472
assumes "r \<le>o r'" and " r' =o r''"
blanchet@48975
   473
shows "r \<le>o r''"
blanchet@48975
   474
proof-
blanchet@48975
   475
  have "Well_order r \<and> Well_order r''"
blanchet@48975
   476
  using assms unfolding ordLeq_def ordIso_def by auto
blanchet@48975
   477
  thus ?thesis using assms unfolding ordLeq_def ordIso_def
blanchet@48975
   478
  using embed_comp_iso by blast
blanchet@48975
   479
qed
blanchet@48975
   480
blanchet@48975
   481
blanchet@48975
   482
lemma ordIso_ordLeq_trans[trans]:
blanchet@48975
   483
assumes "r =o r'" and " r' \<le>o r''"
blanchet@48975
   484
shows "r \<le>o r''"
blanchet@48975
   485
proof-
blanchet@48975
   486
  have "Well_order r \<and> Well_order r''"
blanchet@48975
   487
  using assms unfolding ordLeq_def ordIso_def by auto
blanchet@48975
   488
  thus ?thesis using assms unfolding ordLeq_def ordIso_def
blanchet@48975
   489
  using iso_comp_embed by blast
blanchet@48975
   490
qed
blanchet@48975
   491
blanchet@48975
   492
blanchet@48975
   493
lemma ordLess_ordIso_trans[trans]:
blanchet@48975
   494
assumes "r <o r'" and " r' =o r''"
blanchet@48975
   495
shows "r <o r''"
blanchet@48975
   496
proof-
blanchet@48975
   497
  have "Well_order r \<and> Well_order r''"
blanchet@48975
   498
  using assms unfolding ordLess_def ordIso_def by auto
blanchet@48975
   499
  thus ?thesis using assms unfolding ordLess_def ordIso_def
blanchet@48975
   500
  using embedS_comp_iso by blast
blanchet@48975
   501
qed
blanchet@48975
   502
blanchet@48975
   503
blanchet@48975
   504
lemma ordIso_ordLess_trans[trans]:
blanchet@48975
   505
assumes "r =o r'" and " r' <o r''"
blanchet@48975
   506
shows "r <o r''"
blanchet@48975
   507
proof-
blanchet@48975
   508
  have "Well_order r \<and> Well_order r''"
blanchet@48975
   509
  using assms unfolding ordLess_def ordIso_def by auto
blanchet@48975
   510
  thus ?thesis using assms unfolding ordLess_def ordIso_def
blanchet@48975
   511
  using iso_comp_embedS by blast
blanchet@48975
   512
qed
blanchet@48975
   513
blanchet@48975
   514
blanchet@48975
   515
lemma ordLess_not_embed:
blanchet@48975
   516
assumes "r <o r'"
blanchet@48975
   517
shows "\<not>(\<exists>f'. embed r' r f')"
blanchet@48975
   518
proof-
blanchet@48975
   519
  obtain f where 1: "Well_order r \<and> Well_order r'" and 2: "embed r r' f" and
blanchet@48975
   520
                 3: " \<not> bij_betw f (Field r) (Field r')"
blanchet@48975
   521
  using assms unfolding ordLess_def by (auto simp add: embedS_def)
blanchet@48975
   522
  {fix f' assume *: "embed r' r f'"
blanchet@48975
   523
   hence "bij_betw f (Field r) (Field r')" using 1 2
blanchet@48975
   524
   by (simp add: embed_bothWays_Field_bij_betw)
blanchet@48975
   525
   with 3 have False by contradiction
blanchet@48975
   526
  }
blanchet@48975
   527
  thus ?thesis by blast
blanchet@48975
   528
qed
blanchet@48975
   529
blanchet@48975
   530
blanchet@48975
   531
lemma ordLess_Field:
blanchet@48975
   532
assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f"
blanchet@48975
   533
shows "\<not> (f`(Field r1) = Field r2)"
blanchet@48975
   534
proof-
blanchet@48975
   535
  let ?A1 = "Field r1"  let ?A2 = "Field r2"
blanchet@48975
   536
  obtain g where
blanchet@48975
   537
  0: "Well_order r1 \<and> Well_order r2" and
blanchet@48975
   538
  1: "embed r1 r2 g \<and> \<not>(bij_betw g ?A1 ?A2)"
blanchet@48975
   539
  using OL unfolding ordLess_def by (auto simp add: embedS_def)
blanchet@48975
   540
  hence "\<forall>a \<in> ?A1. f a = g a"
blanchet@48975
   541
  using 0 EMB embed_unique[of r1] by auto
blanchet@48975
   542
  hence "\<not>(bij_betw f ?A1 ?A2)"
blanchet@48975
   543
  using 1 bij_betw_cong[of ?A1] by blast
blanchet@48975
   544
  moreover
blanchet@48975
   545
  have "inj_on f ?A1" using EMB 0 by (simp add: embed_inj_on)
blanchet@48975
   546
  ultimately show ?thesis by (simp add: bij_betw_def)
blanchet@48975
   547
qed
blanchet@48975
   548
blanchet@48975
   549
blanchet@48975
   550
lemma ordLess_iff:
blanchet@48975
   551
"r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))"
blanchet@48975
   552
proof
blanchet@48975
   553
  assume *: "r <o r'"
blanchet@48975
   554
  hence "\<not>(\<exists>f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp
blanchet@48975
   555
  with * show "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"
blanchet@48975
   556
  unfolding ordLess_def by auto
blanchet@48975
   557
next
blanchet@48975
   558
  assume *: "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"
blanchet@48975
   559
  then obtain f where 1: "embed r r' f"
blanchet@48975
   560
  using wellorders_totally_ordered[of r r'] by blast
blanchet@48975
   561
  moreover
blanchet@48975
   562
  {assume "bij_betw f (Field r) (Field r')"
blanchet@48975
   563
   with * 1 have "embed r' r (inv_into (Field r) f) "
blanchet@48975
   564
   using inv_into_Field_embed_bij_betw[of r r' f] by auto
blanchet@48975
   565
   with * have False by blast
blanchet@48975
   566
  }
blanchet@48975
   567
  ultimately show "(r,r') \<in> ordLess"
blanchet@48975
   568
  unfolding ordLess_def using * by (fastforce simp add: embedS_def)
blanchet@48975
   569
qed
blanchet@48975
   570
blanchet@48975
   571
blanchet@48975
   572
lemma ordLess_irreflexive: "\<not> r <o r"
blanchet@48975
   573
proof
blanchet@48975
   574
  assume "r <o r"
blanchet@48975
   575
  hence "Well_order r \<and>  \<not>(\<exists>f. embed r r f)"
blanchet@48975
   576
  unfolding ordLess_iff ..
blanchet@48975
   577
  moreover have "embed r r id" using id_embed[of r] .
blanchet@48975
   578
  ultimately show False by blast
blanchet@48975
   579
qed
blanchet@48975
   580
blanchet@48975
   581
blanchet@48975
   582
lemma ordLeq_iff_ordLess_or_ordIso:
blanchet@48975
   583
"r \<le>o r' = (r <o r' \<or> r =o r')"
blanchet@48975
   584
unfolding ordRels_def embedS_defs iso_defs by blast
blanchet@48975
   585
blanchet@48975
   586
blanchet@48975
   587
lemma ordIso_iff_ordLeq:
blanchet@48975
   588
"(r =o r') = (r \<le>o r' \<and> r' \<le>o r)"
blanchet@48975
   589
proof
blanchet@48975
   590
  assume "r =o r'"
blanchet@48975
   591
  then obtain f where 1: "Well_order r \<and> Well_order r' \<and>
blanchet@48975
   592
                     embed r r' f \<and> bij_betw f (Field r) (Field r')"
blanchet@48975
   593
  unfolding ordIso_def iso_defs by auto
blanchet@48975
   594
  hence "embed r r' f \<and> embed r' r (inv_into (Field r) f)"
blanchet@48975
   595
  by (simp add: inv_into_Field_embed_bij_betw)
blanchet@48975
   596
  thus  "r \<le>o r' \<and> r' \<le>o r"
blanchet@48975
   597
  unfolding ordLeq_def using 1 by auto
blanchet@48975
   598
next
blanchet@48975
   599
  assume "r \<le>o r' \<and> r' \<le>o r"
blanchet@48975
   600
  then obtain f and g where 1: "Well_order r \<and> Well_order r' \<and>
blanchet@48975
   601
                           embed r r' f \<and> embed r' r g"
blanchet@48975
   602
  unfolding ordLeq_def by auto
blanchet@48975
   603
  hence "iso r r' f" by (auto simp add: embed_bothWays_iso)
blanchet@48975
   604
  thus "r =o r'" unfolding ordIso_def using 1 by auto
blanchet@48975
   605
qed
blanchet@48975
   606
blanchet@48975
   607
blanchet@48975
   608
lemma not_ordLess_ordLeq:
blanchet@48975
   609
"r <o r' \<Longrightarrow> \<not> r' \<le>o r"
blanchet@48975
   610
using ordLess_ordLeq_trans ordLess_irreflexive by blast
blanchet@48975
   611
blanchet@48975
   612
blanchet@48975
   613
lemma ordLess_or_ordLeq:
blanchet@48975
   614
assumes WELL: "Well_order r" and WELL': "Well_order r'"
blanchet@48975
   615
shows "r <o r' \<or> r' \<le>o r"
blanchet@48975
   616
proof-
blanchet@48975
   617
  have "r \<le>o r' \<or> r' \<le>o r"
blanchet@48975
   618
  using assms by (simp add: ordLeq_total)
blanchet@48975
   619
  moreover
blanchet@48975
   620
  {assume "\<not> r <o r' \<and> r \<le>o r'"
blanchet@48975
   621
   hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast
blanchet@48975
   622
   hence "r' \<le>o r" using ordIso_symmetric ordIso_iff_ordLeq by blast
blanchet@48975
   623
  }
blanchet@48975
   624
  ultimately show ?thesis by blast
blanchet@48975
   625
qed
blanchet@48975
   626
blanchet@48975
   627
blanchet@48975
   628
lemma not_ordLess_ordIso:
blanchet@48975
   629
"r <o r' \<Longrightarrow> \<not> r =o r'"
blanchet@48975
   630
using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
blanchet@48975
   631
blanchet@48975
   632
blanchet@48975
   633
lemma not_ordLeq_iff_ordLess:
blanchet@48975
   634
assumes WELL: "Well_order r" and WELL': "Well_order r'"
blanchet@48975
   635
shows "(\<not> r' \<le>o r) = (r <o r')"
blanchet@48975
   636
using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
blanchet@48975
   637
blanchet@48975
   638
blanchet@48975
   639
lemma not_ordLess_iff_ordLeq:
blanchet@48975
   640
assumes WELL: "Well_order r" and WELL': "Well_order r'"
blanchet@48975
   641
shows "(\<not> r' <o r) = (r \<le>o r')"
blanchet@48975
   642
using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
blanchet@48975
   643
blanchet@48975
   644
blanchet@48975
   645
lemma ordLess_transitive[trans]:
blanchet@48975
   646
"\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
blanchet@48975
   647
using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
blanchet@48975
   648
blanchet@48975
   649
blanchet@48975
   650
corollary ordLess_trans: "trans ordLess"
blanchet@48975
   651
unfolding trans_def using ordLess_transitive by blast
blanchet@48975
   652
blanchet@48975
   653
blanchet@48975
   654
lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric
blanchet@48975
   655
blanchet@48975
   656
blanchet@48975
   657
lemma ordIso_imp_ordLeq:
blanchet@48975
   658
"r =o r' \<Longrightarrow> r \<le>o r'"
blanchet@48975
   659
using ordIso_iff_ordLeq by blast
blanchet@48975
   660
blanchet@48975
   661
blanchet@48975
   662
lemma ordLess_imp_ordLeq:
blanchet@48975
   663
"r <o r' \<Longrightarrow> r \<le>o r'"
blanchet@48975
   664
using ordLeq_iff_ordLess_or_ordIso by blast
blanchet@48975
   665
blanchet@48975
   666
blanchet@48975
   667
lemma ofilter_subset_ordLeq:
blanchet@48975
   668
assumes WELL: "Well_order r" and
blanchet@48975
   669
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
blanchet@48975
   670
shows "(A \<le> B) = (Restr r A \<le>o Restr r B)"
blanchet@48975
   671
proof
blanchet@48975
   672
  assume "A \<le> B"
blanchet@48975
   673
  thus "Restr r A \<le>o Restr r B"
blanchet@48975
   674
  unfolding ordLeq_def using assms
blanchet@48975
   675
  Well_order_Restr Well_order_Restr ofilter_subset_embed by blast
blanchet@48975
   676
next
blanchet@48975
   677
  assume *: "Restr r A \<le>o Restr r B"
blanchet@48975
   678
  then obtain f where "embed (Restr r A) (Restr r B) f"
blanchet@48975
   679
  unfolding ordLeq_def by blast
blanchet@48975
   680
  {assume "B < A"
blanchet@48975
   681
   hence "Restr r B <o Restr r A"
blanchet@48975
   682
   unfolding ordLess_def using assms
blanchet@48975
   683
   Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast
blanchet@48975
   684
   hence False using * not_ordLess_ordLeq by blast
blanchet@48975
   685
  }
blanchet@48975
   686
  thus "A \<le> B" using OFA OFB WELL
blanchet@48975
   687
  wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast
blanchet@48975
   688
qed
blanchet@48975
   689
blanchet@48975
   690
blanchet@48975
   691
lemma ofilter_subset_ordLess:
blanchet@48975
   692
assumes WELL: "Well_order r" and
blanchet@48975
   693
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
blanchet@48975
   694
shows "(A < B) = (Restr r A <o Restr r B)"
blanchet@48975
   695
proof-
blanchet@48975
   696
  let ?rA = "Restr r A" let ?rB = "Restr r B"
blanchet@48975
   697
  have 1: "Well_order ?rA \<and> Well_order ?rB"
blanchet@48975
   698
  using WELL Well_order_Restr by blast
blanchet@48975
   699
  have "(A < B) = (\<not> B \<le> A)" using assms
blanchet@48975
   700
  wo_rel_def wo_rel.ofilter_linord[of r A B] by blast
blanchet@48975
   701
  also have "\<dots> = (\<not> Restr r B \<le>o Restr r A)"
blanchet@48975
   702
  using assms ofilter_subset_ordLeq by blast
blanchet@48975
   703
  also have "\<dots> = (Restr r A <o Restr r B)"
blanchet@48975
   704
  using 1 not_ordLeq_iff_ordLess by blast
blanchet@48975
   705
  finally show ?thesis .
blanchet@48975
   706
qed
blanchet@48975
   707
blanchet@48975
   708
blanchet@48975
   709
lemma ofilter_ordLess:
blanchet@48975
   710
"\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> (A < Field r) = (Restr r A <o r)"
blanchet@48975
   711
by (simp add: ofilter_subset_ordLess wo_rel.Field_ofilter
blanchet@48975
   712
    wo_rel_def Restr_Field)
blanchet@48975
   713
blanchet@48975
   714
blanchet@48975
   715
corollary underS_Restr_ordLess:
blanchet@48975
   716
assumes "Well_order r" and "Field r \<noteq> {}"
blanchet@55023
   717
shows "Restr r (underS r a) <o r"
blanchet@48975
   718
proof-
blanchet@55023
   719
  have "underS r a < Field r" using assms
blanchet@55023
   720
  by (simp add: underS_Field3)
blanchet@48975
   721
  thus ?thesis using assms
blanchet@48975
   722
  by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
blanchet@48975
   723
qed
blanchet@48975
   724
blanchet@48975
   725
blanchet@48975
   726
lemma embed_ordLess_ofilterIncl:
blanchet@48975
   727
assumes
blanchet@48975
   728
  OL12: "r1 <o r2" and OL23: "r2 <o r3" and
blanchet@48975
   729
  EMB13: "embed r1 r3 f13" and EMB23: "embed r2 r3 f23"
blanchet@48975
   730
shows "(f13`(Field r1), f23`(Field r2)) \<in> (ofilterIncl r3)"
blanchet@48975
   731
proof-
blanchet@48975
   732
  have OL13: "r1 <o r3"
blanchet@48975
   733
  using OL12 OL23 using ordLess_transitive by auto
blanchet@48975
   734
  let ?A1 = "Field r1"  let ?A2 ="Field r2" let ?A3 ="Field r3"
blanchet@48975
   735
  obtain f12 g23 where
blanchet@48975
   736
  0: "Well_order r1 \<and> Well_order r2 \<and> Well_order r3" and
blanchet@48975
   737
  1: "embed r1 r2 f12 \<and> \<not>(bij_betw f12 ?A1 ?A2)" and
blanchet@48975
   738
  2: "embed r2 r3 g23 \<and> \<not>(bij_betw g23 ?A2 ?A3)"
blanchet@48975
   739
  using OL12 OL23 by (auto simp add: ordLess_def embedS_def)
blanchet@48975
   740
  hence "\<forall>a \<in> ?A2. f23 a = g23 a"
blanchet@48975
   741
  using EMB23 embed_unique[of r2 r3] by blast
blanchet@48975
   742
  hence 3: "\<not>(bij_betw f23 ?A2 ?A3)"
blanchet@48975
   743
  using 2 bij_betw_cong[of ?A2 f23 g23] by blast
blanchet@48975
   744
  (*  *)
blanchet@48975
   745
  have 4: "wo_rel.ofilter r2 (f12 ` ?A1) \<and> f12 ` ?A1 \<noteq> ?A2"
blanchet@48975
   746
  using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field)
blanchet@48975
   747
  have 5: "wo_rel.ofilter r3 (f23 ` ?A2) \<and> f23 ` ?A2 \<noteq> ?A3"
blanchet@48975
   748
  using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field)
blanchet@48975
   749
  have 6: "wo_rel.ofilter r3 (f13 ` ?A1)  \<and> f13 ` ?A1 \<noteq> ?A3"
blanchet@48975
   750
  using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field)
blanchet@48975
   751
  (*  *)
blanchet@48975
   752
  have "f12 ` ?A1 < ?A2"
blanchet@48975
   753
  using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def)
blanchet@48975
   754
  moreover have "inj_on f23 ?A2"
blanchet@48975
   755
  using EMB23 0 by (simp add: wo_rel_def embed_inj_on)
blanchet@48975
   756
  ultimately
blanchet@48975
   757
  have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset)
blanchet@48975
   758
  moreover
blanchet@48975
   759
  {have "embed r1 r3 (f23 o f12)"
blanchet@48975
   760
   using 1 EMB23 0 by (auto simp add: comp_embed)
blanchet@48975
   761
   hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a"
blanchet@48975
   762
   using EMB13 0 embed_unique[of r1 r3 "f23 o f12" f13] by auto
blanchet@48975
   763
   hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force
blanchet@48975
   764
  }
blanchet@48975
   765
  ultimately
blanchet@48975
   766
  have "f13 ` ?A1 < f23 ` ?A2" by simp
blanchet@48975
   767
  (*  *)
blanchet@48975
   768
  with 5 6 show ?thesis
blanchet@48975
   769
  unfolding ofilterIncl_def by auto
blanchet@48975
   770
qed
blanchet@48975
   771
blanchet@48975
   772
blanchet@48975
   773
lemma ordLess_iff_ordIso_Restr:
blanchet@48975
   774
assumes WELL: "Well_order r" and WELL': "Well_order r'"
blanchet@55023
   775
shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"
blanchet@48975
   776
proof(auto)
blanchet@55023
   777
  fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"
blanchet@55023
   778
  hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
blanchet@48975
   779
  thus "r' <o r" using ** ordIso_ordLess_trans by blast
blanchet@48975
   780
next
blanchet@48975
   781
  assume "r' <o r"
blanchet@48975
   782
  then obtain f where 1: "Well_order r \<and> Well_order r'" and
blanchet@48975
   783
                      2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r"
blanchet@48975
   784
  unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast
blanchet@48975
   785
  hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast
blanchet@55023
   786
  then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f ` (Field r')"
blanchet@48975
   787
  using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)
blanchet@48975
   788
  have "iso r' (Restr r (f ` (Field r'))) f"
blanchet@48975
   789
  using embed_implies_iso_Restr 2 assms by blast
blanchet@48975
   790
  moreover have "Well_order (Restr r (f ` (Field r')))"
blanchet@48975
   791
  using WELL Well_order_Restr by blast
blanchet@48975
   792
  ultimately have "r' =o Restr r (f ` (Field r'))"
blanchet@48975
   793
  using WELL' unfolding ordIso_def by auto
blanchet@55023
   794
  hence "r' =o Restr r (underS r a)" using 4 by auto
blanchet@55023
   795
  thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto
blanchet@48975
   796
qed
blanchet@48975
   797
blanchet@48975
   798
blanchet@48975
   799
lemma internalize_ordLess:
blanchet@48975
   800
"(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)"
blanchet@48975
   801
proof
blanchet@48975
   802
  assume *: "r' <o r"
blanchet@48975
   803
  hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto
blanchet@55023
   804
  with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)"
blanchet@48975
   805
  using ordLess_iff_ordIso_Restr by blast
blanchet@55023
   806
  let ?p = "Restr r (underS r a)"
blanchet@55023
   807
  have "wo_rel.ofilter r (underS r a)" using 0
blanchet@48975
   808
  by (simp add: wo_rel_def wo_rel.underS_ofilter)
blanchet@55023
   809
  hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast
blanchet@55023
   810
  hence "Field ?p < Field r" using underS_Field2 1 by fast
blanchet@48975
   811
  moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast
blanchet@48975
   812
  ultimately
blanchet@48975
   813
  show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast
blanchet@48975
   814
next
blanchet@48975
   815
  assume "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r"
blanchet@48975
   816
  thus "r' <o r" using ordIso_ordLess_trans by blast
blanchet@48975
   817
qed
blanchet@48975
   818
blanchet@48975
   819
blanchet@48975
   820
lemma internalize_ordLeq:
blanchet@48975
   821
"(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)"
blanchet@48975
   822
proof
blanchet@48975
   823
  assume *: "r' \<le>o r"
blanchet@48975
   824
  moreover
blanchet@48975
   825
  {assume "r' <o r"
blanchet@48975
   826
   then obtain p where "Field p < Field r \<and> r' =o p \<and> p <o r"
blanchet@48975
   827
   using internalize_ordLess[of r' r] by blast
blanchet@48975
   828
   hence "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
blanchet@48975
   829
   using ordLeq_iff_ordLess_or_ordIso by blast
blanchet@48975
   830
  }
blanchet@48975
   831
  moreover
blanchet@48975
   832
  have "r \<le>o r" using * ordLeq_def ordLeq_reflexive by blast
blanchet@48975
   833
  ultimately show "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
blanchet@48975
   834
  using ordLeq_iff_ordLess_or_ordIso by blast
blanchet@48975
   835
next
blanchet@48975
   836
  assume "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
blanchet@48975
   837
  thus "r' \<le>o r" using ordIso_ordLeq_trans by blast
blanchet@48975
   838
qed
blanchet@48975
   839
blanchet@48975
   840
blanchet@48975
   841
lemma ordLeq_iff_ordLess_Restr:
blanchet@48975
   842
assumes WELL: "Well_order r" and WELL': "Well_order r'"
blanchet@55023
   843
shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"
blanchet@48975
   844
proof(auto)
blanchet@48975
   845
  assume *: "r \<le>o r'"
blanchet@48975
   846
  fix a assume "a \<in> Field r"
blanchet@55023
   847
  hence "Restr r (underS r a) <o r"
blanchet@48975
   848
  using WELL underS_Restr_ordLess[of r] by blast
blanchet@55023
   849
  thus "Restr r (underS r a) <o r'"
blanchet@48975
   850
  using * ordLess_ordLeq_trans by blast
blanchet@48975
   851
next
blanchet@55023
   852
  assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'"
blanchet@48975
   853
  {assume "r' <o r"
blanchet@55023
   854
   then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"
blanchet@48975
   855
   using assms ordLess_iff_ordIso_Restr by blast
blanchet@48975
   856
   hence False using * not_ordLess_ordIso ordIso_symmetric by blast
blanchet@48975
   857
  }
blanchet@48975
   858
  thus "r \<le>o r'" using ordLess_or_ordLeq assms by blast
blanchet@48975
   859
qed
blanchet@48975
   860
blanchet@48975
   861
blanchet@48975
   862
lemma finite_ordLess_infinite:
blanchet@48975
   863
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
traytel@54578
   864
        FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
blanchet@48975
   865
shows "r <o r'"
blanchet@48975
   866
proof-
blanchet@48975
   867
  {assume "r' \<le>o r"
blanchet@48975
   868
   then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
blanchet@48975
   869
   unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
traytel@51764
   870
   hence False using finite_imageD finite_subset FIN INF by metis
blanchet@48975
   871
  }
blanchet@48975
   872
  thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
blanchet@48975
   873
qed
blanchet@48975
   874
blanchet@48975
   875
blanchet@48975
   876
lemma finite_well_order_on_ordIso:
blanchet@48975
   877
assumes FIN: "finite A" and
blanchet@48975
   878
        WELL: "well_order_on A r" and WELL': "well_order_on A r'"
blanchet@48975
   879
shows "r =o r'"
blanchet@48975
   880
proof-
blanchet@48975
   881
  have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
blanchet@55023
   882
  using assms well_order_on_Well_order by blast
blanchet@48975
   883
  moreover
blanchet@48975
   884
  have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r'
blanchet@48975
   885
                  \<longrightarrow> r =o r'"
blanchet@48975
   886
  proof(clarify)
blanchet@48975
   887
    fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'"
blanchet@48975
   888
    have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
blanchet@55023
   889
    using * ** well_order_on_Well_order by blast
blanchet@48975
   890
    assume "r \<le>o r'"
blanchet@48975
   891
    then obtain f where 1: "embed r r' f" and
blanchet@48975
   892
                        "inj_on f A \<and> f ` A \<le> A"
blanchet@48975
   893
    unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast
blanchet@48975
   894
    hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast
blanchet@48975
   895
    thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto
blanchet@48975
   896
  qed
blanchet@54482
   897
  ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis
blanchet@48975
   898
qed
blanchet@48975
   899
blanchet@48975
   900
blanchet@48975
   901
subsection{* @{text "<o"} is well-founded *}
blanchet@48975
   902
blanchet@48975
   903
blanchet@48975
   904
text {* Of course, it only makes sense to state that the @{text "<o"} is well-founded
blanchet@48975
   905
on the restricted type @{text "'a rel rel"}.  We prove this by first showing that, for any set
blanchet@48975
   906
of well-orders all embedded in a fixed well-order, the function mapping each well-order
blanchet@48975
   907
in the set to an order filter of the fixed well-order is compatible w.r.t. to @{text "<o"} versus
blanchet@48975
   908
{\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded. *}
blanchet@48975
   909
blanchet@48975
   910
blanchet@48975
   911
definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set"
blanchet@48975
   912
where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f) ` (Field r)"
blanchet@48975
   913
blanchet@48975
   914
blanchet@48975
   915
lemma ord_to_filter_compat:
blanchet@48975
   916
"compat (ordLess Int (ordLess^-1``{r0} \<times> ordLess^-1``{r0}))
blanchet@48975
   917
        (ofilterIncl r0)
blanchet@48975
   918
        (ord_to_filter r0)"
blanchet@48975
   919
proof(unfold compat_def ord_to_filter_def, clarify)
blanchet@48975
   920
  fix r1::"'a rel" and r2::"'a rel"
blanchet@48975
   921
  let ?A1 = "Field r1"  let ?A2 ="Field r2" let ?A0 ="Field r0"
blanchet@48975
   922
  let ?phi10 = "\<lambda> f10. embed r1 r0 f10" let ?f10 = "SOME f. ?phi10 f"
blanchet@48975
   923
  let ?phi20 = "\<lambda> f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f"
blanchet@48975
   924
  assume *: "r1 <o r0" "r2 <o r0" and **: "r1 <o r2"
blanchet@48975
   925
  hence "(\<exists>f. ?phi10 f) \<and> (\<exists>f. ?phi20 f)"
blanchet@48975
   926
  by (auto simp add: ordLess_def embedS_def)
blanchet@48975
   927
  hence "?phi10 ?f10 \<and> ?phi20 ?f20" by (auto simp add: someI_ex)
blanchet@48975
   928
  thus "(?f10 ` ?A1, ?f20 ` ?A2) \<in> ofilterIncl r0"
blanchet@48975
   929
  using * ** by (simp add: embed_ordLess_ofilterIncl)
blanchet@48975
   930
qed
blanchet@48975
   931
blanchet@48975
   932
blanchet@48975
   933
theorem wf_ordLess: "wf ordLess"
blanchet@48975
   934
proof-
blanchet@48975
   935
  {fix r0 :: "('a \<times> 'a) set"
blanchet@48975
   936
   (* need to annotate here!*)
blanchet@48975
   937
   let ?ordLess = "ordLess::('d rel * 'd rel) set"
blanchet@48975
   938
   let ?R = "?ordLess Int (?ordLess^-1``{r0} \<times> ?ordLess^-1``{r0})"
blanchet@48975
   939
   {assume Case1: "Well_order r0"
blanchet@48975
   940
    hence "wf ?R"
blanchet@48975
   941
    using wf_ofilterIncl[of r0]
blanchet@48975
   942
          compat_wf[of ?R "ofilterIncl r0" "ord_to_filter r0"]
blanchet@48975
   943
          ord_to_filter_compat[of r0] by auto
blanchet@48975
   944
   }
blanchet@48975
   945
   moreover
blanchet@48975
   946
   {assume Case2: "\<not> Well_order r0"
blanchet@48975
   947
    hence "?R = {}" unfolding ordLess_def by auto
blanchet@48975
   948
    hence "wf ?R" using wf_empty by simp
blanchet@48975
   949
   }
blanchet@48975
   950
   ultimately have "wf ?R" by blast
blanchet@48975
   951
  }
blanchet@48975
   952
  thus ?thesis by (simp add: trans_wf_iff ordLess_trans)
blanchet@48975
   953
qed
blanchet@48975
   954
blanchet@48975
   955
corollary exists_minim_Well_order:
blanchet@48975
   956
assumes NE: "R \<noteq> {}" and WELL: "\<forall>r \<in> R. Well_order r"
blanchet@48975
   957
shows "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
blanchet@48975
   958
proof-
blanchet@48975
   959
  obtain r where "r \<in> R \<and> (\<forall>r' \<in> R. \<not> r' <o r)"
blanchet@48975
   960
  using NE spec[OF spec[OF subst[OF wf_eq_minimal, of "%x. x", OF wf_ordLess]], of _ R]
blanchet@48975
   961
    equals0I[of R] by blast
blanchet@48975
   962
  with not_ordLeq_iff_ordLess WELL show ?thesis by blast
blanchet@48975
   963
qed
blanchet@48975
   964
blanchet@48975
   965
blanchet@48975
   966
blanchet@48975
   967
subsection {* Copy via direct images  *}
blanchet@48975
   968
blanchet@48975
   969
blanchet@48975
   970
text{* The direct image operator is the dual of the inverse image operator @{text "inv_image"}
blanchet@48975
   971
from @{text "Relation.thy"}.  It is useful for transporting a well-order between
blanchet@48975
   972
different types. *}
blanchet@48975
   973
blanchet@48975
   974
blanchet@48975
   975
definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel"
blanchet@48975
   976
where
blanchet@48975
   977
"dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
blanchet@48975
   978
blanchet@48975
   979
blanchet@48975
   980
lemma dir_image_Field:
blanchet@48975
   981
"Field(dir_image r f) \<le> f ` (Field r)"
blanchet@48975
   982
unfolding dir_image_def Field_def by auto
blanchet@48975
   983
blanchet@48975
   984
blanchet@48975
   985
lemma dir_image_minus_Id:
blanchet@48975
   986
"inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
blanchet@48975
   987
unfolding inj_on_def Field_def dir_image_def by auto
blanchet@48975
   988
blanchet@48975
   989
blanchet@48975
   990
lemma Refl_dir_image:
blanchet@48975
   991
assumes "Refl r"
blanchet@48975
   992
shows "Refl(dir_image r f)"
blanchet@48975
   993
proof-
blanchet@48975
   994
  {fix a' b'
blanchet@48975
   995
   assume "(a',b') \<in> dir_image r f"
blanchet@48975
   996
   then obtain a b where 1: "a' = f a \<and> b' = f b \<and> (a,b) \<in> r"
blanchet@48975
   997
   unfolding dir_image_def by blast
blanchet@48975
   998
   hence "a \<in> Field r \<and> b \<in> Field r" using Field_def by fastforce
blanchet@48975
   999
   hence "(a,a) \<in> r \<and> (b,b) \<in> r" using assms by (simp add: refl_on_def)
blanchet@48975
  1000
   with 1 have "(a',a') \<in> dir_image r f \<and> (b',b') \<in> dir_image r f"
blanchet@48975
  1001
   unfolding dir_image_def by auto
blanchet@48975
  1002
  }
blanchet@48975
  1003
  thus ?thesis
blanchet@48975
  1004
  by(unfold refl_on_def Field_def Domain_def Range_def, auto)
blanchet@48975
  1005
qed
blanchet@48975
  1006
blanchet@48975
  1007
blanchet@48975
  1008
lemma trans_dir_image:
blanchet@48975
  1009
assumes TRANS: "trans r" and INJ: "inj_on f (Field r)"
blanchet@48975
  1010
shows "trans(dir_image r f)"
blanchet@48975
  1011
proof(unfold trans_def, auto)
blanchet@48975
  1012
  fix a' b' c'
blanchet@48975
  1013
  assume "(a',b') \<in> dir_image r f" "(b',c') \<in> dir_image r f"
blanchet@48975
  1014
  then obtain a b1 b2 c where 1: "a' = f a \<and> b' = f b1 \<and> b' = f b2 \<and> c' = f c" and
blanchet@48975
  1015
                         2: "(a,b1) \<in> r \<and> (b2,c) \<in> r"
blanchet@48975
  1016
  unfolding dir_image_def by blast
blanchet@48975
  1017
  hence "b1 \<in> Field r \<and> b2 \<in> Field r"
blanchet@48975
  1018
  unfolding Field_def by auto
blanchet@48975
  1019
  hence "b1 = b2" using 1 INJ unfolding inj_on_def by auto
blanchet@48975
  1020
  hence "(a,c): r" using 2 TRANS unfolding trans_def by blast
blanchet@48975
  1021
  thus "(a',c') \<in> dir_image r f"
blanchet@48975
  1022
  unfolding dir_image_def using 1 by auto
blanchet@48975
  1023
qed
blanchet@48975
  1024
blanchet@48975
  1025
blanchet@48975
  1026
lemma Preorder_dir_image:
blanchet@48975
  1027
"\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)"
blanchet@48975
  1028
by (simp add: preorder_on_def Refl_dir_image trans_dir_image)
blanchet@48975
  1029
blanchet@48975
  1030
blanchet@48975
  1031
lemma antisym_dir_image:
blanchet@48975
  1032
assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
blanchet@48975
  1033
shows "antisym(dir_image r f)"
blanchet@48975
  1034
proof(unfold antisym_def, auto)
blanchet@48975
  1035
  fix a' b'
blanchet@48975
  1036
  assume "(a',b') \<in> dir_image r f" "(b',a') \<in> dir_image r f"
blanchet@48975
  1037
  then obtain a1 b1 a2 b2 where 1: "a' = f a1 \<and> a' = f a2 \<and> b' = f b1 \<and> b' = f b2" and
blanchet@48975
  1038
                           2: "(a1,b1) \<in> r \<and> (b2,a2) \<in> r " and
blanchet@48975
  1039
                           3: "{a1,a2,b1,b2} \<le> Field r"
blanchet@48975
  1040
  unfolding dir_image_def Field_def by blast
blanchet@48975
  1041
  hence "a1 = a2 \<and> b1 = b2" using INJ unfolding inj_on_def by auto
blanchet@48975
  1042
  hence "a1 = b2" using 2 AN unfolding antisym_def by auto
blanchet@48975
  1043
  thus "a' = b'" using 1 by auto
blanchet@48975
  1044
qed
blanchet@48975
  1045
blanchet@48975
  1046
blanchet@48975
  1047
lemma Partial_order_dir_image:
blanchet@48975
  1048
"\<lbrakk>Partial_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Partial_order (dir_image r f)"
blanchet@48975
  1049
by (simp add: partial_order_on_def Preorder_dir_image antisym_dir_image)
blanchet@48975
  1050
blanchet@48975
  1051
blanchet@48975
  1052
lemma Total_dir_image:
blanchet@48975
  1053
assumes TOT: "Total r" and INJ: "inj_on f (Field r)"
blanchet@48975
  1054
shows "Total(dir_image r f)"
blanchet@48975
  1055
proof(unfold total_on_def, intro ballI impI)
blanchet@48975
  1056
  fix a' b'
blanchet@48975
  1057
  assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)"
blanchet@48975
  1058
  then obtain a and b where 1: "a \<in> Field r \<and> b \<in> Field r \<and> f a = a' \<and> f b = b'"
blanchet@48975
  1059
  using dir_image_Field[of r f] by blast
blanchet@48975
  1060
  moreover assume "a' \<noteq> b'"
blanchet@48975
  1061
  ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto
blanchet@48975
  1062
  hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto
blanchet@48975
  1063
  thus "(a',b') \<in> dir_image r f \<or> (b',a') \<in> dir_image r f"
blanchet@48975
  1064
  using 1 unfolding dir_image_def by auto
blanchet@48975
  1065
qed
blanchet@48975
  1066
blanchet@48975
  1067
blanchet@48975
  1068
lemma Linear_order_dir_image:
blanchet@48975
  1069
"\<lbrakk>Linear_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Linear_order (dir_image r f)"
blanchet@48975
  1070
by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image)
blanchet@48975
  1071
blanchet@48975
  1072
blanchet@48975
  1073
lemma wf_dir_image:
blanchet@48975
  1074
assumes WF: "wf r" and INJ: "inj_on f (Field r)"
blanchet@48975
  1075
shows "wf(dir_image r f)"
blanchet@48975
  1076
proof(unfold wf_eq_minimal2, intro allI impI, elim conjE)
blanchet@48975
  1077
  fix A'::"'b set"
blanchet@48975
  1078
  assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}"
blanchet@48975
  1079
  obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast
blanchet@48975
  1080
  have "A \<noteq> {} \<and> A \<le> Field r"
blanchet@48975
  1081
  using A_def dir_image_Field[of r f] SUB NE by blast
blanchet@48975
  1082
  then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
traytel@51764
  1083
  using WF unfolding wf_eq_minimal2 by metis
blanchet@48975
  1084
  have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
blanchet@48975
  1085
  proof(clarify)
blanchet@48975
  1086
    fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
blanchet@48975
  1087
    obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and
blanchet@48975
  1088
                       3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r"
blanchet@48975
  1089
    using ** unfolding dir_image_def Field_def by blast
blanchet@48975
  1090
    hence "a = a1" using 1 A_def INJ unfolding inj_on_def by auto
blanchet@48975
  1091
    hence "b1 \<in> A \<and> (b1,a) \<in> r" using 2 3 A_def * by auto
blanchet@48975
  1092
    with 1 show False by auto
blanchet@48975
  1093
  qed
blanchet@48975
  1094
  thus "\<exists>a'\<in>A'. \<forall>b'\<in>A'. (b', a') \<notin> dir_image r f"
blanchet@48975
  1095
  using A_def 1 by blast
blanchet@48975
  1096
qed
blanchet@48975
  1097
blanchet@48975
  1098
blanchet@48975
  1099
lemma Well_order_dir_image:
blanchet@48975
  1100
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
blanchet@48975
  1101
using assms unfolding well_order_on_def
blanchet@48975
  1102
using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
blanchet@48975
  1103
  dir_image_minus_Id[of f r]
blanchet@48975
  1104
  subset_inj_on[of f "Field r" "Field(r - Id)"]
blanchet@48975
  1105
  mono_Field[of "r - Id" r] by auto
blanchet@48975
  1106
blanchet@48975
  1107
blanchet@48975
  1108
lemma dir_image_Field2:
blanchet@48975
  1109
"Refl r \<Longrightarrow> Field(dir_image r f) = f ` (Field r)"
blanchet@48975
  1110
unfolding Field_def dir_image_def refl_on_def Domain_def Range_def by blast
blanchet@48975
  1111
blanchet@48975
  1112
blanchet@48975
  1113
lemma dir_image_bij_betw:
blanchet@48975
  1114
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
blanchet@48975
  1115
unfolding bij_betw_def
blanchet@48975
  1116
by (simp add: dir_image_Field2 order_on_defs)
blanchet@48975
  1117
blanchet@48975
  1118
blanchet@48975
  1119
lemma dir_image_compat:
blanchet@48975
  1120
"compat r (dir_image r f) f"
blanchet@48975
  1121
unfolding compat_def dir_image_def by auto
blanchet@48975
  1122
blanchet@48975
  1123
blanchet@48975
  1124
lemma dir_image_iso:
blanchet@48975
  1125
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> iso r (dir_image r f) f"
blanchet@48975
  1126
using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast
blanchet@48975
  1127
blanchet@48975
  1128
blanchet@48975
  1129
lemma dir_image_ordIso:
blanchet@48975
  1130
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> r =o dir_image r f"
blanchet@48975
  1131
unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast
blanchet@48975
  1132
blanchet@48975
  1133
blanchet@48975
  1134
lemma Well_order_iso_copy:
blanchet@48975
  1135
assumes WELL: "well_order_on A r" and BIJ: "bij_betw f A A'"
blanchet@48975
  1136
shows "\<exists>r'. well_order_on A' r' \<and> r =o r'"
blanchet@48975
  1137
proof-
blanchet@48975
  1138
   let ?r' = "dir_image r f"
blanchet@48975
  1139
   have 1: "A = Field r \<and> Well_order r"
blanchet@55023
  1140
   using WELL well_order_on_Well_order by blast
blanchet@48975
  1141
   hence 2: "iso r ?r' f"
blanchet@48975
  1142
   using dir_image_iso using BIJ unfolding bij_betw_def by auto
blanchet@48975
  1143
   hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast
blanchet@48975
  1144
   hence "Field ?r' = A'"
blanchet@48975
  1145
   using 1 BIJ unfolding bij_betw_def by auto
blanchet@48975
  1146
   moreover have "Well_order ?r'"
blanchet@48975
  1147
   using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast
blanchet@48975
  1148
   ultimately show ?thesis unfolding ordIso_def using 1 2 by blast
blanchet@48975
  1149
qed
blanchet@48975
  1150
blanchet@48975
  1151
blanchet@48975
  1152
blanchet@48975
  1153
subsection {* Bounded square  *}
blanchet@48975
  1154
blanchet@48975
  1155
blanchet@48975
  1156
text{* This construction essentially defines, for an order relation @{text "r"}, a lexicographic
blanchet@48975
  1157
order @{text "bsqr r"} on @{text "(Field r) \<times> (Field r)"}, applying the
blanchet@48975
  1158
following criteria (in this order):
blanchet@48975
  1159
\begin{itemize}
blanchet@48975
  1160
\item compare the maximums;
blanchet@48975
  1161
\item compare the first components;
blanchet@48975
  1162
\item compare the second components.
blanchet@48975
  1163
\end{itemize}
blanchet@48975
  1164
%
blanchet@48975
  1165
The only application of this construction that we are aware of is
blanchet@48975
  1166
at proving that the square of an infinite set has the same cardinal
blanchet@48975
  1167
as that set. The essential property required there (and which is ensured by this
blanchet@48975
  1168
construction) is that any proper order filter of the product order is included in a rectangle, i.e.,
blanchet@48975
  1169
in a product of proper filters on the original relation (assumed to be a well-order). *}
blanchet@48975
  1170
blanchet@48975
  1171
blanchet@48975
  1172
definition bsqr :: "'a rel => ('a * 'a)rel"
blanchet@48975
  1173
where
blanchet@48975
  1174
"bsqr r = {((a1,a2),(b1,b2)).
blanchet@48975
  1175
           {a1,a2,b1,b2} \<le> Field r \<and>
blanchet@48975
  1176
           (a1 = b1 \<and> a2 = b2 \<or>
blanchet@48975
  1177
            (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
blanchet@48975
  1178
            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
blanchet@48975
  1179
            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1  \<and> (a2,b2) \<in> r - Id
blanchet@48975
  1180
           )}"
blanchet@48975
  1181
blanchet@48975
  1182
blanchet@48975
  1183
lemma Field_bsqr:
blanchet@48975
  1184
"Field (bsqr r) = Field r \<times> Field r"
blanchet@48975
  1185
proof
blanchet@48975
  1186
  show "Field (bsqr r) \<le> Field r \<times> Field r"
blanchet@48975
  1187
  proof-
blanchet@48975
  1188
    {fix a1 a2 assume "(a1,a2) \<in> Field (bsqr r)"
blanchet@48975
  1189
     moreover
blanchet@48975
  1190
     have "\<And> b1 b2. ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r \<Longrightarrow>
blanchet@48975
  1191
                      a1 \<in> Field r \<and> a2 \<in> Field r" unfolding bsqr_def by auto
blanchet@48975
  1192
     ultimately have "a1 \<in> Field r \<and> a2 \<in> Field r" unfolding Field_def by auto
blanchet@48975
  1193
    }
blanchet@48975
  1194
    thus ?thesis unfolding Field_def by force
blanchet@48975
  1195
  qed
blanchet@48975
  1196
next
blanchet@48975
  1197
  show "Field r \<times> Field r \<le> Field (bsqr r)"
blanchet@48975
  1198
  proof(auto)
blanchet@48975
  1199
    fix a1 a2 assume "a1 \<in> Field r" and "a2 \<in> Field r"
blanchet@48975
  1200
    hence "((a1,a2),(a1,a2)) \<in> bsqr r" unfolding bsqr_def by blast
blanchet@48975
  1201
    thus "(a1,a2) \<in> Field (bsqr r)" unfolding Field_def by auto
blanchet@48975
  1202
  qed
blanchet@48975
  1203
qed
blanchet@48975
  1204
blanchet@48975
  1205
blanchet@48975
  1206
lemma bsqr_Refl: "Refl(bsqr r)"
blanchet@48975
  1207
by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
blanchet@48975
  1208
blanchet@48975
  1209
blanchet@48975
  1210
lemma bsqr_Trans:
blanchet@48975
  1211
assumes "Well_order r"
blanchet@48975
  1212
shows "trans (bsqr r)"
blanchet@48975
  1213
proof(unfold trans_def, auto)
blanchet@48975
  1214
  (* Preliminary facts *)
blanchet@48975
  1215
  have Well: "wo_rel r" using assms wo_rel_def by auto
blanchet@48975
  1216
  hence Trans: "trans r" using wo_rel.TRANS by auto
blanchet@48975
  1217
  have Anti: "antisym r" using wo_rel.ANTISYM Well by auto
blanchet@48975
  1218
  hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)
blanchet@48975
  1219
  (* Main proof *)
blanchet@48975
  1220
  fix a1 a2 b1 b2 c1 c2
blanchet@48975
  1221
  assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(c1,c2)) \<in> bsqr r"
blanchet@48975
  1222
  hence 0: "{a1,a2,b1,b2,c1,c2} \<le> Field r" unfolding bsqr_def by auto
blanchet@48975
  1223
  have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
blanchet@48975
  1224
           wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
blanchet@48975
  1225
           wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
blanchet@48975
  1226
  using * unfolding bsqr_def by auto
blanchet@48975
  1227
  have 2: "b1 = c1 \<and> b2 = c2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id \<or>
blanchet@48975
  1228
           wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id \<or>
blanchet@48975
  1229
           wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
blanchet@48975
  1230
  using ** unfolding bsqr_def by auto
blanchet@48975
  1231
  show "((a1,a2),(c1,c2)) \<in> bsqr r"
blanchet@48975
  1232
  proof-
blanchet@48975
  1233
    {assume Case1: "a1 = b1 \<and> a2 = b2"
blanchet@48975
  1234
     hence ?thesis using ** by simp
blanchet@48975
  1235
    }
blanchet@48975
  1236
    moreover
blanchet@48975
  1237
    {assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"
blanchet@48975
  1238
     {assume Case21: "b1 = c1 \<and> b2 = c2"
blanchet@48975
  1239
      hence ?thesis using * by simp
blanchet@48975
  1240
     }
blanchet@48975
  1241
     moreover
blanchet@48975
  1242
     {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
blanchet@48975
  1243
      hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \<in> r - Id"
blanchet@48975
  1244
      using Case2 TransS trans_def[of "r - Id"] by blast
blanchet@48975
  1245
      hence ?thesis using 0 unfolding bsqr_def by auto
blanchet@48975
  1246
     }
blanchet@48975
  1247
     moreover
blanchet@48975
  1248
     {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2"
blanchet@48975
  1249
      hence ?thesis using Case2 0 unfolding bsqr_def by auto
blanchet@48975
  1250
     }
blanchet@48975
  1251
     ultimately have ?thesis using 0 2 by auto
blanchet@48975
  1252
    }
blanchet@48975
  1253
    moreover
blanchet@48975
  1254
    {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"
blanchet@48975
  1255
     {assume Case31: "b1 = c1 \<and> b2 = c2"
blanchet@48975
  1256
      hence ?thesis using * by simp
blanchet@48975
  1257
     }
blanchet@48975
  1258
     moreover
blanchet@48975
  1259
     {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
blanchet@48975
  1260
      hence ?thesis using Case3 0 unfolding bsqr_def by auto
blanchet@48975
  1261
     }
blanchet@48975
  1262
     moreover
blanchet@48975
  1263
     {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
blanchet@48975
  1264
      hence "(a1,c1) \<in> r - Id"
blanchet@48975
  1265
      using Case3 TransS trans_def[of "r - Id"] by blast
blanchet@48975
  1266
      hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto
blanchet@48975
  1267
     }
blanchet@48975
  1268
     moreover
blanchet@48975
  1269
     {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1"
blanchet@48975
  1270
      hence ?thesis using Case3 0 unfolding bsqr_def by auto
blanchet@48975
  1271
     }
blanchet@48975
  1272
     ultimately have ?thesis using 0 2 by auto
blanchet@48975
  1273
    }
blanchet@48975
  1274
    moreover
blanchet@48975
  1275
    {assume Case4: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
blanchet@48975
  1276
     {assume Case41: "b1 = c1 \<and> b2 = c2"
blanchet@48975
  1277
      hence ?thesis using * by simp
blanchet@48975
  1278
     }
blanchet@48975
  1279
     moreover
blanchet@48975
  1280
     {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
traytel@51764
  1281
      hence ?thesis using Case4 0 unfolding bsqr_def by force
blanchet@48975
  1282
     }
blanchet@48975
  1283
     moreover
blanchet@48975
  1284
     {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
blanchet@48975
  1285
      hence ?thesis using Case4 0 unfolding bsqr_def by auto
blanchet@48975
  1286
     }
blanchet@48975
  1287
     moreover
blanchet@48975
  1288
     {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
blanchet@48975
  1289
      hence "(a2,c2) \<in> r - Id"
blanchet@48975
  1290
      using Case4 TransS trans_def[of "r - Id"] by blast
blanchet@48975
  1291
      hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto
blanchet@48975
  1292
     }
blanchet@48975
  1293
     ultimately have ?thesis using 0 2 by auto
blanchet@48975
  1294
    }
blanchet@48975
  1295
    ultimately show ?thesis using 0 1 by auto
blanchet@48975
  1296
  qed
blanchet@48975
  1297
qed
blanchet@48975
  1298
blanchet@48975
  1299
blanchet@48975
  1300
lemma bsqr_antisym:
blanchet@48975
  1301
assumes "Well_order r"
blanchet@48975
  1302
shows "antisym (bsqr r)"
blanchet@48975
  1303
proof(unfold antisym_def, clarify)
blanchet@48975
  1304
  (* Preliminary facts *)
blanchet@48975
  1305
  have Well: "wo_rel r" using assms wo_rel_def by auto
blanchet@48975
  1306
  hence Trans: "trans r" using wo_rel.TRANS by auto
blanchet@48975
  1307
  have Anti: "antisym r" using wo_rel.ANTISYM Well by auto
blanchet@48975
  1308
  hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)
blanchet@48975
  1309
  hence IrrS: "\<forall>a b. \<not>((a,b) \<in> r - Id \<and> (b,a) \<in> r - Id)"
blanchet@48975
  1310
  using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast
blanchet@48975
  1311
  (* Main proof *)
blanchet@48975
  1312
  fix a1 a2 b1 b2
blanchet@48975
  1313
  assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(a1,a2)) \<in> bsqr r"
blanchet@48975
  1314
  hence 0: "{a1,a2,b1,b2} \<le> Field r" unfolding bsqr_def by auto
blanchet@48975
  1315
  have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
blanchet@48975
  1316
           wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
blanchet@48975
  1317
           wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
blanchet@48975
  1318
  using * unfolding bsqr_def by auto
blanchet@48975
  1319
  have 2: "b1 = a1 \<and> b2 = a2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id \<or>
blanchet@48975
  1320
           wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> (b1,a1) \<in> r - Id \<or>
blanchet@48975
  1321
           wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> b1 = a1 \<and> (b2,a2) \<in> r - Id"
blanchet@48975
  1322
  using ** unfolding bsqr_def by auto
blanchet@48975
  1323
  show "a1 = b1 \<and> a2 = b2"
blanchet@48975
  1324
  proof-
blanchet@48975
  1325
    {assume Case1: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"
blanchet@48975
  1326
     {assume Case11: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
blanchet@48975
  1327
      hence False using Case1 IrrS by blast
blanchet@48975
  1328
     }
blanchet@48975
  1329
     moreover
blanchet@48975
  1330
     {assume Case12_3: "wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2"
blanchet@48975
  1331
      hence False using Case1 by auto
blanchet@48975
  1332
     }
blanchet@48975
  1333
     ultimately have ?thesis using 0 2 by auto
blanchet@48975
  1334
    }
blanchet@48975
  1335
    moreover
blanchet@48975
  1336
    {assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"
blanchet@48975
  1337
     {assume Case21: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
blanchet@48975
  1338
       hence False using Case2 by auto
blanchet@48975
  1339
     }
blanchet@48975
  1340
     moreover
blanchet@48975
  1341
     {assume Case22: "(b1,a1) \<in> r - Id"
blanchet@48975
  1342
      hence False using Case2 IrrS by blast
blanchet@48975
  1343
     }
blanchet@48975
  1344
     moreover
blanchet@48975
  1345
     {assume Case23: "b1 = a1"
blanchet@48975
  1346
      hence False using Case2 by auto
blanchet@48975
  1347
     }
blanchet@48975
  1348
     ultimately have ?thesis using 0 2 by auto
blanchet@48975
  1349
    }
blanchet@48975
  1350
    moreover
blanchet@48975
  1351
    {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
blanchet@48975
  1352
     moreover
blanchet@48975
  1353
     {assume Case31: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
blanchet@48975
  1354
      hence False using Case3 by auto
blanchet@48975
  1355
     }
blanchet@48975
  1356
     moreover
blanchet@48975
  1357
     {assume Case32: "(b1,a1) \<in> r - Id"
blanchet@48975
  1358
      hence False using Case3 by auto
blanchet@48975
  1359
     }
blanchet@48975
  1360
     moreover
blanchet@48975
  1361
     {assume Case33: "(b2,a2) \<in> r - Id"
blanchet@48975
  1362
      hence False using Case3 IrrS by blast
blanchet@48975
  1363
     }
blanchet@48975
  1364
     ultimately have ?thesis using 0 2 by auto
blanchet@48975
  1365
    }
blanchet@48975
  1366
    ultimately show ?thesis using 0 1 by blast
blanchet@48975
  1367
  qed
blanchet@48975
  1368
qed
blanchet@48975
  1369
blanchet@48975
  1370
blanchet@48975
  1371
lemma bsqr_Total:
blanchet@48975
  1372
assumes "Well_order r"
blanchet@48975
  1373
shows "Total(bsqr r)"
blanchet@48975
  1374
proof-
blanchet@48975
  1375
  (* Preliminary facts *)
blanchet@48975
  1376
  have Well: "wo_rel r" using assms wo_rel_def by auto
blanchet@48975
  1377
  hence Total: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
blanchet@48975
  1378
  using wo_rel.TOTALS by auto
blanchet@48975
  1379
  (* Main proof *)
blanchet@48975
  1380
  {fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} \<le> Field(bsqr r)"
blanchet@48975
  1381
   hence 0: "a1 \<in> Field r \<and> a2 \<in> Field r \<and> b1 \<in> Field r \<and> b2 \<in> Field r"
blanchet@48975
  1382
   using Field_bsqr by blast
blanchet@48975
  1383
   have "((a1,a2) = (b1,b2) \<or> ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r)"
blanchet@48975
  1384
   proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1385
       (* Why didn't clarsimp simp add: Well 0 do the same job? *)
blanchet@48975
  1386
     assume Case1: "(a1,a2) \<in> r"
blanchet@48975
  1387
     hence 1: "wo_rel.max2 r a1 a2 = a2"
blanchet@48975
  1388
     using Well 0 by (simp add: wo_rel.max2_equals2)
blanchet@48975
  1389
     show ?thesis
blanchet@48975
  1390
     proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1391
       assume Case11: "(b1,b2) \<in> r"
blanchet@48975
  1392
       hence 2: "wo_rel.max2 r b1 b2 = b2"
blanchet@48975
  1393
       using Well 0 by (simp add: wo_rel.max2_equals2)
blanchet@48975
  1394
       show ?thesis
blanchet@48975
  1395
       proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1396
         assume Case111: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
blanchet@48975
  1397
         thus ?thesis using 0 1 2 unfolding bsqr_def by auto
blanchet@48975
  1398
       next
blanchet@48975
  1399
         assume Case112: "a2 = b2"
blanchet@48975
  1400
         show ?thesis
blanchet@48975
  1401
         proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1402
           assume Case1121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
blanchet@48975
  1403
           thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto
blanchet@48975
  1404
         next
blanchet@48975
  1405
           assume Case1122: "a1 = b1"
blanchet@48975
  1406
           thus ?thesis using Case112 by auto
blanchet@48975
  1407
         qed
blanchet@48975
  1408
       qed
blanchet@48975
  1409
     next
blanchet@48975
  1410
       assume Case12: "(b2,b1) \<in> r"
blanchet@48975
  1411
       hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1)
blanchet@48975
  1412
       show ?thesis
blanchet@48975
  1413
       proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1414
         assume Case121: "(a2,b1) \<in> r - Id \<or> (b1,a2) \<in> r - Id"
blanchet@48975
  1415
         thus ?thesis using 0 1 3 unfolding bsqr_def by auto
blanchet@48975
  1416
       next
blanchet@48975
  1417
         assume Case122: "a2 = b1"
blanchet@48975
  1418
         show ?thesis
blanchet@48975
  1419
         proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1420
           assume Case1221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
blanchet@48975
  1421
           thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto
blanchet@48975
  1422
         next
blanchet@48975
  1423
           assume Case1222: "a1 = b1"
blanchet@48975
  1424
           show ?thesis
blanchet@48975
  1425
           proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1426
             assume Case12221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
blanchet@48975
  1427
             thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto
blanchet@48975
  1428
           next
blanchet@48975
  1429
             assume Case12222: "a2 = b2"
blanchet@48975
  1430
             thus ?thesis using Case122 Case1222 by auto
blanchet@48975
  1431
           qed
blanchet@48975
  1432
         qed
blanchet@48975
  1433
       qed
blanchet@48975
  1434
     qed
blanchet@48975
  1435
   next
blanchet@48975
  1436
     assume Case2: "(a2,a1) \<in> r"
blanchet@48975
  1437
     hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1)
blanchet@48975
  1438
     show ?thesis
blanchet@48975
  1439
     proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1440
       assume Case21: "(b1,b2) \<in> r"
blanchet@48975
  1441
       hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2)
blanchet@48975
  1442
       show ?thesis
blanchet@48975
  1443
       proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1444
         assume Case211: "(a1,b2) \<in> r - Id \<or> (b2,a1) \<in> r - Id"
blanchet@48975
  1445
         thus ?thesis using 0 1 2 unfolding bsqr_def by auto
blanchet@48975
  1446
       next
blanchet@48975
  1447
         assume Case212: "a1 = b2"
blanchet@48975
  1448
         show ?thesis
blanchet@48975
  1449
         proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1450
           assume Case2121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
blanchet@48975
  1451
           thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto
blanchet@48975
  1452
         next
blanchet@48975
  1453
           assume Case2122: "a1 = b1"
blanchet@48975
  1454
           show ?thesis
blanchet@48975
  1455
           proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1456
             assume Case21221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
blanchet@48975
  1457
             thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto
blanchet@48975
  1458
           next
blanchet@48975
  1459
             assume Case21222: "a2 = b2"
blanchet@48975
  1460
             thus ?thesis using Case2122 Case212 by auto
blanchet@48975
  1461
           qed
blanchet@48975
  1462
         qed
blanchet@48975
  1463
       qed
blanchet@48975
  1464
     next
blanchet@48975
  1465
       assume Case22: "(b2,b1) \<in> r"
blanchet@48975
  1466
       hence 3: "wo_rel.max2 r b1 b2 = b1"  using Well 0 by (simp add: wo_rel.max2_equals1)
blanchet@48975
  1467
       show ?thesis
blanchet@48975
  1468
       proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1469
         assume Case221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
blanchet@48975
  1470
         thus ?thesis using 0 1 3 unfolding bsqr_def by auto
blanchet@48975
  1471
       next
blanchet@48975
  1472
         assume Case222: "a1 = b1"
blanchet@48975
  1473
         show ?thesis
blanchet@48975
  1474
         proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
blanchet@48975
  1475
           assume Case2221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
blanchet@48975
  1476
           thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto
blanchet@48975
  1477
         next
blanchet@48975
  1478
           assume Case2222: "a2 = b2"
blanchet@48975
  1479
           thus ?thesis using Case222 by auto
blanchet@48975
  1480
         qed
blanchet@48975
  1481
       qed
blanchet@48975
  1482
     qed
blanchet@48975
  1483
   qed
blanchet@48975
  1484
  }
blanchet@48975
  1485
  thus ?thesis unfolding total_on_def by fast
blanchet@48975
  1486
qed
blanchet@48975
  1487
blanchet@48975
  1488
blanchet@48975
  1489
lemma bsqr_Linear_order:
blanchet@48975
  1490
assumes "Well_order r"
blanchet@48975
  1491
shows "Linear_order(bsqr r)"
blanchet@48975
  1492
unfolding order_on_defs
blanchet@48975
  1493
using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast
blanchet@48975
  1494
blanchet@48975
  1495
blanchet@48975
  1496
lemma bsqr_Well_order:
blanchet@48975
  1497
assumes "Well_order r"
blanchet@48975
  1498
shows "Well_order(bsqr r)"
blanchet@48975
  1499
using assms
blanchet@48975
  1500
proof(simp add: bsqr_Linear_order Linear_order_Well_order_iff, intro allI impI)
blanchet@48975
  1501
  have 0: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
blanchet@48975
  1502
  using assms well_order_on_def Linear_order_Well_order_iff by blast
blanchet@48975
  1503
  fix D assume *: "D \<le> Field (bsqr r)" and **: "D \<noteq> {}"
blanchet@48975
  1504
  hence 1: "D \<le> Field r \<times> Field r" unfolding Field_bsqr by simp
blanchet@48975
  1505
  (*  *)
blanchet@48975
  1506
  obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) \<in> D}" by blast
blanchet@48975
  1507
  have "M \<noteq> {}" using 1 M_def ** by auto
blanchet@48975
  1508
  moreover
blanchet@48975
  1509
  have "M \<le> Field r" unfolding M_def
blanchet@48975
  1510
  using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
blanchet@48975
  1511
  ultimately obtain m where m_min: "m \<in> M \<and> (\<forall>a \<in> M. (m,a) \<in> r)"
blanchet@48975
  1512
  using 0 by blast
blanchet@48975
  1513
  (*  *)
blanchet@48975
  1514
  obtain A1 where A1_def: "A1 = {a1. \<exists>a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast
blanchet@48975
  1515
  have "A1 \<le> Field r" unfolding A1_def using 1 by auto
blanchet@48975
  1516
  moreover have "A1 \<noteq> {}" unfolding A1_def using m_min unfolding M_def by blast
blanchet@48975
  1517
  ultimately obtain a1 where a1_min: "a1 \<in> A1 \<and> (\<forall>a \<in> A1. (a1,a) \<in> r)"
blanchet@48975
  1518
  using 0 by blast
blanchet@48975
  1519
  (*  *)
blanchet@48975
  1520
  obtain A2 where A2_def: "A2 = {a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast
blanchet@48975
  1521
  have "A2 \<le> Field r" unfolding A2_def using 1 by auto
blanchet@48975
  1522
  moreover have "A2 \<noteq> {}" unfolding A2_def
blanchet@48975
  1523
  using m_min a1_min unfolding A1_def M_def by blast
blanchet@48975
  1524
  ultimately obtain a2 where a2_min: "a2 \<in> A2 \<and> (\<forall>a \<in> A2. (a2,a) \<in> r)"
blanchet@48975
  1525
  using 0 by blast
blanchet@48975
  1526
  (*   *)
blanchet@48975
  1527
  have 2: "wo_rel.max2 r a1 a2 = m"
blanchet@48975
  1528
  using a1_min a2_min unfolding A1_def A2_def by auto
blanchet@48975
  1529
  have 3: "(a1,a2) \<in> D" using a2_min unfolding A2_def by auto
blanchet@48975
  1530
  (*  *)
blanchet@48975
  1531
  moreover
blanchet@48975
  1532
  {fix b1 b2 assume ***: "(b1,b2) \<in> D"
blanchet@48975
  1533
   hence 4: "{a1,a2,b1,b2} \<le> Field r" using 1 3 by blast
blanchet@48975
  1534
   have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
blanchet@48975
  1535
   using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto
blanchet@48975
  1536
   have "((a1,a2),(b1,b2)) \<in> bsqr r"
blanchet@48975
  1537
   proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2")
blanchet@48975
  1538
     assume Case1: "wo_rel.max2 r a1 a2 \<noteq> wo_rel.max2 r b1 b2"
blanchet@48975
  1539
     thus ?thesis unfolding bsqr_def using 4 5 by auto
blanchet@48975
  1540
   next
blanchet@48975
  1541
     assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"
blanchet@48975
  1542
     hence "b1 \<in> A1" unfolding A1_def using 2 *** by auto
blanchet@48975
  1543
     hence 6: "(a1,b1) \<in> r" using a1_min by auto
blanchet@48975
  1544
     show ?thesis
blanchet@48975
  1545
     proof(cases "a1 = b1")
blanchet@48975
  1546
       assume Case21: "a1 \<noteq> b1"
blanchet@48975
  1547
       thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto
blanchet@48975
  1548
     next
blanchet@48975
  1549
       assume Case22: "a1 = b1"
blanchet@48975
  1550
       hence "b2 \<in> A2" unfolding A2_def using 2 *** Case2 by auto
blanchet@48975
  1551
       hence 7: "(a2,b2) \<in> r" using a2_min by auto
blanchet@48975
  1552
       thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto
blanchet@48975
  1553
     qed
blanchet@48975
  1554
   qed
blanchet@48975
  1555
  }
blanchet@48975
  1556
  (*  *)
blanchet@48975
  1557
  ultimately show "\<exists>d \<in> D. \<forall>d' \<in> D. (d,d') \<in> bsqr r" by fastforce
blanchet@48975
  1558
qed
blanchet@48975
  1559
blanchet@48975
  1560
blanchet@48975
  1561
lemma bsqr_max2:
blanchet@48975
  1562
assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \<in> bsqr r"
blanchet@48975
  1563
shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
blanchet@48975
  1564
proof-
blanchet@48975
  1565
  have "{(a1,a2),(b1,b2)} \<le> Field(bsqr r)"
blanchet@48975
  1566
  using LEQ unfolding Field_def by auto
blanchet@48975
  1567
  hence "{a1,a2,b1,b2} \<le> Field r" unfolding Field_bsqr by auto
blanchet@48975
  1568
  hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} \<le> Field r"
blanchet@48975
  1569
  using WELL wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
blanchet@48975
  1570
  moreover have "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r \<or> wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"
blanchet@48975
  1571
  using LEQ unfolding bsqr_def by auto
blanchet@48975
  1572
  ultimately show ?thesis using WELL unfolding order_on_defs refl_on_def by auto
blanchet@48975
  1573
qed
blanchet@48975
  1574
blanchet@48975
  1575
blanchet@48975
  1576
lemma bsqr_ofilter:
blanchet@48975
  1577
assumes WELL: "Well_order r" and
blanchet@48975
  1578
        OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and
blanchet@55023
  1579
        NE: "\<not> (\<exists>a. Field r = under r a)"
blanchet@48975
  1580
shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"
blanchet@48975
  1581
proof-
blanchet@48975
  1582
  let ?r' = "bsqr r"
blanchet@48975
  1583
  have Well: "wo_rel r" using WELL wo_rel_def by blast
blanchet@48975
  1584
  hence Trans: "trans r" using wo_rel.TRANS by blast
blanchet@48975
  1585
  have Well': "Well_order ?r' \<and> wo_rel ?r'"
blanchet@48975
  1586
  using WELL bsqr_Well_order wo_rel_def by blast
blanchet@48975
  1587
  (*  *)
blanchet@48975
  1588
  have "D < Field ?r'" unfolding Field_bsqr using SUB .
blanchet@48975
  1589
  with OF obtain a1 and a2 where
blanchet@55023
  1590
  "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"
blanchet@48975
  1591
  using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto
blanchet@48975
  1592
  hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto
blanchet@48975
  1593
  let ?m = "wo_rel.max2 r a1 a2"
blanchet@55023
  1594
  have "D \<le> (under r ?m) \<times> (under r ?m)"
blanchet@48975
  1595
  proof(unfold 1)
blanchet@48975
  1596
    {fix b1 b2
blanchet@48975
  1597
     let ?n = "wo_rel.max2 r b1 b2"
blanchet@55023
  1598
     assume "(b1,b2) \<in> underS ?r' (a1,a2)"
blanchet@48975
  1599
     hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"
blanchet@55023
  1600
     unfolding underS_def by blast
blanchet@48975
  1601
     hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)
blanchet@48975
  1602
     moreover
blanchet@48975
  1603
     {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto
blanchet@48975
  1604
      hence "{b1,b2} \<le> Field r" unfolding Field_bsqr by auto
blanchet@48975
  1605
      hence "(b1,?n) \<in> r \<and> (b2,?n) \<in> r"
blanchet@48975
  1606
      using Well by (simp add: wo_rel.max2_greater)
blanchet@48975
  1607
     }
blanchet@48975
  1608
     ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"
blanchet@48975
  1609
     using Trans trans_def[of r] by blast
blanchet@55023
  1610
     hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}
blanchet@55023
  1611
     thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto
blanchet@48975
  1612
  qed
blanchet@55023
  1613
  moreover have "wo_rel.ofilter r (under r ?m)"
blanchet@48975
  1614
  using Well by (simp add: wo_rel.under_ofilter)
blanchet@55023
  1615
  moreover have "under r ?m < Field r"
blanchet@55023
  1616
  using NE under_Field[of r ?m] by blast
blanchet@48975
  1617
  ultimately show ?thesis by blast
blanchet@48975
  1618
qed
blanchet@48975
  1619
traytel@54980
  1620
definition Func where
traytel@54980
  1621
"Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
traytel@54980
  1622
traytel@54980
  1623
lemma Func_empty:
traytel@54980
  1624
"Func {} B = {\<lambda>x. undefined}"
traytel@54980
  1625
unfolding Func_def by auto
traytel@54980
  1626
traytel@54980
  1627
lemma Func_elim:
traytel@54980
  1628
assumes "g \<in> Func A B" and "a \<in> A"
traytel@54980
  1629
shows "\<exists> b. b \<in> B \<and> g a = b"
traytel@54980
  1630
using assms unfolding Func_def by (cases "g a = undefined") auto
traytel@54980
  1631
traytel@54980
  1632
definition curr where
traytel@54980
  1633
"curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
traytel@54980
  1634
traytel@54980
  1635
lemma curr_in:
traytel@54980
  1636
assumes f: "f \<in> Func (A <*> B) C"
traytel@54980
  1637
shows "curr A f \<in> Func A (Func B C)"
traytel@54980
  1638
using assms unfolding curr_def Func_def by auto
traytel@54980
  1639
traytel@54980
  1640
lemma curr_inj:
traytel@54980
  1641
assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"
traytel@54980
  1642
shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
traytel@54980
  1643
proof safe
traytel@54980
  1644
  assume c: "curr A f1 = curr A f2"
traytel@54980
  1645
  show "f1 = f2"
traytel@54980
  1646
  proof (rule ext, clarify)
traytel@54980
  1647
    fix a b show "f1 (a, b) = f2 (a, b)"
traytel@54980
  1648
    proof (cases "(a,b) \<in> A <*> B")
traytel@54980
  1649
      case False
traytel@54980
  1650
      thus ?thesis using assms unfolding Func_def by auto
traytel@54980
  1651
    next
traytel@54980
  1652
      case True hence a: "a \<in> A" and b: "b \<in> B" by auto
traytel@54980
  1653
      thus ?thesis
traytel@54980
  1654
      using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp
traytel@54980
  1655
    qed
traytel@54980
  1656
  qed
traytel@54980
  1657
qed
traytel@54980
  1658
traytel@54980
  1659
lemma curr_surj:
traytel@54980
  1660
assumes "g \<in> Func A (Func B C)"
traytel@54980
  1661
shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
traytel@54980
  1662
proof
traytel@54980
  1663
  let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
traytel@54980
  1664
  show "curr A ?f = g"
traytel@54980
  1665
  proof (rule ext)
traytel@54980
  1666
    fix a show "curr A ?f a = g a"
traytel@54980
  1667
    proof (cases "a \<in> A")
traytel@54980
  1668
      case False
traytel@54980
  1669
      hence "g a = undefined" using assms unfolding Func_def by auto
traytel@54980
  1670
      thus ?thesis unfolding curr_def using False by simp
traytel@54980
  1671
    next
traytel@54980
  1672
      case True
traytel@54980
  1673
      obtain g1 where "g1 \<in> Func B C" and "g a = g1"
traytel@54980
  1674
      using assms using Func_elim[OF assms True] by blast
traytel@54980
  1675
      thus ?thesis using True unfolding Func_def curr_def by auto
traytel@54980
  1676
    qed
traytel@54980
  1677
  qed
traytel@54980
  1678
  show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto
traytel@54980
  1679
qed
traytel@54980
  1680
traytel@54980
  1681
lemma bij_betw_curr:
traytel@54980
  1682
"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
traytel@54980
  1683
unfolding bij_betw_def inj_on_def image_def
traytel@54980
  1684
apply (intro impI conjI ballI)
traytel@54980
  1685
apply (erule curr_inj[THEN iffD1], assumption+)
traytel@54980
  1686
apply auto
traytel@54980
  1687
apply (erule curr_in)
traytel@54980
  1688
using curr_surj by blast
traytel@54980
  1689
traytel@54980
  1690
definition Func_map where
traytel@54980
  1691
"Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
traytel@54980
  1692
traytel@54980
  1693
lemma Func_map:
traytel@54980
  1694
assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
traytel@54980
  1695
shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
traytel@54980
  1696
using assms unfolding Func_def Func_map_def mem_Collect_eq by auto
traytel@54980
  1697
traytel@54980
  1698
lemma Func_non_emp:
traytel@54980
  1699
assumes "B \<noteq> {}"
traytel@54980
  1700
shows "Func A B \<noteq> {}"
traytel@54980
  1701
proof-
traytel@54980
  1702
  obtain b where b: "b \<in> B" using assms by auto
traytel@54980
  1703
  hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto
traytel@54980
  1704
  thus ?thesis by blast
traytel@54980
  1705
qed
traytel@54980
  1706
traytel@54980
  1707
lemma Func_is_emp:
traytel@54980
  1708
"Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")
traytel@54980
  1709
proof
traytel@54980
  1710
  assume L: ?L
traytel@54980
  1711
  moreover {assume "A = {}" hence False using L Func_empty by auto}
traytel@54980
  1712
  moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis}
traytel@54980
  1713
  ultimately show ?R by blast
traytel@54980
  1714
next
traytel@54980
  1715
  assume R: ?R
traytel@54980
  1716
  moreover
traytel@54980
  1717
  {fix f assume "f \<in> Func A B"
traytel@54980
  1718
   moreover obtain a where "a \<in> A" using R by blast
traytel@54980
  1719
   ultimately obtain b where "b \<in> B" unfolding Func_def by blast
traytel@54980
  1720
   with R have False by blast
traytel@54980
  1721
  }
traytel@54980
  1722
  thus ?L by blast
traytel@54980
  1723
qed
traytel@54980
  1724
traytel@54980
  1725
lemma Func_map_surj:
traytel@54980
  1726
assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2"
traytel@54980
  1727
and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"
traytel@54980
  1728
shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1"
traytel@54980
  1729
proof(cases "B2 = {}")
traytel@54980
  1730
  case True
traytel@54980
  1731
  thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def)
traytel@54980
  1732
next
traytel@54980
  1733
  case False note B2 = False
traytel@54980
  1734
  show ?thesis
traytel@54980
  1735
  proof safe
traytel@54980
  1736
    fix h assume h: "h \<in> Func B2 B1"
traytel@54980
  1737
    def j1 \<equiv> "inv_into A1 f1"
traytel@54980
  1738
    have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
traytel@54980
  1739
    then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis
traytel@54980
  1740
    {fix b2 assume b2: "b2 \<in> B2"
traytel@54980
  1741
     hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
traytel@54980
  1742
     moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
traytel@54980
  1743
     ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
traytel@54980
  1744
    } note kk = this
traytel@54980
  1745
    obtain b22 where b22: "b22 \<in> B2" using B2 by auto
traytel@54980
  1746
    def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22"
traytel@54980
  1747
    have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
traytel@54980
  1748
    have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
traytel@54980
  1749
    using kk unfolding j2_def by auto
traytel@54980
  1750
    def g \<equiv> "Func_map A2 j1 j2 h"
traytel@54980
  1751
    have "Func_map B2 f1 f2 g = h"
traytel@54980
  1752
    proof (rule ext)
traytel@54980
  1753
      fix b2 show "Func_map B2 f1 f2 g b2 = h b2"
traytel@54980
  1754
      proof(cases "b2 \<in> B2")
traytel@54980
  1755
        case True
traytel@54980
  1756
        show ?thesis
traytel@54980
  1757
        proof (cases "h b2 = undefined")
traytel@54980
  1758
          case True
traytel@54980
  1759
          hence b1: "h b2 \<in> f1 ` A1" using h `b2 \<in> B2` unfolding B1 Func_def by auto
traytel@54980
  1760
          show ?thesis using A2 f_inv_into_f[OF b1]
traytel@54980
  1761
            unfolding True g_def Func_map_def j1_def j2[OF `b2 \<in> B2`] by auto
traytel@54980
  1762
        qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def,
traytel@54980
  1763
          auto intro: f_inv_into_f)
traytel@54980
  1764
      qed(insert h, unfold Func_def Func_map_def, auto)
traytel@54980
  1765
    qed
traytel@54980
  1766
    moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
traytel@54980
  1767
    using inv_into_into j2A2 B1 A2 inv_into_into
traytel@54980
  1768
    unfolding j1_def image_def by fast+
traytel@54980
  1769
    ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
traytel@54980
  1770
    unfolding Func_map_def[abs_def] unfolding image_def by auto
traytel@54980
  1771
  qed(insert B1 Func_map[OF _ _ A2(2)], auto)
traytel@54980
  1772
qed
blanchet@48975
  1773
blanchet@48975
  1774
end