# HG changeset patch
# User traytel
# Date 1373896239 -7200
# Node ID 7f7311d04727c5ee8e343693c196c2763a63c275
# Parent  58b87aa4dc3bc47a050c879f7c49d91d0fd5642e
killed unused theorems

diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/BNF_Comp.thy
--- 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
 
diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/BNF_Def.thy
--- 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
diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/BNF_FP_Basic.thy
--- 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
diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/BNF_GFP.thy
--- 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
 
diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/Basic_BNFs.thy
--- 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
 
diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/Countable_Type.thy
--- 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}"
diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/More_BNFs.thy
--- 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)"
diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/Tools/bnf_comp.ML
--- 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;
diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/Tools/bnf_fp_util.ML
--- 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 =