author | wenzelm |
Wed, 30 Dec 2015 18:25:39 +0100 | |
changeset 61986 | 2461779da2b8 |
parent 61983 | 8fb53badad99 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
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 | 5 |
section \<open>Orders\<close> |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
6 |
|
16417 | 7 |
theory Orders imports Main begin |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
8 |
|
61986 | 9 |
subsection \<open>Ordered structures\<close> |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
10 |
|
61986 | 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 | 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 | 18 |
\<close> |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
19 |
|
35317 | 20 |
class leq = |
61983 | 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 | 23 |
class quasi_order = leq + |
24 |
assumes leq_refl [intro?]: "x \<sqsubseteq> x" |
|
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 | 27 |
class partial_order = quasi_order + |
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 | 30 |
class linear_order = partial_order + |
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 | 38 |
subsection \<open>Duality\<close> |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
39 |
|
61986 | 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 | 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 | 44 |
\<close> |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
45 |
|
58310 | 46 |
datatype 'a dual = dual 'a |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
47 |
|
39246 | 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 | 51 |
instantiation dual :: (leq) leq |
52 |
begin |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
53 |
|
35317 | 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 | 57 |
instance .. |
58 |
||
59 |
end |
|
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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 118 |
lemma range_dual [simp]: "surj dual" |
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 | 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 | 146 |
subsection \<open>Transforming orders\<close> |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
147 |
|
61986 | 148 |
subsubsection \<open>Duals\<close> |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
149 |
|
61986 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 195 |
begin |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
196 |
|
35317 | 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 | 200 |
instance .. |
201 |
||
202 |
end |
|
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 | 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 | 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 | 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 | 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 | 254 |
\<close> |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
255 |
|
35317 | 256 |
instantiation "fun" :: (type, leq) leq |
257 |
begin |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
258 |
|
35317 | 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 | 262 |
instance .. |
263 |
||
264 |
end |
|
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 | 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 | 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 |