# HG changeset patch
# User traytel
# Date 1348223276 -7200
# Node ID 675b9df572dfe6d7f5eaedc936baf24697693a48
# Parent  6b48c76f5b3fadb3cb891d3e9f7361e447501497
rel_Gr does not depend on map_wpull

diff -r 6b48c76f5b3f -r 675b9df572df src/HOL/Codatatype/BNF_Def.thy
--- a/src/HOL/Codatatype/BNF_Def.thy	Fri Sep 21 12:07:59 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Def.thy	Fri Sep 21 12:27:56 2012 +0200
@@ -25,6 +25,23 @@
 "R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
 unfolding converse_def by auto
 
+definition convol ("<_ , _>") where
+"<f , g> \<equiv> %a. (f a, g a)"
+
+lemma fst_convol:
+"fst o <f , g> = f"
+apply(rule ext)
+unfolding convol_def by simp
+
+lemma snd_convol:
+"snd o <f , g> = g"
+apply(rule ext)
+unfolding convol_def by simp
+
+lemma convol_memI:
+"\<lbrakk>f x = f' x; g x = g' x; P x\<rbrakk> \<Longrightarrow> <f , g> x \<in> {(f' a, g' a) |a. P a}"
+unfolding convol_def by auto
+
 definition csquare where
 "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
 
diff -r 6b48c76f5b3f -r 675b9df572df src/HOL/Codatatype/BNF_FP.thy
--- a/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 21 12:07:59 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 21 12:27:56 2012 +0200
@@ -38,19 +38,6 @@
 lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
 by simp
 
-definition convol ("<_ , _>") where
-"<f , g> \<equiv> %a. (f a, g a)"
-
-lemma fst_convol:
-"fst o <f , g> = f"
-apply(rule ext)
-unfolding convol_def by simp
-
-lemma snd_convol:
-"snd o <f , g> = g"
-apply(rule ext)
-unfolding convol_def by simp
-
 lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x"
 unfolding o_def fun_eq_iff by simp
 
diff -r 6b48c76f5b3f -r 675b9df572df src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 12:07:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 12:27:56 2012 +0200
@@ -989,8 +989,7 @@
             val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
           in
             Skip_Proof.prove lthy [] [] goal
-              (mk_rel_Gr_tac rel_O_Grs (#map_id axioms) (#map_cong axioms)
-                (#map_wpull axioms) (Lazy.force in_cong) (Lazy.force map_id')
+              (mk_rel_Gr_tac rel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
                 (Lazy.force map_comp') (map Lazy.force set_natural'))
             |> Thm.close_derivation
           end;
diff -r 6b48c76f5b3f -r 675b9df572df src/HOL/Codatatype/Tools/bnf_def_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 12:07:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 12:27:56 2012 +0200
@@ -15,7 +15,7 @@
   val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_set_natural': thm -> thm
 
-  val mk_rel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
+  val mk_rel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
   val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
   val mk_rel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
@@ -63,7 +63,7 @@
         rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
         rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
 
-fun mk_rel_Gr_tac rel_O_Grs map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
+fun mk_rel_Gr_tac rel_O_Grs map_id map_cong map_id' map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
@@ -89,17 +89,19 @@
         rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
         REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac,
-        rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
-        REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
-        rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
-        CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
-          rtac @{thm image_mono}, atac]) set_naturals,
-        rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
         rtac @{thm relcompI}, rtac @{thm converseI},
-        REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
-          rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, etac sym,
-          etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
-          REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
+        EVERY' (map2 (fn convol => fn map_id =>
+          EVERY' [rtac CollectI, rtac exI, rtac conjI,
+            rtac Pair_eqI, rtac conjI, rtac refl, rtac sym,
+            rtac (box_equals OF [map_cong, map_comp RS sym, map_id]),
+            REPEAT_DETERM_N n o rtac (convol RS fun_cong),
+            REPEAT_DETERM o eresolve_tac [CollectE, conjE],
+            rtac CollectI,
+            CONJ_WRAP' (fn thm =>
+              EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
+                rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac])
+            set_naturals])
+          @{thms fst_convol snd_convol} [map_id', refl])] 1
   end;
 
 fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =