--- 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
--- 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
--- 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
--- 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
--- 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)"
--- 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