src/HOL/Order_Relation.thy
author blanchet
Fri Jan 17 10:02:50 2014 +0100 (2014-01-17)
changeset 55027 a74ea6d75571
parent 55026 258fa7b5a621
child 55173 5556470a02b7
permissions -rw-r--r--
folded 'Wellfounded_More_FP' into 'Wellfounded'
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
nipkow@26273
     6
header {* Orders as Relations *}
nipkow@26273
     7
nipkow@26273
     8
theory Order_Relation
blanchet@55027
     9
imports Wfrec
nipkow@26273
    10
begin
nipkow@26273
    11
nipkow@26295
    12
subsection{* Orders on a set *}
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
nipkow@26295
    59
subsection{* Orders on the field *}
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
nipkow@26295
   118
subsection{* Orders on a type *}
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
blanchet@55026
   127
subsection {* Order-like relations *}
blanchet@55026
   128
blanchet@55026
   129
text{* 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
blanchet@55026
   131
total relations. We also further define upper and lower bounds operators. *}
blanchet@55026
   132
blanchet@55026
   133
blanchet@55026
   134
subsubsection {* Auxiliaries *}
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
blanchet@55026
   180
subsubsection {* The upper and lower bounds operators  *}
blanchet@55026
   181
blanchet@55026
   182
text{* Here we define upper (``above") and lower (``below") bounds operators.
blanchet@55026
   183
We think of @{text "r"} 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.,
blanchet@55026
   185
@{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).
blanchet@55026
   186
Capitalization of the first letter in the name reminds that the operator acts on sets, rather
blanchet@55026
   187
than on individual elements. *}
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
blanchet@55026
   213
text{* Note:  In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
blanchet@55026
   214
  we bounded comprehension by @{text "Field r"} in order to properly cover
blanchet@55026
   215
  the case of @{text "A"} being empty. *}
blanchet@55026
   216
blanchet@55026
   217
lemma underS_subset_under: "underS r a \<le> under r a"
blanchet@55026
   218
by(auto simp add: underS_def under_def)
blanchet@55026
   219
blanchet@55026
   220
lemma underS_notIn: "a \<notin> underS r a"
blanchet@55026
   221
by(simp add: underS_def)
blanchet@55026
   222
blanchet@55026
   223
lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"
blanchet@55026
   224
by(simp add: refl_on_def under_def)
blanchet@55026
   225
blanchet@55026
   226
lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
blanchet@55026
   227
by(auto simp add: AboveS_def)
blanchet@55026
   228
blanchet@55026
   229
lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
blanchet@55026
   230
by(auto simp add: AboveS_def underS_def)
blanchet@55026
   231
blanchet@55026
   232
lemma Refl_under_underS:
blanchet@55026
   233
  assumes "Refl r" "a \<in> Field r"
blanchet@55026
   234
  shows "under r a = underS r a \<union> {a}"
blanchet@55026
   235
unfolding under_def underS_def
blanchet@55026
   236
using assms refl_on_def[of _ r] by fastforce
blanchet@55026
   237
blanchet@55026
   238
lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
blanchet@55026
   239
by (auto simp: Field_def underS_def)
blanchet@55026
   240
blanchet@55026
   241
lemma under_Field: "under r a \<le> Field r"
blanchet@55026
   242
by(unfold under_def Field_def, auto)
blanchet@55026
   243
blanchet@55026
   244
lemma underS_Field: "underS r a \<le> Field r"
blanchet@55026
   245
by(unfold underS_def Field_def, auto)
blanchet@55026
   246
blanchet@55026
   247
lemma underS_Field2:
blanchet@55026
   248
"a \<in> Field r \<Longrightarrow> underS r a < Field r"
blanchet@55026
   249
using underS_notIn underS_Field by fast
blanchet@55026
   250
blanchet@55026
   251
lemma underS_Field3:
blanchet@55026
   252
"Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
blanchet@55026
   253
by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
blanchet@55026
   254
blanchet@55026
   255
lemma AboveS_Field: "AboveS r A \<le> Field r"
blanchet@55026
   256
by(unfold AboveS_def Field_def, auto)
blanchet@55026
   257
