# HG changeset patch
# User haftmann
# Date 1237792463 -3600
# Node ID 396be15b95d5422296c3e3a32bde70f914c1ea4a
# Parent  54858c8ad2266eeb01be33f2c82441f3f09c74db
added instances for bot, top, wellorder

diff -r 54858c8ad226 -r 396be15b95d5 src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Option_ord.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,15 +1,14 @@
 (*  Title:      HOL/Library/Option_ord.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 header {* Canonical order on option type *}
 
 theory Option_ord
-imports Plain
+imports Option Main
 begin
 
-instantiation option :: (order) order
+instantiation option :: (preorder) preorder
 begin
 
 definition less_eq_option where
@@ -48,12 +47,63 @@
 lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
   by (simp add: less_option_def)
 
-instance by default
-  (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance proof
+qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
 
 end 
 
-instance option :: (linorder) linorder
-  by default (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance option :: (order) order proof
+qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instance option :: (linorder) linorder proof
+qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instantiation option :: (preorder) bot
+begin
+
+definition "bot = None"
+
+instance proof
+qed (simp add: bot_option_def)
+
+end
+
+instantiation option :: (top) top
+begin
+
+definition "top = Some top"
+
+instance proof
+qed (simp add: top_option_def less_eq_option_def split: option.split)
 
 end
+
+instance option :: (wellorder) wellorder proof
+  fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
+  assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  have "P None" by (rule H) simp
+  then have P_Some [case_names Some]:
+    "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
+  proof -
+    fix z
+    assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
+    with `P None` show "P z" by (cases z) simp_all
+  qed
+  show "P z" proof (cases z rule: P_Some)
+    case (Some w)
+    show "(P o Some) w" proof (induct rule: less_induct)
+      case (less x)
+      have "P (Some x)" proof (rule H)
+        fix y :: "'a option"
+        assume "y < Some x"
+        show "P y" proof (cases y rule: P_Some)
+          case (Some v) with `y < Some x` have "v < x" by simp
+          with less show "(P o Some) v" .
+        qed
+      qed
+      then show ?case by simp
+    qed
+  qed
+qed
+
+end