src/HOL/Library/Product_Lexorder.thy
 author haftmann Wed Jul 18 20:51:21 2018 +0200 (11 months ago) changeset 68658 16cc1161ad7f parent 60679 ade12ef2773c permissions -rw-r--r--
tuned equation
```     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
```