blanchet@55026
   258
lemma under_incr:
blanchet@55026
   259
  assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
blanchet@55026
   260
  shows "under r a \<le> under r b"
blanchet@55026
   261
proof(unfold under_def, auto)
blanchet@55026
   262
  fix x assume "(x,a) \<in> r"
blanchet@55026
   263
  with REL TRANS trans_def[of r]
blanchet@55026
   264
  show "(x,b) \<in> r" by blast
blanchet@55026
   265
qed
blanchet@55026
   266
blanchet@55026
   267
lemma underS_incr:
blanchet@55026
   268
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55026
   269
        REL: "(a,b) \<in> r"
blanchet@55026
   270
shows "underS r a \<le> underS r b"
blanchet@55026
   271
proof(unfold underS_def, auto)
blanchet@55026
   272
  assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
blanchet@55026
   273
  with ANTISYM antisym_def[of r] REL
blanchet@55026
   274
  show False by blast
blanchet@55026
   275
next
blanchet@55026
   276
  fix x assume "x \<noteq> a" "(x,a) \<in> r"
blanchet@55026
   277
  with REL TRANS trans_def[of r]
blanchet@55026
   278
  show "(x,b) \<in> r" by blast
blanchet@55026
   279
qed
blanchet@55026
   280
blanchet@55026
   281
lemma underS_incl_iff:
blanchet@55026
   282
assumes LO: "Linear_order r" and
blanchet@55026
   283
        INa: "a \<in> Field r" and INb: "b \<in> Field r"
blanchet@55026
   284
shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"
blanchet@55026
   285
proof
blanchet@55026
   286
  assume "(a,b) \<in> r"
blanchet@55026
   287
  thus "underS r a \<le> underS r b" using LO
blanchet@55026
   288
  by (simp add: order_on_defs underS_incr)
blanchet@55026
   289
next
blanchet@55026
   290
  assume *: "underS r a \<le> underS r b"
blanchet@55026
   291
  {assume "a = b"
blanchet@55026
   292
   hence "(a,b) \<in> r" using assms
blanchet@55026
   293
   by (simp add: order_on_defs refl_on_def)
blanchet@55026
   294
  }
blanchet@55026
   295
  moreover
blanchet@55026
   296
  {assume "a \<noteq> b \<and> (b,a) \<in> r"
blanchet@55026
   297
   hence "b \<in> underS r a" unfolding underS_def by blast
blanchet@55026
   298
   hence "b \<in> underS r b" using * by blast
blanchet@55026
   299
   hence False by (simp add: underS_notIn)
blanchet@55026
   300
  }
blanchet@55026
   301
  ultimately
blanchet@55026
   302
  show "(a,b) \<in> r" using assms
blanchet@55026
   303
  order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
blanchet@55026
   304
qed
blanchet@55026
   305
blanchet@55027
   306
blanchet@55027
   307
subsection {* Variations on Well-Founded Relations  *}
blanchet@55027
   308
blanchet@55027
   309
text {*
blanchet@55027
   310
This subsection contains some variations of the results from @{theory Wellfounded}:
blanchet@55027
   311
\begin{itemize}
blanchet@55027
   312
\item means for slightly more direct definitions by well-founded recursion;
blanchet@55027
   313
\item variations of well-founded induction;
blanchet@55027
   314
\item means for proving a linear order to be a well-order.
blanchet@55027
   315
\end{itemize}
blanchet@55027
   316
*}
blanchet@55027
   317
blanchet@55027
   318
blanchet@55027
   319
subsubsection {* Well-founded recursion via genuine fixpoints *}
blanchet@55027
   320
blanchet@55027
   321
lemma wfrec_fixpoint:
blanchet@55027
   322
fixes r :: "('a * 'a) set" and
blanchet@55027
   323
      H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
blanchet@55027
   324
assumes WF: "wf r" and ADM: "adm_wf r H"
blanchet@55027
   325
shows "wfrec r H = H (wfrec r H)"
blanchet@55027
   326
proof(rule ext)
blanchet@55027
   327
  fix x
