equal
deleted
inserted
replaced
841 |
841 |
842 lemma obj_sum_step: |
842 lemma obj_sum_step: |
843 "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P" |
843 "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P" |
844 by (metis obj_sumE) |
844 by (metis obj_sumE) |
845 |
845 |
|
846 lemma sum_map_if: |
|
847 "sum_map f g (if p then Inl x else Inr y) = (if p then Inl (f x) else Inr (g y))" |
|
848 by simp |
|
849 |
|
850 lemma sum_case_if: |
|
851 "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" |
|
852 by simp |
|
853 |
846 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y" |
854 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y" |
847 by simp |
855 by simp |
848 |
856 |
849 end |
857 end |