equal
deleted
inserted
replaced
78 by simp |
78 by simp |
79 |
79 |
80 lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P" |
80 lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P" |
81 by blast |
81 by blast |
82 |
82 |
|
83 lemma obj_sumE_f': |
|
84 "\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f x \<longrightarrow> P" |
|
85 by (cases x) blast+ |
|
86 |
83 lemma obj_sumE_f: |
87 lemma obj_sumE_f: |
84 "\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P" |
88 "\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P" |
85 by (metis sum.exhaust) |
89 by (rule allI) (rule obj_sumE_f') |
86 |
90 |
87 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
91 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
88 by (cases s) auto |
92 by (cases s) auto |
89 |
93 |
|
94 lemma obj_sum_step': |
|
95 "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f (Inr x) \<longrightarrow> P" |
|
96 by (cases x) blast+ |
|
97 |
90 lemma obj_sum_step: |
98 lemma obj_sum_step: |
91 "\<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" |
99 "\<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" |
92 by (metis obj_sumE) |
100 by (rule allI) (rule obj_sum_step') |
93 |
101 |
94 lemma sum_case_if: |
102 lemma sum_case_if: |
95 "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" |
103 "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" |
96 by simp |
104 by simp |
97 |
105 |