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