blanchet@55027
   328
  have "wfrec r H x = H (cut (wfrec r H) r x) x"
blanchet@55027
   329
  using wfrec[of r H] WF by simp
blanchet@55027
   330
  also
blanchet@55027
   331
  {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
blanchet@55027
   332
   by (auto simp add: cut_apply)
blanchet@55027
   333
   hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
blanchet@55027
   334
   using ADM adm_wf_def[of r H] by auto
blanchet@55027
   335
  }
blanchet@55027
   336
  finally show "wfrec r H x = H (wfrec r H) x" .
blanchet@55027
   337
qed
blanchet@55027
   338
blanchet@55027
   339
blanchet@55027
   340
subsubsection {* Characterizations of well-foundedness *}
blanchet@55027
   341
blanchet@55027
   342
text {* A transitive relation is well-founded iff it is ``locally'' well-founded,
blanchet@55027
   343
i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}
blanchet@55027
   344
blanchet@55027
   345
lemma trans_wf_iff:
blanchet@55027
   346
assumes "trans r"
blanchet@55027
   347
shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
blanchet@55027
   348
proof-
blanchet@55027
   349
  obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
blanchet@55027
   350
  {assume *: "wf r"
blanchet@55027
   351
   {fix a
blanchet@55027
   352
    have "wf(R a)"
blanchet@55027
   353
    using * R_def wf_subset[of r "R a"] by auto
blanchet@55027
   354
   }
blanchet@55027
   355
  }
blanchet@55027
   356
  (*  *)
blanchet@55027
   357
  moreover
blanchet@55027
   358
  {assume *: "\<forall>a. wf(R a)"
blanchet@55027
   359
   have "wf r"
blanchet@55027
   360
   proof(unfold wf_def, clarify)
blanchet@55027
   361
     fix phi a
blanchet@55027
   362
     assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
blanchet@55027
   363
     obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
blanchet@55027
   364
     with * have "wf (R a)" by auto
blanchet@55027
   365
     hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
blanchet@55027
   366
     unfolding wf_def by blast
blanchet@55027
   367
     moreover
blanchet@55027
   368
     have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
blanchet@55027
   369
     proof(auto simp add: chi_def R_def)
blanchet@55027
   370
       fix b
blanchet@55027
   371
       assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
blanchet@55027
   372
       hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
blanchet@55027
   373
       using assms trans_def[of r] by blast
blanchet@55027
   374
       thus "phi b" using ** by blast
blanchet@55027
   375
     qed
blanchet@55027
   376
     ultimately have  "\<forall>b. chi b" by (rule mp)
blanchet@55027
   377
     with ** chi_def show "phi a" by blast
blanchet@55027
   378
   qed
blanchet@55027
   379
  }
blanchet@55027
   380
  ultimately show ?thesis using R_def by blast
blanchet@55027
   381
qed
blanchet@55027
   382
blanchet@55027
   383
text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
blanchet@55027
   384
allowing one to assume the set included in the field.  *}
blanchet@55027
   385
blanchet@55027
   386
lemma wf_eq_minimal2:
blanchet@55027
   387
"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
   388
proof-
blanchet@55027
   389
  let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
blanchet@55027
   390
  have "wf r = (\<forall>A. ?phi A)"
blanchet@55027
   391
  by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
blanchet@55027
   392
     (rule wfI_min, fast)
blanchet@55027
   393
  (*  *)
blanchet@55027
   394
  also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
blanchet@55027
   395
  proof
blanchet@55027
   396
    assume "\<forall>A. ?phi A"
blanchet@55027
   397
    thus "\<forall>B \<le> Field r. ?phi B" by simp
blanchet@55027
   398
  next
blanchet@55027
   399
    assume *: "\<forall>B \<le> Field r. ?phi B"
blanchet@55027
   400
    show "\<forall>A. ?phi A"
blanchet@55027
   401
    proof(clarify)
blanchet@55027
   402
      fix A::"'a set" assume **: "A \<noteq> {}"
blanchet@55027
   403
      obtain B where B_def: "B = A Int (Field r)" by blast
blanchet@55027
   404
      show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
