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