src/HOL/Order_Relation.thy
author Andreas Lochbihler
Fri Jul 29 09:49:23 2016 +0200 (2016-07-29)
changeset 63561 fba08009ff3e
parent 61799 4cf66f21b764
child 63563 0bcd79da075b
permissions -rw-r--r--
add lemmas contributed by Peter Gammie
blanchet@54552
     1
(*  Title:      HOL/Order_Relation.thy
blanchet@54552
     2
    Author:     Tobias Nipkow
blanchet@55026
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@54552
     4
*)
nipkow@26273
     5
wenzelm@60758
     6
section \<open>Orders as Relations\<close>
nipkow@26273
     7
nipkow@26273
     8
theory Order_Relation
blanchet@55027
     9
imports Wfrec
nipkow@26273
    10
begin
nipkow@26273
    11
wenzelm@60758
    12
subsection\<open>Orders on a set\<close>
nipkow@26295
    13
nipkow@30198
    14
definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
nipkow@26295
    15
nipkow@26295
    16
definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
nipkow@26273
    17
nipkow@26295
    18
definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
nipkow@26295
    19
nipkow@26295
    20
definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
nipkow@26295
    21
nipkow@26295
    22
definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
nipkow@26273
    23
nipkow@26295
    24
lemmas order_on_defs =
nipkow@26295
    25
  preorder_on_def partial_order_on_def linear_order_on_def
nipkow@26295
    26
  strict_linear_order_on_def well_order_on_def
nipkow@26295
    27
nipkow@26273
    28
nipkow@26295
    29
lemma preorder_on_empty[simp]: "preorder_on {} {}"
nipkow@26295
    30
by(simp add:preorder_on_def trans_def)
nipkow@26295
    31
nipkow@26295
    32
lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
nipkow@26295
    33
by(simp add:partial_order_on_def)
nipkow@26273
    34
nipkow@26295
    35
lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
nipkow@26295
    36
by(simp add:linear_order_on_def)
nipkow@26295
    37
nipkow@26295
    38
lemma well_order_on_empty[simp]: "well_order_on {} {}"
nipkow@26295
    39
by(simp add:well_order_on_def)
nipkow@26295
    40
nipkow@26273
    41
nipkow@26295
    42
lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
nipkow@26295
    43
by (simp add:preorder_on_def)
nipkow@26295
    44
nipkow@26295
    45
lemma partial_order_on_converse[simp]:
nipkow@26295
    46
  "partial_order_on A (r^-1) = partial_order_on A r"
nipkow@26295
    47
by (simp add: partial_order_on_def)
nipkow@26273
    48
nipkow@26295
    49
lemma linear_order_on_converse[simp]:
nipkow@26295
    50
  "linear_order_on A (r^-1) = linear_order_on A r"
nipkow@26295
    51
by (simp add: linear_order_on_def)
nipkow@26295
    52
nipkow@26273
    53
nipkow@26295
    54
lemma strict_linear_order_on_diff_Id:
nipkow@26295
    55
  "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
nipkow@26295
    56
by(simp add: order_on_defs trans_diff_Id)
nipkow@26295
    57
Andreas@63561
    58
lemma linear_order_on_singleton [iff]: "linear_order_on {x} {(x, x)}"
Andreas@63561
    59
unfolding order_on_defs by simp
Andreas@63561
    60
Andreas@63561
    61
lemma linear_order_on_acyclic:
Andreas@63561
    62
  assumes "linear_order_on A r"
Andreas@63561
    63
  shows "acyclic (r - Id)"
Andreas@63561
    64
using strict_linear_order_on_diff_Id[OF assms] 
Andreas@63561
    65
by(auto simp add: acyclic_irrefl strict_linear_order_on_def)
Andreas@63561
    66
Andreas@63561
    67
lemma linear_order_on_well_order_on:
Andreas@63561
    68
  assumes "finite r"
Andreas@63561
    69
  shows "linear_order_on A r \<longleftrightarrow> well_order_on A r"
