src/HOL/Library/Option_ord.thy
changeset 30662 396be15b95d5
parent 28562 4e74209f113e
child 37765 26bdfb7b680b
     1.1 --- a/src/HOL/Library/Option_ord.thy	Mon Mar 23 08:14:23 2009 +0100
     1.2 +++ b/src/HOL/Library/Option_ord.thy	Mon Mar 23 08:14:23 2009 +0100
     1.3 @@ -1,15 +1,14 @@
     1.4  (*  Title:      HOL/Library/Option_ord.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Florian Haftmann, TU Muenchen
     1.7  *)
     1.8  
     1.9  header {* Canonical order on option type *}
    1.10  
    1.11  theory Option_ord
    1.12 -imports Plain
    1.13 +imports Option Main
    1.14  begin
    1.15  
    1.16 -instantiation option :: (order) order
    1.17 +instantiation option :: (preorder) preorder
    1.18  begin
    1.19  
    1.20  definition less_eq_option where
    1.21 @@ -48,12 +47,63 @@
    1.22  lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
    1.23    by (simp add: less_option_def)
    1.24  
    1.25 -instance by default
    1.26 -  (auto simp add: less_eq_option_def less_option_def split: option.splits)
    1.27 +instance proof
    1.28 +qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
    1.29  
    1.30  end 
    1.31  
    1.32 -instance option :: (linorder) linorder
    1.33 -  by default (auto simp add: less_eq_option_def less_option_def split: option.splits)
    1.34 +instance option :: (order) order proof
    1.35 +qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
    1.36 +
    1.37 +instance option :: (linorder) linorder proof
    1.38 +qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
    1.39 +
    1.40 +instantiation option :: (preorder) bot
    1.41 +begin
    1.42 +
    1.43 +definition "bot = None"
    1.44 +
    1.45 +instance proof
    1.46 +qed (simp add: bot_option_def)
    1.47 +
    1.48 +end
    1.49 +
    1.50 +instantiation option :: (top) top
    1.51 +begin
    1.52 +
    1.53 +definition "top = Some top"
    1.54 +
    1.55 +instance proof
    1.56 +qed (simp add: top_option_def less_eq_option_def split: option.split)
    1.57  
    1.58  end
    1.59 +
    1.60 +instance option :: (wellorder) wellorder proof
    1.61 +  fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
    1.62 +  assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
    1.63 +  have "P None" by (rule H) simp
    1.64 +  then have P_Some [case_names Some]:
    1.65 +    "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
    1.66 +  proof -
    1.67 +    fix z
    1.68 +    assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
    1.69 +    with `P None` show "P z" by (cases z) simp_all
    1.70 +  qed
    1.71 +  show "P z" proof (cases z rule: P_Some)
    1.72 +    case (Some w)
    1.73 +    show "(P o Some) w" proof (induct rule: less_induct)
    1.74 +      case (less x)
    1.75 +      have "P (Some x)" proof (rule H)
    1.76 +        fix y :: "'a option"
    1.77 +        assume "y < Some x"
    1.78 +        show "P y" proof (cases y rule: P_Some)
    1.79 +          case (Some v) with `y < Some x` have "v < x" by simp
    1.80 +          with less show "(P o Some) v" .
    1.81 +        qed
    1.82 +      qed
    1.83 +      then show ?case by simp
    1.84 +    qed
    1.85 +  qed
    1.86 +qed
    1.87 +
    1.88 +end