1.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Fri Sep 21 18:25:17 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Fri Sep 21 19:17:49 2012 +0200
     1.3 @@ -33,6 +33,8 @@
     1.4    val ctor_foldsN: string
     1.5    val ctor_recN: string
     1.6    val ctor_recsN: string
     1.7 +  val ctor_relN: string
     1.8 +  val ctor_srelN: string
     1.9    val disc_unfold_iffN: string
    1.10    val disc_unfoldsN: string
    1.11    val disc_corec_iffN: string
    1.12 @@ -42,9 +44,10 @@
    1.13    val dtor_relN: string
    1.14    val dtor_corecN: string
    1.15    val dtor_corecsN: string
    1.16 +  val dtor_ctorN: string
    1.17    val dtor_exhaustN: string
    1.18 -  val dtor_ctorN: string
    1.19    val dtor_injectN: string
    1.20 +  val dtor_srelN: string
    1.21    val dtor_strong_coinductN: string
    1.22    val dtor_unfoldN: string
    1.23    val dtor_unfold_uniqueN: string
    1.24 @@ -74,7 +77,6 @@
    1.25    val set_set_inclN: string
    1.26    val simpsN: string
    1.27    val srel_coinductN: string
    1.28 -  val dtor_srelN: string
    1.29    val srel_strong_coinductN: string
    1.30    val strTN: string
    1.31    val str_initN: string
    1.32 @@ -225,7 +227,9 @@
    1.33  val rel_coinductN = relN ^ "_" ^ coinductN
    1.34  val srel_coinductN = srelN ^ "_" ^ coinductN
    1.35  val simpN = "_simp";
    1.36 +val ctor_srelN = ctorN ^ "_" ^ srelN
    1.37  val dtor_srelN = dtorN ^ "_" ^ srelN
    1.38 +val ctor_relN = ctorN ^ "_" ^ relN
    1.39  val dtor_relN = dtorN ^ "_" ^ relN
    1.40  val strongN = "strong_"
    1.41  val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Fri Sep 21 18:25:17 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Fri Sep 21 19:17:49 2012 +0200
     2.3 @@ -499,6 +499,9 @@
     2.4          ((wrap, define_rec_likes), lthy')
     2.5        end;
     2.6  
     2.7 +    fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) =
     2.8 +      fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list8
     2.9 +
    2.10      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    2.11      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
    2.12      val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
    2.13 @@ -854,7 +857,6 @@
    2.14  
    2.15          val notes =
    2.16            [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
    2.17 -           (unfoldsN, unfold_thmss, []),
    2.18             (corecsN, corec_thmss, []),
    2.19             (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs),
    2.20             (disc_unfoldsN, disc_unfold_thmss, simp_attrs),
    2.21 @@ -862,7 +864,8 @@
    2.22             (disc_corecsN, disc_corec_thmss, simp_attrs),
    2.23             (sel_unfoldsN, sel_unfold_thmss, simp_attrs),
    2.24             (sel_corecsN, sel_corec_thmss, simp_attrs),
    2.25 -           (simpsN, simp_thmss, [])]
    2.26 +           (simpsN, simp_thmss, []),
    2.27 +           (unfoldsN, unfold_thmss, [])]
    2.28            |> maps (fn (thmN, thmss, attrs) =>
    2.29              map_filter (fn (_, []) => NONE | (b, thms) =>
    2.30                SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
    2.31 @@ -871,16 +874,19 @@
    2.32          lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
    2.33        end;
    2.34  
    2.35 -    fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) =
    2.36 -      fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list8
    2.37 +    fun derive_pred_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _, ctr_defss, unfold_defs,
    2.38 +        corec_defs), lthy) =
    2.39 +      lthy;
    2.40  
    2.41      val lthy' = lthy
    2.42        |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_folds ~~
    2.43          fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
    2.44          ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
    2.45        |>> split_list |> wrap_types_and_define_rec_likes
    2.46 -      |> (if lfp then derive_induct_fold_rec_thms_for_types
    2.47 -          else derive_coinduct_unfold_corec_thms_for_types);
    2.48 +      |> `(if lfp then derive_induct_fold_rec_thms_for_types
    2.49 +           else derive_coinduct_unfold_corec_thms_for_types)
    2.50 +      |> swap |>> fst
    2.51 +      |> derive_pred_thms_for_types;
    2.52  
    2.53      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
    2.54        (if lfp then "" else "co") ^ "datatype"));

     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 21 18:25:17 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 21 19:17:49 2012 +0200
     3.3 @@ -2925,7 +2925,7 @@
     3.4            in
     3.5              map3 (fn goal => fn srel_def => fn dtor_Jsrel =>
     3.6                Skip_Proof.prove lthy [] [] goal
     3.7 -                (mk_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel)
     3.8 +                (mk_ctor_or_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel)
     3.9                |> Thm.close_derivation)
    3.10              goals srel_defs dtor_Jsrel_thms
    3.11            end;

     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 21 18:25:17 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 21 19:17:49 2012 +0200
     4.3 @@ -1742,7 +1742,7 @@
     4.4          val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
     4.5          val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
     4.6  
     4.7 -        val dtor_Isrel_thms =
     4.8 +        val ctor_Isrel_thms =
     4.9            let
    4.10              fun mk_goal xF yF ctor ctor' IsrelR srelR = fold_rev Logic.all (xF :: yF :: IRs)
    4.11                (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IsrelR),
    4.12 @@ -1753,24 +1753,24 @@
    4.13                fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor =>
    4.14                fn set_naturals => fn set_incls => fn set_set_inclss =>
    4.15                Skip_Proof.prove lthy [] [] goal
    4.16 -               (K (mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps
    4.17 +               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps
    4.18                   ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
    4.19                |> Thm.close_derivation)
    4.20              ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
    4.21                ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
    4.22            end;
    4.23  
    4.24 -        val dtor_Irel_thms =
    4.25 +        val ctor_Irel_thms =
    4.26            let
    4.27              fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
    4.28                (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF));
    4.29              val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
    4.30            in
    4.31 -            map3 (fn goal => fn srel_def => fn dtor_Isrel =>
    4.32 +            map3 (fn goal => fn srel_def => fn ctor_Isrel =>
    4.33                Skip_Proof.prove lthy [] [] goal
    4.34 -                (mk_dtor_rel_tac srel_def Irel_defs Isrel_defs dtor_Isrel)
    4.35 +                (mk_ctor_or_dtor_rel_tac srel_def Irel_defs Isrel_defs ctor_Isrel)
    4.36                |> Thm.close_derivation)
    4.37 -            goals srel_defs dtor_Isrel_thms
    4.38 +            goals srel_defs ctor_Isrel_thms
    4.39            end;
    4.40  
    4.41          val timer = time (timer "additional properties");
    4.42 @@ -1783,8 +1783,8 @@
    4.43              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    4.44  
    4.45          val Ibnf_notes =
    4.46 -          [(dtor_relN, map single dtor_Irel_thms),
    4.47 -          (dtor_srelN, map single dtor_Isrel_thms),
    4.48 +          [(ctor_relN, map single ctor_Irel_thms),
    4.49 +          (ctor_srelN, map single ctor_Isrel_thms),
    4.50            (map_simpsN, map single folded_map_simp_thms),
    4.51            (set_inclN, set_incl_thmss),
    4.52            (set_set_inclN, map flat set_set_incl_thmsss)] @

     5.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Fri Sep 21 19:17:49 2012 +0200
     5.3 @@ -22,9 +22,9 @@
     5.4      thm list -> tactic
     5.5    val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
     5.6      {prems: 'a, context: Proof.context} -> tactic
     5.7 +  val mk_ctor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
     5.8 +    thm list -> thm list -> thm list list -> tactic
     5.9    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
    5.10 -  val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
    5.11 -    thm list -> thm list -> thm list list -> tactic
    5.12    val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
    5.13    val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
    5.14    val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm ->
    5.15 @@ -770,7 +770,7 @@
    5.16            EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
    5.17              REPEAT_DETERM_N n o etac UnE]))))] 1);
    5.18  
    5.19 -fun mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
    5.20 +fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
    5.21    ctor_dtor set_naturals set_incls set_set_inclss =
    5.22    let
    5.23      val m = length set_incls;

     6.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Fri Sep 21 19:17:49 2012 +0200
     6.3 @@ -27,8 +27,8 @@
     6.4    val mk_Abs_inj_thm: thm -> thm
     6.5  
     6.6    val simple_srel_O_Gr_tac: Proof.context -> tactic
     6.7 -  val mk_dtor_rel_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
     6.8 -    tactic
     6.9 +  val mk_ctor_or_dtor_rel_tac:
    6.10 +    thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
    6.11  
    6.12    val mk_map_comp_id_tac: thm -> tactic
    6.13    val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
    6.14 @@ -101,7 +101,7 @@
    6.15  fun simple_srel_O_Gr_tac ctxt =
    6.16    unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
    6.17  
    6.18 -fun mk_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
    6.19 +fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
    6.20    unfold_thms_tac ctxt IJrel_defs THEN
    6.21    subst_tac ctxt [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
    6.22      @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel] 1 THEN