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