killed more needless theorems
authorblanchet
Tue Nov 19 01:30:14 2013 +0100 (2013-11-19)
changeset 54485b61b8c9e4cf7
parent 54484 ef90494cc827
child 54486 d8d276c922f2
killed more needless theorems
src/HOL/BNF/BNF_Comp.thy
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/BNF_FP_Base.thy
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/BNF_Util.thy
src/HOL/BNF/Basic_BNFs.thy
     1.1 --- a/src/HOL/BNF/BNF_Comp.thy	Tue Nov 19 01:29:50 2013 +0100
     1.2 +++ b/src/HOL/BNF/BNF_Comp.thy	Tue Nov 19 01:30:14 2013 +0100
     1.3 @@ -11,6 +11,9 @@
     1.4  imports Basic_BNFs
     1.5  begin
     1.6  
     1.7 +lemma wpull_id: "wpull UNIV B1 B2 id id id id"
     1.8 +unfolding wpull_def by simp
     1.9 +
    1.10  lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
    1.11  by (rule ext) simp
    1.12  
     2.1 --- a/src/HOL/BNF/BNF_Def.thy	Tue Nov 19 01:29:50 2013 +0100
     2.2 +++ b/src/HOL/BNF/BNF_Def.thy	Tue Nov 19 01:30:14 2013 +0100
     2.3 @@ -190,9 +190,6 @@
     2.4  lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
     2.5    unfolding vimage2p_def by -
     2.6  
     2.7 -lemma vimage2pD: "vimage2p f g R x y \<Longrightarrow> R (f x) (g y)"
     2.8 -  unfolding vimage2p_def by -
     2.9 -
    2.10  lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
    2.11    unfolding fun_rel_def vimage2p_def by auto
    2.12  
     3.1 --- a/src/HOL/BNF/BNF_FP_Base.thy	Tue Nov 19 01:29:50 2013 +0100
     3.2 +++ b/src/HOL/BNF/BNF_FP_Base.thy	Tue Nov 19 01:30:14 2013 +0100
     3.3 @@ -13,12 +13,6 @@
     3.4  imports BNF_Comp Ctr_Sugar
     3.5  begin
     3.6  
     3.7 -lemma not_TrueE: "\<not> True \<Longrightarrow> P"
     3.8 -by (erule notE, rule TrueI)
     3.9 -
    3.10 -lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
    3.11 -by fast
    3.12 -
    3.13  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
    3.14  by auto
    3.15  
     4.1 --- a/src/HOL/BNF/BNF_GFP.thy	Tue Nov 19 01:29:50 2013 +0100
     4.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Tue Nov 19 01:30:14 2013 +0100
     4.3 @@ -15,6 +15,12 @@
     4.4    "primcorec" :: thy_decl
     4.5  begin
     4.6  
     4.7 +lemma not_TrueE: "\<not> True \<Longrightarrow> P"
     4.8 +by (erule notE, rule TrueI)
     4.9 +
    4.10 +lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
    4.11 +by fast
    4.12 +
    4.13  lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
    4.14  by (auto split: sum.splits)
    4.15  
    4.16 @@ -37,7 +43,6 @@
    4.17  (* Operators: *)
    4.18  definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
    4.19  
    4.20 -
    4.21  lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
    4.22  unfolding Id_on_def by simp
    4.23  
    4.24 @@ -74,6 +79,12 @@
    4.25  lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
    4.26  unfolding Gr_def by auto
    4.27  
    4.28 +lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    4.29 +by blast
    4.30 +
    4.31 +lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
    4.32 +by blast
    4.33 +
    4.34  lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
    4.35  unfolding fun_eq_iff by auto
    4.36  
     5.1 --- a/src/HOL/BNF/BNF_Util.thy	Tue Nov 19 01:29:50 2013 +0100
     5.2 +++ b/src/HOL/BNF/BNF_Util.thy	Tue Nov 19 01:30:14 2013 +0100
     5.3 @@ -12,12 +12,6 @@
     5.4  imports "../Cardinals/Cardinal_Arithmetic_FP"
     5.5  begin
     5.6  
     5.7 -lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
     5.8 -by blast
     5.9 -
    5.10 -lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
    5.11 -by blast
    5.12 -
    5.13  definition collect where
    5.14  "collect F x = (\<Union>f \<in> F. f x)"
    5.15  
     6.1 --- a/src/HOL/BNF/Basic_BNFs.thy	Tue Nov 19 01:29:50 2013 +0100
     6.2 +++ b/src/HOL/BNF/Basic_BNFs.thy	Tue Nov 19 01:30:14 2013 +0100
     6.3 @@ -13,14 +13,8 @@
     6.4  imports BNF_Def
     6.5  begin
     6.6  
     6.7 -lemma wpull_id: "wpull UNIV B1 B2 id id id id"
     6.8 -unfolding wpull_def by simp
     6.9 -
    6.10  lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
    6.11  
    6.12 -lemma ctwo_card_order: "card_order ctwo"
    6.13 -using Card_order_ctwo by (unfold ctwo_def Field_card_of)
    6.14 -
    6.15  lemma natLeq_cinfinite: "cinfinite natLeq"
    6.16  unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
    6.17  
    6.18 @@ -229,22 +223,6 @@
    6.19    thus ?thesis using that by fastforce
    6.20  qed
    6.21  
    6.22 -lemma card_of_bounded_range:
    6.23 -  "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|")
    6.24 -proof -
    6.25 -  let ?f = "\<lambda>f. %x. if f x \<in> B then f x else undefined"
    6.26 -  have "inj_on ?f ?LHS" unfolding inj_on_def
    6.27 -  proof (unfold fun_eq_iff, safe)
    6.28 -    fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x
    6.29 -    assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x"
    6.30 -    hence "f x \<in> B" "g x \<in> B" by auto
    6.31 -    with eq have "Some (f x) = Some (g x)" by metis
    6.32 -    thus "f x = g x" by simp
    6.33 -  qed
    6.34 -  moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
    6.35 -  ultimately show ?thesis using card_of_ordLeq by fast
    6.36 -qed
    6.37 -
    6.38  bnf "'a \<Rightarrow> 'b"
    6.39    map: "op \<circ>"
    6.40    sets: range