# Theory Orders

theory Orders
imports Main

section

theory Orders imports Main begin

subsection

text

class leq =
fixes leq ::   (infixl  50)

class quasi_order = leq +
assumes leq_refl [intro?]:
assumes leq_trans [trans]:

class partial_order = quasi_order +
assumes leq_antisym [trans]:

class linear_order = partial_order +
assumes leq_linear:

lemma linear_order_cases:

by (insert leq_linear) blast

subsection

text

datatype 'a dual = dual 'a

primrec undual ::  where
undual_dual:

instantiation dual :: (leq) leq
begin

definition
leq_dual_def:

instance ..

end

lemma undual_leq [iff?]:

lemma dual_leq [iff?]:

text

lemma dual_undual [simp]:
by (cases x') simp

lemma undual_dual_id [simp]:
by (rule ext) simp

lemma dual_undual_id [simp]:
by (rule ext) simp

text

lemma undual_equality [iff?]:
by (cases x', cases y') simp

lemma dual_equality [iff?]:
by simp

lemma dual_ball [iff?]:
proof
assume a:
show
proof
fix x' assume x':
have
proof -
from x' have  by simp
qed
with a have  ..
also have  by simp
finally show  .
qed
next
assume a:
show
proof
fix x assume
hence  by simp
with a show  ..
qed
qed

lemma range_dual [simp]:
proof -
have  by simp
thus  by (rule surjI)
qed

lemma dual_all [iff?]:
proof -
have
by (rule dual_ball)
thus ?thesis by simp
qed

lemma dual_ex:
proof -
have
by (rule dual_all)
thus ?thesis by blast
qed

lemma dual_Collect:
proof -
have
by (simp only: dual_ex [symmetric])
thus ?thesis by blast
qed

subsection

subsubsection

text

instance dual :: (quasi_order) quasi_order
proof
fix x' y' z' ::
have  .. thus  ..
assume  hence  ..
also assume  hence  ..
finally show  ..
qed

instance dual :: (partial_order) partial_order
proof
fix x' y' ::
assume  hence  ..
also assume  hence  ..
finally show  ..
qed

instance dual :: (linear_order) linear_order
proof
fix x' y' ::
show
proof (rule linear_order_cases)
assume
hence  .. thus ?thesis ..
next
assume
hence  .. thus ?thesis ..
qed
qed

subsubsection

text

instantiation prod :: (leq, leq) leq
begin

definition
leq_prod_def:

instance ..

end

lemma leq_prodI [intro?]:

by (unfold leq_prod_def) blast

lemma leq_prodE [elim?]:

by (unfold leq_prod_def) blast

instance prod :: (quasi_order, quasi_order) quasi_order
proof
fix p q r ::
show
proof
show  ..
show  ..
qed
assume pq:  and qr:
show
proof
from pq have  ..
also from qr have  ..
finally show  .
from pq have  ..
also from qr have  ..
finally show  .
qed
qed

instance prod :: (partial_order, partial_order) partial_order
proof
fix p q ::
assume pq:  and qp:
show
proof
from pq have  ..
also from qp have  ..
finally show  .
from pq have  ..
also from qp have  ..
finally show  .
qed
qed

subsubsection

text

instantiation  :: (type, leq) leq
begin

definition
leq_fun_def:

instance ..

end

lemma leq_funI [intro?]:
by (unfold leq_fun_def) blast

lemma leq_funD [dest?]:
by (unfold leq_fun_def) blast

instance  :: (type, quasi_order) quasi_order
proof
fix f g h ::
show
proof
fix x show  ..
qed
assume fg:  and gh:
show
proof
fix x from fg have  ..
also from gh have  ..
finally show  .
qed
qed

instance  :: (type, partial_order) partial_order
proof
fix f g ::
assume fg:  and gf:
show
proof
fix x from fg have  ..
also from gf have  ..
finally show  .
qed
qed

end