src/HOL/Lattice/CompleteLattice.thy
author wenzelm
Fri, 06 Oct 2000 01:04:56 +0200
changeset 10157 6d3987f3aad9
child 10175 76646fc8b1bf
permissions -rw-r--r--
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Lattice/CompleteLattice.thy
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     4
*)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     5
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     6
header {* Complete lattices *}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     7
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     8
theory CompleteLattice = Lattice:
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     9
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    10
subsection {* Complete lattice operations *}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    11
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    12
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    13
  A \emph{complete lattice} is a partial order with general
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    14
  (infinitary) infimum of any set of elements.  General supremum
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    15
  exists as well, as a consequence of the connection of infinitary
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    16
  bounds (see \S\ref{sec:connect-bounds}).
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    17
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    18
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    19
axclass complete_lattice < partial_order
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    20
  ex_Inf: "\<exists>inf. is_Inf A inf"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    21
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    22
theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    23
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    24
  from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    25
  hence "is_Sup A sup" by (rule Inf_Sup)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    26
  thus ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    27
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    28
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    29
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    30
  The general @{text \<Sqinter>} (meet) and @{text \<Squnion>} (join) operations select
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    31
  such infimum and supremum elements.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    32
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    33
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    34
consts
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    35
  Meet :: "'a::complete_lattice set \<Rightarrow> 'a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    36
  Join :: "'a::complete_lattice set \<Rightarrow> 'a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    37
syntax (symbols)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    38
  Meet :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Sqinter>_" [90] 90)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    39
  Join :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Squnion>_" [90] 90)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    40
