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.5  lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
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.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.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.19  lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
1.20 -by auto
1.21 +by blast
1.23  lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
1.24  by simp
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.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.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.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.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.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.62  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
1.63 -by auto
1.64 +by simp
1.66  end