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

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

     3.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue Aug 20 16:10:58 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue Aug 20 17:39:07 2013 +0200
     3.3 @@ -179,6 +179,8 @@
     3.4    val mk_xtor_un_fold_o_map_thms: fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     3.5      thm list -> thm list -> thm list
     3.6  
     3.7 +  val mk_strong_coinduct_thm: int -> thm -> thm list -> thm list -> Proof.context -> thm
     3.8 +
     3.9    val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
    3.10        BNF_Def.bnf list -> local_theory -> 'a) ->
    3.11      binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory ->
    3.12 @@ -552,6 +554,24 @@
    3.13      split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems)
    3.14    end;
    3.15  
    3.16 +fun mk_strong_coinduct_thm m coind rel_eqs rel_monos ctxt =
    3.17 +  let
    3.18 +    val n = Thm.nprems_of coind;
    3.19 +    fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
    3.20 +      |> pairself (certify ctxt);
    3.21 +    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
    3.22 +    fun mk_unfold rel_eq rel_mono =
    3.23 +      let
    3.24 +        val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
    3.25 +        val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
    3.26 +      in eq RS (mono RS @{thm predicate2D}) RS @{thm eqTrueI} end;
    3.27 +    val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
    3.28 +      imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
    3.29 +  in
    3.30 +    Thm.instantiate ([], insts) coind
    3.31 +    |> unfold_thms ctxt unfolds
    3.32 +  end;
    3.33 +
    3.34  fun fp_bnf construct_fp bs resBs eqs lthy =
    3.35    let
    3.36      val timer = time (Timer.startRealTimer ());

     4.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Aug 20 16:10:58 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Aug 20 17:39:07 2013 +0200
     4.3 @@ -2019,48 +2019,36 @@
     4.4  
     4.5      val timer = time (timer "corec definitions & thms");
     4.6  
     4.7 -    (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
     4.8 -    val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm, dtor_strong_coinduct_thm) =
     4.9 +    val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) =
    4.10        let
    4.11          val zs = Jzs1 @ Jzs2;
    4.12          val frees = phis @ zs;
    4.13  
    4.14 -        fun mk_phi strong_eq phi z1 z2 = if strong_eq
    4.15 -          then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2)
    4.16 -            (HOLogic.mk_disj (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2))))
    4.17 -          else phi;
    4.18 -
    4.19 -        fun phi_rels strong_eq =
    4.20 -          map3 (fn phi => fn z1 => fn z2 => mk_phi strong_eq phi z1 z2) phis Jzs1 Jzs2;
    4.21 -
    4.22          val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
    4.23  
    4.24          fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
    4.25          val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    4.26            (map3 mk_concl phis Jzs1 Jzs2));
    4.27  
    4.28 -        fun mk_rel_prem strong_eq phi dtor rel Jz Jz_copy =
    4.29 +        fun mk_rel_prem phi dtor rel Jz Jz_copy =
    4.30            let
    4.31 -            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phi_rels strong_eq) $
    4.32 +            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phis) $
    4.33                (dtor $ Jz) $ (dtor $ Jz_copy);
    4.34            in
    4.35              HOLogic.mk_Trueprop
    4.36                (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
    4.37            end;
    4.38  
    4.39 -        val rel_prems = map5 (mk_rel_prem false) phis dtors rels Jzs Jzs_copy;
    4.40 -        val rel_strong_prems = map5 (mk_rel_prem true) phis dtors rels Jzs Jzs_copy;
    4.41 -
    4.42 +        val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy;
    4.43          val dtor_coinduct_goal =
    4.44            fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
    4.45 -        val coinduct_params = rev (Term.add_tfrees dtor_coinduct_goal []);
    4.46  
    4.47          val dtor_coinduct =
    4.48            Goal.prove_sorry lthy [] [] dtor_coinduct_goal
    4.49              (K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs))
    4.50            |> Thm.close_derivation;
    4.51  
    4.52 -        fun mk_prem strong_eq phi dtor map_nth sets Jz Jz_copy FJz =
    4.53 +        fun mk_prem phi dtor map_nth sets Jz Jz_copy FJz =
    4.54            let
    4.55              val xs = [Jz, Jz_copy];
    4.56  
    4.57 @@ -2070,7 +2058,7 @@
    4.58              fun mk_set_conjunct set phi z1 z2 =
    4.59                list_all_free [z1, z2]
    4.60                  (HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (z1, z2), set $ FJz),
    4.61 -                  mk_phi strong_eq phi z1 z2 $ z1 $ z2));
    4.62 +                  phi $ z1 $ z2));
    4.63  
    4.64              val concl = list_exists_free [FJz] (HOLogic.mk_conj
    4.65                (Library.foldr1 HOLogic.mk_conj (map2 mk_map_conjunct [fstsTs, sndsTs] xs),
    4.66 @@ -2081,31 +2069,21 @@
    4.67                (HOLogic.mk_Trueprop (Term.list_comb (phi, xs)), HOLogic.mk_Trueprop concl))
    4.68            end;
    4.69  
    4.70 -        fun mk_prems strong_eq =
    4.71 -          map7 (mk_prem strong_eq) phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs;
    4.72 -
    4.73 -        val prems = mk_prems false;
    4.74 -        val strong_prems = mk_prems true;
    4.75 +        val prems = map7 mk_prem phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs;
    4.76  
    4.77          val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl));
    4.78          val dtor_map_coinduct =
    4.79            Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal
    4.80              (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
    4.81            |> Thm.close_derivation;
    4.82 -
    4.83 -        val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
    4.84 -        val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
    4.85 -
    4.86 -        val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
    4.87 -          (Goal.prove_sorry lthy [] []
    4.88 -            (fold_rev Logic.all zs (Logic.list_implies (rel_strong_prems, concl)))
    4.89 -            (K (mk_dtor_strong_coinduct_tac lthy m cTs cts dtor_coinduct rel_monos rel_eqs)))
    4.90 -          |> Thm.close_derivation;
    4.91        in
    4.92 -        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []),
    4.93 -         dtor_coinduct, dtor_strong_coinduct)
    4.94 +        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_coinduct)
    4.95        end;
    4.96  
    4.97 +    (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
    4.98 +    val dtor_strong_coinduct_thm =
    4.99 +      mk_strong_coinduct_thm m dtor_coinduct_thm rel_eqs rel_monos lthy;
   4.100 +
   4.101      val timer = time (timer "coinduction");
   4.102  
   4.103      fun mk_dtor_map_DEADID_thm dtor_inject map_id =

     5.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Aug 20 16:10:58 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Aug 20 17:39:07 2013 +0200
     5.3 @@ -41,8 +41,6 @@
     5.4    val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
     5.5    val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
     5.6    val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
     5.7 -  val mk_dtor_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
     5.8 -    cterm option list -> thm -> thm list -> thm list -> tactic
     5.9    val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
    5.10      thm -> thm -> thm list -> thm list -> thm list list -> tactic
    5.11    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
    5.12 @@ -989,18 +987,6 @@
    5.13      CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
    5.14        rtac CollectI, etac @{thm prod_caseI}])) rel_congs] 1;
    5.15  
    5.16 -fun mk_dtor_strong_coinduct_tac ctxt m cTs cts dtor_coinduct rel_monos rel_eqs =
    5.17 -  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct),
    5.18 -    EVERY' (map2 (fn rel_mono => fn rel_eq =>
    5.19 -      EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
    5.20 -        etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (rel_mono RS @{thm predicate2D}),
    5.21 -        REPEAT_DETERM_N m o rtac @{thm order_refl},
    5.22 -        REPEAT_DETERM_N (length rel_monos) o rtac @{thm eq_subset},
    5.23 -        rtac (rel_eq RS sym RS @{thm eq_refl} RS @{thm predicate2D}), rtac refl])
    5.24 -    rel_monos rel_eqs),
    5.25 -    rtac impI, REPEAT_DETERM o etac conjE,
    5.26 -    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_eqs] 1;
    5.27 -
    5.28  fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
    5.29    let
    5.30      val n = length ks;