# HG changeset patch
# User blanchet
# Date 1384821014 -3600
# Node ID b61b8c9e4cf71b28d34b9008f9db67e6d519dc21
# Parent  ef90494cc827edcc26c7c119944186bc3b5955ce
killed more needless theorems

diff -r ef90494cc827 -r b61b8c9e4cf7 src/HOL/BNF/BNF_Comp.thy
--- a/src/HOL/BNF/BNF_Comp.thy	Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/BNF/BNF_Comp.thy	Tue Nov 19 01:30:14 2013 +0100
@@ -11,6 +11,9 @@
 imports Basic_BNFs
 begin
 
+lemma wpull_id: "wpull UNIV B1 B2 id id id id"
+unfolding wpull_def by simp
+
 lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
 by (rule ext) simp
 
diff -r ef90494cc827 -r b61b8c9e4cf7 src/HOL/BNF/BNF_Def.thy
--- a/src/HOL/BNF/BNF_Def.thy	Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/BNF/BNF_Def.thy	Tue Nov 19 01:30:14 2013 +0100
@@ -190,9 +190,6 @@
 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
   unfolding vimage2p_def by -
 
-lemma vimage2pD: "vimage2p f g R x y \<Longrightarrow> R (f x) (g y)"
-  unfolding vimage2p_def by -
-
 lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
   unfolding fun_rel_def vimage2p_def by auto
 
diff -r ef90494cc827 -r b61b8c9e4cf7 src/HOL/BNF/BNF_FP_Base.thy
--- a/src/HOL/BNF/BNF_FP_Base.thy	Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Tue Nov 19 01:30:14 2013 +0100
@@ -13,12 +13,6 @@
 imports BNF_Comp Ctr_Sugar
 begin
 
-lemma not_TrueE: "\<not> True \<Longrightarrow> P"
-by (erule notE, rule TrueI)
-
-lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
-by fast
-
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
 by auto
 
diff -r ef90494cc827 -r b61b8c9e4cf7 src/HOL/BNF/BNF_GFP.thy
--- a/src/HOL/BNF/BNF_GFP.thy	Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/BNF/BNF_GFP.thy	Tue Nov 19 01:30:14 2013 +0100
@@ -15,6 +15,12 @@
   "primcorec" :: thy_decl
 begin
 
+lemma not_TrueE: "\<not> True \<Longrightarrow> P"
+by (erule notE, rule TrueI)
+
+lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
+by fast
+
 lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
 by (auto split: sum.splits)
 
@@ -37,7 +43,6 @@
 (* Operators: *)
 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
 
-
 lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
 unfolding Id_on_def by simp
 
@@ -74,6 +79,12 @@
 lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
 unfolding Gr_def by auto
 
+lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
+by blast
+
+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})"
+by blast
+
 lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
 unfolding fun_eq_iff by auto
 
diff -r ef90494cc827 -r b61b8c9e4cf7 src/HOL/BNF/BNF_Util.thy
--- a/src/HOL/BNF/BNF_Util.thy	Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/BNF/BNF_Util.thy	Tue Nov 19 01:30:14 2013 +0100
@@ -12,12 +12,6 @@
 imports "../Cardinals/Cardinal_Arithmetic_FP"
 begin
 
-lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
-by blast
-
-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})"
-by blast
-
 definition collect where
 "collect F x = (\<Union>f \<in> F. f x)"
 
diff -r ef90494cc827 -r b61b8c9e4cf7 src/HOL/BNF/Basic_BNFs.thy
--- a/src/HOL/BNF/Basic_BNFs.thy	Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/BNF/Basic_BNFs.thy	Tue Nov 19 01:30:14 2013 +0100
@@ -13,14 +13,8 @@
 imports BNF_Def
 begin
 
-lemma wpull_id: "wpull UNIV B1 B2 id id id id"
-unfolding wpull_def by simp
-
 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
 
-lemma ctwo_card_order: "card_order ctwo"
-using Card_order_ctwo by (unfold ctwo_def Field_card_of)
-
 lemma natLeq_cinfinite: "cinfinite natLeq"
 unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
 
@@ -229,22 +223,6 @@
   thus ?thesis using that by fastforce
 qed
 
-lemma card_of_bounded_range:
-  "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|")
-proof -
-  let ?f = "\<lambda>f. %x. if f x \<in> B then f x else undefined"
-  have "inj_on ?f ?LHS" unfolding inj_on_def
-  proof (unfold fun_eq_iff, safe)
-    fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x
-    assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x"
-    hence "f x \<in> B" "g x \<in> B" by auto
-    with eq have "Some (f x) = Some (g x)" by metis
-    thus "f x = g x" by simp
-  qed
-  moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
-  ultimately show ?thesis using card_of_ordLeq by fast
-qed
-
 bnf "'a \<Rightarrow> 'b"
   map: "op \<circ>"
   sets: range