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