src/HOL/Cardinals/Wellorder_Relation.thy
author blanchet
Wed Sep 12 05:29:21 2012 +0200 (2012-09-12)
changeset 49310 6e30078de4f0
parent 48979 src/HOL/Ordinals_and_Cardinals/Wellorder_Relation.thy@b62d14275b89
child 51764 67f05cb13e08
permissions -rw-r--r--
renamed "Ordinals_and_Cardinals" to "Cardinals"
blanchet@49310
     1
(*  Title:      HOL/Cardinals/Wellorder_Relation.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
Well-order relations.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* Well-Order Relations *}
blanchet@48975
     9
blanchet@48975
    10
theory Wellorder_Relation
blanchet@48979
    11
imports Wellorder_Relation_Base Wellfounded_More
blanchet@48975
    12
begin
blanchet@48975
    13
blanchet@48975
    14
blanchet@48975
    15
subsection {* Auxiliaries *}
blanchet@48975
    16
blanchet@48975
    17
lemma (in wo_rel) PREORD: "Preorder r"
blanchet@48975
    18
using WELL order_on_defs[of _ r] by auto
blanchet@48975
    19
blanchet@48975
    20
lemma (in wo_rel) PARORD: "Partial_order r"
blanchet@48975
    21
using WELL order_on_defs[of _ r] by auto
blanchet@48975
    22
blanchet@48975
    23
lemma (in wo_rel) cases_Total2:
blanchet@48975
    24
"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b);
blanchet@48975
    25
              ((b,a) \<in> r - Id \<Longrightarrow> phi a b); (a = b \<Longrightarrow> phi a b)\<rbrakk>
blanchet@48975
    26
             \<Longrightarrow> phi a b"
blanchet@48975
    27
using TOTALS by auto
blanchet@48975
    28
blanchet@48975
    29
blanchet@48975
    30
subsection {* Well-founded induction and recursion adapted to non-strict well-order relations  *}
blanchet@48975
    31
blanchet@48975
    32
lemma (in wo_rel) worec_unique_fixpoint:
blanchet@48975
    33
assumes ADM: "adm_wo H" and fp: "f = H f"
blanchet@48975
    34
shows "f = worec H"
blanchet@48975
    35
proof-
blanchet@48975
    36
  have "adm_wf (r - Id) H"
blanchet@48975
    37
  unfolding adm_wf_def
blanchet@48975
    38
  using ADM adm_wo_def[of H] underS_def by auto
blanchet@48975
    39
  hence "f = wfrec (r - Id) H"
blanchet@48975
    40
  using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
blanchet@48975
    41
  thus ?thesis unfolding worec_def .
blanchet@48975
    42
qed
blanchet@48975
    43
blanchet@48975
    44
blanchet@48975
    45
subsubsection {* Properties of max2 *}
blanchet@48975
    46
blanchet@48975
    47
lemma (in wo_rel) max2_iff:
blanchet@48975
    48
assumes "a \<in> Field r" and "b \<in> Field r"
blanchet@48975
    49
shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)"
blanchet@48975
    50
proof
blanchet@48975
    51
  assume "(max2 a b, c) \<in> r"
blanchet@48975
    52
  thus "(a,c) \<in> r \<and> (b,c) \<in> r"
blanchet@48975
    53
  using assms max2_greater[of a b] TRANS trans_def[of r] by blast
blanchet@48975
    54
next
blanchet@48975
    55
  assume "(a,c) \<in> r \<and> (b,c) \<in> r"
blanchet@48975
    56
  thus "(max2 a b, c) \<in> r"
blanchet@48975
    57
  using assms max2_among[of a b] by auto
blanchet@48975
    58
qed
blanchet@48975
    59
blanchet@48975
    60
blanchet@48975
    61
subsubsection{* Properties of minim *}
blanchet@48975
    62
blanchet@48975
    63
lemma (in wo_rel) minim_Under:
blanchet@48975
    64
"\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
blanchet@48975
    65
