1 header {* Order on product types *}

     2 

     3 theory Precedence_ord

     4 imports Main

     5 begin

     6 

     7 datatype precedence = Prc nat nat

     8 

     9 instantiation precedence :: order

    10 begin

    11 

    12 definition

    13   precedence_le_def: "x \<le> y \<longleftrightarrow> (case (x, y) of

    14                                    (Prc fx sx, Prc fy sy) \<Rightarrow> 

    15                                  fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))"

    16 

    17 definition

    18   precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of

    19                                (Prc fx sx, Prc fy sy) \<Rightarrow> 

    20                                      fx < fy \<or> (fx \<le> fy \<and> sy < sx))"

    21 

    22 instance

    23 proof

    24 qed (auto simp: precedence_le_def precedence_less_def 

    25               intro: order_trans split:precedence.splits)

    26 end

    27 

    28 instance precedence :: preorder ..

    29 

    30 instance precedence :: linorder 

    31 proof

    32 qed (auto simp: precedence_le_def precedence_less_def 

    33               intro: order_trans split:precedence.splits)

    34 

    35 instantiation precedence :: zero

    36 begin

    37 

    38 definition Zero_precedence_def:

    39   "0 = Prc 0 0"

    40 

    41 instance ..

    42 

    43 end

    44 

    45 end