src/HOL/Option.thy
author haftmann
Sat, 10 Nov 2018 07:57:19 +0000
changeset 69275 9bbd5497befd
parent 68460 b047339bd11c
permissions -rw-r--r--
clarified status of legacy input abbreviations
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Option.thy
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
     2
    Author:     Folklore
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
     3
*)
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
     4
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
     5
section \<open>Datatype option\<close>
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
     6
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
     7
theory Option
66364
fa3247e6ee4b tuning imports
blanchet
parents: 63648
diff changeset
     8
  imports Lifting
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
     9
begin
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    10
58310
91ea607a34d8 updated news
blanchet
parents: 58154
diff changeset
    11
datatype 'a option =
57091
1fa9c19ba2c9 got rid of '=:' squiggly
blanchet
parents: 55867
diff changeset
    12
    None
55406
186076d100d3 compatibility names
blanchet
parents: 55405
diff changeset
    13
  | Some (the: 'a)
57123
b5324647e0f1 tuned whitespace, to make datatype definitions slightly less intimidating
blanchet
parents: 57091
diff changeset
    14
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55518
diff changeset
    15
datatype_compat option
55404
5cb95b79a51f transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
blanchet
parents: 55129
diff changeset
    16
55406
186076d100d3 compatibility names
blanchet
parents: 55405
diff changeset
    17
lemma [case_names None Some, cases type: option]:
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61630
diff changeset
    18
  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 55414
diff changeset
    19
  "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> P) \<Longrightarrow> P"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    20
  by (rule option.exhaust)
55406
186076d100d3 compatibility names
blanchet
parents: 55405
diff changeset
    21
186076d100d3 compatibility names
blanchet
parents: 55405
diff changeset
    22
lemma [case_names None Some, induct type: option]:
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61630
diff changeset
    23
  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
55406
186076d100d3 compatibility names
blanchet
parents: 55405
diff changeset
    24
  "P None \<Longrightarrow> (\<And>option. P (Some option)) \<Longrightarrow> P option"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    25
  by (rule option.induct)
55406
186076d100d3 compatibility names
blanchet
parents: 55405
diff changeset
    26
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
    27
text \<open>Compatibility:\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
    28
setup \<open>Sign.mandatory_path "option"\<close>
55404
5cb95b79a51f transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
blanchet
parents: 55129
diff changeset
    29
lemmas inducts = option.induct
5cb95b79a51f transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
blanchet
parents: 55129
diff changeset
    30
lemmas cases = option.case
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
    31
setup \<open>Sign.parent_path\<close>
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    32
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    33
lemma not_None_eq [iff]: "x \<noteq> None \<longleftrightarrow> (\<exists>y. x = Some y)"
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    34
  by (induct x) auto
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    35
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    36
lemma not_Some_eq [iff]: "(\<forall>y. x \<noteq> Some y) \<longleftrightarrow> x = None"
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    37
  by (induct x) auto
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    38
68460
b047339bd11c added simp rules
nipkow
parents: 68011
diff changeset
    39
lemma comp_the_Some[simp]: "the o Some = id"
b047339bd11c added simp rules
nipkow
parents: 68011
diff changeset
    40
by auto
b047339bd11c added simp rules
nipkow
parents: 68011
diff changeset
    41
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    42
text \<open>Although it may appear that both of these equalities are helpful
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    43
only when applied to assumptions, in practice it seems better to give
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
    44
them the uniform iff attribute.\<close>
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    45
31080
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 30327
diff changeset
    46
lemma inj_Some [simp]: "inj_on Some A"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    47
  by (rule inj_onI) simp
31080
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 30327
diff changeset
    48
55404
5cb95b79a51f transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
blanchet
parents: 55129
diff changeset
    49
lemma case_optionE:
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    50
  assumes c: "(case x of None \<Rightarrow> P | Some y \<Rightarrow> Q y)"
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    51
  obtains
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    52
    (None) "x = None" and P
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    53
  | (Some) y where "x = Some y" and "Q y"
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    54
  using c by (cases x) simp_all
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    55
53010
ec5e6f69bd65 move useful lemmas to Main
kuncar
parents: 52435
diff changeset
    56
lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    57
  by (auto intro: option.induct)
53010
ec5e6f69bd65 move useful lemmas to Main
kuncar
parents: 52435
diff changeset
    58
ec5e6f69bd65 move useful lemmas to Main
kuncar
parents: 52435
diff changeset
    59
lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    60
  using split_option_all[of "\<lambda>x. \<not> P x"] by blast
53010
ec5e6f69bd65 move useful lemmas to Main
kuncar
parents: 52435
diff changeset
    61
31080
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 30327
diff changeset
    62
lemma UNIV_option_conv: "UNIV = insert None (range Some)"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    63
  by (auto intro: classical)
31080
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 30327
diff changeset
    64
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
    65
lemma rel_option_None1 [simp]: "rel_option P None x \<longleftrightarrow> x = None"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    66
  by (cases x) simp_all
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
    67
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
    68
lemma rel_option_None2 [simp]: "rel_option P x None \<longleftrightarrow> x = None"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    69
  by (cases x) simp_all
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
    70
61630
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
    71
lemma option_rel_Some1: "rel_option A (Some x) y \<longleftrightarrow> (\<exists>y'. y = Some y' \<and> A x y')" (* Option *)
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
    72
by(cases y) simp_all
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
    73
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
    74
lemma option_rel_Some2: "rel_option A x (Some y) \<longleftrightarrow> (\<exists>x'. x = Some x' \<and> A x' y)" (* Option *)
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
    75
by(cases x) simp_all
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
    76
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    77
lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)"
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    78
  (is "?lhs = ?rhs")
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    79
proof (rule antisym)
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    80
  show "?lhs \<le> ?rhs" by (auto elim: option.rel_cases)
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    81
  show "?rhs \<le> ?lhs" by (auto elim: option.rel_mono_strong)
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    82
qed
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
    83
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
    84
