--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Precedence_ord.thy~	Thu Jan 07 08:33:13 2016 +0800
@@ -0,0 +1,45 @@
+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))"
+
+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