by(auto simp add: Under_def
blanchet@48975
    66
minim_in
blanchet@48975
    67
minim_inField
blanchet@48975
    68
minim_least
blanchet@48975
    69
under_ofilter
blanchet@48975
    70
underS_ofilter
blanchet@48975
    71
Field_ofilter
blanchet@48975
    72
ofilter_Under
blanchet@48975
    73
ofilter_UnderS
blanchet@48975
    74
ofilter_Un
blanchet@48975
    75
)
blanchet@48975
    76
blanchet@48975
    77
lemma (in wo_rel) equals_minim_Under:
blanchet@48975
    78
"\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk>
blanchet@48975
    79
 \<Longrightarrow> a = minim B"
blanchet@48975
    80
by(auto simp add: Under_def equals_minim)
blanchet@48975
    81
blanchet@48975
    82
lemma (in wo_rel) minim_iff_In_Under:
blanchet@48975
    83
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
blanchet@48975
    84
shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)"
blanchet@48975
    85
proof
blanchet@48975
    86
  assume "a = minim B"
blanchet@48975
    87
  thus "a \<in> B \<and> a \<in> Under B"
blanchet@48975
    88
  using assms minim_in minim_Under by simp
blanchet@48975
    89
next
blanchet@48975
    90
  assume "a \<in> B \<and> a \<in> Under B"
blanchet@48975
    91
  thus "a = minim B"
blanchet@48975
    92
  using assms equals_minim_Under by simp
blanchet@48975
    93
qed
blanchet@48975
    94
blanchet@48975
    95
lemma (in wo_rel) minim_Under_under:
blanchet@48975
    96
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
blanchet@48975
    97
shows "Under A = under (minim A)"
blanchet@48975
    98
proof-
blanchet@48975
    99
  (* Preliminary facts *)
blanchet@48975
   100
  have 1: "minim A \<in> A"
blanchet@48975
   101
  using assms minim_in by auto
blanchet@48975
   102
  have 2: "\<forall>x \<in> A. (minim A, x) \<in> r"
blanchet@48975
   103
  using assms minim_least by auto
blanchet@48975
   104
  (* Main proof *)
blanchet@48975
   105
  have "Under A \<le> under (minim A)"
blanchet@48975
   106
  proof
blanchet@48975
   107
    fix x assume "x \<in> Under A"
blanchet@48975
   108
    with 1 Under_def have "(x,minim A) \<in> r" by auto
blanchet@48975
   109
    thus "x \<in> under(minim A)" unfolding under_def by simp
blanchet@48975
   110
  qed
blanchet@48975
   111
  (*  *)
blanchet@48975
   112
  moreover
blanchet@48975
   113
  (*  *)
blanchet@48975
   114
  have "under (minim A) \<le> Under A"
blanchet@48975
   115
  proof
blanchet@48975
   116
    fix x assume "x \<in> under(minim A)"
blanchet@48975
   117
    hence 11: "(x,minim A) \<in> r" unfolding under_def by simp
blanchet@48975
   118
    hence "x \<in> Field r" unfolding Field_def by auto
blanchet@48975
   119
    moreover
blanchet@48975
   120
    {fix a assume "a \<in> A"
blanchet@48975
   121
     with 2 have "(minim A, a) \<in> r" by simp
blanchet@48975
   122
     with 11 have "(x,a) \<in> r"
blanchet@48975
   123
     using TRANS trans_def[of r] by blast
blanchet@48975
   124
    }
blanchet@48975
   125
    ultimately show "x \<in> Under A" by (unfold Under_def, auto)
blanchet@48975
   126
  qed
blanchet@48975
   127
  (*  *)
blanchet@48975
   128
  ultimately show ?thesis by blast
blanchet@48975
   129
qed
blanchet@48975
   130
blanchet@48975
   131
lemma (in wo_rel) minim_UnderS_underS:
blanchet@48975
   132
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
blanchet@48975
   133
