simpler (forward) derivation of strong (up-to equality) coinduction properties

--- a/src/HOL/BNF/BNF_FP_Basic.thy	Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy	Tue Aug 20 17:39:07 2013 +0200
@@ -147,6 +147,12 @@
   "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
   unfolding fun_rel_def ..
 
+lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
+  by auto
+
+lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
+  by auto
+
 ML_file "Tools/bnf_fp_util.ML"
 ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/bnf_fp_def_sugar.ML"

--- a/src/HOL/BNF/BNF_GFP.thy	Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Tue Aug 20 17:39:07 2013 +0200
@@ -70,9 +70,6 @@
 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
 unfolding image2_def by auto
 
-lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
-by auto
-
 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
 by auto
 

--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue Aug 20 17:39:07 2013 +0200
@@ -179,6 +179,8 @@
   val mk_xtor_un_fold_o_map_thms: fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
 
+  val mk_strong_coinduct_thm: int -> thm -> thm list -> thm list -> Proof.context -> thm
+
   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> 'a) ->
     binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory ->
@@ -552,6 +554,24 @@
     split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems)
   end;
 
+fun mk_strong_coinduct_thm m coind rel_eqs rel_monos ctxt =
+  let
+    val n = Thm.nprems_of coind;
+    fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
+      |> pairself (certify ctxt);
+    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
+    fun mk_unfold rel_eq rel_mono =
+      let
+        val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
+        val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
+      in eq RS (mono RS @{thm predicate2D}) RS @{thm eqTrueI} end;
+    val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
+      imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
+  in
+    Thm.instantiate ([], insts) coind
+    |> unfold_thms ctxt unfolds
+  end;
+
 fun fp_bnf construct_fp bs resBs eqs lthy =
   let
     val timer = time (Timer.startRealTimer ());

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Aug 20 17:39:07 2013 +0200
@@ -2019,48 +2019,36 @@
 
     val timer = time (timer "corec definitions & thms");
 
-    (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
-    val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm, dtor_strong_coinduct_thm) =
+    val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) =
       let
         val zs = Jzs1 @ Jzs2;
         val frees = phis @ zs;
 
-        fun mk_phi strong_eq phi z1 z2 = if strong_eq
-          then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2)
-            (HOLogic.mk_disj (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2))))
-          else phi;
-
-        fun phi_rels strong_eq =
-          map3 (fn phi => fn z1 => fn z2 => mk_phi strong_eq phi z1 z2) phis Jzs1 Jzs2;
-
         val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
 
         fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map3 mk_concl phis Jzs1 Jzs2));
 
-        fun mk_rel_prem strong_eq phi dtor rel Jz Jz_copy =
+        fun mk_rel_prem phi dtor rel Jz Jz_copy =
           let
-            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phi_rels strong_eq) $
+            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phis) $
               (dtor $ Jz) $ (dtor $ Jz_copy);
           in
             HOLogic.mk_Trueprop
               (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
           end;
 
-        val rel_prems = map5 (mk_rel_prem false) phis dtors rels Jzs Jzs_copy;
-        val rel_strong_prems = map5 (mk_rel_prem true) phis dtors rels Jzs Jzs_copy;
-
+        val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy;
         val dtor_coinduct_goal =
           fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
-        val coinduct_params = rev (Term.add_tfrees dtor_coinduct_goal []);
 
         val dtor_coinduct =
           Goal.prove_sorry lthy [] [] dtor_coinduct_goal
             (K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs))
           |> Thm.close_derivation;
 
-        fun mk_prem strong_eq phi dtor map_nth sets Jz Jz_copy FJz =
+        fun mk_prem phi dtor map_nth sets Jz Jz_copy FJz =
           let
             val xs = [Jz, Jz_copy];
 
@@ -2070,7 +2058,7 @@
             fun mk_set_conjunct set phi z1 z2 =
               list_all_free [z1, z2]
                 (HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (z1, z2), set $ FJz),
-                  mk_phi strong_eq phi z1 z2 $ z1 $ z2));
+                  phi $ z1 $ z2));
 
             val concl = list_exists_free [FJz] (HOLogic.mk_conj
               (Library.foldr1 HOLogic.mk_conj (map2 mk_map_conjunct [fstsTs, sndsTs] xs),
@@ -2081,31 +2069,21 @@
               (HOLogic.mk_Trueprop (Term.list_comb (phi, xs)), HOLogic.mk_Trueprop concl))
           end;
 
-        fun mk_prems strong_eq =
-          map7 (mk_prem strong_eq) phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs;
-
-        val prems = mk_prems false;
-        val strong_prems = mk_prems true;
+        val prems = map7 mk_prem phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs;
 
         val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl));
         val dtor_map_coinduct =
           Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal
             (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
           |> Thm.close_derivation;
-
-        val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
-        val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
-
-        val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] []
-            (fold_rev Logic.all zs (Logic.list_implies (rel_strong_prems, concl)))
-            (K (mk_dtor_strong_coinduct_tac lthy m cTs cts dtor_coinduct rel_monos rel_eqs)))
-          |> Thm.close_derivation;
       in
-        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []),
-         dtor_coinduct, dtor_strong_coinduct)
+        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_coinduct)
       end;
 
+    (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
+    val dtor_strong_coinduct_thm =
+      mk_strong_coinduct_thm m dtor_coinduct_thm rel_eqs rel_monos lthy;
+
     val timer = time (timer "coinduction");
 
     fun mk_dtor_map_DEADID_thm dtor_inject map_id =

--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Aug 20 17:39:07 2013 +0200
@@ -41,8 +41,6 @@
   val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
   val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
   val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
-  val mk_dtor_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
-    cterm option list -> thm -> thm list -> thm list -> tactic
   val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
     thm -> thm -> thm list -> thm list -> thm list list -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
@@ -989,18 +987,6 @@
     CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
       rtac CollectI, etac @{thm prod_caseI}])) rel_congs] 1;
 
-fun mk_dtor_strong_coinduct_tac ctxt m cTs cts dtor_coinduct rel_monos rel_eqs =
-  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct),
-    EVERY' (map2 (fn rel_mono => fn rel_eq =>
-      EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
-        etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (rel_mono RS @{thm predicate2D}),
-        REPEAT_DETERM_N m o rtac @{thm order_refl},
-        REPEAT_DETERM_N (length rel_monos) o rtac @{thm eq_subset},
-        rtac (rel_eq RS sym RS @{thm eq_refl} RS @{thm predicate2D}), rtac refl])
-    rel_monos rel_eqs),
-    rtac impI, REPEAT_DETERM o etac conjE,
-    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_eqs] 1;
-
 fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
   let
     val n = length ks;