equal
deleted
inserted
replaced
129 unfolding comp_def by (auto split: sum.splits) |
129 unfolding comp_def by (auto split: sum.splits) |
130 |
130 |
131 lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x" |
131 lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x" |
132 unfolding case_sum_o_map_sum id_comp comp_id .. |
132 unfolding case_sum_o_map_sum id_comp comp_id .. |
133 |
133 |
134 lemma fun_rel_def_butlast: |
134 lemma rel_fun_def_butlast: |
135 "fun_rel R (fun_rel S T) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))" |
135 "rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))" |
136 unfolding fun_rel_def .. |
136 unfolding rel_fun_def .. |
137 |
137 |
138 lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)" |
138 lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)" |
139 by auto |
139 by auto |
140 |
140 |
141 lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)" |
141 lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)" |