equal
deleted
inserted
replaced
145 "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g" |
145 "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g" |
146 unfolding Let_def by blast |
146 unfolding Let_def by blast |
147 |
147 |
148 lemmas [fundef_cong] = |
148 lemmas [fundef_cong] = |
149 if_cong image_cong INT_cong UN_cong |
149 if_cong image_cong INT_cong UN_cong |
150 bex_cong ball_cong imp_cong |
150 bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong |
151 |
151 |
152 lemma split_cong [fundef_cong]: |
152 lemma split_cong [fundef_cong]: |
153 "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q |
153 "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q |
154 \<Longrightarrow> split f p = split g q" |
154 \<Longrightarrow> split f p = split g q" |
155 by (auto simp: split_def) |
155 by (auto simp: split_def) |