lemma rel_option_reflI:
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
    85
  "(\<And>x. x \<in> set_option y \<Longrightarrow> P x x) \<Longrightarrow> rel_option P y y"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    86
  by (cases y) auto
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
    87
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59522
diff changeset
    88
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
    89
subsubsection \<open>Operations\<close>
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    90
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    91
lemma ospec [dest]: "(\<forall>x\<in>set_option A. P x) \<Longrightarrow> A = Some x \<Longrightarrow> P x"
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    92
  by simp
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    93
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
    94
setup \<open>map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec}))\<close>
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    95
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
    96
lemma elem_set [iff]: "(x \<in> set_option xo) = (xo = Some x)"
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    97
  by (cases xo) auto
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
    98
55518
1ddb2edf5ceb folded 'Option.set' into BNF-generated 'set_option'
blanchet
parents: 55467
diff changeset
    99
lemma set_empty_eq [simp]: "(set_option xo = {}) = (xo = None)"
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   100
  by (cases xo) auto
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   101
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   102
lemma map_option_case: "map_option f y = (case y of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))"
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55442
diff changeset
   103
  by (auto split: option.split)
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   104
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   105
lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 63343
diff changeset
   106
  by (simp add: map_option_case split: option.split)
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   107
61630
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   108
lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None"
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   109
by(cases x) simp_all
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   110
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   111
lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 63343
diff changeset
   112
  by (simp add: map_option_case split: option.split)
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   113
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55442
diff changeset
   114
lemma map_option_o_case_sum [simp]:
67091
1393c2340eec more symbols;
wenzelm
parents: 66364
diff changeset
   115
    "map_option f \<circ> case_sum g h = case_sum (map_option f \<circ> g) (map_option f \<circ> h)"
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55442
diff changeset
   116
  by (rule o_case_sum)
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   117
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55442
diff changeset
   118
lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   119
  by (cases x) auto
46526
c4cf9d03c352 added congruence rules for Option.{map|bind}
krauss
parents: 41505
diff changeset
   120
61630
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   121
lemma map_option_idI: "(\<And>y. y \<in> set_option x \<Longrightarrow> f y = y) \<Longrightarrow> map_option f x = x"
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   122
by(cases x)(simp_all)
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   123
59521
ef8ac8d2315e tuned proof
Andreas Lochbihler
parents: 58916
diff changeset
   124
functor map_option: map_option
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   125
  by (simp_all add: option.map_comp fun_eq_iff option.map_id)
40609
efb0d7878538 mapper for option type
haftmann
parents: 39272
diff changeset
   126
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   127
lemma case_map_option [simp]: "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
51096
60e4b75fefe1 combinator List.those;
haftmann
parents: 49189
diff changeset
   128
  by (cases x) simp_all
60e4b75fefe1 combinator List.those;
haftmann
parents: 49189
diff changeset
   129
61630
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   130
lemma None_notin_image_Some [simp]: "None \<notin> Some ` A"
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   131
by auto
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   132
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   133
lemma notin_range_Some: "x \<notin> range Some \<longleftrightarrow> x = None"
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   134
by(cases x) auto
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   135
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   136
lemma rel_option_iff:
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   137
  "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   138
    | (Some x, Some y) \<Rightarrow> R x y
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   139
    | _ \<Rightarrow> False)"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   140
  by (auto split: prod.split option.split)
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   141
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   142
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   143
definition combine_options :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> 'a option"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   144
  where "combine_options f x y = 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   145
           (case x of None \<Rightarrow> y | Some x \<Rightarrow> (case y of None \<Rightarrow> Some x | Some y \<Rightarrow> Some (f x y)))"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   146
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   147
lemma combine_options_simps [simp]:
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   148
  "combine_options f None y = y"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   149
  "combine_options f x None = x"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   150
  "combine_options f (Some a) (Some b) = Some (f a b)"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   151
  by (simp_all add: combine_options_def split: option.splits)
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   152
  
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   153
lemma combine_options_cases [case_names None1 None2 Some]:
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   154
  "(x = None \<Longrightarrow> P x y) \<Longrightarrow> (y = None \<Longrightarrow> P x y) \<Longrightarrow> 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   155
     (\<And>a b. x = Some a \<Longrightarrow> y = Some b \<Longrightarrow> P x y) \<Longrightarrow> P x y"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   156
  by (cases x; cases y) simp_all
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   157
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   158
lemma combine_options_commute: 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   159
  "(\<And>x y. f x y = f y x) \<Longrightarrow> combine_options f x y = combine_options f y x"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   160
  using combine_options_cases[of x ]
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   161
  by (induction x y rule: combine_options_cases) simp_all
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   162
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   163
lemma combine_options_assoc:
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   164
  "(\<And>x y z. f (f x y) z = f x (f y z)) \<Longrightarrow> 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   165
     combine_options f (combine_options f x y) z =
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   166
     combine_options f x (combine_options f y z)"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   167
  by (auto simp: combine_options_def split: option.splits)
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   168
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   169
lemma combine_options_left_commute:
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   170
  "(\<And>x y. f x y = f y x) \<Longrightarrow> (\<And>x y z. f (f x y) z = f x (f y z)) \<Longrightarrow> 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   171
     combine_options f y (combine_options f x z) =
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   172
     combine_options f x (combine_options f y z)"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   173
  by (auto simp: combine_options_def split: option.splits)
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   174
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   175
lemmas combine_options_ac = 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   176
  combine_options_commute combine_options_assoc combine_options_left_commute
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   177
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61799
diff changeset
   178
