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