equal
deleted
inserted
replaced
197 unfolding rel_fun_def rel_sum_def by (auto split: sum.splits) |
197 unfolding rel_fun_def rel_sum_def by (auto split: sum.splits) |
198 |
198 |
199 lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x" |
199 lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x" |
200 by (case_tac x) simp+ |
200 by (case_tac x) simp+ |
201 |
201 |
|
202 lemma case_prod_o_map_prod: "case_prod f \<circ> map_prod g1 g2 = case_prod (\<lambda>l r. f (g1 l) (g2 r))" |
|
203 unfolding comp_def by auto |
|
204 |
202 lemma case_prod_transfer: |
205 lemma case_prod_transfer: |
203 "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod" |
206 "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod" |
204 unfolding rel_fun_def rel_prod_def by simp |
207 unfolding rel_fun_def rel_prod_def by simp |
205 |
208 |
206 lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)" |
209 lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)" |