--- a/src/HOL/BNF/BNF_Comp.thy Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/BNF_Comp.thy Mon Jul 15 15:50:39 2013 +0200
@@ -64,15 +64,6 @@
"\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
by simp
-lemma Id_def': "Id = {(a,b). a = b}"
-by auto
-
-lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R"
-unfolding Gr_def by auto
-
-lemma O_Gr_cong: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
-by simp
-
lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
unfolding Grp_def fun_eq_iff relcompp.simps by auto
--- a/src/HOL/BNF/BNF_Def.thy Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy Mon Jul 15 15:50:39 2013 +0200
@@ -17,10 +17,6 @@
lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
by (rule ext) (auto simp only: o_apply collect_def)
-lemma converse_mono:
-"R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
-unfolding converse_def by auto
-
lemma conversep_mono:
"R1 ^--1 \<le> R2 ^--1 \<longleftrightarrow> R1 \<le> R2"
unfolding conversep.simps by auto
--- a/src/HOL/BNF/BNF_FP_Basic.thy Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy Mon Jul 15 15:50:39 2013 +0200
@@ -65,25 +65,13 @@
lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
by blast
-lemma obj_sumE_f':
-"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f x \<longrightarrow> P"
-by (cases x) blast+
-
lemma obj_sumE_f:
"\<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"
-by (rule allI) (rule obj_sumE_f')
+by (rule allI) (metis sumE)
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (cases s) auto
-lemma obj_sum_step':
-"\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f (Inr x) \<longrightarrow> P"
-by (cases x) blast+
-
-lemma obj_sum_step:
-"\<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"
-by (rule allI) (rule obj_sum_step')
-
lemma sum_case_if:
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
--- a/src/HOL/BNF/BNF_GFP.thy Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy Mon Jul 15 15:50:39 2013 +0200
@@ -174,9 +174,6 @@
lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
by simp
-lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}"
-by auto
-
lemma image_convolD: "\<lbrakk>(a, b) \<in> <f, g> ` X\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> X \<and> a = f x \<and> b = g x"
unfolding convol_def by auto
@@ -213,14 +210,6 @@
lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
unfolding Shift_def by simp
-lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
-unfolding Succ_def proof
- assume "prefCl Kl" "k # kl \<in> Kl"
- moreover have "prefixeq (k # []) (k # kl)" by auto
- ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
- thus "[] @ [k] \<in> Kl" by simp
-qed
-
lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
unfolding Succ_def by simp
@@ -235,18 +224,6 @@
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
unfolding Succ_def Shift_def by auto
-lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k"
-unfolding Shift_def by simp
-
-lemma Func_cexp: "|Func A B| =o |B| ^c |A|"
-unfolding cexp_def Field_card_of by (simp only: card_of_refl)
-
-lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r"
-unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
-
-lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
-unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto
-
lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
unfolding clists_def Field_card_of by auto
--- a/src/HOL/BNF/Basic_BNFs.thy Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/Basic_BNFs.thy Mon Jul 15 15:50:39 2013 +0200
@@ -24,9 +24,6 @@
lemma natLeq_cinfinite: "cinfinite natLeq"
unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
-lemma wpull_Gr_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Gr B1 f1 O (Gr B2 f2)\<inverse> \<subseteq> (Gr A p1)\<inverse> O Gr A p2"
- unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
-
lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2"
unfolding wpull_def Grp_def by auto
--- a/src/HOL/BNF/Countable_Type.thy Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/Countable_Type.thy Mon Jul 15 15:50:39 2013 +0200
@@ -53,16 +53,6 @@
shows "countable A"
using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
-lemma ordLeq_countable:
-assumes "|A| \<le>o |B|" and "countable B"
-shows "countable A"
-using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
-
-lemma ordLess_countable:
-assumes A: "|A| <o |B|" and B: "countable B"
-shows "countable A"
-by (rule ordLeq_countable[OF ordLess_imp_ordLeq[OF A] B])
-
subsection{* The type of countable sets *}
typedef 'a cset = "{A :: 'a set. countable A}"
--- a/src/HOL/BNF/More_BNFs.thy Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Mon Jul 15 15:50:39 2013 +0200
@@ -73,34 +73,6 @@
split: option.splits)
qed
-lemma card_of_list_in:
- "|{xs. set xs \<subseteq> A}| \<le>o |Pfunc (UNIV :: nat set) A|" (is "|?LHS| \<le>o |?RHS|")
-proof -
- let ?f = "%xs. %i. if i < length xs \<and> set xs \<subseteq> A then Some (nth xs i) else None"
- have "inj_on ?f ?LHS" unfolding inj_on_def fun_eq_iff
- proof safe
- fix xs :: "'a list" and ys :: "'a list"
- assume su: "set xs \<subseteq> A" "set ys \<subseteq> A" and eq: "\<forall>i. ?f xs i = ?f ys i"
- hence *: "length xs = length ys"
- by (metis linorder_cases option.simps(2) order_less_irrefl)
- thus "xs = ys" by (rule nth_equalityI) (metis * eq su option.inject)
- qed
- moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Pfunc_def by fastforce
- ultimately show ?thesis using card_of_ordLeq by blast
-qed
-
-lemma list_in_empty: "A = {} \<Longrightarrow> {x. set x \<subseteq> A} = {[]}"
-by simp
-
-lemma card_of_Func: "|Func A B| =o |B| ^c |A|"
-unfolding cexp_def Field_card_of by (rule card_of_refl)
-
-lemma not_emp_czero_notIn_ordIso_Card_order:
-"A \<noteq> {} \<Longrightarrow> ( |A|, czero) \<notin> ordIso \<and> Card_order |A|"
- apply (rule conjI)
- apply (metis Field_card_of czeroE)
- by (rule card_of_Card_order)
-
lemma wpull_map:
assumes "wpull A B1 B2 f1 f2 p1 p2"
shows "wpull {x. set x \<subseteq> A} {x. set x \<subseteq> B1} {x. set x \<subseteq> B2} (map f1) (map f2) (map p1) (map p2)"
@@ -143,9 +115,7 @@
next
fix x
show "|set x| \<le>o natLeq"
- apply (rule ordLess_imp_ordLeq)
- apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order])
- unfolding Field_natLeq Field_card_of by (auto simp: card_of_well_order_on)
+ by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
qed (simp add: wpull_map)+
(* Finite sets *)
@@ -186,9 +156,6 @@
by (transfer, clarsimp, metis fst_conv)
qed
-lemma abs_fset_rep_fset[simp]: "abs_fset (rep_fset x) = x"
- by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
-
lemma wpull_image:
assumes "wpull A B1 B2 f1 f2 p1 p2"
shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
--- a/src/HOL/BNF/Tools/bnf_comp.ML Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Mon Jul 15 15:50:39 2013 +0200
@@ -331,8 +331,7 @@
rel_conversep_of_bnf bnf RS sym], rel_Grp],
trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
(replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
- replicate (live - n) @{thm Grp_fst_snd})]]] RS sym)
- (*|> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv})*);
+ replicate (live - n) @{thm Grp_fst_snd})]]] RS sym);
in
rtac thm 1
end;
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Mon Jul 15 15:50:39 2013 +0200
@@ -426,7 +426,7 @@
fun mk_sumEN 1 = @{thm one_pointE}
| mk_sumEN 2 = @{thm sumE}
| mk_sumEN n =
- (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
+ (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
replicate n (impI RS allI);
fun mk_obj_sumEN_balanced n =