src/HOL/Library/Product_ord.thy
author wenzelm
Wed Sep 12 13:42:28 2012 +0200 (2012-09-12)
changeset 49322 fbb320d02420
parent 47961 e0a85be4fca0
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Library/Product_ord.thy
     2     Author:     Norbert Voelker
     3 *)
     4 
     5 header {* Order on product types *}
     6 
     7 theory Product_ord
     8 imports Main
     9 begin
    10 
    11 instantiation prod :: (ord, ord) ord
    12 begin
    13 
    14 definition
    15   prod_le_def: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
    16 
    17 definition
    18   prod_less_def: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
    19 
    20 instance ..
    21 
    22 end
    23 
    24 lemma [code]:
    25   "(x1::'a::{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
    26   "(x1::'a::{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
    27   unfolding prod_le_def prod_less_def by simp_all
    28 
    29 instance prod :: (preorder, preorder) preorder
    30   by default (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
    31 
    32 instance prod :: (order, order) order
    33   by default (auto simp add: prod_le_def)
    34 
    35 instance prod :: (linorder, linorder) linorder
    36   by default (auto simp: prod_le_def)
    37 
    38 instantiation prod :: (linorder, linorder) distrib_lattice
    39 begin
    40 
    41 definition
    42   inf_prod_def: "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
    43 
    44 definition
    45   sup_prod_def: "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    46 
    47 instance
    48   by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    49 
    50 end
    51 
    52 instantiation prod :: (bot, bot) bot
    53 begin
    54 
    55 definition
    56   bot_prod_def: "bot = (bot, bot)"
    57 
    58 instance
    59   by default (auto simp add: bot_prod_def prod_le_def)
    60 
    61 end
    62 
    63 instantiation prod :: (top, top) top
    64 begin
    65 
    66 definition
    67   top_prod_def: "top = (top, top)"
    68 
    69 instance
    70   by default (auto simp add: top_prod_def prod_le_def)
    71 
    72 end
    73 
    74 text {* A stronger version of the definition holds for partial orders. *}
    75 
    76 lemma prod_less_eq:
    77   fixes x y :: "'a::order \<times> 'b::ord"
    78   shows "x < y \<longleftrightarrow> fst x < fst y \<or> (fst x = fst y \<and> snd x < snd y)"
    79   unfolding prod_less_def fst_conv snd_conv le_less by auto
    80 
    81 instance prod :: (wellorder, wellorder) wellorder
    82 proof
    83   fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
    84   assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
    85   show "P z"
    86   proof (induct z)
    87     case (Pair a b)
    88     show "P (a, b)"
    89     proof (induct a arbitrary: b rule: less_induct)
    90       case (less a\<^isub>1) note a\<^isub>1 = this
    91       show "P (a\<^isub>1, b)"
    92       proof (induct b rule: less_induct)
    93         case (less b\<^isub>1) note b\<^isub>1 = this
    94         show "P (a\<^isub>1, b\<^isub>1)"
    95         proof (rule P)
    96           fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
    97           show "P p"
    98           proof (cases "fst p < a\<^isub>1")
    99             case True
   100             then have "P (fst p, snd p)" by (rule a\<^isub>1)
   101             then show ?thesis by simp
   102           next
   103             case False
   104             with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
   105               by (simp_all add: prod_less_eq)
   106             from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
   107             with 1 show ?thesis by simp
   108           qed
   109         qed
   110       qed
   111     qed
   112   qed
   113 qed
   114 
   115 end