Andreas@63561
    70
unfolding well_order_on_def
Andreas@63561
    71
using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast
Andreas@63561
    72
nipkow@26295
    73
wenzelm@60758
    74
subsection\<open>Orders on the field\<close>
nipkow@26273
    75
nipkow@30198
    76
abbreviation "Refl r \<equiv> refl_on (Field r) r"
nipkow@26295
    77
nipkow@26295
    78
abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
nipkow@26295
    79
nipkow@26295
    80
abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
nipkow@26273
    81
nipkow@26295
    82
abbreviation "Total r \<equiv> total_on (Field r) r"
nipkow@26295
    83
nipkow@26295
    84
abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
nipkow@26295
    85
nipkow@26295
    86
abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
nipkow@26295
    87
nipkow@26273
    88
nipkow@26273
    89
lemma subset_Image_Image_iff:
nipkow@26273
    90
  "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
nipkow@26273
    91
   r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
blanchet@48750
    92
unfolding preorder_on_def refl_on_def Image_def
blanchet@48750
    93
apply (simp add: subset_eq)
blanchet@48750
    94
unfolding trans_def by fast
nipkow@26273
    95
nipkow@26273
    96
lemma subset_Image1_Image1_iff:
nipkow@26273
    97
  "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
nipkow@26273
    98
by(simp add:subset_Image_Image_iff)
nipkow@26273
    99
nipkow@26273
   100
lemma Refl_antisym_eq_Image1_Image1_iff:
blanchet@54552
   101
  assumes r: "Refl r" and as: "antisym r" and abf: "a \<in> Field r" "b \<in> Field r"
blanchet@54552
   102
  shows "r `` {a} = r `` {b} \<longleftrightarrow> a = b"
blanchet@54552
   103
proof
blanchet@54552
   104
  assume "r `` {a} = r `` {b}"
blanchet@54552
   105
  hence e: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r" by (simp add: set_eq_iff)
blanchet@54552
   106
  have "(a, a) \<in> r" "(b, b) \<in> r" using r abf by (simp_all add: refl_on_def)
blanchet@54552
   107
  hence "(a, b) \<in> r" "(b, a) \<in> r" using e[of a] e[of b] by simp_all
blanchet@54552
   108
  thus "a = b" using as[unfolded antisym_def] by blast
blanchet@54552
   109
qed fast
nipkow@26273
   110
nipkow@26273
   111
lemma Partial_order_eq_Image1_Image1_iff:
nipkow@26273
   112
  "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
nipkow@26295
   113
by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
nipkow@26295
   114
popescua@52182
   115
lemma Total_Id_Field:
popescua@52182
   116
assumes TOT: "Total r" and NID: "\<not> (r <= Id)"
popescua@52182
   117
shows "Field r = Field(r - Id)"
popescua@52182
   118
using mono_Field[of "r - Id" r] Diff_subset[of r Id]
popescua@52182
   119
proof(auto)
popescua@52182
   120
  have "r \<noteq> {}" using NID by fast
blanchet@54482
   121
  then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto
popescua@52182
   122
  hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
blanchet@54552
   123
popescua@52182
   124
  fix a assume *: "a \<in> Field r"
popescua@52182
   125
  obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
popescua@52182
   126
  using * 1 by auto
popescua@52182
   127
  hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
popescua@52182
   128
  by (simp add: total_on_def)
popescua@52182
   129
  thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
popescua@52182
   130
qed
popescua@52182
   131
nipkow@26295
   132
wenzelm@60758
   133
subsection\<open>Orders on a type\<close>
nipkow@26295
   134
nipkow@26295
   135
abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
nipkow@26295
   136
nipkow@26295
   137
abbreviation "linear_order \<equiv> linear_order_on UNIV"
nipkow@26295
   138
blanchet@54551
   139
abbreviation "well_order \<equiv> well_order_on UNIV"
nipkow@26273
   140
blanchet@55026
   141
wenzelm@60758
   142
