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