src/HOL/BNF_FP_Base.thy
 changeset 55966 972f0aa7091b parent 55945 e96383acecf9 child 56640 0a35354137a5
```     1.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 22:15:01 2014 +0100
1.2 +++ b/src/HOL/BNF_FP_Base.thy	Fri Mar 07 01:02:21 2014 +0100
1.3 @@ -28,12 +28,6 @@
1.4  lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
1.5  by simp
1.6
1.7 -lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
1.8 -by clarify
1.9 -
1.10 -lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
1.11 -by auto
1.12 -
1.13  lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
1.14  unfolding comp_def fun_eq_iff by simp
1.15
1.16 @@ -58,9 +52,6 @@
1.17  "case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
1.18  by auto
1.19
1.20 -lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.21 -by simp
1.22 -
1.23  lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
1.24  by blast
1.25
1.26 @@ -76,9 +67,6 @@
1.27    fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto
1.28  qed
1.29
1.30 -lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.31 -by (cases s) auto
1.32 -
1.33  lemma case_sum_if:
1.34  "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
1.35  by simp
```