src/HOL/Library/Product_Lexorder.thy
author wenzelm
Mon Dec 28 17:43:30 2015 +0100 (2015-12-28)
changeset 61952 546958347e05
parent 60679 ade12ef2773c
permissions -rw-r--r--
prefer symbols for "Union", "Inter";
     1 (*  Title:      HOL/Library/Product_Lexorder.thy
     2     Author:     Norbert Voelker
     3 *)
     4 
     5 section \<open>Lexicographic order on product types\<close>
     6 
     7 theory Product_Lexorder
     8 imports Main
     9 begin
    10 
    11 instantiation prod :: (ord, ord) ord
    12 begin
    13 
    14 definition
    15   "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
    16 
    17 definition
    18   "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 less_eq_prod_simp [simp, code]:
    25   "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
    26   by (simp add: less_eq_prod_def)
    27 
    28 lemma less_prod_simp [simp, code]:
    29   "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
    30   by (simp add: less_prod_def)
    31 
    32 text \<open>A stronger version for partial orders.\<close>
    33 
    34 lemma less_prod_def':
    35   fixes x y :: "'a::order \<times> 'b::ord"
    36   shows "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
    37   by (auto simp add: less_prod_def le_less)
    38 
    39 instance prod :: (preorder, preorder) preorder
    40   by standard (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
    41 
    42 instance prod :: (order, order) order
    43   by standard (auto simp add: less_eq_prod_def)
    44 
    45 instance prod :: (linorder, linorder) linorder
    46   by standard (auto simp: less_eq_prod_def)
    47 
    48 instantiation prod :: (linorder, linorder) distrib_lattice
    49 begin
    50 
    51 definition
    52   "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
    53 
    54 definition
    55   "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    56 
    57 instance
    58   by standard (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
    59 
    60 end
    61 
    62 instantiation prod :: (bot, bot) bot
    63 begin
    64 
    65 definition
    66   "bot = (bot, bot)"
    67 
    68 instance ..
    69 
    70 end
    71 
    72 instance prod :: (order_bot, order_bot) order_bot
    73   by standard (auto simp add: bot_prod_def)
    74 
    75 instantiation prod :: (top, top) top
    76 begin
    77 
    78 definition
    79   "top = (top, top)"
    80 
    81 instance ..
    82 
    83 end
    84 
    85 instance prod :: (order_top, order_top) order_top
    86   by standard (auto simp add: top_prod_def)
    87 
    88 instance prod :: (wellorder, wellorder) wellorder
    89 proof
    90   fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
    91   assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
    92   show "P z"
    93   proof (induct z)
    94     case (Pair a b)
    95     show "P (a, b)"
    96     proof (induct a arbitrary: b rule: less_induct)
    97       case (less a\<^sub>1) note a\<^sub>1 = this
    98       show "P (a\<^sub>1, b)"
    99       proof (induct b rule: less_induct)
   100         case (less b\<^sub>1) note b\<^sub>1 = this
   101         show "P (a\<^sub>1, b\<^sub>1)"
   102         proof (rule P)
   103           fix p assume p: "p < (a\<^sub>1, b\<^sub>1)"
   104           show "P p"
   105           proof (cases "fst p < a\<^sub>1")
   106             case True
   107             then have "P (fst p, snd p)" by (rule a\<^sub>1)
   108             then show ?thesis by simp
   109           next
   110             case False
   111             with p have 1: "a\<^sub>1 = fst p" and 2: "snd p < b\<^sub>1"
   112               by (simp_all add: less_prod_def')
   113             from 2 have "P (a\<^sub>1, snd p)" by (rule b\<^sub>1)
   114             with 1 show ?thesis by simp
   115           qed
   116         qed
   117       qed
   118     qed
   119   qed
   120 qed
   121 
   122 text \<open>Legacy lemma bindings\<close>
   123 
   124 lemmas prod_le_def = less_eq_prod_def
   125 lemmas prod_less_def = less_prod_def
   126 lemmas prod_less_eq = less_prod_def'
   127 
   128 end
   129