src/HOL/Order_Relation.thy
author blanchet
Fri, 17 Jan 2014 10:02:49 +0100
changeset 55026 258fa7b5a621
parent 54552 5d57cbec0f0f
child 55027 a74ea6d75571
permissions -rw-r--r--
folded 'Order_Relation_More_FP' into 'Order_Relation'
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
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
     6
header {* Orders as Relations *}
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
     7
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
     8
theory Order_Relation
54552
5d57cbec0f0f moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents: 54551
diff changeset
     9
imports Wellfounded
26273
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    10
begin
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    11
26295
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    12
subsection{* Orders on a set *}
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
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    58
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    59
subsection{* Orders on the field *}
26273
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    60
30198
922f944f03b2 name changes
nipkow
parents: 29859
diff changeset
    61
abbreviation "Refl r \<equiv> refl_on (Field r) r"
26295
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    62
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    63
abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    64
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    65
abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
26273
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    66
26295
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    67
abbreviation "Total r \<equiv> total_on (Field r) r"
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    68
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    69
abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    70
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    71
abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    72
26273
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    73
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    74
lemma subset_Image_Image_iff:
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    75
  "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    76
   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
    77
unfolding preorder_on_def refl_on_def Image_def
a151db85a62b tuned proofs
blanchet
parents: 39302
diff changeset
    78
apply (simp add: subset_eq)
a151db85a62b tuned proofs
blanchet
parents: 39302
diff changeset
    79
unfolding trans_def by fast
26273
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    80
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    81
lemma subset_Image1_Image1_iff:
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    82
  "\<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
    83
by(simp add:subset_Image_Image_iff)
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    84
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    85
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
    86
  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
    87
  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
    88
proof
5d57cbec0f0f moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents: 54551
diff changeset
    89
  assume "r `` {a} = r `` {b}"
5d57cbec0f0f moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents: 54551
diff changeset
    90
  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
    91
  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
    92
  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
    93
  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
    94
qed fast
26273
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    95
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    96
lemma Partial_order_eq_Image1_Image1_iff:
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
    97
  "\<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
    98
by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
    99
52182
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   100
lemma Total_Id_Field:
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   101
assumes TOT: "Total r" and NID: "\<not> (r <= Id)"
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   102
shows "Field r = Field(r - Id)"
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   103
using mono_Field[of "r - Id" r] Diff_subset[of r Id]
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   104
proof(auto)
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   105
  have "r \<noteq> {}" using NID by fast
54482
a2874c8b3558 optimized 'bad apple' method calls
blanchet
parents: 52182
diff changeset
   106
  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
   107
  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
   108
52182
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   109
  fix a assume *: "a \<in> Field r"
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   110
  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
   111
  using * 1 by auto
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   112
  hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   113
  by (simp add: total_on_def)
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   114
  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
   115
qed
57b4fdc59d3b well-order extension (by Christian Sternagel)
popescua
parents: 48750
diff changeset
   116
26295
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
   117
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
   118
subsection{* Orders on a type *}
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
   119
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
   120
abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
   121
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
   122
abbreviation "linear_order \<equiv> linear_order_on UNIV"
afc43168ed85 More defns and thms
nipkow
parents: 26273
diff changeset
   123
54551
4cd6deb430c3 fixed apparent copy-paste bug
blanchet
parents: 54482
diff changeset
   124
abbreviation "well_order \<equiv> well_order_on UNIV"
26273
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
   125
55026
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   126
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   127
subsection {* Order-like relations *}
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   128
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   129
text{* In this subsection, we develop basic concepts and results pertaining
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   130
to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   131
total relations. We also further define upper and lower bounds operators. *}
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   132
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   133
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   134
subsubsection {* Auxiliaries *}
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   135
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   136
lemma refl_on_domain:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   137
"\<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
   138
by(auto simp add: refl_on_def)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   139
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   140
corollary well_order_on_domain:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   141
"\<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
   142
by (auto simp add: refl_on_domain order_on_defs)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   143
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   144
lemma well_order_on_Field:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   145
"well_order_on A r \<Longrightarrow> A = Field r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   146
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
   147
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   148
lemma well_order_on_Well_order:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   149
"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
   150
