src/HOL/Library/Option_ord.thy
 author Christian Sternagel Thu Aug 30 15:44:03 2012 +0900 (2012-08-30) changeset 49093 fdc301f592c4 parent 43815 4f6e2965d821 child 49190 e1e1d427747d permissions -rw-r--r--
 haftmann@26241 ` 1` ```(* Title: HOL/Library/Option_ord.thy ``` haftmann@26241 ` 2` ``` Author: Florian Haftmann, TU Muenchen ``` haftmann@26241 ` 3` ```*) ``` haftmann@26241 ` 4` haftmann@26263 ` 5` ```header {* Canonical order on option type *} ``` haftmann@26241 ` 6` haftmann@26241 ` 7` ```theory Option_ord ``` haftmann@30662 ` 8` ```imports Option Main ``` haftmann@26241 ` 9` ```begin ``` haftmann@26241 ` 10` haftmann@30662 ` 11` ```instantiation option :: (preorder) preorder ``` haftmann@26241 ` 12` ```begin ``` haftmann@26241 ` 13` haftmann@26241 ` 14` ```definition less_eq_option where ``` haftmann@37765 ` 15` ``` "x \ y \ (case x of None \ True | Some x \ (case y of None \ False | Some y \ x \ y))" ``` haftmann@26241 ` 16` haftmann@26241 ` 17` ```definition less_option where ``` haftmann@37765 ` 18` ``` "x < y \ (case y of None \ False | Some y \ (case x of None \ True | Some x \ x < y))" ``` haftmann@26241 ` 19` haftmann@26258 ` 20` ```lemma less_eq_option_None [simp]: "None \ x" ``` haftmann@26241 ` 21` ``` by (simp add: less_eq_option_def) ``` haftmann@26241 ` 22` haftmann@26258 ` 23` ```lemma less_eq_option_None_code [code]: "None \ x \ True" ``` haftmann@26241 ` 24` ``` by simp ``` haftmann@26241 ` 25` haftmann@26258 ` 26` ```lemma less_eq_option_None_is_None: "x \ None \ x = None" ``` haftmann@26241 ` 27` ``` by (cases x) (simp_all add: less_eq_option_def) ``` haftmann@26241 ` 28` haftmann@26258 ` 29` ```lemma less_eq_option_Some_None [simp, code]: "Some x \ None \ False" ``` haftmann@26241 ` 30` ``` by (simp add: less_eq_option_def) ``` haftmann@26241 ` 31` haftmann@26258 ` 32` ```lemma less_eq_option_Some [simp, code]: "Some x \ Some y \ x \ y" ``` haftmann@26241 ` 33` ``` by (simp add: less_eq_option_def) ``` haftmann@26241 ` 34` haftmann@26258 ` 35` ```lemma less_option_None [simp, code]: "x < None \ False" ``` haftmann@26241 ` 36` ``` by (simp add: less_option_def) ``` haftmann@26241 ` 37` haftmann@26258 ` 38` ```lemma less_option_None_is_Some: "None < x \ \z. x = Some z" ``` haftmann@26241 ` 39` ``` by (cases x) (simp_all add: less_option_def) ``` haftmann@26241 ` 40` haftmann@26258 ` 41` ```lemma less_option_None_Some [simp]: "None < Some x" ``` haftmann@26241 ` 42` ``` by (simp add: less_option_def) ``` haftmann@26241 ` 43` haftmann@26258 ` 44` ```lemma less_option_None_Some_code [code]: "None < Some x \ True" ``` haftmann@26241 ` 45` ``` by simp ``` haftmann@26241 ` 46` haftmann@26258 ` 47` ```lemma less_option_Some [simp, code]: "Some x < Some y \ x < y" ``` haftmann@26241 ` 48` ``` by (simp add: less_option_def) ``` haftmann@26241 ` 49` haftmann@30662 ` 50` ```instance proof ``` haftmann@30662 ` 51` ```qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits) ``` haftmann@26241 ` 52` haftmann@26241 ` 53` ```end ``` haftmann@26241 ` 54` haftmann@30662 ` 55` ```instance option :: (order) order proof ``` haftmann@30662 ` 56` ```qed (auto simp add: less_eq_option_def less_option_def split: option.splits) ``` haftmann@30662 ` 57` haftmann@30662 ` 58` ```instance option :: (linorder) linorder proof ``` haftmann@30662 ` 59` ```qed (auto simp add: less_eq_option_def less_option_def split: option.splits) ``` haftmann@30662 ` 60` haftmann@43815 ` 61` ```instantiation option :: (order) bot ``` haftmann@30662 ` 62` ```begin ``` haftmann@30662 ` 63` haftmann@30662 ` 64` ```definition "bot = None" ``` haftmann@30662 ` 65` haftmann@30662 ` 66` ```instance proof ``` haftmann@30662 ` 67` ```qed (simp add: bot_option_def) ``` haftmann@30662 ` 68` haftmann@30662 ` 69` ```end ``` haftmann@30662 ` 70` haftmann@30662 ` 71` ```instantiation option :: (top) top ``` haftmann@30662 ` 72` ```begin ``` haftmann@30662 ` 73` haftmann@30662 ` 74` ```definition "top = Some top" ``` haftmann@30662 ` 75` haftmann@30662 ` 76` ```instance proof ``` haftmann@30662 ` 77` ```qed (simp add: top_option_def less_eq_option_def split: option.split) ``` haftmann@26241 ` 78` haftmann@26241 ` 79` ```end ``` haftmann@30662 ` 80` haftmann@30662 ` 81` ```instance option :: (wellorder) wellorder proof ``` haftmann@30662 ` 82` ``` fix P :: "'a option \ bool" and z :: "'a option" ``` haftmann@30662 ` 83` ``` assume H: "\x. (\y. y < x \ P y) \ P x" ``` haftmann@30662 ` 84` ``` have "P None" by (rule H) simp ``` haftmann@30662 ` 85` ``` then have P_Some [case_names Some]: ``` haftmann@30662 ` 86` ``` "\z. (\x. z = Some x \ (P o Some) x) \ P z" ``` haftmann@30662 ` 87` ``` proof - ``` haftmann@30662 ` 88` ``` fix z ``` haftmann@30662 ` 89` ``` assume "\x. z = Some x \ (P o Some) x" ``` haftmann@30662 ` 90` ``` with `P None` show "P z" by (cases z) simp_all ``` haftmann@30662 ` 91` ``` qed ``` haftmann@30662 ` 92` ``` show "P z" proof (cases z rule: P_Some) ``` haftmann@30662 ` 93` ``` case (Some w) ``` haftmann@30662 ` 94` ``` show "(P o Some) w" proof (induct rule: less_induct) ``` haftmann@30662 ` 95` ``` case (less x) ``` haftmann@30662 ` 96` ``` have "P (Some x)" proof (rule H) ``` haftmann@30662 ` 97` ``` fix y :: "'a option" ``` haftmann@30662 ` 98` ``` assume "y < Some x" ``` haftmann@30662 ` 99` ``` show "P y" proof (cases y rule: P_Some) ``` haftmann@30662 ` 100` ``` case (Some v) with `y < Some x` have "v < x" by simp ``` haftmann@30662 ` 101` ``` with less show "(P o Some) v" . ``` haftmann@30662 ` 102` ``` qed ``` haftmann@30662 ` 103` ``` qed ``` haftmann@30662 ` 104` ``` then show ?case by simp ``` haftmann@30662 ` 105` ``` qed ``` haftmann@30662 ` 106` ``` qed ``` haftmann@30662 ` 107` ```qed ``` haftmann@30662 ` 108` haftmann@30662 ` 109` ```end ```