removed unused/inlinable theorems
authortraytel
Thu Sep 12 11:23:49 2013 +0200 (2013-09-12)
changeset 535604b5f42cfa244
parent 53559 3858246c7c8f
child 53561 92bcac4f9ac9
removed unused/inlinable theorems
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/BNF_Util.thy
src/HOL/BNF/Tools/bnf_tactics.ML
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:05:19 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:23:49 2013 +0200
     1.3 @@ -110,10 +110,6 @@
     1.4  lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
     1.5  unfolding Grp_def o_def by auto
     1.6  
     1.7 -lemma wpull_Grp:
     1.8 -"wpull (Collect (split (Grp A f))) A (f ` A) f id fst snd"
     1.9 -unfolding wpull_def Grp_def by auto
    1.10 -
    1.11  definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
    1.12  
    1.13  lemma pick_middlep:
     2.1 --- a/src/HOL/BNF/BNF_Util.thy	Thu Sep 12 11:05:19 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_Util.thy	Thu Sep 12 11:23:49 2013 +0200
     2.3 @@ -47,16 +47,9 @@
     2.4  lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
     2.5  unfolding bij_def inj_on_def by auto blast
     2.6  
     2.7 -lemma pair_mem_Collect_split:
     2.8 -"(\<lambda>x y. (x, y) \<in> {(x, y). P x y}) = P"
     2.9 -by simp
    2.10 -
    2.11  lemma Collect_pair_mem_eq: "{(x, y). (x, y) \<in> R} = R"
    2.12  by simp
    2.13  
    2.14 -lemma Collect_fst_snd_mem_eq: "{p. (fst p, snd p) \<in> A} = A"
    2.15 -by simp
    2.16 -
    2.17  (* Operator: *)
    2.18  definition "Gr A f = {(a, f a) | a. a \<in> A}"
    2.19  
     3.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Sep 12 11:05:19 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Sep 12 11:23:49 2013 +0200
     3.3 @@ -102,7 +102,7 @@
     3.4    rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
     3.5      @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
     3.6    unfold_thms_tac ctxt (srel_def ::
     3.7 -    @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
     3.8 +    @{thms pair_collapse Collect_mem_eq mem_Collect_eq prod.cases fst_conv snd_conv
     3.9        split_conv}) THEN
    3.10    rtac refl 1;
    3.11