using well_order_on_Field by auto
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   151
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   152
lemma Total_subset_Id:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   153
assumes TOT: "Total r" and SUB: "r \<le> Id"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   154
shows "r = {} \<or> (\<exists>a. r = {(a,a)})"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   155
proof-
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   156
  {assume "r \<noteq> {}"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   157
   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
   158
   hence "a = b" using SUB by blast
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   159
   hence 2: "(a,a) \<in> r" using 1 by simp
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   160
   {fix c d assume "(c,d) \<in> r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   161
    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
   162
    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
   163
           ((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
   164
    using TOT unfolding total_on_def by blast
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   165
    hence "a = c \<and> a = d" using SUB by blast
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
   hence "r \<le> {(a,a)}" by auto
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   168
   with 2 have "\<exists>a. r = {(a,a)}" by blast
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   169
  }
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   170
  thus ?thesis by blast
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   171
qed
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   172
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   173
lemma Linear_order_in_diff_Id:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   174
assumes LI: "Linear_order r" and
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   175
        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
   176
shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   177
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
   178
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   179
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   180
subsubsection {* The upper and lower bounds operators  *}
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
text{* Here we define upper (``above") and lower (``below") bounds operators.
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   183
We think of @{text "r"} as a {\em non-strict} relation.  The suffix ``S"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   184
at the names of some operators indicates that the bounds are strict -- e.g.,
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   185
@{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   186
Capitalization of the first letter in the name reminds that the operator acts on sets, rather
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   187
than on individual elements. *}
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   188
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   189
definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   190
where "under r a \<equiv> {b. (b,a) \<in> r}"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   191
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   192
definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   193
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
   194
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   195
definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   196
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
   197
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   198
definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   199
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
   200
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   201
definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   202
where "above r a \<equiv> {b. (a,b) \<in> r}"
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 aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   205
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
   206
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   207
definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   208
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
   209
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   210
definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   211
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
   212
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   213
text{* Note:  In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   214
  we bounded comprehension by @{text "Field r"} in order to properly cover
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   215
  the case of @{text "A"} being empty. *}
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   216
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   217
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
   218
by(auto simp add: underS_def under_def)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   219
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   220
lemma underS_notIn: "a \<notin> underS r a"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   221
by(simp add: underS_def)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   222
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   223
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
   224
by(simp add: refl_on_def under_def)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   225
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   226
lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   227
by(auto simp add: AboveS_def)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   228
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   229
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
   230
by(auto simp add: AboveS_def underS_def)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   231
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   232
lemma Refl_under_underS:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   233
  assumes "Refl r" "a \<in> Field r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   234
  shows "under r a = underS r a \<union> {a}"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   235
unfolding under_def underS_def
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   236
using assms refl_on_def[of _ r] by fastforce
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_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   239
by (auto simp: Field_def 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 under_Field: "under r a \<le> Field r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   242
by(unfold under_def Field_def, auto)
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 underS_Field: "underS r a \<le> Field r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   245
by(unfold underS_def Field_def, auto)
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 underS_Field2:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   248
"a \<in> Field r \<Longrightarrow> underS r a < Field r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   249
using underS_notIn underS_Field by fast
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   250
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   251
lemma underS_Field3:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   252
"Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   253
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
   254
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   255
lemma AboveS_Field: "AboveS r A \<le> Field r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   256
by(unfold AboveS_def Field_def, auto)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   257
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   258
lemma under_incr:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   259
  assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   260
  shows "under r a \<le> under r b"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   261
proof(unfold under_def, auto)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   262
  fix x assume "(x,a) \<in> r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   263
  with REL TRANS trans_def[of r]
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   264
  show "(x,b) \<in> r" by blast
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   265
qed
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   266
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   267
lemma underS_incr:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   268
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   269
        REL: "(a,b) \<in> r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   270
shows "underS r a \<le> underS r b"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   271
proof(unfold underS_def, auto)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   272
  assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   273
  with ANTISYM antisym_def[of r] REL
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   274
  show False by blast
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   275
next
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   276
  fix x assume "x \<noteq> a" "(x,a) \<in> r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   277
  with REL TRANS trans_def[of r]
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   278
  show "(x,b) \<in> r" by blast
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   279
qed
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   280
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   281
lemma underS_incl_iff:
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   282
assumes LO: "Linear_order r" and
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   283
        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
   284
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
   285
proof
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   286
  assume "(a,b) \<in> r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   287
  thus "underS r a \<le> underS r b" using LO
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   288
  by (simp add: order_on_defs underS_incr)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   289
next
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   290
  assume *: "underS r a \<le> underS r b"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   291
  {assume "a = b"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   292
   hence "(a,b) \<in> r" using assms
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   293
   by (simp add: order_on_defs refl_on_def)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   294
  }
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   295
  moreover
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   296
  {assume "a \<noteq> b \<and> (b,a) \<in> r"
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   297
   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
   298
   hence "b \<in> underS r b" using * by blast
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   299
   hence False by (simp add: underS_notIn)
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   300
  }
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   301
  ultimately
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   302
  show "(a,b) \<in> r" using assms
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   303
  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
   304
qed
258fa7b5a621 folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents: 54552
diff changeset
   305
26273
6c4d534af98d Orders as relations
nipkow
parents:
diff changeset
   306
end