61068
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   179
context
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   180
begin
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   181
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   182
qualified definition is_none :: "'a option \<Rightarrow> bool"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   183
  where [code_post]: "is_none x \<longleftrightarrow> x = None"
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   184
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   185
lemma is_none_simps [simp]:
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   186
  "is_none None"
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   187
  "\<not> is_none (Some x)"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   188
  by (simp_all add: is_none_def)
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   189
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   190
lemma is_none_code [code]:
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   191
  "is_none None = True"
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   192
  "is_none (Some x) = False"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   193
  by simp_all
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   194
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   195
lemma rel_option_unfold:
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   196
  "rel_option R x y \<longleftrightarrow>
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   197
   (is_none x \<longleftrightarrow> is_none y) \<and> (\<not> is_none x \<longrightarrow> \<not> is_none y \<longrightarrow> R (the x) (the y))"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   198
  by (simp add: rel_option_iff split: option.split)
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   199
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   200
lemma rel_optionI:
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   201
  "\<lbrakk> is_none x \<longleftrightarrow> is_none y; \<lbrakk> \<not> is_none x; \<not> is_none y \<rbrakk> \<Longrightarrow> P (the x) (the y) \<rbrakk>
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   202
  \<Longrightarrow> rel_option P x y"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   203
  by (simp add: rel_option_unfold)
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   204
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   205
lemma is_none_map_option [simp]: "is_none (map_option f x) \<longleftrightarrow> is_none x"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   206
  by (simp add: is_none_def)
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   207
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   208
lemma the_map_option: "\<not> is_none x \<Longrightarrow> the (map_option f x) = f (the x)"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   209
  by (auto simp add: is_none_def)
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   210
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   211
61068
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   212
qualified primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   213
where
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   214
  bind_lzero: "bind None f = None"
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   215
| bind_lunit: "bind (Some x) f = f x"
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   216
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   217
lemma is_none_bind: "is_none (bind f g) \<longleftrightarrow> is_none f \<or> is_none (g (the f))"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   218
  by (cases f) simp_all
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   219
39149
aabd6d4a5c3a added Option.bind
krauss
parents: 38857
diff changeset
   220
lemma bind_runit[simp]: "bind x Some = x"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   221
  by (cases x) auto
39149
aabd6d4a5c3a added Option.bind
krauss
parents: 38857
diff changeset
   222
aabd6d4a5c3a added Option.bind
krauss
parents: 38857
diff changeset
   223
lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\<lambda>y. bind (f y) g)"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   224
  by (cases x) auto
39149
aabd6d4a5c3a added Option.bind
krauss
parents: 38857
diff changeset
   225
aabd6d4a5c3a added Option.bind
krauss
parents: 38857
diff changeset
   226
lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   227
  by (cases x) auto
39149
aabd6d4a5c3a added Option.bind
krauss
parents: 38857
diff changeset
   228
61068
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   229
qualified lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   230
  by (cases x) auto
46526
c4cf9d03c352 added congruence rules for Option.{map|bind}
krauss
parents: 41505
diff changeset
   231
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   232
lemma bind_split: "P (bind m f) \<longleftrightarrow> (m = None \<longrightarrow> P None) \<and> (\<forall>v. m = Some v \<longrightarrow> P (f v))"
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   233
  by (cases m) auto
58895
de0a4a76d7aa Added Option.bind_split{,_asm,s}
lammich <lammich@in.tum.de>
parents: 58889
diff changeset
   234
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   235
lemma bind_split_asm: "P (bind m f) \<longleftrightarrow> \<not> (m = None \<and> \<not> P None \<or> (\<exists>x. m = Some x \<and> \<not> P (f x)))"
58895
de0a4a76d7aa Added Option.bind_split{,_asm,s}
lammich <lammich@in.tum.de>
parents: 58889
diff changeset
   236
  by (cases m) auto
de0a4a76d7aa Added Option.bind_split{,_asm,s}
lammich <lammich@in.tum.de>
parents: 58889
diff changeset
   237
de0a4a76d7aa Added Option.bind_split{,_asm,s}
lammich <lammich@in.tum.de>
parents: 58889
diff changeset
   238