defs
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    41
  Meet_def: "\<Sqinter>A \<equiv> SOME inf. is_Inf A inf"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    42
  Join_def: "\<Squnion>A \<equiv> SOME sup. is_Sup A sup"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    43
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    44
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    45
  Due to unique existence of bounds, the complete lattice operations
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    46
  may be exhibited as follows.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    47
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    48
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    49
lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    50
proof (unfold Meet_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    51
  assume "is_Inf A inf"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    52
  thus "(SOME inf. is_Inf A inf) = inf"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    53
    by (rule some_equality) (rule is_Inf_uniq)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    54
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    55
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    56
lemma MeetI [intro?]:
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    57
  "(\<And>a. a \<in> A \<Longrightarrow> inf \<sqsubseteq> a) \<Longrightarrow>
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    58
    (\<And>b. \<forall>a \<in> A. b \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> inf) \<Longrightarrow>
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    59
    \<Sqinter>A = inf"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    60
  by (rule Meet_equality, rule is_InfI) blast+
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    61
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    62
lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    63
proof (unfold Join_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    64
  assume "is_Sup A sup"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    65
  thus "(SOME sup. is_Sup A sup) = sup"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    66
    by (rule some_equality) (rule is_Sup_uniq)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    67
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    68
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    69
lemma JoinI [intro?]:
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    70
  "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> sup) \<Longrightarrow>
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    71
    (\<And>b. \<forall>a \<in> A. a \<sqsubseteq> b \<Longrightarrow> sup \<sqsubseteq> b) \<Longrightarrow>
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    72
    \<Squnion>A = sup"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    73
  by (rule Join_equality, rule is_SupI) blast+
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    74
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    75
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    76
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    77
  \medskip The @{text \<Sqinter>} and @{text \<Squnion>} operations indeed determine
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    78
  bounds on a complete lattice structure.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    79
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    80
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    81
lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    82
proof (unfold Meet_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    83
  from ex_Inf show "is_Inf A (SOME inf. is_Inf A inf)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    84
    by (rule ex_someI)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    85
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    86
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    87
lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    88
  by (rule is_Inf_greatest, rule is_Inf_Meet) blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    89
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    90
lemma Meet_lower [intro?]: "a \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    91
  by (rule is_Inf_lower) (rule is_Inf_Meet)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    92
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    93
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    94
lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    95
proof (unfold Join_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    96
  from ex_Sup show "is_Sup A (SOME sup. is_Sup A sup)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    97
    by (rule ex_someI)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    98
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    99
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   100
lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   101
  by (rule is_Sup_least, rule is_Sup_Join) blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   102
lemma Join_lower [intro?]: "a \<in> A \<Longrightarrow> a \<sqsubseteq> \<Squnion>A"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   103
  by (rule is_Sup_upper) (rule is_Sup_Join)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   104
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   105
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   106
subsection {* The Knaster-Tarski Theorem *}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   107
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   108
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   109
  The Knaster-Tarski Theorem (in its simplest formulation) states that
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   110
  any monotone function on a complete lattice has a least fixed-point
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   111
  (see \cite[pages 93--94]{Davey-Priestley:1990} for example).  This
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   112
  is a consequence of the basic boundary properties of the complete
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   113
  lattice operations.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   114
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   115
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   116
theorem Knaster_Tarski:
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   117
  "(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y) \<Longrightarrow> \<exists>a::'a::complete_lattice. f a = a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   118
proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   119
  assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   120
  let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   121
  have ge: "f ?a \<sqsubseteq> ?a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   122
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   123
    fix x assume x: "x \<in> ?H"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   124
    hence "?a \<sqsubseteq> x" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   125
    hence "f ?a \<sqsubseteq> f x" by (rule mono)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   126
    also from x have "... \<sqsubseteq> x" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   127
    finally show "f ?a \<sqsubseteq> x" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   128
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   129
  also have "?a \<sqsubseteq> f ?a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   130
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   131
    from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   132
    thus "f ?a : ?H" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   133
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   134
  finally show "f ?a = ?a" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   135
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   136
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   137
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   138
subsection {* Bottom and top elements *}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   139
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   140
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   141
  With general bounds available, complete lattices also have least and
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   142
  greatest elements.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   143
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   144
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   145
constdefs
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   146
  bottom :: "'a::complete_lattice"    ("\<bottom>")
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   147
  "\<bottom> \<equiv> \<Sqinter>UNIV"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   148
  top :: "'a::complete_lattice"    ("\<top>")
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   149
  "\<top> \<equiv> \<Squnion>UNIV"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   150
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   151
lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   152
proof (unfold bottom_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   153
  have "x \<in> UNIV" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   154
  thus "\<Sqinter>UNIV \<sqsubseteq> x" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   155
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   156
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   157
lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   158
proof (unfold bottom_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   159
  assume "\<And>a. x \<sqsubseteq> a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   160
  show "\<Sqinter>UNIV = x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   161
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   162
    fix a show "x \<sqsubseteq> a" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   163
  next
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   164
    fix b :: "'a::complete_lattice"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   165
    assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   166
    have "x \<in> UNIV" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   167
    with b show "b \<sqsubseteq> x" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   168
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   169
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   170
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   171
lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   172
proof (unfold top_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   173
  have "x \<in> UNIV" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   174
  thus "x \<sqsubseteq> \<Squnion>UNIV" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   175
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   176
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   177
lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   178
proof (unfold top_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   179
  assume "\<And>a. a \<sqsubseteq> x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   180
  show "\<Squnion>UNIV = x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   181
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   182
    fix a show "a \<sqsubseteq> x" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   183
  next
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   184
    fix b :: "'a::complete_lattice"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   185
    assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   186
    have "x \<in> UNIV" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   187
    with b show "x \<sqsubseteq> b" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   188
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   189
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   190
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   191
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   192
subsection {* Duality *}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   193
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   194
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   195
  The class of complete lattices is closed under formation of dual
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   196
  structures.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   197
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   198
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   199
instance dual :: (complete_lattice) complete_lattice
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   200
proof intro_classes
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   201
  fix A' :: "'a::complete_lattice dual set"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   202
  show "\<exists>inf'. is_Inf A' inf'"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   203
  proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   204
    have "\<exists>sup. is_Sup (undual `` A') sup" by (rule ex_Sup)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   205
    hence "\<exists>sup. is_Inf (dual `` undual `` A') (dual sup)" by (simp only: dual_Inf)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   206
    thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   207
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   208
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   209
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   210
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   211
  Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   212
  other.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   213
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   214
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   215
theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual `` A)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   216
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   217
  from is_Inf_Meet have "is_Sup (dual `` A) (dual (\<Sqinter>A))" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   218
  hence "\<Squnion>(dual `` A) = dual (\<Sqinter>A)" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   219
  thus ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   220
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   221
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   222
theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual `` A)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   223
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   224
  from is_Sup_Join have "is_Inf (dual `` A) (dual (\<Squnion>A))" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   225
  hence "\<Sqinter>(dual `` A) = dual (\<Squnion>A)" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   226
  thus ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   227
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   228
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   229
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   230
  Likewise are @{text \<bottom>} and @{text \<top>} duals of each other.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   231
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   232
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   233
theorem dual_bottom [intro?]: "dual \<bottom> = \<top>"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   234
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   235
  have "\<top> = dual \<bottom>"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   236
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   237
    fix a' have "\<bottom> \<sqsubseteq> undual a'" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   238
    hence "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   239
    thus "a' \<sqsubseteq> dual \<bottom>" by simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   240
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   241
  thus ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   242
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   243
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   244
theorem dual_top [intro?]: "dual \<top> = \<bottom>"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   245
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   246
  have "\<bottom> = dual \<top>"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   247
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   248
    fix a' have "undual a' \<sqsubseteq> \<top>" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   249
    hence "dual \<top> \<sqsubseteq> dual (undual a')" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   250
    thus "dual \<top> \<sqsubseteq> a'" by simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   251
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   252
  thus ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   253
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   254
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   255
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   256
subsection {* Complete lattices are lattices *}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   257
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   258
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   259
  Complete lattices (with general bounds) available are indeed plain
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   260
  lattices as well.  This holds due to the connection of general
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   261
  versus binary bounds that has been formally established in
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   262
  \S\ref{sec:gen-bin-bounds}.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   263
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   264
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   265
lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   266
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   267
  have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   268
  thus ?thesis by (simp only: is_Inf_binary)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   269
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   270
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   271
lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   272
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   273
  have "is_Sup {x, y} (\<Squnion>{x, y})" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   274
  thus ?thesis by (simp only: is_Sup_binary)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   275
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   276
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   277
instance complete_lattice < lattice
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   278
proof intro_classes
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   279
  fix x y :: "'a::complete_lattice"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   280
  from is_inf_binary show "\<exists>inf. is_inf x y inf" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   281
  from is_sup_binary show "\<exists>sup. is_sup x y sup" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   282
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   283
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   284
theorem meet_binary: "x \<sqinter> y = \<Sqinter>{x, y}"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   285
  by (rule meet_equality) (rule is_inf_binary)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   286
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   287
theorem join_binary: "x \<squnion> y = \<Squnion>{x, y}"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   288
  by (rule join_equality) (rule is_sup_binary)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   289
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   290
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   291
subsection {* Complete lattices and set-theory operations *}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   292
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   293
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   294
  The complete lattice operations are (anti) monotone wrt.\ set
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   295
  inclusion.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   296
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   297
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   298
theorem Meet_subset_antimono: "A \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   299
proof (rule Meet_greatest)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   300
  fix a assume "a \<in> A"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   301
  also assume "A \<subseteq> B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   302
  finally have "a \<in> B" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   303
  thus "\<Sqinter>B \<sqsubseteq> a" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   304
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   305
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   306
theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   307
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   308
  assume "A \<subseteq> B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   309
  hence "dual `` A \<subseteq> dual `` B" by blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   310
  hence "\<Sqinter>(dual `` B) \<sqsubseteq> \<Sqinter>(dual `` A)" by (rule Meet_subset_antimono)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   311
  hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   312
  thus ?thesis by (simp only: dual_leq)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   313
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   314
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   315
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   316
  Bounds over unions of sets may be obtained separately.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   317
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   318
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   319
theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   320
proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   321
  fix a assume "a \<in> A \<union> B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   322
  thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   323
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   324
    assume a: "a \<in> A"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   325
    have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   326
    also from a have "\<dots> \<sqsubseteq> a" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   327
    finally show ?thesis .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   328
  next
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   329
    assume a: "a \<in> B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   330
    have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   331
    also from a have "\<dots> \<sqsubseteq> a" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   332
    finally show ?thesis .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   333
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   334
next
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   335
  fix b assume b: "\<forall>a \<in> A \<union> B. b \<sqsubseteq> a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   336
  show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   337
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   338
    show "b \<sqsubseteq> \<Sqinter>A"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   339
    proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   340
      fix a assume "a \<in> A"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   341
      hence "a \<in>  A \<union> B" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   342
      with b show "b \<sqsubseteq> a" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   343
    qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   344
    show "b \<sqsubseteq> \<Sqinter>B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   345
    proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   346
      fix a assume "a \<in> B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   347
      hence "a \<in>  A \<union> B" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   348
      with b show "b \<sqsubseteq> a" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   349
    qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   350
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   351
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   352
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   353
theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   354
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   355
  have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual `` A \<union> dual `` B)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   356
    by (simp only: dual_Join image_Un)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   357
  also have "\<dots> = \<Sqinter>(dual `` A) \<sqinter> \<Sqinter>(dual `` B)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   358
    by (rule Meet_Un)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   359
  also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   360
    by (simp only: dual_join dual_Join)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   361
  finally show ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   362
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   363
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   364
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   365
  Bounds over singleton sets are trivial.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   366
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   367
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   368
theorem Meet_singleton: "\<Sqinter>{x} = x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   369
proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   370
  fix a assume "a \<in> {x}"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   371
  hence "a = x" by simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   372
  thus "x \<sqsubseteq> a" by (simp only: leq_refl)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   373
next
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   374
  fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   375
  thus "b \<sqsubseteq> x" by simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   376
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   377
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   378
theorem Join_singleton: "\<Squnion>{x} = x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   379
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   380
  have "dual (\<Squnion>{x}) = \<Sqinter>{dual x}" by (simp add: dual_Join)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   381
  also have "\<dots> = dual x" by (rule Meet_singleton)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   382
  finally show ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   383
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   384
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   385
text {*
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   386
  Bounds over the empty and universal set correspond to each other.
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   387
*}
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   388
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   389
theorem Meet_empty: "\<Sqinter>{} = \<Squnion>UNIV"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   390
proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   391
  fix a :: "'a::complete_lattice"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   392
  assume "a \<in> {}"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   393
  hence False by simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   394
  thus "\<Squnion>UNIV \<sqsubseteq> a" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   395
next
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   396
  fix b :: "'a::complete_lattice"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   397
  have "b \<in> UNIV" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   398
  thus "b \<sqsubseteq> \<Squnion>UNIV" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   399
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   400
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   401
theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   402
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   403
  have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   404
  also have "\<dots> = \<Squnion>UNIV" by (rule Meet_empty)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   405
  also have "\<dots> = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   406
  finally show ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   407
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   408
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   409
end