author traytel Thu Sep 12 11:23:49 2013 +0200 (2013-09-12) changeset 53560 4b5f42cfa244 parent 53559 3858246c7c8f child 53561 92bcac4f9ac9
removed unused/inlinable theorems
 src/HOL/BNF/BNF_Def.thy file | annotate | diff | revisions src/HOL/BNF/BNF_Util.thy file | annotate | diff | revisions src/HOL/BNF/Tools/bnf_tactics.ML file | annotate | diff | revisions
```     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
```