src/HOL/Lattice/Orders.thy
 author haftmann Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) changeset 37659 14cabf5fa710 parent 35317 d57da4abb47d child 37678 0040bafffdef permissions -rw-r--r--
more speaking names
     1 (*  Title:      HOL/Lattice/Orders.thy

     2     Author:     Markus Wenzel, TU Muenchen

     3 *)

     4

     5 header {* Orders *}

     6

     7 theory Orders imports Main begin

     8

     9 subsection {* Ordered structures *}

    10

    11 text {*

    12   We define several classes of ordered structures over some type @{typ

    13   'a} with relation @{text "\<sqsubseteq> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool"}.  For a

    14   \emph{quasi-order} that relation is required to be reflexive and

    15   transitive, for a \emph{partial order} it also has to be

    16   anti-symmetric, while for a \emph{linear order} all elements are

    17   required to be related (in either direction).

    18 *}

    19

    20 class leq =

    21   fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)

    22

    23 notation (xsymbols)

    24   leq  (infixl "\<sqsubseteq>" 50)

    25

    26 class quasi_order = leq +

    27   assumes leq_refl [intro?]: "x \<sqsubseteq> x"

    28   assumes leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"

    29

    30 class partial_order = quasi_order +

    31   assumes leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"

    32

    33 class linear_order = partial_order +

    34   assumes leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"

    35

    36 lemma linear_order_cases:

    37     "((x::'a::linear_order) \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> (y \<sqsubseteq> x \<Longrightarrow> C) \<Longrightarrow> C"

    38   by (insert leq_linear) blast

    39

    40

    41 subsection {* Duality *}

    42

    43 text {*

    44   The \emph{dual} of an ordered structure is an isomorphic copy of the

    45   underlying type, with the @{text \<sqsubseteq>} relation defined as the inverse

    46   of the original one.

    47 *}

    48

    49 datatype 'a dual = dual 'a

    50

    51 consts

    52   undual :: "'a dual \<Rightarrow> 'a"

    53 primrec

    54   undual_dual: "undual (dual x) = x"

    55

    56 instantiation dual :: (leq) leq

    57 begin

    58

    59 definition

    60   leq_dual_def: "x' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"

    61

    62 instance ..

    63

    64 end

    65

    66 lemma undual_leq [iff?]: "(undual x' \<sqsubseteq> undual y') = (y' \<sqsubseteq> x')"

    67   by (simp add: leq_dual_def)

    68

    69 lemma dual_leq [iff?]: "(dual x \<sqsubseteq> dual y) = (y \<sqsubseteq> x)"

    70   by (simp add: leq_dual_def)

    71

    72 text {*

    73   \medskip Functions @{term dual} and @{term undual} are inverse to

    74   each other; this entails the following fundamental properties.

    75 *}

    76

    77 lemma dual_undual [simp]: "dual (undual x') = x'"

    78   by (cases x') simp

    79

    80 lemma undual_dual_id [simp]: "undual o dual = id"

    81   by (rule ext) simp

    82

    83 lemma dual_undual_id [simp]: "dual o undual = id"

    84   by (rule ext) simp

    85

    86 text {*

    87   \medskip Since @{term dual} (and @{term undual}) are both injective

    88   and surjective, the basic logical connectives (equality,

    89   quantification etc.) are transferred as follows.

    90 *}

    91

    92 lemma undual_equality [iff?]: "(undual x' = undual y') = (x' = y')"

    93   by (cases x', cases y') simp

    94

    95 lemma dual_equality [iff?]: "(dual x = dual y) = (x = y)"

    96   by simp

    97

    98 lemma dual_ball [iff?]: "(\<forall>x \<in> A. P (dual x)) = (\<forall>x' \<in> dual  A. P x')"

    99 proof

   100   assume a: "\<forall>x \<in> A. P (dual x)"

   101   show "\<forall>x' \<in> dual  A. P x'"

   102   proof

   103     fix x' assume x': "x' \<in> dual  A"

   104     have "undual x' \<in> A"

   105     proof -

   106       from x' have "undual x' \<in> undual  dual  A" by simp

   107       thus "undual x' \<in> A" by (simp add: image_compose [symmetric])

   108     qed

   109     with a have "P (dual (undual x'))" ..

   110     also have "\<dots> = x'" by simp

   111     finally show "P x'" .

   112   qed

   113 next

   114   assume a: "\<forall>x' \<in> dual  A. P x'"

   115   show "\<forall>x \<in> A. P (dual x)"

   116   proof

   117     fix x assume "x \<in> A"

   118     hence "dual x \<in> dual  A" by simp

   119     with a show "P (dual x)" ..

   120   qed

   121 qed

   122

   123 lemma range_dual [simp]: "dual  UNIV = UNIV"

   124 proof (rule surj_range)

   125   have "\<And>x'. dual (undual x') = x'" by simp

   126   thus "surj dual" by (rule surjI)

   127 qed

   128

   129 lemma dual_all [iff?]: "(\<forall>x. P (dual x)) = (\<forall>x'. P x')"

   130 proof -

   131   have "(\<forall>x \<in> UNIV. P (dual x)) = (\<forall>x' \<in> dual  UNIV. P x')"

   132     by (rule dual_ball)

   133   thus ?thesis by simp

   134 qed

   135

   136 lemma dual_ex: "(\<exists>x. P (dual x)) = (\<exists>x'. P x')"

   137 proof -

   138   have "(\<forall>x. \<not> P (dual x)) = (\<forall>x'. \<not> P x')"

   139     by (rule dual_all)

   140   thus ?thesis by blast

   141 qed

   142

   143 lemma dual_Collect: "{dual x| x. P (dual x)} = {x'. P x'}"

   144 proof -

   145   have "{dual x| x. P (dual x)} = {x'. \<exists>x''. x' = x'' \<and> P x''}"

   146     by (simp only: dual_ex [symmetric])

   147   thus ?thesis by blast

   148 qed

   149

   150

   151 subsection {* Transforming orders *}

   152

   153 subsubsection {* Duals *}

   154

   155 text {*

   156   The classes of quasi, partial, and linear orders are all closed

   157   under formation of dual structures.

   158 *}

   159

   160 instance dual :: (quasi_order) quasi_order

   161 proof

   162   fix x' y' z' :: "'a::quasi_order dual"

   163   have "undual x' \<sqsubseteq> undual x'" .. thus "x' \<sqsubseteq> x'" ..

   164   assume "y' \<sqsubseteq> z'" hence "undual z' \<sqsubseteq> undual y'" ..

   165   also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..

   166   finally show "x' \<sqsubseteq> z'" ..

   167 qed

   168

   169 instance dual :: (partial_order) partial_order

   170 proof

   171   fix x' y' :: "'a::partial_order dual"

   172   assume "y' \<sqsubseteq> x'" hence "undual x' \<sqsubseteq> undual y'" ..

   173   also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..

   174   finally show "x' = y'" ..

   175 qed

   176

   177 instance dual :: (linear_order) linear_order

   178 proof

   179   fix x' y' :: "'a::linear_order dual"

   180   show "x' \<sqsubseteq> y' \<or> y' \<sqsubseteq> x'"

   181   proof (rule linear_order_cases)

   182     assume "undual y' \<sqsubseteq> undual x'"

   183     hence "x' \<sqsubseteq> y'" .. thus ?thesis ..

   184   next

   185     assume "undual x' \<sqsubseteq> undual y'"

   186     hence "y' \<sqsubseteq> x'" .. thus ?thesis ..

   187   qed

   188 qed

   189

   190

   191 subsubsection {* Binary products \label{sec:prod-order} *}

   192

   193 text {*

   194   The classes of quasi and partial orders are closed under binary

   195   products.  Note that the direct product of linear orders need

   196   \emph{not} be linear in general.

   197 *}

   198

   199 instantiation * :: (leq, leq) leq

   200 begin

   201

   202 definition

   203   leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"

   204

   205 instance ..

   206

   207 end

   208

   209 lemma leq_prodI [intro?]:

   210     "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q"

   211   by (unfold leq_prod_def) blast

   212

   213 lemma leq_prodE [elim?]:

   214     "p \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> C"

   215   by (unfold leq_prod_def) blast

   216

   217 instance * :: (quasi_order, quasi_order) quasi_order

   218 proof

   219   fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"

   220   show "p \<sqsubseteq> p"

   221   proof

   222     show "fst p \<sqsubseteq> fst p" ..

   223     show "snd p \<sqsubseteq> snd p" ..

   224   qed

   225   assume pq: "p \<sqsubseteq> q" and qr: "q \<sqsubseteq> r"

   226   show "p \<sqsubseteq> r"

   227   proof

   228     from pq have "fst p \<sqsubseteq> fst q" ..

   229     also from qr have "\<dots> \<sqsubseteq> fst r" ..

   230     finally show "fst p \<sqsubseteq> fst r" .

   231     from pq have "snd p \<sqsubseteq> snd q" ..

   232     also from qr have "\<dots> \<sqsubseteq> snd r" ..

   233     finally show "snd p \<sqsubseteq> snd r" .

   234   qed

   235 qed

   236

   237 instance * :: (partial_order, partial_order) partial_order

   238 proof

   239   fix p q :: "'a::partial_order \<times> 'b::partial_order"

   240   assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"

   241   show "p = q"

   242   proof

   243     from pq have "fst p \<sqsubseteq> fst q" ..

   244     also from qp have "\<dots> \<sqsubseteq> fst p" ..

   245     finally show "fst p = fst q" .

   246     from pq have "snd p \<sqsubseteq> snd q" ..

   247     also from qp have "\<dots> \<sqsubseteq> snd p" ..

   248     finally show "snd p = snd q" .

   249   qed

   250 qed

   251

   252

   253 subsubsection {* General products \label{sec:fun-order} *}

   254

   255 text {*

   256   The classes of quasi and partial orders are closed under general

   257   products (function spaces).  Note that the direct product of linear

   258   orders need \emph{not} be linear in general.

   259 *}

   260

   261 instantiation "fun" :: (type, leq) leq

   262 begin

   263

   264 definition

   265   leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"

   266

   267 instance ..

   268

   269 end

   270

   271 lemma leq_funI [intro?]: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"

   272   by (unfold leq_fun_def) blast

   273

   274 lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"

   275   by (unfold leq_fun_def) blast

   276

   277 instance "fun" :: (type, quasi_order) quasi_order

   278 proof

   279   fix f g h :: "'a \<Rightarrow> 'b::quasi_order"

   280   show "f \<sqsubseteq> f"

   281   proof

   282     fix x show "f x \<sqsubseteq> f x" ..

   283   qed

   284   assume fg: "f \<sqsubseteq> g" and gh: "g \<sqsubseteq> h"

   285   show "f \<sqsubseteq> h"

   286   proof

   287     fix x from fg have "f x \<sqsubseteq> g x" ..

   288     also from gh have "\<dots> \<sqsubseteq> h x" ..

   289     finally show "f x \<sqsubseteq> h x" .

   290   qed

   291 qed

   292

   293 instance "fun" :: (type, partial_order) partial_order

   294 proof

   295   fix f g :: "'a \<Rightarrow> 'b::partial_order"

   296   assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"

   297   show "f = g"

   298   proof

   299     fix x from fg have "f x \<sqsubseteq> g x" ..

   300     also from gf have "\<dots> \<sqsubseteq> f x" ..

   301     finally show "f x = g x" .

   302   qed

   303 qed

   304

   305 end
`