lemmas bind_splits = bind_split bind_split_asm
de0a4a76d7aa Added Option.bind_split{,_asm,s}
lammich <lammich@in.tum.de>
parents: 58889
diff changeset
   239
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   240
lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   241
  by (cases f) simp_all
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   242
61630
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   243
lemma bind_eq_None_conv: "Option.bind a f = None \<longleftrightarrow> a = None \<or> f (the a) = None"
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   244
by(cases a) simp_all
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   245
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   246
lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   247
  by (cases x) simp_all
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   248
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   249
lemma bind_option_cong:
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   250
  "\<lbrakk> x = y; \<And>z. z \<in> set_option y \<Longrightarrow> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   251
  by (cases y) simp_all
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   252
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   253
lemma bind_option_cong_simp:
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   254
  "\<lbrakk> x = y; \<And>z. z \<in> set_option y =simp=> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   255
  unfolding simp_implies_def by (rule bind_option_cong)
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   256
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   257
lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f"
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   258
  by simp
61068
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   259
61630
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   260
lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)"
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   261
by(cases x) simp_all
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   262
69275
9bbd5497befd clarified status of legacy input abbreviations
haftmann
parents: 68460
diff changeset
   263
lemma set_bind_option [simp]: "set_option (bind x f) = (\<Union>((set_option \<circ> f) ` set_option x))"
61630
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   264
by(cases x) auto
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   265
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   266
lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)"
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   267
by(cases x) simp_all
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 61068
diff changeset
   268
61068
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   269
end
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   270
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   271
setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   272
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   273
61068
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   274
context
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   275
begin
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   276
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   277
qualified definition these :: "'a option set \<Rightarrow> 'a set"
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   278
  where "these A = the ` {x \<in> A. x \<noteq> None}"
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   279
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   280
lemma these_empty [simp]: "these {} = {}"
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   281
  by (simp add: these_def)
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   282
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   283
lemma these_insert_None [simp]: "these (insert None A) = these A"
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   284
  by (auto simp add: these_def)
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   285
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   286
lemma these_insert_Some [simp]: "these (insert (Some x) A) = insert x (these A)"
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   287
proof -
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   288
  have "{y \<in> insert (Some x) A. y \<noteq> None} = insert (Some x) {y \<in> A. y \<noteq> None}"
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   289
    by auto
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   290
  then show ?thesis by (simp add: these_def)
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   291
qed
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   292
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   293
lemma in_these_eq: "x \<in> these A \<longleftrightarrow> Some x \<in> A"
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   294
proof
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   295
  assume "Some x \<in> A"
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   296
  then obtain B where "A = insert (Some x) B" by auto
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   297
  then show "x \<in> these A" by (auto simp add: these_def intro!: image_eqI)
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   298
next
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   299
  assume "x \<in> these A"
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   300
  then show "Some x \<in> A" by (auto simp add: these_def)
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   301
qed
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   302
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   303
lemma these_image_Some_eq [simp]: "these (Some ` A) = A"
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   304
  by (auto simp add: these_def intro!: image_eqI)
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   305
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   306
lemma Some_image_these_eq: "Some ` these A = {x\<in>A. x \<noteq> None}"
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   307
  by (auto simp add: these_def image_image intro!: image_eqI)
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   308
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   309
lemma these_empty_eq: "these B = {} \<longleftrightarrow> B = {} \<or> B = {None}"
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   310
  by (auto simp add: these_def)
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   311
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   312
lemma these_not_empty_eq: "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   313
  by (auto simp add: these_empty_eq)
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   314
61068
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   315
end
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   316
68011
fb6469cdf094 moved lemma to more appropriate place
haftmann
parents: 67399
diff changeset
   317
lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)"
fb6469cdf094 moved lemma to more appropriate place
haftmann
parents: 67399
diff changeset
   318
  by (auto dest: finite_imageD intro: inj_Some)
fb6469cdf094 moved lemma to more appropriate place
haftmann
parents: 67399
diff changeset
   319
