header {* Order on product types *}

theory Precedence_ord
imports Main
begin

datatype precedence = Prc nat nat

instantiation precedence :: order
begin

definition
  precedence_le_def: "x \<le> y \<longleftrightarrow> (case (x, y) of
                                   (Prc fx sx, Prc fy sy) \<Rightarrow> 
                                 fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))"

lemma preced_leI1[intro]: 
  assumes "fx < fy"
  shows "Prc fx sx \<le> Prc fy sy"
  using assms
  by (simp add: precedence_le_def) 

lemma preced_leI2[intro]: 
  assumes "fx \<le> fy"
  and "sy \<le> sx"
  shows "Prc fx sx \<le> Prc fy sy"
  using assms
  by (simp add: precedence_le_def) 

definition
  precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of
                               (Prc fx sx, Prc fy sy) \<Rightarrow> 
                                     fx < fy \<or> (fx \<le> fy \<and> sy < sx))"

instance
proof
qed (auto simp: precedence_le_def precedence_less_def 
              intro: order_trans split:precedence.splits)
end

instance precedence :: preorder ..

instance precedence :: linorder 
proof
qed (auto simp: precedence_le_def precedence_less_def 
              intro: order_trans split:precedence.splits)

instantiation precedence :: zero
begin

definition Zero_precedence_def:
  "0 = Prc 0 0"

instance ..

end

end