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