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