shows "UnderS A = underS (minim A)"
blanchet@48975
   134
proof-
blanchet@48975
   135
  (* Preliminary facts *)
blanchet@48975
   136
  have 1: "minim A \<in> A"
blanchet@48975
   137
  using assms minim_in by auto
blanchet@48975
   138
  have 2: "\<forall>x \<in> A. (minim A, x) \<in> r"
blanchet@48975
   139
  using assms minim_least by auto
blanchet@48975
   140
  (* Main proof *)
blanchet@48975
   141
  have "UnderS A \<le> underS (minim A)"
blanchet@48975
   142
  proof
blanchet@48975
   143
    fix x assume "x \<in> UnderS A"
blanchet@48975
   144
    with 1 UnderS_def have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
blanchet@48975
   145
    thus "x \<in> underS(minim A)" unfolding underS_def by simp
blanchet@48975
   146
  qed
blanchet@48975
   147
  (*  *)
blanchet@48975
   148
  moreover
blanchet@48975
   149
  (*  *)
blanchet@48975
   150
  have "underS (minim A) \<le> UnderS A"
blanchet@48975
   151
  proof
blanchet@48975
   152
    fix x assume "x \<in> underS(minim A)"
blanchet@48975
   153
    hence 11: "x \<noteq> minim A \<and> (x,minim A) \<in> r" unfolding underS_def by simp
blanchet@48975
   154
    hence "x \<in> Field r" unfolding Field_def by auto
blanchet@48975
   155
    moreover
blanchet@48975
   156
    {fix a assume "a \<in> A"
blanchet@48975
   157
     with 2 have 3: "(minim A, a) \<in> r" by simp
blanchet@48975
   158
     with 11 have "(x,a) \<in> r"
blanchet@48975
   159
     using TRANS trans_def[of r] by blast
blanchet@48975
   160
     moreover
blanchet@48975
   161
     have "x \<noteq> a"
blanchet@48975
   162
     proof
blanchet@48975
   163
       assume "x = a"
blanchet@48975
   164
       with 11 3 ANTISYM antisym_def[of r]
blanchet@48975
   165
       show False by auto
blanchet@48975
   166
     qed
blanchet@48975
   167
     ultimately
blanchet@48975
   168
     have "x \<noteq> a \<and> (x,a) \<in> r" by simp
blanchet@48975
   169
    }
blanchet@48975
   170
    ultimately show "x \<in> UnderS A" by (unfold UnderS_def, auto)
blanchet@48975
   171
  qed
blanchet@48975
   172
  (*  *)
blanchet@48975
   173
  ultimately show ?thesis by blast
blanchet@48975
   174
qed
blanchet@48975
   175
blanchet@48975
   176
blanchet@48975
   177
subsubsection{* Properties of supr *}
blanchet@48975
   178
blanchet@48975
   179
lemma (in wo_rel) supr_Above:
blanchet@48975
   180
assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
blanchet@48975
   181
shows "supr B \<in> Above B"
blanchet@48975
   182
proof(unfold supr_def)
blanchet@48975
   183
  have "Above B \<le> Field r"
blanchet@48975
   184
  using Above_Field by auto
blanchet@48975
   185
  thus "minim (Above B) \<in> Above B"
blanchet@48975
   186
  using assms by (simp add: minim_in)
blanchet@48975
   187
qed
blanchet@48975
   188
blanchet@48975
   189
lemma (in wo_rel) supr_greater:
blanchet@48975
   190
assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" and
blanchet@48975
   191
        IN: "b \<in> B"
blanchet@48975
   192
shows "(b, supr B) \<in> r"
blanchet@48975
   193
proof-
blanchet@48975
   194
  from assms supr_Above
blanchet@48975
   195
  have "supr B \<in> Above B" by simp
blanchet@48975
   196
  with IN Above_def show ?thesis by simp
blanchet@48975
   197
qed
blanchet@48975
   198
blanchet@48975
   199
lemma (in wo_rel) supr_least_Above:
blanchet@48975
   200
