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