subsection \<open>Order-like relations\<close>
blanchet@55026
   143
wenzelm@60758
   144
text\<open>In this subsection, we develop basic concepts and results pertaining
blanchet@55026
   145
to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
wenzelm@60758
   146
total relations. We also further define upper and lower bounds operators.\<close>
blanchet@55026
   147
blanchet@55026
   148
wenzelm@60758
   149
subsubsection \<open>Auxiliaries\<close>
blanchet@55026
   150
blanchet@55026
   151
lemma refl_on_domain:
blanchet@55026
   152
"\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
blanchet@55026
   153
by(auto simp add: refl_on_def)
blanchet@55026
   154
blanchet@55026
   155
corollary well_order_on_domain:
blanchet@55026
   156
"\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
blanchet@55026
   157
by (auto simp add: refl_on_domain order_on_defs)
blanchet@55026
   158
blanchet@55026
   159
lemma well_order_on_Field:
blanchet@55026
   160
"well_order_on A r \<Longrightarrow> A = Field r"
blanchet@55026
   161
by(auto simp add: refl_on_def Field_def order_on_defs)
blanchet@55026
   162
blanchet@55026
   163
lemma well_order_on_Well_order:
blanchet@55026
   164
"well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
blanchet@55026
   165
using well_order_on_Field by auto
blanchet@55026
   166
blanchet@55026
   167
lemma Total_subset_Id:
blanchet@55026
   168
assumes TOT: "Total r" and SUB: "r \<le> Id"
blanchet@55026
   169
shows "r = {} \<or> (\<exists>a. r = {(a,a)})"
blanchet@55026
   170
proof-
blanchet@55026
   171
  {assume "r \<noteq> {}"
blanchet@55026
   172
   then obtain a b where 1: "(a,b) \<in> r" by fast
blanchet@55026
   173
   hence "a = b" using SUB by blast
blanchet@55026
   174
   hence 2: "(a,a) \<in> r" using 1 by simp
blanchet@55026
   175
   {fix c d assume "(c,d) \<in> r"
blanchet@55026
   176
    hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast
blanchet@55026
   177
    hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and>
blanchet@55026
   178
           ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)"
blanchet@55026
   179
    using TOT unfolding total_on_def by blast
blanchet@55026
   180
    hence "a = c \<and> a = d" using SUB by blast
blanchet@55026
   181
   }
blanchet@55026
   182
   hence "r \<le> {(a,a)}" by auto
blanchet@55026
   183
   with 2 have "\<exists>a. r = {(a,a)}" by blast
blanchet@55026
   184
  }
blanchet@55026
   185
  thus ?thesis by blast
blanchet@55026
   186
qed
blanchet@55026
   187
blanchet@55026
   188
lemma Linear_order_in_diff_Id:
blanchet@55026
   189
assumes LI: "Linear_order r" and
blanchet@55026
   190
        IN1: "a \<in> Field r" and IN2: "b \<in> Field r"
blanchet@55026
   191
shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"
blanchet@55026
   192
using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
blanchet@55026
   193
blanchet@55026
   194
wenzelm@60758
   195
subsubsection \<open>The upper and lower bounds operators\<close>
blanchet@55026
   196
wenzelm@60758
   197
text\<open>Here we define upper (``above") and lower (``below") bounds operators.
wenzelm@61799
   198
We think of \<open>r\<close> as a {\em non-strict} relation.  The suffix ``S"
blanchet@55026
   199
at the names of some operators indicates that the bounds are strict -- e.g.,
wenzelm@61799
   200
\<open>underS a\<close> is the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>).
blanchet@55026
   201
Capitalization of the first letter in the name reminds that the operator acts on sets, rather
wenzelm@60758
   202
than on individual elements.\<close>
blanchet@55026
   203
blanchet@55026
   204
definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
blanchet@55026
   205
where "under r a \<equiv> {b. (b,a) \<in> r}"
blanchet@55026
   206
blanchet@55026
   207
definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
blanchet@55026
   208
where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
blanchet@55026
   209
blanchet@55026
   210
definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
blanchet@55026
   211
where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
blanchet@55026
   212
blanchet@55026
   213
definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
blanchet@55026
   214
where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
blanchet@55026
   215
blanchet@55026
   216
definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
blanchet@55026
   217
where "above r a \<equiv> {b. (a,b) \<in> r}"
blanchet@55026
   218
blanchet@55026
   219
definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
blanchet@55026
   220
where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
blanchet@55026
   221
blanchet@55026
   222
definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
blanchet@55026
   223
where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
blanchet@55026
   224
blanchet@55026
   225
definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
blanchet@55026
   226
where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
blanchet@55026
   227
traytel@55173
   228
definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
traytel@55173
   229
where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"
traytel@55173
   230
wenzelm@61799
   231
text\<open>Note:  In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>,
wenzelm@61799
   232
  we bounded comprehension by \<open>Field r\<close> in order to properly cover
wenzelm@61799
   233
  the case of \<open>A\<close> being empty.\<close>
blanchet@55026
   234
blanchet@55026
   235
lemma underS_subset_under: "underS r a \<le> under r a"
blanchet@55026
   236
by(auto simp add: underS_def under_def)
blanchet@55026
   237
blanchet@55026
   238
lemma underS_notIn: "a \<notin> underS r a"
blanchet@55026
   239
by(simp add: underS_def)
blanchet@55026
   240
blanchet@55026
   241
lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"
blanchet@55026
   242
by(simp add: refl_on_def under_def)
blanchet@55026
   243
blanchet@55026
   244
lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
blanchet@55026
   245
by(auto simp add: AboveS_def)
blanchet@55026
   246
blanchet@55026
   247
lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
blanchet@55026
   248
by(auto simp add: AboveS_def underS_def)
blanchet@55026
   249
blanchet@55026
   250
lemma Refl_under_underS:
blanchet@55026
   251
  assumes "Refl r" "a \<in> Field r"
blanchet@55026
   252
  shows "under r a = underS r a \<union> {a}"
blanchet@55026
   253
unfolding under_def underS_def
blanchet@55026
   254
using assms refl_on_def[of _ r] by fastforce
blanchet@55026
   255
blanchet@55026
   256
lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
blanchet@55026
   257
by (auto simp: Field_def underS_def)
blanchet@55026
   258
blanchet@55026
   259
lemma under_Field: "under r a \<le> Field r"
blanchet@55026
   260
by(unfold under_def Field_def, auto)
blanchet@55026
   261
blanchet@55026
   262
lemma underS_Field: "underS r a \<le> Field r"
blanchet@55026
   263
by(unfold underS_def Field_def, auto)
blanchet@55026
   264
blanchet@55026
   265
lemma underS_Field2:
blanchet@55026
   266
"a \<in> Field r \<Longrightarrow> underS r a < Field r"
blanchet@55026
   267
using underS_notIn underS_Field by fast
blanchet@55026
   268
blanchet@55026
   269
lemma underS_Field3:
blanchet@55026
   270
"Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
blanchet@55026
   271
by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
blanchet@55026
   272
blanchet@55026
   273
lemma AboveS_Field: "AboveS r A \<le> Field r"
blanchet@55026
   274
by(unfold AboveS_def Field_def, auto)
blanchet@55026
   275
blanchet@55026
   276
lemma under_incr:
blanchet@55026
   277
  assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
blanchet@55026
   278
  shows "under r a \<le> under r b"
blanchet@55026
   279
proof(unfold under_def, auto)
blanchet@55026
   280
  fix x assume "(x,a) \<in> r"
blanchet@55026
   281
  with REL TRANS trans_def[of r]
blanchet@55026
   282
  show "(x,b) \<in> r" by blast
blanchet@55026
   283
qed
blanchet@55026
   284
blanchet@55026
   285
lemma underS_incr:
blanchet@55026
   286
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55026
   287
        REL: "(a,b) \<in> r"