assumes SUB: "B \<le> Field r" and
blanchet@48975
   201
        ABOVE: "a \<in> Above B"
blanchet@48975
   202
shows "(supr B, a) \<in> r"
blanchet@48975
   203
proof(unfold supr_def)
blanchet@48975
   204
  have "Above B \<le> Field r"
blanchet@48975
   205
  using Above_Field by auto
blanchet@48975
   206
  thus "(minim (Above B), a) \<in> r"
blanchet@48975
   207
  using assms minim_least
blanchet@48975
   208
  by simp
blanchet@48975
   209
qed
blanchet@48975
   210
blanchet@48975
   211
lemma (in wo_rel) supr_least:
blanchet@48975
   212
"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk>
blanchet@48975
   213
 \<Longrightarrow> (supr B, a) \<in> r"
blanchet@48975
   214
by(auto simp add: supr_least_Above Above_def)
blanchet@48975
   215
blanchet@48975
   216
lemma (in wo_rel) equals_supr_Above:
blanchet@48975
   217
assumes SUB: "B \<le> Field r" and ABV: "a \<in> Above B" and
blanchet@48975
   218
        MINIM: "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
blanchet@48975
   219
shows "a = supr B"
blanchet@48975
   220
proof(unfold supr_def)
blanchet@48975
   221
  have "Above B \<le> Field r"
blanchet@48975
   222
  using Above_Field by auto
blanchet@48975
   223
  thus "a = minim (Above B)"
blanchet@48975
   224
  using assms equals_minim by simp
blanchet@48975
   225
qed
blanchet@48975
   226
blanchet@48975
   227
lemma (in wo_rel) equals_supr:
blanchet@48975
   228
assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
blanchet@48975
   229
        ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and
blanchet@48975
   230
        MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
blanchet@48975
   231
shows "a = supr B"
blanchet@48975
   232
proof-
blanchet@48975
   233
  have "a \<in> Above B"
blanchet@48975
   234
  unfolding Above_def using ABV IN by simp
blanchet@48975
   235
  moreover
blanchet@48975
   236
  have "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
blanchet@48975
   237
  unfolding Above_def using MINIM by simp
blanchet@48975
   238
  ultimately show ?thesis
blanchet@48975
   239
  using equals_supr_Above SUB by auto
blanchet@48975
   240
qed
blanchet@48975
   241
blanchet@48975
   242
lemma (in wo_rel) supr_inField:
blanchet@48975
   243
assumes "B \<le> Field r" and  "Above B \<noteq> {}"
blanchet@48975
   244
shows "supr B \<in> Field r"
blanchet@48975
   245
proof-
blanchet@48975
   246
  have "supr B \<in> Above B" using supr_Above assms by simp
blanchet@48975
   247
  thus ?thesis using assms Above_Field by auto
blanchet@48975
   248
qed
blanchet@48975
   249
blanchet@48975
   250
lemma (in wo_rel) supr_above_Above:
blanchet@48975
   251
assumes SUB: "B \<le> Field r" and  ABOVE: "Above B \<noteq> {}"
blanchet@48975
   252
shows "Above B = above (supr B)"
blanchet@48975
   253
proof(unfold Above_def above_def, auto)
blanchet@48975
   254
  fix a assume "a \<in> Field r" "\<forall>b \<in> B. (b,a) \<in> r"
blanchet@48975
   255
  with supr_least assms
blanchet@48975
   256
  show "(supr B, a) \<in> r" by auto
blanchet@48975
   257
next
blanchet@48975
   258
  fix b assume "(supr B, b) \<in> r"
blanchet@48975
   259
  thus "b \<in> Field r"
blanchet@48975
   260
  using REFL refl_on_def[of _ r] by auto
blanchet@48975
   261
next
blanchet@48975
   262
  fix a b
blanchet@48975
   263
  assume 1: "(supr B, b) \<in> r" and 2: "a \<in> B"
blanchet@48975
   264
  with assms supr_greater