49189
3f85cd15a0cc combinator Option.these
haftmann
parents: 46526
diff changeset
   320
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
   321
subsection \<open>Transfer rules for the Transfer package\<close>
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   322
63343
fb5d8a50c641 bundle lifting_syntax;
wenzelm
parents: 63194
diff changeset
   323
context includes lifting_syntax
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   324
begin
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   325
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   326
lemma option_bind_transfer [transfer_rule]:
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   327
  "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   328
    Option.bind Option.bind"
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   329
  unfolding rel_fun_def split_option_all by simp
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   330
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59522
diff changeset
   331
lemma pred_option_parametric [transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   332
  "((A ===> (=)) ===> rel_option A ===> (=)) pred_option pred_option"
61068
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   333
  by (rule rel_funI)+ (auto simp add: rel_option_unfold Option.is_none_def dest: rel_funD)
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59522
diff changeset
   334
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   335
end
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   336
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58895
diff changeset
   337
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
   338
subsubsection \<open>Interaction with finite sets\<close>
55089
181751ad852f swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet
parents: 53940
diff changeset
   339
181751ad852f swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet
parents: 53940
diff changeset
   340
lemma finite_option_UNIV [simp]:
181751ad852f swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet
parents: 53940
diff changeset
   341
  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
181751ad852f swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet
parents: 53940
diff changeset
   342
  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
181751ad852f swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet
parents: 53940
diff changeset
   343
181751ad852f swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet
parents: 53940
diff changeset
   344
instance option :: (finite) finite
61066
00a169fe5de4 misc tuning and modernization;
wenzelm
parents: 60758
diff changeset
   345
  by standard (simp add: UNIV_option_conv)
55089
181751ad852f swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet
parents: 53940
diff changeset
   346
181751ad852f swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet
parents: 53940
diff changeset
   347
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59523
diff changeset
   348
subsubsection \<open>Code generator setup\<close>
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   349
59522
0c5c5ad5d2e0 add lemmas about functions on option
Andreas Lochbihler
parents: 59521
diff changeset
   350
lemma equal_None_code_unfold [code_unfold]:
61068
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   351
  "HOL.equal x None \<longleftrightarrow> Option.is_none x"
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   352
  "HOL.equal None = Option.is_none"
6cb92c2a5ece proper qualified naming;
wenzelm
parents: 61066
diff changeset
   353
  by (auto simp add: equal Option.is_none_def)
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   354
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   355
code_printing
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   356
  type_constructor option \<rightharpoonup>
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   357
    (SML) "_ option"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   358
    and (OCaml) "_ option"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   359
    and (Haskell) "Maybe _"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   360
    and (Scala) "!Option[(_)]"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   361
| constant None \<rightharpoonup>
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   362
    (SML) "NONE"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   363
    and (OCaml) "None"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   364
    and (Haskell) "Nothing"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   365
    and (Scala) "!None"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   366
| constant Some \<rightharpoonup>
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   367
    (SML) "SOME"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   368
    and (OCaml) "Some _"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   369
    and (Haskell) "Just"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   370
    and (Scala) "Some"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   371
| class_instance option :: equal \<rightharpoonup>
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   372
    (Haskell) -
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   373
| constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup>
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51703
diff changeset
   374
    (Haskell) infix 4 "=="
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   375
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   376
code_reserved SML
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   377
  option NONE SOME
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   378
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   379
code_reserved OCaml
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   380
  option None Some
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   381
34886
873c31d9f10d some syntax setup for Scala
haftmann
parents: 32069
diff changeset
   382
code_reserved Scala
873c31d9f10d some syntax setup for Scala
haftmann
parents: 32069
diff changeset
   383
  Option None Some
873c31d9f10d some syntax setup for Scala
haftmann
parents: 32069
diff changeset
   384
30246
8253519dfc90 Option.thy
nipkow
parents:
diff changeset
   385
end