blanchet@55026
   288
shows "underS r a \<le> underS r b"
blanchet@55026
   289
proof(unfold underS_def, auto)
blanchet@55026
   290
  assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
blanchet@55026
   291
  with ANTISYM antisym_def[of r] REL
blanchet@55026
   292
  show False by blast
blanchet@55026
   293
next
blanchet@55026
   294
  fix x assume "x \<noteq> a" "(x,a) \<in> r"
blanchet@55026
   295
  with REL TRANS trans_def[of r]
blanchet@55026
   296
  show "(x,b) \<in> r" by blast
blanchet@55026
   297
qed
blanchet@55026
   298
blanchet@55026
   299
lemma underS_incl_iff:
blanchet@55026
   300
assumes LO: "Linear_order r" and
blanchet@55026
   301
        INa: "a \<in> Field r" and INb: "b \<in> Field r"
blanchet@55026
   302
shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"
blanchet@55026
   303
proof
blanchet@55026
   304
  assume "(a,b) \<in> r"
blanchet@55026
   305
  thus "underS r a \<le> underS r b" using LO
blanchet@55026
   306
  by (simp add: order_on_defs underS_incr)
blanchet@55026
   307
next
blanchet@55026
   308
  assume *: "underS r a \<le> underS r b"
blanchet@55026
   309
  {assume "a = b"
blanchet@55026
   310
   hence "(a,b) \<in> r" using assms
blanchet@55026
   311
   by (simp add: order_on_defs refl_on_def)
blanchet@55026
   312
  }
blanchet@55026
   313
  moreover
blanchet@55026
   314
  {assume "a \<noteq> b \<and> (b,a) \<in> r"
blanchet@55026
   315
   hence "b \<in> underS r a" unfolding underS_def by blast
blanchet@55026
   316
   hence "b \<in> underS r b" using * by blast
blanchet@55026
   317
   hence False by (simp add: underS_notIn)
blanchet@55026
   318
  }
blanchet@55026
   319
  ultimately
blanchet@55026
   320
  show "(a,b) \<in> r" using assms
blanchet@55026
   321
  order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
blanchet@55026
   322
qed
blanchet@55026
   323
Andreas@63561
   324
lemma finite_Linear_order_induct[consumes 3, case_names step]:
Andreas@63561
   325
  assumes "Linear_order r"
Andreas@63561
   326
  and "x \<in> Field r"
Andreas@63561
   327
  and "finite r"
Andreas@63561
   328
  and step: "\<And>x. \<lbrakk>x \<in> Field r; \<And>y. y \<in> aboveS r x \<Longrightarrow> P y\<rbrakk> \<Longrightarrow> P x"
Andreas@63561
   329
  shows "P x"
Andreas@63561
   330
using assms(2)
Andreas@63561
   331
proof(induct rule: wf_induct[of "r\<inverse> - Id"])
Andreas@63561
   332
  from assms(1,3) show "wf (r\<inverse> - Id)"
Andreas@63561
   333
    using linear_order_on_well_order_on linear_order_on_converse
Andreas@63561
   334
    unfolding well_order_on_def by blast
Andreas@63561
   335
next
Andreas@63561
   336
  case (2 x) then show ?case
Andreas@63561
   337
    by - (rule step; auto simp: aboveS_def intro: FieldI2)
Andreas@63561
   338
qed
Andreas@63561
   339
blanchet@55027
   340
wenzelm@60758
   341
subsection \<open>Variations on Well-Founded Relations\<close>
blanchet@55027
   342
wenzelm@60758
   343
text \<open>
blanchet@55027
   344
This subsection contains some variations of the results from @{theory Wellfounded}:
blanchet@55027
   345
\begin{itemize}
blanchet@55027
   346
\item means for slightly more direct definitions by well-founded recursion;
blanchet@55027
   347
\item variations of well-founded induction;
blanchet@55027
   348
\item means for proving a linear order to be a well-order.
blanchet@55027
   349