blanchet@48975
   265
  have "(a,supr B) \<in> r" by auto
blanchet@48975
   266
  thus "(a,b) \<in> r"
blanchet@48975
   267
  using 1 TRANS trans_def[of r] by blast
blanchet@48975
   268
qed
blanchet@48975
   269
blanchet@48975
   270
lemma (in wo_rel) supr_under:
blanchet@48975
   271
assumes IN: "a \<in> Field r"
blanchet@48975
   272
shows "a = supr (under a)"
blanchet@48975
   273
proof-
blanchet@48975
   274
  have "under a \<le> Field r"
blanchet@48975
   275
  using under_Field by auto
blanchet@48975
   276
  moreover
blanchet@48975
   277
  have "under a \<noteq> {}"
blanchet@48975
   278
  using IN Refl_under_in REFL by auto
blanchet@48975
   279
  moreover
blanchet@48975
   280
  have "a \<in> Above (under a)"
blanchet@48975
   281
  using in_Above_under IN by auto
blanchet@48975
   282
  moreover
blanchet@48975
   283
  have "\<forall>a' \<in> Above (under a). (a,a') \<in> r"
blanchet@48975
   284
  proof(unfold Above_def under_def, auto)
blanchet@48975
   285
    fix a'
blanchet@48975
   286
    assume "\<forall>aa. (aa, a) \<in> r \<longrightarrow> (aa, a') \<in> r"
blanchet@48975
   287
    hence "(a,a) \<in> r \<longrightarrow> (a,a') \<in> r" by blast
blanchet@48975
   288
    moreover have "(a,a) \<in> r"
blanchet@48975
   289
    using REFL IN by (auto simp add: refl_on_def)
blanchet@48975
   290
    ultimately
blanchet@48975
   291
    show  "(a, a') \<in> r" by (rule mp)
blanchet@48975
   292
  qed
blanchet@48975
   293
  ultimately show ?thesis
blanchet@48975
   294
  using equals_supr_Above by auto
blanchet@48975
   295
qed
blanchet@48975
   296
blanchet@48975
   297
blanchet@48975
   298
subsubsection{* Properties of successor *}
blanchet@48975
   299
blanchet@48975
   300
lemma (in wo_rel) suc_least:
blanchet@48975
   301
"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk>
blanchet@48975
   302
 \<Longrightarrow> (suc B, a) \<in> r"
blanchet@48975
   303
by(auto simp add: suc_least_AboveS AboveS_def)
blanchet@48975
   304
blanchet@48975
   305
lemma (in wo_rel) equals_suc:
blanchet@48975
   306
assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
blanchet@48975
   307
 ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and
blanchet@48975
   308
 MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
blanchet@48975
   309
shows "a = suc B"
blanchet@48975
   310
proof-
blanchet@48975
   311
  have "a \<in> AboveS B"
blanchet@48975
   312
  unfolding AboveS_def using ABVS IN by simp
blanchet@48975
   313
  moreover
blanchet@48975
   314
  have "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
blanchet@48975
   315
  unfolding AboveS_def using MINIM by simp
blanchet@48975
   316
  ultimately show ?thesis
blanchet@48975
   317
  using equals_suc_AboveS SUB by auto
blanchet@48975
   318
qed
blanchet@48975
   319
blanchet@48975
   320
lemma (in wo_rel) suc_above_AboveS:
blanchet@48975
   321
assumes SUB: "B \<le> Field r" and
blanchet@48975
   322
        ABOVE: "AboveS B \<noteq> {}"
blanchet@48975
   323
shows "AboveS B = above (suc B)"
blanchet@48975
   324
proof(unfold AboveS_def above_def, auto)
blanchet@48975
   325
  fix a assume "a \<in> Field r" "\<forall>b \<in> B. a \<noteq> b \<and> (b,a) \<in> r"
blanchet@48975
   326
  with suc_least assms
blanchet@48975
   327
  show "(suc B,a) \<in> r" by auto
