src/HOL/Library/Option_ord.thy
author haftmann
Fri, 10 Oct 2008 06:45:53 +0200
changeset 28562 4e74209f113e
parent 27368 9f90ac19e32b
child 30662 396be15b95d5
permissions -rw-r--r--
`code func` now just `code`
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Option_ord.thy
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     2
    ID:         $Id$
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     4
*)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     5
26263
c95b91870e3b dropped dangerous antiquotation
haftmann
parents: 26259
diff changeset
     6
header {* Canonical order on option type *}
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     7
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     8
theory Option_ord
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 26263
diff changeset
     9
imports Plain
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    10
begin
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    11
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    12
instantiation option :: (order) order
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    13
begin
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    14
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    15
definition less_eq_option where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 27368
diff changeset
    16
  [code 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))"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    17
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    18
definition less_option where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 27368
diff changeset
    19
  [code del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    20
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    21
lemma less_eq_option_None [simp]: "None \<le> x"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    22
  by (simp add: less_eq_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    23
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    24
lemma less_eq_option_None_code [code]: "None \<le> x \<longleftrightarrow> True"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    25
  by simp
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    26
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    27
lemma less_eq_option_None_is_None: "x \<le> None \<Longrightarrow> x = None"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    28
  by (cases x) (simp_all add: less_eq_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    29
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    30
lemma less_eq_option_Some_None [simp, code]: "Some x \<le> None \<longleftrightarrow> False"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    31
  by (simp add: less_eq_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    32
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    33
lemma less_eq_option_Some [simp, code]: "Some x \<le> Some y \<longleftrightarrow> x \<le> y"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    34
  by (simp add: less_eq_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    35
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    36
lemma less_option_None [simp, code]: "x < None \<longleftrightarrow> False"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    37
  by (simp add: less_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    38
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    39
lemma less_option_None_is_Some: "None < x \<Longrightarrow> \<exists>z. x = Some z"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    40
  by (cases x) (simp_all add: less_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    41
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    42
lemma less_option_None_Some [simp]: "None < Some x"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    43
  by (simp add: less_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    44
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    45
lemma less_option_None_Some_code [code]: "None < Some x \<longleftrightarrow> True"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    46
  by simp
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    47
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    48
lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    49
  by (simp add: less_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    50
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    51
instance by default
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    52
  (auto simp add: less_eq_option_def less_option_def split: option.splits)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    53
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    54
end 
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    55
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    56
instance option :: (linorder) linorder
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    57
  by default (auto simp add: less_eq_option_def less_option_def split: option.splits)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    58
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    59
end