src/HOL/Codatatype/BNF_Library.thy
changeset 49255 2ecc533d6697
parent 49125 5fc5211cf104
child 49263 669a820ef213
     1.1 --- a/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:32:39 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:35:53 2012 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
     1.6  
     1.7 -lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by auto
     1.8 +lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
     1.9  
    1.10  lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
    1.11  by presburger
    1.12 @@ -89,23 +89,23 @@
    1.13  by (rule ext) (auto simp add: collect_def)
    1.14  
    1.15  lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
    1.16 -by auto
    1.17 +by blast
    1.18  
    1.19  lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
    1.20 -by auto
    1.21 +by blast
    1.22  
    1.23  lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
    1.24  by simp
    1.25  
    1.26  lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
    1.27 -by auto
    1.28 +by simp
    1.29  
    1.30  lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
    1.31 -by auto
    1.32 +by blast
    1.33  
    1.34  lemma image_Collect_subsetI:
    1.35    "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
    1.36 -by auto
    1.37 +by blast
    1.38  
    1.39  lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>(\<lambda>f. f x) ` X| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
    1.40  by (unfold o_apply collect_def SUP_def)
    1.41 @@ -826,17 +826,21 @@
    1.42    "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
    1.43  by auto
    1.44  
    1.45 +lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.46 +by simp
    1.47 +
    1.48 +lemma obj_sumE_f:
    1.49 +"\<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"
    1.50 +by (metis sum.exhaust)
    1.51 +
    1.52  lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.53  by (cases s) auto
    1.54  
    1.55 -lemma obj_sum_base: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.56 -by auto
    1.57 -
    1.58  lemma obj_sum_step:
    1.59    "\<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"
    1.60  by (metis obj_sumE)
    1.61  
    1.62  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
    1.63 -by auto
    1.64 +by simp
    1.65  
    1.66  end