blanchet@48975
   328
next
blanchet@48975
   329
  fix b assume "(suc B, b) \<in> r"
blanchet@48975
   330
  thus "b \<in> Field r"
blanchet@48975
   331
  using REFL refl_on_def[of _ r] by auto
blanchet@48975
   332
next
blanchet@48975
   333
  fix a b
blanchet@48975
   334
  assume 1: "(suc B, b) \<in> r" and 2: "a \<in> B"
blanchet@48975
   335
  with assms suc_greater[of B a]
blanchet@48975
   336
  have "(a,suc B) \<in> r" by auto
blanchet@48975
   337
  thus "(a,b) \<in> r"
blanchet@48975
   338
  using 1 TRANS trans_def[of r] by blast
blanchet@48975
   339
next
blanchet@48975
   340
  fix a
blanchet@48975
   341
  assume 1: "(suc B, a) \<in> r" and 2: "a \<in> B"
blanchet@48975
   342
  with assms suc_greater[of B a]
blanchet@48975
   343
  have "(a,suc B) \<in> r" by auto
blanchet@48975
   344
  moreover have "suc B \<in> Field r"
blanchet@48975
   345
  using assms suc_inField by simp
blanchet@48975
   346
  ultimately have "a = suc B"
blanchet@48975
   347
  using 1 2 SUB ANTISYM antisym_def[of r] by auto
blanchet@48975
   348
  thus False
blanchet@48975
   349
  using assms suc_greater[of B a] 2 by auto
blanchet@48975
   350
qed
blanchet@48975
   351
blanchet@48975
   352
lemma (in wo_rel) suc_singl_pred:
blanchet@48975
   353
assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and
blanchet@48975
   354
        REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}"
blanchet@48975
   355
shows "a' = a \<or> (a',a) \<in> r"
blanchet@48975
   356
proof-
blanchet@48975
   357
  have *: "suc {a} \<in> Field r \<and> a' \<in> Field r"
blanchet@48975
   358
  using WELL REL well_order_on_domain by auto
blanchet@48975
   359
  {assume **: "a' \<noteq> a"
blanchet@48975
   360
   hence "(a,a') \<in> r \<or> (a',a) \<in> r"
blanchet@48975
   361
   using TOTAL IN * by (auto simp add: total_on_def)
blanchet@48975
   362
   moreover
blanchet@48975
   363
   {assume "(a,a') \<in> r"
blanchet@48975
   364
    with ** * assms WELL suc_least[of "{a}" a']
blanchet@48975
   365
    have "(suc {a},a') \<in> r" by auto
blanchet@48975
   366
    with REL DIFF * ANTISYM antisym_def[of r]
blanchet@48975
   367
    have False by simp
blanchet@48975
   368
   }
blanchet@48975
   369
   ultimately have "(a',a) \<in> r"
blanchet@48975
   370
   by blast
blanchet@48975
   371
  }
blanchet@48975
   372
  thus ?thesis by blast
blanchet@48975
   373
qed
blanchet@48975
   374
blanchet@48975
   375
lemma (in wo_rel) under_underS_suc:
blanchet@48975
   376
assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}"
blanchet@48975
   377
shows "underS (suc {a}) = under a"
blanchet@48975
   378
proof-
blanchet@48975
   379
  have 1: "AboveS {a} \<noteq> {}"
blanchet@48975
   380
  using ABV aboveS_AboveS_singl by auto
blanchet@48975
   381
  have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r"
blanchet@48975
   382
  using suc_greater[of "{a}" a] IN 1 by auto
blanchet@48975
   383
  (*   *)
blanchet@48975
   384
  have "underS (suc {a}) \<le> under a"
blanchet@48975
   385
  proof(unfold underS_def under_def, auto)
blanchet@48975
   386
    fix x assume *: "x \<noteq> suc {a}" and **: "(x,suc {a}) \<in> r"
blanchet@48975
   387
    with suc_singl_pred[of a x] IN ABV
