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