added Option_ord.thy
authorhaftmann
Fri Mar 07 16:46:57 2008 +0100 (2008-03-07)
changeset 26241b7d8c2338585
parent 26240 cc630a75b62a
child 26242 d64510d3c7b7
added Option_ord.thy
src/HOL/Library/Option_ord.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Option_ord.thy	Fri Mar 07 16:46:57 2008 +0100
     1.3 @@ -0,0 +1,59 @@
     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 ATP_Linkup
    1.13 +begin
    1.14 +
    1.15 +instantiation option :: (order) order
    1.16 +begin
    1.17 +
    1.18 +definition less_eq_option where
    1.19 +  [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))"
    1.20 +
    1.21 +definition less_option where
    1.22 +  [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))"
    1.23 +
    1.24 +lemma less_eq_option_None [simp]: "None \<le> (x\<Colon>'a option)"
    1.25 +  by (simp add: less_eq_option_def)
    1.26 +
    1.27 +lemma less_eq_option_None_code [code]: "None \<le> (x\<Colon>'a option) \<longleftrightarrow> True"
    1.28 +  by simp
    1.29 +
    1.30 +lemma less_eq_option_None_is_None: "(x\<Colon>'a option) \<le> None \<Longrightarrow> x = None"
    1.31 +  by (cases x) (simp_all add: less_eq_option_def)
    1.32 +
    1.33 +lemma less_eq_option_Some_None [simp, code]: "Some (x\<Colon>'a) \<le> None \<longleftrightarrow> False"
    1.34 +  by (simp add: less_eq_option_def)
    1.35 +
    1.36 +lemma less_eq_option_Some [simp, code]: "Some (x\<Colon>'a) \<le> Some y \<longleftrightarrow> x \<le> y"
    1.37 +  by (simp add: less_eq_option_def)
    1.38 +
    1.39 +lemma less_option_None [simp, code]: "(x\<Colon>'a option) < None \<longleftrightarrow> False"
    1.40 +  by (simp add: less_option_def)
    1.41 +
    1.42 +lemma less_option_None_is_Some: "None < (x\<Colon>'a option) \<Longrightarrow> \<exists>z. x = Some z"
    1.43 +  by (cases x) (simp_all add: less_option_def)
    1.44 +
    1.45 +lemma less_option_None_Some [simp]: "None < Some (x\<Colon>'a)"
    1.46 +  by (simp add: less_option_def)
    1.47 +
    1.48 +lemma less_option_None_Some_code [code]: "None < Some (x\<Colon>'a) \<longleftrightarrow> True"
    1.49 +  by simp
    1.50 +
    1.51 +lemma less_option_Some [simp, code]: "Some (x\<Colon>'a) < Some y \<longleftrightarrow> x < y"
    1.52 +  by (simp add: less_option_def)
    1.53 +
    1.54 +instance by default
    1.55 +  (auto simp add: less_eq_option_def less_option_def split: option.splits)
    1.56 +
    1.57 +end 
    1.58 +
    1.59 +instance option :: (linorder) linorder
    1.60 +  by default (auto simp add: less_eq_option_def less_option_def split: option.splits)
    1.61 +
    1.62 +end