equal
deleted
inserted
replaced
79 |
79 |
80 lemma option_map_o_sum_case [simp]: |
80 lemma option_map_o_sum_case [simp]: |
81 "map f o sum_case g h = sum_case (map f o g) (map f o h)" |
81 "map f o sum_case g h = sum_case (map f o g) (map f o h)" |
82 by (rule ext) (simp split: sum.split) |
82 by (rule ext) (simp split: sum.split) |
83 |
83 |
|
84 lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y" |
|
85 by (cases x) auto |
|
86 |
84 enriched_type map: Option.map proof - |
87 enriched_type map: Option.map proof - |
85 fix f g |
88 fix f g |
86 show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)" |
89 show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)" |
87 proof |
90 proof |
88 fix x |
91 fix x |
109 by (cases x) auto |
112 by (cases x) auto |
110 |
113 |
111 lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None" |
114 lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None" |
112 by (cases x) auto |
115 by (cases x) auto |
113 |
116 |
|
117 lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g" |
|
118 by (cases x) auto |
|
119 |
114 hide_const (open) set map bind |
120 hide_const (open) set map bind |
|
121 hide_fact (open) map_cong bind_cong |
115 |
122 |
116 subsubsection {* Code generator setup *} |
123 subsubsection {* Code generator setup *} |
117 |
124 |
118 definition is_none :: "'a option \<Rightarrow> bool" where |
125 definition is_none :: "'a option \<Rightarrow> bool" where |
119 [code_post]: "is_none x \<longleftrightarrow> x = None" |
126 [code_post]: "is_none x \<longleftrightarrow> x = None" |