blanchet@55027
   405
      proof(cases "B = {}")
blanchet@55027
   406
        assume Case1: "B = {}"
blanchet@55027
   407
        obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
blanchet@55027
   408
        using ** Case1 unfolding B_def by blast
blanchet@55027
   409
        hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
blanchet@55027
   410
        thus ?thesis using 1 by blast
blanchet@55027
   411
      next
blanchet@55027
   412
        assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
blanchet@55027
   413
        obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
blanchet@55027
   414
        using Case2 1 * by blast
blanchet@55027
   415
        have "\<forall>a' \<in> A. (a',a) \<notin> r"
blanchet@55027
   416
        proof(clarify)
blanchet@55027
   417
          fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
blanchet@55027
   418
          hence "a' \<in> B" unfolding B_def Field_def by blast
blanchet@55027
   419
          thus False using 2 ** by blast
blanchet@55027
   420
        qed
blanchet@55027
   421
        thus ?thesis using 2 unfolding B_def by blast
blanchet@55027
   422
      qed
blanchet@55027
   423
    qed
blanchet@55027
   424
  qed
blanchet@55027
   425
  finally show ?thesis by blast
blanchet@55027
   426
qed
blanchet@55027
   427
blanchet@55027
   428
blanchet@55027
   429
subsubsection {* Characterizations of well-foundedness *}
blanchet@55027
   430
blanchet@55027
   431
text {* The next lemma and its corollary enable one to prove that
blanchet@55027
   432
a linear order is a well-order in a way which is more standard than
blanchet@55027
   433
via well-foundedness of the strict version of the relation.  *}
blanchet@55027
   434
blanchet@55027
   435
lemma Linear_order_wf_diff_Id:
blanchet@55027
   436
assumes LI: "Linear_order r"
blanchet@55027
   437
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
   438
proof(cases "r \<le> Id")
blanchet@55027
   439
  assume Case1: "r \<le> Id"
blanchet@55027
   440
  hence temp: "r - Id = {}" by blast
blanchet@55027
   441
  hence "wf(r - Id)" by (simp add: temp)
blanchet@55027
   442
  moreover
blanchet@55027
   443
  {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
blanchet@55027
   444
   obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
blanchet@55027
   445
   unfolding order_on_defs using Case1 Total_subset_Id by auto
blanchet@55027
   446
   hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
blanchet@55027
   447
   hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
blanchet@55027
   448
  }
blanchet@55027
   449
  ultimately show ?thesis by blast
blanchet@55027
   450
next
blanchet@55027
   451
  assume Case2: "\<not> r \<le> Id"
blanchet@55027
   452
  hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
blanchet@55027
   453
  unfolding order_on_defs by blast
blanchet@55027
   454
  show ?thesis
blanchet@55027
   455
  proof
blanchet@55027
   456
    assume *: "wf(r - Id)"
blanchet@55027
   457
    show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
blanchet@55027
   458
    proof(clarify)
blanchet@55027
   459
      fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
blanchet@55027
   460
      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
blanchet@55027
   461
      using 1 * unfolding wf_eq_minimal2 by simp
blanchet@55027
   462
      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
blanchet@55027
   463
      using Linear_order_in_diff_Id[of r] ** LI by blast
blanchet@55027
   464
      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
blanchet@55027
   465
    qed
blanchet@55027
   466
  next
blanchet@55027
   467
    assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
blanchet@55027
   468
    show "wf(r - Id)"
blanchet@55027
   469
    proof(unfold wf_eq_minimal2, clarify)
blanchet@55027
   470
      fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
blanchet@55027
   471
      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
blanchet@55027
   472
      using 1 * by simp
blanchet@55027
   473
      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
blanchet@55027
   474
      using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
blanchet@55027
   475
      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
blanchet@55027
   476
    qed
blanchet@55027
   477
  qed
blanchet@55027
   478
qed
blanchet@55027
   479
blanchet@55027
   480
corollary Linear_order_Well_order_iff:
blanchet@55027
   481
assumes "Linear_order r"
blanchet@55027
   482
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
   483
using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
blanchet@55027
   484
nipkow@26273
   485
end