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