src/HOL/Library/Option_ord.thy
author haftmann
Fri Mar 07 16:46:57 2008 +0100 (2008-03-07)
changeset 26241 b7d8c2338585
child 26258 20dfaa28e5e5
permissions -rw-r--r--
added Option_ord.thy
     1 (*  Title:      HOL/Library/Option_ord.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 header {* Canonical order on option type *}
     7 
     8 theory Option_ord
     9 imports ATP_Linkup
    10 begin
    11 
    12 instantiation option :: (order) order
    13 begin
    14 
    15 definition less_eq_option where
    16   [code func del]: "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))"
    17 
    18 definition less_option where
    19   [code func del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
    20 
    21 lemma less_eq_option_None [simp]: "None \<le> (x\<Colon>'a option)"
    22   by (simp add: less_eq_option_def)
    23 
    24 lemma less_eq_option_None_code [code]: "None \<le> (x\<Colon>'a option) \<longleftrightarrow> True"
    25   by simp
    26 
    27 lemma less_eq_option_None_is_None: "(x\<Colon>'a option) \<le> None \<Longrightarrow> x = None"
    28   by (cases x) (simp_all add: less_eq_option_def)
    29 
    30 lemma less_eq_option_Some_None [simp, code]: "Some (x\<Colon>'a) \<le> None \<longleftrightarrow> False"
    31   by (simp add: less_eq_option_def)
    32 
    33 lemma less_eq_option_Some [simp, code]: "Some (x\<Colon>'a) \<le> Some y \<longleftrightarrow> x \<le> y"
    34   by (simp add: less_eq_option_def)
    35 
    36 lemma less_option_None [simp, code]: "(x\<Colon>'a option) < None \<longleftrightarrow> False"
    37   by (simp add: less_option_def)
    38 
    39 lemma less_option_None_is_Some: "None < (x\<Colon>'a option) \<Longrightarrow> \<exists>z. x = Some z"
    40   by (cases x) (simp_all add: less_option_def)
    41 
    42 lemma less_option_None_Some [simp]: "None < Some (x\<Colon>'a)"
    43   by (simp add: less_option_def)
    44 
    45 lemma less_option_None_Some_code [code]: "None < Some (x\<Colon>'a) \<longleftrightarrow> True"
    46   by simp
    47 
    48 lemma less_option_Some [simp, code]: "Some (x\<Colon>'a) < Some y \<longleftrightarrow> x < y"
    49   by (simp add: less_option_def)
    50 
    51 instance by default
    52   (auto simp add: less_eq_option_def less_option_def split: option.splits)
    53 
    54 end 
    55 
    56 instance option :: (linorder) linorder
    57   by default (auto simp add: less_eq_option_def less_option_def split: option.splits)
    58 
    59 end