blanchet@48975
   388
    have "x = a \<or> (x,a) \<in> r" by auto
blanchet@48975
   389
    with REFL refl_on_def[of _ r] IN
blanchet@48975
   390
    show "(x,a) \<in> r" by auto
blanchet@48975
   391
  qed
blanchet@48975
   392
  (*  *)
blanchet@48975
   393
  moreover
blanchet@48975
   394
  (*   *)
blanchet@48975
   395
  have "under a \<le> underS (suc {a})"
blanchet@48975
   396
  proof(unfold underS_def under_def, auto)
blanchet@48975
   397
    assume "(suc {a}, a) \<in> r"
blanchet@48975
   398
    with 2 ANTISYM antisym_def[of r]
blanchet@48975
   399
    show False by auto
blanchet@48975
   400
  next
blanchet@48975
   401
    fix x assume *: "(x,a) \<in> r"
blanchet@48975
   402
    with 2 TRANS trans_def[of r]
blanchet@48975
   403
    show "(x,suc {a}) \<in> r" by blast
blanchet@48975
   404
  (*  blast is often better than auto/auto for transitivity-like properties *)
blanchet@48975
   405
  qed
blanchet@48975
   406
  (*  *)
blanchet@48975
   407
  ultimately show ?thesis by blast
blanchet@48975
   408
qed
blanchet@48975
   409
blanchet@48975
   410
blanchet@48975
   411
subsubsection {* Properties of order filters  *}
blanchet@48975
   412
blanchet@48975
   413
lemma (in wo_rel) ofilter_INTER:
blanchet@48975
   414
"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)"
blanchet@48975
   415
unfolding ofilter_def by blast
blanchet@48975
   416
blanchet@48975
   417
lemma (in wo_rel) ofilter_Inter:
blanchet@48975
   418
"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (Inter S)"
blanchet@48975
   419
unfolding ofilter_def by blast
blanchet@48975
   420
blanchet@48975
   421
lemma (in wo_rel) ofilter_Union:
blanchet@48975
   422
"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (Union S)"
blanchet@48975
   423
unfolding ofilter_def by blast
blanchet@48975
   424
blanchet@48975
   425
lemma (in wo_rel) ofilter_under_Union:
blanchet@48975
   426
"ofilter A \<Longrightarrow> A = Union {under a| a. a \<in> A}"
blanchet@48975
   427
using ofilter_under_UNION[of A]
blanchet@48975
   428
by(unfold Union_eq, auto)
blanchet@48975
   429
blanchet@48975
   430
blanchet@48975
   431
subsubsection{* Other properties *}
blanchet@48975
   432
blanchet@48975
   433
lemma (in wo_rel) Trans_Under_regressive:
blanchet@48975
   434
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
blanchet@48975
   435
shows "Under(Under A) \<le> Under A"
blanchet@48975
   436
proof
blanchet@48975
   437
  let ?a = "minim A"
blanchet@48975
   438
  (*  Preliminary facts *)
blanchet@48975
   439
  have 1: "minim A \<in> Under A"
blanchet@48975
   440
  using assms minim_Under by auto
blanchet@48975
   441
  have 2: "\<forall>y \<in> A. (minim A, y) \<in> r"
blanchet@48975
   442
  using assms minim_least by auto
blanchet@48975
   443
  (* Main proof *)
blanchet@48975
   444
  fix x assume "x \<in> Under(Under A)"
blanchet@48975
   445
  with 1 have 1: "(x,minim A) \<in> r"
blanchet@48975
   446
  using Under_def by auto
blanchet@48975
   447
  with Field_def have "x \<in> Field r" by fastforce
blanchet@48975
   448
  moreover
blanchet@48975
   449
  {fix y assume *: "y \<in> A"
blanchet@48975
   450
   hence "(x,y) \<in> r"
blanchet@48975
   451
   using 1 2 TRANS trans_def[of r] by blast
blanchet@48975
   452
   with Field_def have "(x,y) \<in> r" by auto
blanchet@48975
   453
  }
