src/HOL/Lattice/Orders.thy
author wenzelm
Wed, 30 Dec 2015 18:25:39 +0100
changeset 61986 2461779da2b8
parent 61983 8fb53badad99
child 69597 ff784d5a5bfb
permissions -rw-r--r--
isabelle update_cartouches -c -t;
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/Orders.thy
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     3
*)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     4
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
     5
section \<open>Orders\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12338
diff changeset
     7
theory Orders imports Main begin
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
     8
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
     9
subsection \<open>Ordered structures\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    10
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    11
text \<open>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    12
  We define several classes of ordered structures over some type @{typ
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    13
  'a} with relation \<open>\<sqsubseteq> :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.  For a
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    14
  \emph{quasi-order} that relation is required to be reflexive and
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    15
  transitive, for a \emph{partial order} it also has to be
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    16
  anti-symmetric, while for a \emph{linear order} all elements are
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    17
  required to be related (in either direction).
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    18
\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    19
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    20
class leq =
61983
8fb53badad99 more symbols;
wenzelm
parents: 61076
diff changeset
    21
  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sqsubseteq>" 50)
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    22
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    23
class quasi_order = leq +
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    24
  assumes leq_refl [intro?]: "x \<sqsubseteq> x"
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    25
  assumes leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    26
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    27
class partial_order = quasi_order +
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    28
  assumes leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    29
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    30
class linear_order = partial_order +
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    31
  assumes leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
10157
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
lemma linear_order_cases:
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    34
    "((x::'a::linear_order) \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> (y \<sqsubseteq> x \<Longrightarrow> C) \<Longrightarrow> C"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    35
  by (insert leq_linear) blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    36
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    37
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    38
subsection \<open>Duality\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    39
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    40
text \<open>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    41
  The \emph{dual} of an ordered structure is an isomorphic copy of the
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    42
  underlying type, with the \<open>\<sqsubseteq>\<close> relation defined as the inverse
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    43
  of the original one.
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    44
\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    45
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    46
datatype 'a dual = dual 'a
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    47
39246
9e58f0499f57 modernized primrec
haftmann
parents: 37678
diff changeset
    48
primrec undual :: "'a dual \<Rightarrow> 'a" where
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    49
  undual_dual: "undual (dual x) = x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    50
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    51
instantiation dual :: (leq) leq
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    52
begin
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    53
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    54
definition
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    55
  leq_dual_def: "x' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    56
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    57
instance ..
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    58
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    59
end
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
    60
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    61
lemma undual_leq [iff?]: "(undual x' \<sqsubseteq> undual y') = (y' \<sqsubseteq> x')"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    62
  by (simp add: leq_dual_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    63
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    64
lemma dual_leq [iff?]: "(dual x \<sqsubseteq> dual y) = (y \<sqsubseteq> x)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    65
  by (simp add: leq_dual_def)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    66
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    67
text \<open>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    68
  \medskip Functions @{term dual} and @{term undual} are inverse to
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    69
  each other; this entails the following fundamental properties.
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    70
\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    71
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    72
lemma dual_undual [simp]: "dual (undual x') = x'"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    73
  by (cases x') simp
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
lemma undual_dual_id [simp]: "undual o dual = id"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    76
  by (rule ext) simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    77
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    78
lemma dual_undual_id [simp]: "dual o undual = id"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    79
  by (rule ext) simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    80
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    81
text \<open>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    82
  \medskip Since @{term dual} (and @{term undual}) are both injective
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    83
  and surjective, the basic logical connectives (equality,
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    84
  quantification etc.) are transferred as follows.
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
    85
\<close>
10157
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 undual_equality [iff?]: "(undual x' = undual y') = (x' = y')"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    88
  by (cases x', cases y') simp
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 dual_equality [iff?]: "(dual x = dual y) = (x = y)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    91
  by simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    92
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10309
diff changeset
    93
lemma dual_ball [iff?]: "(\<forall>x \<in> A. P (dual x)) = (\<forall>x' \<in> dual ` A. P x')"
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    94
proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    95
  assume a: "\<forall>x \<in> A. P (dual x)"
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10309
diff changeset
    96
  show "\<forall>x' \<in> dual ` A. P x'"
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    97
  proof
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10309
diff changeset
    98
    fix x' assume x': "x' \<in> dual ` A"
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
    99
    have "undual x' \<in> A"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   100
    proof -
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10309
diff changeset
   101
      from x' have "undual x' \<in> undual ` dual ` A" by simp
56154
f0a927235162 more complete set of lemmas wrt. image and composition
haftmann
parents: 40702
diff changeset
   102
      thus "undual x' \<in> A" by (simp add: image_comp)
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   103
    qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   104
    with a have "P (dual (undual x'))" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   105
    also have "\<dots> = x'" by simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   106
    finally show "P x'" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   107
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   108
next
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10309
diff changeset
   109
  assume a: "\<forall>x' \<in> dual ` A. P x'"
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   110
  show "\<forall>x \<in> A. P (dual x)"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   111
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   112
    fix x assume "x \<in> A"
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10309
diff changeset
   113
    hence "dual x \<in> dual ` A" by simp
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   114
    with a show "P (dual x)" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   115
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   116
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   117
40702
cf26dd7395e4 Replace surj by abbreviation; remove surj_on.
hoelzl
parents: 39246
diff changeset
   118
lemma range_dual [simp]: "surj dual"
cf26dd7395e4 Replace surj by abbreviation; remove surj_on.
hoelzl
parents: 39246
diff changeset
   119
proof -
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   120
  have "\<And>x'. dual (undual x') = x'" by simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   121
  thus "surj dual" by (rule surjI)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   122
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   123
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   124
lemma dual_all [iff?]: "(\<forall>x. P (dual x)) = (\<forall>x'. P x')"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   125
proof -
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10309
diff changeset
   126
  have "(\<forall>x \<in> UNIV. P (dual x)) = (\<forall>x' \<in> dual ` UNIV. P x')"
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   127
    by (rule dual_ball)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   128
  thus ?thesis by simp
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   129
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   130
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   131
lemma dual_ex: "(\<exists>x. P (dual x)) = (\<exists>x'. P x')"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   132
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   133
  have "(\<forall>x. \<not> P (dual x)) = (\<forall>x'. \<not> P x')"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   134
    by (rule dual_all)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   135
  thus ?thesis by blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   136
qed
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
lemma dual_Collect: "{dual x| x. P (dual x)} = {x'. P x'}"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   139
proof -
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   140
  have "{dual x| x. P (dual x)} = {x'. \<exists>x''. x' = x'' \<and> P x''}"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   141
    by (simp only: dual_ex [symmetric])
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   142
  thus ?thesis by blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   143
qed
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
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   146
subsection \<open>Transforming orders\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   147
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   148
subsubsection \<open>Duals\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   149
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   150
text \<open>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   151
  The classes of quasi, partial, and linear orders are all closed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   152
  under formation of dual structures.
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   153
\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   154
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   155
instance dual :: (quasi_order) quasi_order
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10157
diff changeset
   156
proof
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   157
  fix x' y' z' :: "'a::quasi_order dual"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   158
  have "undual x' \<sqsubseteq> undual x'" .. thus "x' \<sqsubseteq> x'" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   159
  assume "y' \<sqsubseteq> z'" hence "undual z' \<sqsubseteq> undual y'" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   160
  also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   161
  finally show "x' \<sqsubseteq> z'" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   162
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   163
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   164
instance dual :: (partial_order) partial_order
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10157
diff changeset
   165
proof
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   166
  fix x' y' :: "'a::partial_order dual"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   167
  assume "y' \<sqsubseteq> x'" hence "undual x' \<sqsubseteq> undual y'" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   168
  also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   169
  finally show "x' = y'" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   170
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   171
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   172
instance dual :: (linear_order) linear_order
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10157
diff changeset
   173
proof
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   174
  fix x' y' :: "'a::linear_order dual"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   175
  show "x' \<sqsubseteq> y' \<or> y' \<sqsubseteq> x'"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   176
  proof (rule linear_order_cases)
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   177
    assume "undual y' \<sqsubseteq> undual x'"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   178
    hence "x' \<sqsubseteq> y'" .. thus ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   179
  next
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   180
    assume "undual x' \<sqsubseteq> undual y'"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   181
    hence "y' \<sqsubseteq> x'" .. thus ?thesis ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   182
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   183
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   184
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   185
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   186
subsubsection \<open>Binary products \label{sec:prod-order}\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   187
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   188
text \<open>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   189
  The classes of quasi and partial orders are closed under binary
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   190
  products.  Note that the direct product of linear orders need
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   191
  \emph{not} be linear in general.
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   192
\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   193
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 35317
diff changeset
   194
instantiation prod :: (leq, leq) leq
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   195
begin
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   196
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   197
definition
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   198
  leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   199
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   200
instance ..
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   201
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   202
end
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   203
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   204
lemma leq_prodI [intro?]:
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   205
    "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   206
  by (unfold leq_prod_def) blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   207
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   208
lemma leq_prodE [elim?]:
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   209
    "p \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> C"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   210
  by (unfold leq_prod_def) blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   211
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 35317
diff changeset
   212
instance prod :: (quasi_order, quasi_order) quasi_order
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10157
diff changeset
   213
proof
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   214
  fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   215
  show "p \<sqsubseteq> p"
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
    show "fst p \<sqsubseteq> fst p" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   218
    show "snd p \<sqsubseteq> snd p" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   219
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   220
  assume pq: "p \<sqsubseteq> q" and qr: "q \<sqsubseteq> r"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   221
  show "p \<sqsubseteq> r"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   222
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   223
    from pq have "fst p \<sqsubseteq> fst q" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   224
    also from qr have "\<dots> \<sqsubseteq> fst r" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   225
    finally show "fst p \<sqsubseteq> fst r" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   226
    from pq have "snd p \<sqsubseteq> snd q" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   227
    also from qr have "\<dots> \<sqsubseteq> snd r" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   228
    finally show "snd p \<sqsubseteq> snd r" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   229
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   230
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   231
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 35317
diff changeset
   232
instance prod :: (partial_order, partial_order) partial_order
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10157
diff changeset
   233
proof
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   234
  fix p q :: "'a::partial_order \<times> 'b::partial_order"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   235
  assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   236
  show "p = q"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   237
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   238
    from pq have "fst p \<sqsubseteq> fst q" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   239
    also from qp have "\<dots> \<sqsubseteq> fst p" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   240
    finally show "fst p = fst q" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   241
    from pq have "snd p \<sqsubseteq> snd q" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   242
    also from qp have "\<dots> \<sqsubseteq> snd p" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   243
    finally show "snd p = snd q" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   244
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   245
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   246
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   247
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   248
subsubsection \<open>General products \label{sec:fun-order}\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   249
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   250
text \<open>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   251
  The classes of quasi and partial orders are closed under general
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   252
  products (function spaces).  Note that the direct product of linear
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   253
  orders need \emph{not} be linear in general.
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61983
diff changeset
   254
\<close>
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   255
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   256
instantiation "fun" :: (type, leq) leq
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   257
begin
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   258
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   259
definition
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   260
  leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   261
35317
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   262
instance ..
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   263
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   264
end
d57da4abb47d dropped axclass; dropped Id
haftmann
parents: 21210
diff changeset
   265
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   266
lemma leq_funI [intro?]: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   267
  by (unfold leq_fun_def) blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   268
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   269
lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   270
  by (unfold leq_fun_def) blast
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   271
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19736
diff changeset
   272
instance "fun" :: (type, quasi_order) quasi_order
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10157
diff changeset
   273
proof
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   274
  fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   275
  show "f \<sqsubseteq> f"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   276
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   277
    fix x show "f x \<sqsubseteq> f x" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   278
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   279
  assume fg: "f \<sqsubseteq> g" and gh: "g \<sqsubseteq> h"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   280
  show "f \<sqsubseteq> h"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   281
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   282
    fix x from fg have "f x \<sqsubseteq> g x" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   283
    also from gh have "\<dots> \<sqsubseteq> h x" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   284
    finally show "f x \<sqsubseteq> h x" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   285
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   286
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   287
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19736
diff changeset
   288
instance "fun" :: (type, partial_order) partial_order
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10157
diff changeset
   289
proof
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   290
  fix f g :: "'a \<Rightarrow> 'b::partial_order"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   291
  assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   292
  show "f = g"
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   293
  proof
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   294
    fix x from fg have "f x \<sqsubseteq> g x" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   295
    also from gf have "\<dots> \<sqsubseteq> f x" ..
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   296
    finally show "f x = g x" .
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   297
  qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   298
qed
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   299
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff changeset
   300
end