\end{itemize}
wenzelm@60758
   350
\<close>
blanchet@55027
   351
blanchet@55027
   352
wenzelm@60758
   353
subsubsection \<open>Characterizations of well-foundedness\<close>
blanchet@55027
   354
wenzelm@60758
   355
text \<open>A transitive relation is well-founded iff it is ``locally'' well-founded,
wenzelm@60758
   356
i.e., iff its restriction to the lower bounds of of any element is well-founded.\<close>
blanchet@55027
   357
blanchet@55027
   358
lemma trans_wf_iff:
blanchet@55027
   359
assumes "trans r"
blanchet@55027
   360
shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
blanchet@55027
   361
proof-
blanchet@55027
   362
  obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
blanchet@55027
   363
  {assume *: "wf r"
blanchet@55027
   364
   {fix a
blanchet@55027
   365
    have "wf(R a)"
blanchet@55027
   366
    using * R_def wf_subset[of r "R a"] by auto
blanchet@55027
   367
   }
blanchet@55027
   368
  }
blanchet@55027
   369
  (*  *)
blanchet@55027
   370
  moreover
blanchet@55027
   371
  {assume *: "\<forall>a. wf(R a)"
blanchet@55027
   372
   have "wf r"
blanchet@55027
   373
   proof(unfold wf_def, clarify)
blanchet@55027
   374
     fix phi a
blanchet@55027
   375
     assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
blanchet@55027
   376
     obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
blanchet@55027
   377
     with * have "wf (R a)" by auto
blanchet@55027
   378
     hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
blanchet@55027
   379
     unfolding wf_def by blast
blanchet@55027
   380
     moreover
blanchet@55027
   381
     have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
blanchet@55027
   382
     proof(auto simp add: chi_def R_def)
blanchet@55027
   383
       fix b
blanchet@55027
   384
       assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
blanchet@55027
   385
       hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
blanchet@55027
   386
       using assms trans_def[of r] by blast
blanchet@55027
   387
       thus "phi b" using ** by blast
blanchet@55027
   388
     qed
blanchet@55027
   389
     ultimately have  "\<forall>b. chi b" by (rule mp)
blanchet@55027
   390
     with ** chi_def show "phi a" by blast
blanchet@55027
   391
   qed
blanchet@55027
   392
  }
blanchet@55027
   393
  ultimately show ?thesis using R_def by blast
blanchet@55027
   394
qed
blanchet@55027
   395
wenzelm@61799
   396
text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
wenzelm@60758
   397
allowing one to assume the set included in the field.\<close>
blanchet@55027
   398
blanchet@55027
   399
lemma wf_eq_minimal2:
blanchet@55027
   400
"wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"
blanchet@55027
   401
proof-
blanchet@55027
   402
  let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
blanchet@55027
   403
  have "wf r = (\<forall>A. ?phi A)"
blanchet@55027
   404
  by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
blanchet@55027
   405
     (rule wfI_min, fast)
blanchet@55027
   406
  (*  *)
blanchet@55027
   407
  also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
blanchet@55027
   408
  proof
blanchet@55027
   409
    assume "\<forall>A. ?phi A"
blanchet@55027
   410
    thus "\<forall>B \<le> Field r. ?phi B" by simp
blanchet@55027
   411
  next
blanchet@55027
   412
    assume *: "\<forall>B \<le> Field r. ?phi B"
blanchet@55027
   413
    show "\<forall>A. ?phi A"
blanchet@55027
   414
    proof(clarify)
blanchet@55027
   415
      fix A::"'a set" assume **: "A \<noteq> {}"
blanchet@55027
   416
      obtain B where B_def: "B = A Int (Field r)" by blast
blanchet@55027
   417
      show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
blanchet@55027
   418
      proof(cases "B = {}")
blanchet@55027
   419
        assume Case1: "B = {}"
blanchet@55027
   420
        obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
blanchet@55027
   421
        using ** Case1 unfolding B_def by blast
