src/HOL/Cardinals/Wellorder_Relation_FP.thy
author blanchet
Fri Jan 17 10:02:50 2014 +0100 (2014-01-17)
changeset 55027 a74ea6d75571
parent 55026 258fa7b5a621
permissions -rw-r--r--
folded 'Wellfounded_More_FP' into 'Wellfounded'
blanchet@54481
     1
(*  Title:      HOL/Cardinals/Wellorder_Relation_FP.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@54481
     5
Well-order relations (FP).
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@54481
     8
header {* Well-Order Relations (FP) *}
blanchet@48975
     9
blanchet@54481
    10
theory Wellorder_Relation_FP
blanchet@55027
    11
imports Order_Relation
blanchet@48975
    12
begin
blanchet@48975
    13
blanchet@48975
    14
blanchet@48975
    15
text{* In this section, we develop basic concepts and results pertaining
blanchet@48975
    16
to well-order relations.  Note that we consider well-order relations
blanchet@48975
    17
as {\em non-strict relations},
blanchet@48975
    18
i.e., as containing the diagonals of their fields. *}
blanchet@48975
    19
blanchet@48975
    20
blanchet@55023
    21
locale wo_rel =
blanchet@55023
    22
  fixes r :: "'a rel"
blanchet@55023
    23
  assumes WELL: "Well_order r"
blanchet@48975
    24
begin
blanchet@48975
    25
blanchet@48975
    26
text{* The following context encompasses all this section. In other words,
blanchet@48975
    27
for the whole section, we consider a fixed well-order relation @{term "r"}. *}
blanchet@48975
    28
blanchet@48975
    29
(* context wo_rel  *)
blanchet@48975
    30
blanchet@55026
    31
abbreviation under where "under \<equiv> Order_Relation.under r"
blanchet@55026
    32
abbreviation underS where "underS \<equiv> Order_Relation.underS r"
blanchet@55026
    33
abbreviation Under where "Under \<equiv> Order_Relation.Under r"
blanchet@55026
    34
abbreviation UnderS where "UnderS \<equiv> Order_Relation.UnderS r"
blanchet@55026
    35
abbreviation above where "above \<equiv> Order_Relation.above r"
blanchet@55026
    36
abbreviation aboveS where "aboveS \<equiv> Order_Relation.aboveS r"
blanchet@55026
    37
abbreviation Above where "Above \<equiv> Order_Relation.Above r"
blanchet@55026
    38
abbreviation AboveS where "AboveS \<equiv> Order_Relation.AboveS r"
blanchet@55023
    39
blanchet@48975
    40
blanchet@48975
    41
subsection {* Auxiliaries *}
blanchet@48975
    42
blanchet@48975
    43
blanchet@48975
    44
lemma REFL: "Refl r"
blanchet@48975
    45
using WELL order_on_defs[of _ r] by auto
blanchet@48975
    46
blanchet@48975
    47
blanchet@48975
    48
lemma TRANS: "trans r"
blanchet@48975
    49
using WELL order_on_defs[of _ r] by auto
blanchet@48975
    50
blanchet@48975
    51
blanchet@48975
    52
lemma ANTISYM: "antisym r"
blanchet@48975
    53
using WELL order_on_defs[of _ r] by auto
blanchet@48975
    54
blanchet@48975
    55
blanchet@48975
    56
lemma TOTAL: "Total r"
blanchet@48975
    57
using WELL order_on_defs[of _ r] by auto
blanchet@48975
    58
blanchet@48975
    59
blanchet@48975
    60
lemma TOTALS: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
blanchet@48975
    61
using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force
blanchet@48975
    62
blanchet@48975
    63
blanchet@48975
    64
lemma LIN: "Linear_order r"
blanchet@48975
    65
using WELL well_order_on_def[of _ r] by auto
blanchet@48975
    66
blanchet@48975
    67
blanchet@48975
    68
lemma WF: "wf (r - Id)"
blanchet@48975
    69
using WELL well_order_on_def[of _ r] by auto
blanchet@48975
    70
blanchet@48975
    71
blanchet@48975
    72
lemma cases_Total:
blanchet@48975
    73
"\<And> phi a b. \<lbrakk>{a,b} <= Field r; ((a,b) \<in> r \<Longrightarrow> phi a b); ((b,a) \<in> r \<Longrightarrow> phi a b)\<rbrakk>
blanchet@48975
    74
             \<Longrightarrow> phi a b"
blanchet@48975
    75
using TOTALS by auto
blanchet@48975
    76
blanchet@48975
    77
blanchet@48975
    78
lemma cases_Total3:
blanchet@48975
    79
"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<or> (b,a) \<in> r - Id \<Longrightarrow> phi a b);
blanchet@48975
    80
              (a = b \<Longrightarrow> phi a b)\<rbrakk>  \<Longrightarrow> phi a b"
blanchet@48975
    81
using TOTALS by auto
blanchet@48975
    82
blanchet@48975
    83
blanchet@48975
    84
subsection {* Well-founded induction and recursion adapted to non-strict well-order relations  *}
blanchet@48975
    85
blanchet@48975
    86
blanchet@48975
    87
text{* Here we provide induction and recursion principles specific to {\em non-strict}
blanchet@48975
    88
well-order relations.
blanchet@48975
    89
Although minor variations of those for well-founded relations, they will be useful
blanchet@48975
    90
for doing away with the tediousness of
blanchet@48975
    91
having to take out the diagonal each time in order to switch to a well-founded relation. *}
blanchet@48975
    92
blanchet@48975
    93
blanchet@48975
    94
lemma well_order_induct:
blanchet@48975
    95
assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
blanchet@48975
    96
shows "P a"
blanchet@48975
    97
proof-
blanchet@48975
    98
  have "\<And>x. \<forall>y. (y, x) \<in> r - Id \<longrightarrow> P y \<Longrightarrow> P x"
blanchet@48975
    99
  using IND by blast
blanchet@48975
   100
  thus "P a" using WF wf_induct[of "r - Id" P a] by blast
blanchet@48975
   101
qed
blanchet@48975
   102
blanchet@48975
   103
blanchet@48975
   104
definition
blanchet@48975
   105
worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
blanchet@48975
   106
where
blanchet@48975
   107
"worec F \<equiv> wfrec (r - Id) F"
blanchet@48975
   108
blanchet@48975
   109
blanchet@48975
   110
definition
blanchet@48975
   111
adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
blanchet@48975
   112
where
blanchet@48975
   113
"adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x"
blanchet@48975
   114
blanchet@48975
   115
blanchet@48975
   116
lemma worec_fixpoint:
blanchet@48975
   117
assumes ADM: "adm_wo H"
blanchet@48975
   118
shows "worec H = H (worec H)"
blanchet@48975
   119
proof-
blanchet@48975
   120
  let ?rS = "r - Id"
blanchet@48975
   121
  have "adm_wf (r - Id) H"
blanchet@48975
   122
  unfolding adm_wf_def
blanchet@55023
   123
  using ADM adm_wo_def[of H] underS_def[of r] by auto
blanchet@48975
   124
  hence "wfrec ?rS H = H (wfrec ?rS H)"
blanchet@48975
   125
  using WF wfrec_fixpoint[of ?rS H] by simp
blanchet@48975
   126
  thus ?thesis unfolding worec_def .
blanchet@48975
   127
qed
blanchet@48975
   128
blanchet@48975
   129
blanchet@48975
   130
subsection {* The notions of maximum, minimum, supremum, successor and order filter  *}
blanchet@48975
   131
blanchet@48975
   132
blanchet@48975
   133
text{*
blanchet@48975
   134
We define the successor {\em of a set}, and not of an element (the latter is of course
blanchet@48975
   135
a particular case).  Also, we define the maximum {\em of two elements}, @{text "max2"},
blanchet@48975
   136
and the minimum {\em of a set}, @{text "minim"} -- we chose these variants since we
blanchet@48975
   137
consider them the most useful for well-orders.  The minimum is defined in terms of the
blanchet@48975
   138
auxiliary relational operator @{text "isMinim"}.  Then, supremum and successor are
blanchet@48975
   139
defined in terms of minimum as expected.
blanchet@48975
   140
The minimum is only meaningful for non-empty sets, and the successor is only
blanchet@48975
   141
meaningful for sets for which strict upper bounds exist.
blanchet@48975
   142
Order filters for well-orders are also known as ``initial segments". *}
blanchet@48975
   143
blanchet@48975
   144
blanchet@48975
   145
definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
blanchet@48975
   146
where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
blanchet@48975
   147
blanchet@48975
   148
blanchet@48975
   149
definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
blanchet@48975
   150
where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
blanchet@48975
   151
blanchet@48975
   152
definition minim :: "'a set \<Rightarrow> 'a"
blanchet@48975
   153
where "minim A \<equiv> THE b. isMinim A b"
blanchet@48975
   154
blanchet@48975
   155
blanchet@48975
   156
definition supr :: "'a set \<Rightarrow> 'a"
blanchet@48975
   157
where "supr A \<equiv> minim (Above A)"
blanchet@48975
   158
blanchet@48975
   159
definition suc :: "'a set \<Rightarrow> 'a"
blanchet@48975
   160
where "suc A \<equiv> minim (AboveS A)"
blanchet@48975
   161
blanchet@48975
   162
definition ofilter :: "'a set \<Rightarrow> bool"
blanchet@48975
   163
where
blanchet@48975
   164
"ofilter A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under a \<le> A)"
blanchet@48975
   165
blanchet@48975
   166
blanchet@48975
   167
subsubsection {* Properties of max2 *}
blanchet@48975
   168
blanchet@48975
   169
blanchet@48975
   170
lemma max2_greater_among:
blanchet@48975
   171
assumes "a \<in> Field r" and "b \<in> Field r"
blanchet@48975
   172
shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
blanchet@48975
   173
proof-
blanchet@48975
   174
  {assume "(a,b) \<in> r"
blanchet@48975
   175
   hence ?thesis using max2_def assms REFL refl_on_def
blanchet@48975
   176
   by (auto simp add: refl_on_def)
blanchet@48975
   177
  }
blanchet@48975
   178
  moreover
blanchet@48975
   179
  {assume "a = b"
blanchet@48975
   180
   hence "(a,b) \<in> r" using REFL  assms
blanchet@48975
   181
   by (auto simp add: refl_on_def)
blanchet@48975
   182
  }
blanchet@48975
   183
  moreover
blanchet@48975
   184
  {assume *: "a \<noteq> b \<and> (b,a) \<in> r"
blanchet@48975
   185
   hence "(a,b) \<notin> r" using ANTISYM
blanchet@48975
   186
   by (auto simp add: antisym_def)
blanchet@48975
   187
   hence ?thesis using * max2_def assms REFL refl_on_def
blanchet@48975
   188
   by (auto simp add: refl_on_def)
blanchet@48975
   189
  }
blanchet@48975
   190
  ultimately show ?thesis using assms TOTAL
blanchet@48975
   191
  total_on_def[of "Field r" r] by blast
blanchet@48975
   192
qed
blanchet@48975
   193
blanchet@48975
   194
blanchet@48975
   195
lemma max2_greater:
blanchet@48975
   196
assumes "a \<in> Field r" and "b \<in> Field r"
blanchet@48975
   197
shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
blanchet@48975
   198
using assms by (auto simp add: max2_greater_among)
blanchet@48975
   199
blanchet@48975
   200
blanchet@48975
   201
lemma max2_among:
blanchet@48975
   202
assumes "a \<in> Field r" and "b \<in> Field r"
blanchet@48975
   203
shows "max2 a b \<in> {a, b}"
blanchet@48975
   204
using assms max2_greater_among[of a b] by simp
blanchet@48975
   205
blanchet@48975
   206
blanchet@48975
   207
lemma max2_equals1:
blanchet@48975
   208
assumes "a \<in> Field r" and "b \<in> Field r"
blanchet@48975
   209
shows "(max2 a b = a) = ((b,a) \<in> r)"
blanchet@48975
   210
using assms ANTISYM unfolding antisym_def using TOTALS
blanchet@48975
   211
by(auto simp add: max2_def max2_among)
blanchet@48975
   212
blanchet@48975
   213
blanchet@48975
   214
lemma max2_equals2:
blanchet@48975
   215
assumes "a \<in> Field r" and "b \<in> Field r"
blanchet@48975
   216
shows "(max2 a b = b) = ((a,b) \<in> r)"
blanchet@48975
   217
using assms ANTISYM unfolding antisym_def using TOTALS
blanchet@48975
   218
unfolding max2_def by auto
blanchet@48975
   219
blanchet@48975
   220
blanchet@48975
   221
subsubsection {* Existence and uniqueness for isMinim and well-definedness of minim *}
blanchet@48975
   222
blanchet@48975
   223
blanchet@48975
   224
lemma isMinim_unique:
blanchet@48975
   225
assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
blanchet@48975
   226
shows "a = a'"
blanchet@48975
   227
proof-
blanchet@48975
   228
  {have "a \<in> B"
blanchet@48975
   229
   using MINIM isMinim_def by simp
blanchet@48975
   230
   hence "(a',a) \<in> r"
blanchet@48975
   231
   using MINIM' isMinim_def by simp
blanchet@48975
   232
  }
blanchet@48975
   233
  moreover
blanchet@48975
   234
  {have "a' \<in> B"
blanchet@48975
   235
   using MINIM' isMinim_def by simp
blanchet@48975
   236
   hence "(a,a') \<in> r"
blanchet@48975
   237
   using MINIM isMinim_def by simp
blanchet@48975
   238
  }
blanchet@48975
   239
  ultimately
blanchet@48975
   240
  show ?thesis using ANTISYM antisym_def[of r] by blast
blanchet@48975
   241
qed
blanchet@48975
   242
blanchet@48975
   243
blanchet@48975
   244
lemma Well_order_isMinim_exists:
blanchet@48975
   245
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
blanchet@48975
   246
shows "\<exists>b. isMinim B b"
blanchet@48975
   247
proof-
traytel@51764
   248
  from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
traytel@51764
   249
  *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
blanchet@48975
   250
  show ?thesis
blanchet@48975
   251
  proof(simp add: isMinim_def, rule exI[of _ b], auto)
blanchet@48975
   252
    show "b \<in> B" using * by simp
blanchet@48975
   253
  next
blanchet@48975
   254
    fix b' assume As: "b' \<in> B"
blanchet@48975
   255
    hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto
blanchet@48975
   256
    (*  *)
blanchet@48975
   257
    from As  * have "b' = b \<or> (b',b) \<notin> r" by auto
blanchet@48975
   258
    moreover
blanchet@48975
   259
    {assume "b' = b"
blanchet@48975
   260
     hence "(b,b') \<in> r"
blanchet@48975
   261
     using ** REFL by (auto simp add: refl_on_def)
blanchet@48975
   262
    }
blanchet@48975
   263
    moreover
blanchet@48975
   264
    {assume "b' \<noteq> b \<and> (b',b) \<notin> r"
blanchet@48975
   265
     hence "(b,b') \<in> r"
blanchet@48975
   266
     using ** TOTAL by (auto simp add: total_on_def)
blanchet@48975
   267
    }
blanchet@48975
   268
    ultimately show "(b,b') \<in> r" by blast
blanchet@48975
   269
  qed
blanchet@48975
   270
qed
blanchet@48975
   271
blanchet@48975
   272
blanchet@48975
   273
lemma minim_isMinim:
blanchet@48975
   274
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
blanchet@48975
   275
shows "isMinim B (minim B)"
blanchet@48975
   276
proof-
blanchet@48975
   277
  let ?phi = "(\<lambda> b. isMinim B b)"
blanchet@48975
   278
  from assms Well_order_isMinim_exists
blanchet@48975
   279
  obtain b where *: "?phi b" by blast
blanchet@48975
   280
  moreover
blanchet@48975
   281
  have "\<And> b'. ?phi b' \<Longrightarrow> b' = b"
blanchet@48975
   282
  using isMinim_unique * by auto
blanchet@48975
   283
  ultimately show ?thesis
blanchet@48975
   284
  unfolding minim_def using theI[of ?phi b] by blast
blanchet@48975
   285
qed
blanchet@48975
   286
blanchet@48975
   287
blanchet@48975
   288
subsubsection{* Properties of minim *}
blanchet@48975
   289
blanchet@48975
   290
blanchet@48975
   291
lemma minim_in:
blanchet@48975
   292
assumes "B \<le> Field r" and "B \<noteq> {}"
blanchet@48975
   293
shows "minim B \<in> B"
blanchet@48975
   294
proof-
blanchet@48975
   295
  from minim_isMinim[of B] assms
blanchet@48975
   296
  have "isMinim B (minim B)" by simp
blanchet@48975
   297
  thus ?thesis by (simp add: isMinim_def)
blanchet@48975
   298
qed
blanchet@48975
   299
blanchet@48975
   300
blanchet@48975
   301
lemma minim_inField:
blanchet@48975
   302
assumes "B \<le> Field r" and "B \<noteq> {}"
blanchet@48975
   303
shows "minim B \<in> Field r"
blanchet@48975
   304
proof-
blanchet@48975
   305
  have "minim B \<in> B" using assms by (simp add: minim_in)
blanchet@48975
   306
  thus ?thesis using assms by blast
blanchet@48975
   307
qed
blanchet@48975
   308
blanchet@48975
   309
blanchet@48975
   310
lemma minim_least:
blanchet@48975
   311
assumes  SUB: "B \<le> Field r" and IN: "b \<in> B"
blanchet@48975
   312
shows "(minim B, b) \<in> r"
blanchet@48975
   313
proof-
blanchet@48975
   314
  from minim_isMinim[of B] assms
blanchet@48975
   315
  have "isMinim B (minim B)" by auto
blanchet@48975
   316
  thus ?thesis by (auto simp add: isMinim_def IN)
blanchet@48975
   317
qed
blanchet@48975
   318
blanchet@48975
   319
blanchet@48975
   320
lemma equals_minim:
blanchet@48975
   321
assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
blanchet@48975
   322
        LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
blanchet@48975
   323
shows "a = minim B"
blanchet@48975
   324
proof-
blanchet@48975
   325
  from minim_isMinim[of B] assms
blanchet@48975
   326
  have "isMinim B (minim B)" by auto
blanchet@48975
   327
  moreover have "isMinim B a" using IN LEAST isMinim_def by auto
blanchet@48975
   328
  ultimately show ?thesis
blanchet@48975
   329
  using isMinim_unique by auto
blanchet@48975
   330
qed
blanchet@48975
   331
blanchet@48975
   332
blanchet@48975
   333
subsubsection{* Properties of successor *}
blanchet@48975
   334
blanchet@48975
   335
blanchet@48975
   336
lemma suc_AboveS:
blanchet@48975
   337
assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
blanchet@48975
   338
shows "suc B \<in> AboveS B"
blanchet@48975
   339
proof(unfold suc_def)
blanchet@48975
   340
  have "AboveS B \<le> Field r"
blanchet@55023
   341
  using AboveS_Field[of r] by auto
blanchet@48975
   342
  thus "minim (AboveS B) \<in> AboveS B"
blanchet@48975
   343
  using assms by (simp add: minim_in)
blanchet@48975
   344
qed
blanchet@48975
   345
blanchet@48975
   346
blanchet@48975
   347
lemma suc_greater:
blanchet@48975
   348
assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
blanchet@48975
   349
        IN: "b \<in> B"
blanchet@48975
   350
shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
blanchet@48975
   351
proof-
blanchet@48975
   352
  from assms suc_AboveS
blanchet@48975
   353
  have "suc B \<in> AboveS B" by simp
blanchet@55023
   354
  with IN AboveS_def[of r] show ?thesis by simp
blanchet@48975
   355
qed
blanchet@48975
   356
blanchet@48975
   357
blanchet@48975
   358
lemma suc_least_AboveS:
blanchet@48975
   359
assumes ABOVES: "a \<in> AboveS B"
blanchet@48975
   360
shows "(suc B,a) \<in> r"
blanchet@48975
   361
proof(unfold suc_def)
blanchet@48975
   362
  have "AboveS B \<le> Field r"
blanchet@55023
   363
  using AboveS_Field[of r] by auto
blanchet@48975
   364
  thus "(minim (AboveS B),a) \<in> r"
blanchet@48975
   365
  using assms minim_least by simp
blanchet@48975
   366
qed
blanchet@48975
   367
blanchet@48975
   368
blanchet@48975
   369
lemma suc_inField:
blanchet@48975
   370
assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
blanchet@48975
   371
shows "suc B \<in> Field r"
blanchet@48975
   372
proof-
blanchet@48975
   373
  have "suc B \<in> AboveS B" using suc_AboveS assms by simp
blanchet@48975
   374
  thus ?thesis
blanchet@55023
   375
  using assms AboveS_Field[of r] by auto
blanchet@48975
   376
qed
blanchet@48975
   377
blanchet@48975
   378
blanchet@48975
   379
lemma equals_suc_AboveS:
blanchet@48975
   380
assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
blanchet@48975
   381
        MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
blanchet@48975
   382
shows "a = suc B"
blanchet@48975
   383
proof(unfold suc_def)
blanchet@48975
   384
  have "AboveS B \<le> Field r"
blanchet@55023
   385
  using AboveS_Field[of r B] by auto
blanchet@48975
   386
  thus "a = minim (AboveS B)"
blanchet@48975
   387
  using assms equals_minim
blanchet@48975
   388
  by simp
blanchet@48975
   389
qed
blanchet@48975
   390
blanchet@48975
   391
blanchet@48975
   392
lemma suc_underS:
blanchet@48975
   393
assumes IN: "a \<in> Field r"
blanchet@48975
   394
shows "a = suc (underS a)"
blanchet@48975
   395
proof-
blanchet@48975
   396
  have "underS a \<le> Field r"
blanchet@55023
   397
  using underS_Field[of r] by auto
blanchet@48975
   398
  moreover
blanchet@48975
   399
  have "a \<in> AboveS (underS a)"
blanchet@55023
   400
  using in_AboveS_underS IN by fast
blanchet@48975
   401
  moreover
blanchet@48975
   402
  have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
blanchet@48975
   403
  proof(clarify)
blanchet@48975
   404
    fix a'
blanchet@48975
   405
    assume *: "a' \<in> AboveS (underS a)"
blanchet@48975
   406
    hence **: "a' \<in> Field r"
blanchet@55023
   407
    using AboveS_Field by fast
blanchet@48975
   408
    {assume "(a,a') \<notin> r"
blanchet@48975
   409
     hence "a' = a \<or> (a',a) \<in> r"
blanchet@48975
   410
     using TOTAL IN ** by (auto simp add: total_on_def)
blanchet@48975
   411
     moreover
blanchet@48975
   412
     {assume "a' = a"
blanchet@48975
   413
      hence "(a,a') \<in> r"
blanchet@48975
   414
      using REFL IN ** by (auto simp add: refl_on_def)
blanchet@48975
   415
     }
blanchet@48975
   416
     moreover
blanchet@48975
   417
     {assume "a' \<noteq> a \<and> (a',a) \<in> r"
blanchet@48975
   418
      hence "a' \<in> underS a"
blanchet@48975
   419
      unfolding underS_def by simp
blanchet@48975
   420
      hence "a' \<notin> AboveS (underS a)"
blanchet@55023
   421
      using AboveS_disjoint by fast
blanchet@48975
   422
      with * have False by simp
blanchet@48975
   423
     }
blanchet@48975
   424
     ultimately have "(a,a') \<in> r" by blast
blanchet@48975
   425
    }
blanchet@48975
   426
    thus  "(a, a') \<in> r" by blast
blanchet@48975
   427
  qed
blanchet@48975
   428
  ultimately show ?thesis
blanchet@48975
   429
  using equals_suc_AboveS by auto
blanchet@48975
   430
qed
blanchet@48975
   431
blanchet@48975
   432
blanchet@54477
   433
subsubsection {* Properties of order filters *}
blanchet@48975
   434
blanchet@48975
   435
blanchet@48975
   436
lemma under_ofilter:
blanchet@48975
   437
"ofilter (under a)"
blanchet@48975
   438
proof(unfold ofilter_def under_def, auto simp add: Field_def)
blanchet@48975
   439
  fix aa x
blanchet@48975
   440
  assume "(aa,a) \<in> r" "(x,aa) \<in> r"
blanchet@48975
   441
  thus "(x,a) \<in> r"
blanchet@48975
   442
  using TRANS trans_def[of r] by blast
blanchet@48975
   443
qed
blanchet@48975
   444
blanchet@48975
   445
blanchet@48975
   446
lemma underS_ofilter:
blanchet@48975
   447
"ofilter (underS a)"
blanchet@48975
   448
proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
blanchet@48975
   449
  fix aa assume "(a, aa) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a"
blanchet@48975
   450
  thus False
blanchet@48975
   451
  using ANTISYM antisym_def[of r] by blast
blanchet@48975
   452
next
blanchet@48975
   453
  fix aa x
blanchet@48975
   454
  assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r"
blanchet@48975
   455
  thus "(x,a) \<in> r"
blanchet@48975
   456
  using TRANS trans_def[of r] by blast
blanchet@48975
   457
qed
blanchet@48975
   458
blanchet@48975
   459
blanchet@48975
   460
lemma Field_ofilter:
blanchet@48975
   461
"ofilter (Field r)"
blanchet@48975
   462
by(unfold ofilter_def under_def, auto simp add: Field_def)
blanchet@48975
   463
blanchet@48975
   464
blanchet@48975
   465
lemma ofilter_underS_Field:
blanchet@48975
   466
"ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
blanchet@48975
   467
proof
blanchet@48975
   468
  assume "(\<exists>a\<in>Field r. A = underS a) \<or> A = Field r"
blanchet@48975
   469
  thus "ofilter A"
blanchet@48975
   470
  by (auto simp: underS_ofilter Field_ofilter)
blanchet@48975
   471
next
blanchet@48975
   472
  assume *: "ofilter A"
blanchet@48975
   473
  let ?One = "(\<exists>a\<in>Field r. A = underS a)"
blanchet@48975
   474
  let ?Two = "(A = Field r)"
blanchet@48975
   475
  show "?One \<or> ?Two"
blanchet@48975
   476
  proof(cases ?Two, simp)
blanchet@48975
   477
    let ?B = "(Field r) - A"
blanchet@48975
   478
    let ?a = "minim ?B"
blanchet@48975
   479
    assume "A \<noteq> Field r"
blanchet@48975
   480
    moreover have "A \<le> Field r" using * ofilter_def by simp
blanchet@48975
   481
    ultimately have 1: "?B \<noteq> {}" by blast
blanchet@48975
   482
    hence 2: "?a \<in> Field r" using minim_inField[of ?B] by blast
blanchet@48975
   483
    have 3: "?a \<in> ?B" using minim_in[of ?B] 1 by blast
blanchet@48975
   484
    hence 4: "?a \<notin> A" by blast
blanchet@48975
   485
    have 5: "A \<le> Field r" using * ofilter_def[of A] by auto
blanchet@48975
   486
    (*  *)
blanchet@48975
   487
    moreover
blanchet@48975
   488
    have "A = underS ?a"
blanchet@48975
   489
    proof
blanchet@48975
   490
      show "A \<le> underS ?a"
blanchet@48975
   491
      proof(unfold underS_def, auto simp add: 4)
blanchet@48975
   492
        fix x assume **: "x \<in> A"
blanchet@48975
   493
        hence 11: "x \<in> Field r" using 5 by auto
blanchet@48975
   494
        have 12: "x \<noteq> ?a" using 4 ** by auto
blanchet@48975
   495
        have 13: "under x \<le> A" using * ofilter_def ** by auto
blanchet@48975
   496
        {assume "(x,?a) \<notin> r"
blanchet@48975
   497
         hence "(?a,x) \<in> r"
blanchet@48975
   498
         using TOTAL total_on_def[of "Field r" r]
blanchet@48975
   499
               2 4 11 12 by auto
blanchet@55023
   500
         hence "?a \<in> under x" using under_def[of r] by auto
blanchet@48975
   501
         hence "?a \<in> A" using ** 13 by blast
blanchet@48975
   502
         with 4 have False by simp
blanchet@48975
   503
        }
blanchet@48975
   504
        thus "(x,?a) \<in> r" by blast
blanchet@48975
   505
      qed
blanchet@48975
   506
    next
blanchet@48975
   507
      show "underS ?a \<le> A"
blanchet@48975
   508
      proof(unfold underS_def, auto)
blanchet@48975
   509
        fix x
blanchet@48975
   510
        assume **: "x \<noteq> ?a" and ***: "(x,?a) \<in> r"
blanchet@48975
   511
        hence 11: "x \<in> Field r" using Field_def by fastforce
blanchet@48975
   512
         {assume "x \<notin> A"
blanchet@48975
   513
          hence "x \<in> ?B" using 11 by auto
blanchet@48975
   514
          hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast
blanchet@48975
   515
          hence False
blanchet@48975
   516
          using ANTISYM antisym_def[of r] ** *** by auto
blanchet@48975
   517
         }
blanchet@48975
   518
        thus "x \<in> A" by blast
blanchet@48975
   519
      qed
blanchet@48975
   520
    qed
blanchet@48975
   521
    ultimately have ?One using 2 by blast
blanchet@48975
   522
    thus ?thesis by simp
blanchet@48975
   523
  qed
blanchet@48975
   524
qed
blanchet@48975
   525
blanchet@48975
   526
blanchet@48975
   527
lemma ofilter_UNION:
blanchet@48975
   528
"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
blanchet@48975
   529
unfolding ofilter_def by blast
blanchet@48975
   530
blanchet@48975
   531
blanchet@48975
   532
lemma ofilter_under_UNION:
blanchet@48975
   533
assumes "ofilter A"
blanchet@48975
   534
shows "A = (\<Union> a \<in> A. under a)"
blanchet@48975
   535
proof
blanchet@48975
   536
  have "\<forall>a \<in> A. under a \<le> A"
blanchet@48975
   537
  using assms ofilter_def by auto
blanchet@48975
   538
  thus "(\<Union> a \<in> A. under a) \<le> A" by blast
blanchet@48975
   539
next
blanchet@48975
   540
  have "\<forall>a \<in> A. a \<in> under a"
blanchet@55023
   541
  using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
blanchet@48975
   542
  thus "A \<le> (\<Union> a \<in> A. under a)" by blast
blanchet@48975
   543
qed
blanchet@48975
   544
blanchet@48975
   545
blanchet@48975
   546
subsubsection{* Other properties *}
blanchet@48975
   547
blanchet@48975
   548
blanchet@48975
   549
lemma ofilter_linord:
blanchet@48975
   550
assumes OF1: "ofilter A" and OF2: "ofilter B"
blanchet@48975
   551
shows "A \<le> B \<or> B \<le> A"
blanchet@48975
   552
proof(cases "A = Field r")
blanchet@48975
   553
  assume Case1: "A = Field r"
blanchet@48975
   554
  hence "B \<le> A" using OF2 ofilter_def by auto
blanchet@48975
   555
  thus ?thesis by simp
blanchet@48975
   556
next
blanchet@48975
   557
  assume Case2: "A \<noteq> Field r"
blanchet@48975
   558
  with ofilter_underS_Field OF1 obtain a where
blanchet@48975
   559
  1: "a \<in> Field r \<and> A = underS a" by auto
blanchet@48975
   560
  show ?thesis
blanchet@48975
   561
  proof(cases "B = Field r")
blanchet@48975
   562
    assume Case21: "B = Field r"
blanchet@48975
   563
    hence "A \<le> B" using OF1 ofilter_def by auto
blanchet@48975
   564
    thus ?thesis by simp
blanchet@48975
   565
  next
blanchet@48975
   566
    assume Case22: "B \<noteq> Field r"
blanchet@48975
   567
    with ofilter_underS_Field OF2 obtain b where
blanchet@48975
   568
    2: "b \<in> Field r \<and> B = underS b" by auto
blanchet@48975
   569
    have "a = b \<or> (a,b) \<in> r \<or> (b,a) \<in> r"
blanchet@48975
   570
    using 1 2 TOTAL total_on_def[of _ r] by auto
blanchet@48975
   571
    moreover
blanchet@48975
   572
    {assume "a = b" with 1 2 have ?thesis by auto
blanchet@48975
   573
    }
blanchet@48975
   574
    moreover
blanchet@48975
   575
    {assume "(a,b) \<in> r"
blanchet@55023
   576
     with underS_incr[of r] TRANS ANTISYM 1 2
blanchet@48975
   577
     have "A \<le> B" by auto
blanchet@48975
   578
     hence ?thesis by auto
blanchet@48975
   579
    }
blanchet@48975
   580
    moreover
blanchet@48975
   581
     {assume "(b,a) \<in> r"
blanchet@55023
   582
     with underS_incr[of r] TRANS ANTISYM 1 2
blanchet@48975
   583
     have "B \<le> A" by auto
blanchet@48975
   584
     hence ?thesis by auto
blanchet@48975
   585
    }
blanchet@48975
   586
    ultimately show ?thesis by blast
blanchet@48975
   587
  qed
blanchet@48975
   588
qed
blanchet@48975
   589
blanchet@48975
   590
blanchet@48975
   591
lemma ofilter_AboveS_Field:
blanchet@48975
   592
assumes "ofilter A"
blanchet@48975
   593
shows "A \<union> (AboveS A) = Field r"
blanchet@48975
   594
proof
blanchet@48975
   595
  show "A \<union> (AboveS A) \<le> Field r"
blanchet@55023
   596
  using assms ofilter_def AboveS_Field[of r] by auto
blanchet@48975
   597
next
blanchet@48975
   598
  {fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
blanchet@48975
   599
   {fix y assume ***: "y \<in> A"
blanchet@48975
   600
    with ** have 1: "y \<noteq> x" by auto
blanchet@48975
   601
    {assume "(y,x) \<notin> r"
blanchet@48975
   602
     moreover
blanchet@48975
   603
     have "y \<in> Field r" using assms ofilter_def *** by auto
blanchet@48975
   604
     ultimately have "(x,y) \<in> r"
blanchet@48975
   605
     using 1 * TOTAL total_on_def[of _ r] by auto
blanchet@55023
   606
     with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
blanchet@48975
   607
     with ** have False by contradiction
blanchet@48975
   608
    }
blanchet@48975
   609
    hence "(y,x) \<in> r" by blast
blanchet@48975
   610
    with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
blanchet@48975
   611
   }
blanchet@48975
   612
   with * have "x \<in> AboveS A" unfolding AboveS_def by auto
blanchet@48975
   613
  }
blanchet@48975
   614
  thus "Field r \<le> A \<union> (AboveS A)" by blast
blanchet@48975
   615
qed
blanchet@48975
   616
blanchet@48975
   617
blanchet@48975
   618
lemma suc_ofilter_in:
blanchet@48975
   619
assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
blanchet@48975
   620
        REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
blanchet@48975
   621
shows "b \<in> A"
blanchet@48975
   622
proof-
blanchet@48975
   623
  have *: "suc A \<in> Field r \<and> b \<in> Field r"
blanchet@55023
   624
  using WELL REL well_order_on_domain[of "Field r"] by auto
blanchet@48975
   625
  {assume **: "b \<notin> A"
blanchet@48975
   626
   hence "b \<in> AboveS A"
blanchet@48975
   627
   using OF * ofilter_AboveS_Field by auto
blanchet@48975
   628
   hence "(suc A, b) \<in> r"
blanchet@48975
   629
   using suc_least_AboveS by auto
blanchet@48975
   630
   hence False using REL DIFF ANTISYM *
blanchet@48975
   631
   by (auto simp add: antisym_def)
blanchet@48975
   632
  }
blanchet@48975
   633
  thus ?thesis by blast
blanchet@48975
   634
qed
blanchet@48975
   635
blanchet@48975
   636
blanchet@48975
   637
blanchet@48975
   638
end (* context wo_rel *)
blanchet@48975
   639
blanchet@48975
   640
blanchet@48975
   641
blanchet@48975
   642
end