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