1 (*  Title:      HOL/Library/Product_ord.thy

     2     Author:     Norbert Voelker

     3 *)

     4 

     5 header {* Order on product types *}

     6 

     7 theory Precedence_ord

     8 imports Main

     9 begin

    10 

    11 datatype precedence = Prc nat nat

    12 

    13 instantiation precedence :: order

    14 begin

    15 

    16 definition

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

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

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

    20 

    21 definition

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

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

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

    25 

    26 instance

    27 proof

    28 qed (auto simp: precedence_le_def precedence_less_def 

    29               intro: order_trans split:precedence.splits)

    30 end

    31 

    32 instance precedence :: preorder ..

    33 

    34 instance precedence :: linorder proof

    35 qed (auto simp: precedence_le_def precedence_less_def 

    36               intro: order_trans split:precedence.splits)

    37 

    38 end