blanchet@48975
   454
  ultimately
blanchet@48975
   455
  show "x \<in> Under A" unfolding Under_def by auto
blanchet@48975
   456
qed
blanchet@48975
   457
blanchet@48975
   458
lemma (in wo_rel) ofilter_suc_Field:
blanchet@48975
   459
assumes OF: "ofilter A" and NE: "A \<noteq> Field r"
blanchet@48975
   460
shows "ofilter (A \<union> {suc A})"
blanchet@48975
   461
proof-
blanchet@48975
   462
  (* Preliminary facts *)
blanchet@48975
   463
  have 1: "A \<le> Field r" using OF ofilter_def by auto
blanchet@48975
   464
  hence 2: "AboveS A \<noteq> {}"
blanchet@48975
   465
  using ofilter_AboveS_Field NE OF by blast
blanchet@48975
   466
  from 1 2 suc_inField
blanchet@48975
   467
  have 3: "suc A \<in> Field r" by auto
blanchet@48975
   468
  (* Main proof *)
blanchet@48975
   469
  show ?thesis
blanchet@48975
   470
  proof(unfold ofilter_def, auto simp add: 1 3)
blanchet@48975
   471
    fix a x
blanchet@48975
   472
    assume "a \<in> A" "x \<in> under a" "x \<notin> A"
blanchet@48975
   473
    with OF ofilter_def have False by auto
blanchet@48975
   474
    thus "x = suc A" by simp
blanchet@48975
   475
  next
blanchet@48975
   476
    fix x assume *: "x \<in> under (suc A)" and **: "x \<notin> A"
blanchet@48975
   477
    hence "x \<in> Field r" using under_def Field_def by fastforce
blanchet@48975
   478
    with ** have "x \<in> AboveS A"
blanchet@48975
   479
    using ofilter_AboveS_Field[of A] OF by auto
blanchet@48975
   480
    hence "(suc A,x) \<in> r"
blanchet@48975
   481
    using suc_least_AboveS by auto
blanchet@48975
   482
    moreover
blanchet@48975
   483
    have "(x,suc A) \<in> r" using * under_def by auto
blanchet@48975
   484
    ultimately show "x = suc A"
blanchet@48975
   485
    using ANTISYM antisym_def[of r] by auto
blanchet@48975
   486
  qed
blanchet@48975
   487
qed
blanchet@48975
   488
blanchet@48975
   489
(* FIXME: needed? *)
blanchet@48975
   490
declare (in wo_rel)
blanchet@48975
   491
  minim_in[simp]
blanchet@48975
   492
  minim_inField[simp]
blanchet@48975
   493
  minim_least[simp]
blanchet@48975
   494
  under_ofilter[simp]
blanchet@48975
   495
  underS_ofilter[simp]
blanchet@48975
   496
  Field_ofilter[simp]
blanchet@48975
   497
  ofilter_Under[simp]
blanchet@48975
   498
  ofilter_UnderS[simp]
blanchet@48975
   499
  ofilter_Int[simp]
blanchet@48975
   500
  ofilter_Un[simp]
blanchet@48975
   501
blanchet@48975
   502
abbreviation "worec \<equiv> wo_rel.worec"
blanchet@48975
   503
abbreviation "adm_wo \<equiv> wo_rel.adm_wo"
blanchet@48975
   504
abbreviation "isMinim \<equiv> wo_rel.isMinim"
blanchet@48975
   505
abbreviation "minim \<equiv> wo_rel.minim"
blanchet@48975
   506
abbreviation "max2 \<equiv> wo_rel.max2"
blanchet@48975
   507
abbreviation "supr \<equiv> wo_rel.supr"
blanchet@48975
   508
abbreviation "suc \<equiv> wo_rel.suc"
blanchet@48975
   509
abbreviation "ofilter \<equiv> wo_rel.ofilter"
blanchet@48975
   510
blanchet@48975
   511
end