blanchet@55027
   422
        hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
blanchet@55027
   423
        thus ?thesis using 1 by blast
blanchet@55027
   424
      next
blanchet@55027
   425
        assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
blanchet@55027
   426
        obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
blanchet@55027
   427
        using Case2 1 * by blast
blanchet@55027
   428
        have "\<forall>a' \<in> A. (a',a) \<notin> r"
blanchet@55027
   429
        proof(clarify)
blanchet@55027
   430
          fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
blanchet@55027
   431
          hence "a' \<in> B" unfolding B_def Field_def by blast
blanchet@55027
   432
          thus False using 2 ** by blast
blanchet@55027
   433
        qed
blanchet@55027
   434
        thus ?thesis using 2 unfolding B_def by blast
blanchet@55027
   435
      qed
blanchet@55027
   436
    qed
blanchet@55027
   437
  qed
blanchet@55027
   438
  finally show ?thesis by blast
blanchet@55027
   439
qed
blanchet@55027
   440
blanchet@55027
   441
wenzelm@60758
   442
subsubsection \<open>Characterizations of well-foundedness\<close>
blanchet@55027
   443
wenzelm@60758
   444
text \<open>The next lemma and its corollary enable one to prove that
blanchet@55027
   445
a linear order is a well-order in a way which is more standard than
wenzelm@60758
   446
via well-foundedness of the strict version of the relation.\<close>
blanchet@55027
   447
blanchet@55027
   448
lemma Linear_order_wf_diff_Id:
blanchet@55027
   449
assumes LI: "Linear_order r"
blanchet@55027
   450
shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
blanchet@55027
   451
proof(cases "r \<le> Id")
blanchet@55027
   452
  assume Case1: "r \<le> Id"
blanchet@55027
   453
  hence temp: "r - Id = {}" by blast
blanchet@55027
   454
  hence "wf(r - Id)" by (simp add: temp)
blanchet@55027
   455
  moreover
blanchet@55027
   456
  {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
blanchet@55027
   457
   obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
blanchet@55027
   458
   unfolding order_on_defs using Case1 Total_subset_Id by auto
blanchet@55027
   459
   hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
blanchet@55027
   460
   hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
blanchet@55027
   461
  }
blanchet@55027
   462
  ultimately show ?thesis by blast
blanchet@55027
   463
next
blanchet@55027
   464
  assume Case2: "\<not> r \<le> Id"
blanchet@55027
   465
  hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
blanchet@55027
   466
  unfolding order_on_defs by blast
blanchet@55027
   467
  show ?thesis
blanchet@55027
   468
  proof
blanchet@55027
   469
    assume *: "wf(r - Id)"
blanchet@55027
   470
    show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
blanchet@55027
   471
    proof(clarify)
blanchet@55027
   472
      fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
blanchet@55027
   473
      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
blanchet@55027
   474
      using 1 * unfolding wf_eq_minimal2 by simp
blanchet@55027
   475
      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
blanchet@55027
   476
      using Linear_order_in_diff_Id[of r] ** LI by blast
blanchet@55027
   477
      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
blanchet@55027
   478
    qed
blanchet@55027
   479
  next
blanchet@55027
   480
    assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
blanchet@55027
   481
    show "wf(r - Id)"
blanchet@55027
   482
    proof(unfold wf_eq_minimal2, clarify)
blanchet@55027
   483
      fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
blanchet@55027
   484
      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
blanchet@55027
   485
      using 1 * by simp
blanchet@55027
   486
      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
blanchet@55027
   487
      using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
blanchet@55027
   488
      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
blanchet@55027
   489
    qed
blanchet@55027
   490
  qed
blanchet@55027
   491
qed
blanchet@55027
   492
blanchet@55027
   493
corollary Linear_order_Well_order_iff:
blanchet@55027
   494
assumes "Linear_order r"
blanchet@55027
   495
shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
blanchet@55027
   496
using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
blanchet@55027
   497
nipkow@26273
   498
end