equal
deleted
inserted
replaced
87 unfolding sum_set_defs by simp+ |
87 unfolding sum_set_defs by simp+ |
88 |
88 |
89 lemma Inl_Inr_False: "(Inl x = Inr y) = False" |
89 lemma Inl_Inr_False: "(Inl x = Inr y) = False" |
90 by simp |
90 by simp |
91 |
91 |
|
92 lemma Inr_Inl_False: "(Inr x = Inl y) = False" |
|
93 by simp |
|
94 |
92 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" |
95 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" |
93 by blast |
96 by blast |
94 |
97 |
95 lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r" |
98 lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r" |
96 unfolding comp_def fun_eq_iff by auto |
99 unfolding comp_def fun_eq_iff by auto |