killed unused theorems
authortraytel
Mon Jul 15 15:50:39 2013 +0200 (2013-07-15)
changeset 526607f7311d04727
parent 52659 58b87aa4dc3b
child 52661 a3b04f0ab6a4
child 52663 6e71d43775e5
killed unused theorems
src/HOL/BNF/BNF_Comp.thy
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/BNF_FP_Basic.thy
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/Basic_BNFs.thy
src/HOL/BNF/Countable_Type.thy
src/HOL/BNF/More_BNFs.thy
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_fp_util.ML
     1.1 --- a/src/HOL/BNF/BNF_Comp.thy	Mon Jul 15 14:23:51 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Comp.thy	Mon Jul 15 15:50:39 2013 +0200
     1.3 @@ -64,15 +64,6 @@
     1.4  "\<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"
     1.5  by simp
     1.6  
     1.7 -lemma Id_def': "Id = {(a,b). a = b}"
     1.8 -by auto
     1.9 -
    1.10 -lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R"
    1.11 -unfolding Gr_def by auto
    1.12 -
    1.13 -lemma O_Gr_cong: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
    1.14 -by simp
    1.15 -
    1.16  lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
    1.17  unfolding Grp_def fun_eq_iff relcompp.simps by auto
    1.18  
     2.1 --- a/src/HOL/BNF/BNF_Def.thy	Mon Jul 15 14:23:51 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_Def.thy	Mon Jul 15 15:50:39 2013 +0200
     2.3 @@ -17,10 +17,6 @@
     2.4  lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
     2.5  by (rule ext) (auto simp only: o_apply collect_def)
     2.6  
     2.7 -lemma converse_mono:
     2.8 -"R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
     2.9 -unfolding converse_def by auto
    2.10 -
    2.11  lemma conversep_mono:
    2.12  "R1 ^--1 \<le> R2 ^--1 \<longleftrightarrow> R1 \<le> R2"
    2.13  unfolding conversep.simps by auto
     3.1 --- a/src/HOL/BNF/BNF_FP_Basic.thy	Mon Jul 15 14:23:51 2013 +0200
     3.2 +++ b/src/HOL/BNF/BNF_FP_Basic.thy	Mon Jul 15 15:50:39 2013 +0200
     3.3 @@ -65,25 +65,13 @@
     3.4  lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
     3.5  by blast
     3.6  
     3.7 -lemma obj_sumE_f':
     3.8 -"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f x \<longrightarrow> P"
     3.9 -by (cases x) blast+
    3.10 -
    3.11  lemma obj_sumE_f:
    3.12  "\<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"
    3.13 -by (rule allI) (rule obj_sumE_f')
    3.14 +by (rule allI) (metis sumE)
    3.15  
    3.16  lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    3.17  by (cases s) auto
    3.18  
    3.19 -lemma obj_sum_step':
    3.20 -"\<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"
    3.21 -by (cases x) blast+
    3.22 -
    3.23 -lemma obj_sum_step:
    3.24 -"\<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"
    3.25 -by (rule allI) (rule obj_sum_step')
    3.26 -
    3.27  lemma sum_case_if:
    3.28  "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    3.29  by simp
     4.1 --- a/src/HOL/BNF/BNF_GFP.thy	Mon Jul 15 14:23:51 2013 +0200
     4.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Mon Jul 15 15:50:39 2013 +0200
     4.3 @@ -174,9 +174,6 @@
     4.4  lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
     4.5  by simp
     4.6  
     4.7 -lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}"
     4.8 -by auto
     4.9 -
    4.10  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"
    4.11  unfolding convol_def by auto
    4.12  
    4.13 @@ -213,14 +210,6 @@
    4.14  lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
    4.15  unfolding Shift_def by simp
    4.16  
    4.17 -lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
    4.18 -unfolding Succ_def proof
    4.19 -  assume "prefCl Kl" "k # kl \<in> Kl"
    4.20 -  moreover have "prefixeq (k # []) (k # kl)" by auto
    4.21 -  ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
    4.22 -  thus "[] @ [k] \<in> Kl" by simp
    4.23 -qed
    4.24 -
    4.25  lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
    4.26  unfolding Succ_def by simp
    4.27  
    4.28 @@ -235,18 +224,6 @@
    4.29  lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
    4.30  unfolding Succ_def Shift_def by auto
    4.31  
    4.32 -lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k"
    4.33 -unfolding Shift_def by simp
    4.34 -
    4.35 -lemma Func_cexp: "|Func A B| =o |B| ^c |A|"
    4.36 -unfolding cexp_def Field_card_of by (simp only: card_of_refl)
    4.37 -
    4.38 -lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r"
    4.39 -unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
    4.40 -
    4.41 -lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
    4.42 -unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto
    4.43 -
    4.44  lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
    4.45  unfolding clists_def Field_card_of by auto
    4.46  
     5.1 --- a/src/HOL/BNF/Basic_BNFs.thy	Mon Jul 15 14:23:51 2013 +0200
     5.2 +++ b/src/HOL/BNF/Basic_BNFs.thy	Mon Jul 15 15:50:39 2013 +0200
     5.3 @@ -24,9 +24,6 @@
     5.4  lemma natLeq_cinfinite: "cinfinite natLeq"
     5.5  unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
     5.6  
     5.7 -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"
     5.8 -  unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
     5.9 -
    5.10  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"
    5.11    unfolding wpull_def Grp_def by auto
    5.12  
     6.1 --- a/src/HOL/BNF/Countable_Type.thy	Mon Jul 15 14:23:51 2013 +0200
     6.2 +++ b/src/HOL/BNF/Countable_Type.thy	Mon Jul 15 15:50:39 2013 +0200
     6.3 @@ -53,16 +53,6 @@
     6.4  shows "countable A"
     6.5  using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
     6.6  
     6.7 -lemma ordLeq_countable:
     6.8 -assumes "|A| \<le>o |B|" and "countable B"
     6.9 -shows "countable A"
    6.10 -using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
    6.11 -
    6.12 -lemma ordLess_countable:
    6.13 -assumes A: "|A| <o |B|" and B: "countable B"
    6.14 -shows "countable A"
    6.15 -by (rule ordLeq_countable[OF ordLess_imp_ordLeq[OF A] B])
    6.16 -
    6.17  subsection{*  The type of countable sets *}
    6.18  
    6.19  typedef 'a cset = "{A :: 'a set. countable A}"
     7.1 --- a/src/HOL/BNF/More_BNFs.thy	Mon Jul 15 14:23:51 2013 +0200
     7.2 +++ b/src/HOL/BNF/More_BNFs.thy	Mon Jul 15 15:50:39 2013 +0200
     7.3 @@ -73,34 +73,6 @@
     7.4             split: option.splits)
     7.5  qed
     7.6  
     7.7 -lemma card_of_list_in:
     7.8 -  "|{xs. set xs \<subseteq> A}| \<le>o |Pfunc (UNIV :: nat set) A|" (is "|?LHS| \<le>o |?RHS|")
     7.9 -proof -
    7.10 -  let ?f = "%xs. %i. if i < length xs \<and> set xs \<subseteq> A then Some (nth xs i) else None"
    7.11 -  have "inj_on ?f ?LHS" unfolding inj_on_def fun_eq_iff
    7.12 -  proof safe
    7.13 -    fix xs :: "'a list" and ys :: "'a list"
    7.14 -    assume su: "set xs \<subseteq> A" "set ys \<subseteq> A" and eq: "\<forall>i. ?f xs i = ?f ys i"
    7.15 -    hence *: "length xs = length ys"
    7.16 -    by (metis linorder_cases option.simps(2) order_less_irrefl)
    7.17 -    thus "xs = ys" by (rule nth_equalityI) (metis * eq su option.inject)
    7.18 -  qed
    7.19 -  moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Pfunc_def by fastforce
    7.20 -  ultimately show ?thesis using card_of_ordLeq by blast
    7.21 -qed
    7.22 -
    7.23 -lemma list_in_empty: "A = {} \<Longrightarrow> {x. set x \<subseteq> A} = {[]}"
    7.24 -by simp
    7.25 -
    7.26 -lemma card_of_Func: "|Func A B| =o |B| ^c |A|"
    7.27 -unfolding cexp_def Field_card_of by (rule card_of_refl)
    7.28 -
    7.29 -lemma not_emp_czero_notIn_ordIso_Card_order:
    7.30 -"A \<noteq> {} \<Longrightarrow> ( |A|, czero) \<notin> ordIso \<and> Card_order |A|"
    7.31 -  apply (rule conjI)
    7.32 -  apply (metis Field_card_of czeroE)
    7.33 -  by (rule card_of_Card_order)
    7.34 -
    7.35  lemma wpull_map:
    7.36    assumes "wpull A B1 B2 f1 f2 p1 p2"
    7.37    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)"
    7.38 @@ -143,9 +115,7 @@
    7.39  next
    7.40    fix x
    7.41    show "|set x| \<le>o natLeq"
    7.42 -    apply (rule ordLess_imp_ordLeq)
    7.43 -    apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order])
    7.44 -    unfolding Field_natLeq Field_card_of by (auto simp: card_of_well_order_on)
    7.45 +    by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
    7.46  qed (simp add: wpull_map)+
    7.47  
    7.48  (* Finite sets *)
    7.49 @@ -186,9 +156,6 @@
    7.50    by (transfer, clarsimp, metis fst_conv)
    7.51  qed
    7.52  
    7.53 -lemma abs_fset_rep_fset[simp]: "abs_fset (rep_fset x) = x"
    7.54 -  by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
    7.55 -
    7.56  lemma wpull_image:
    7.57    assumes "wpull A B1 B2 f1 f2 p1 p2"
    7.58    shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
     8.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Mon Jul 15 14:23:51 2013 +0200
     8.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Mon Jul 15 15:50:39 2013 +0200
     8.3 @@ -331,8 +331,7 @@
     8.4                  rel_conversep_of_bnf bnf RS sym], rel_Grp],
     8.5                trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
     8.6                  (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
     8.7 -                 replicate (live - n) @{thm Grp_fst_snd})]]] RS sym)
     8.8 -          (*|> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv})*);
     8.9 +                 replicate (live - n) @{thm Grp_fst_snd})]]] RS sym);
    8.10        in
    8.11          rtac thm 1
    8.12        end;
     9.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Mon Jul 15 14:23:51 2013 +0200
     9.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Mon Jul 15 15:50:39 2013 +0200
     9.3 @@ -426,7 +426,7 @@
     9.4  fun mk_sumEN 1 = @{thm one_pointE}
     9.5    | mk_sumEN 2 = @{thm sumE}
     9.6    | mk_sumEN n =
     9.7 -    (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
     9.8 +    (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
     9.9        replicate n (impI RS allI);
    9.10  
    9.11  fun mk_obj_sumEN_balanced n =