generate 'set_induct' theorem for codatatypes
authordesharna
Wed Jul 30 10:50:28 2014 +0200 (2014-07-30)
changeset 57700a2c4adb839a9
parent 57699 a6cf197c1f1e
child 57701 13b446b62825
generate 'set_induct' theorem for codatatypes
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jul 30 00:50:41 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jul 30 10:50:28 2014 +0200
     1.3 @@ -103,6 +103,7 @@
     1.4  val sel_mapN = "sel_map";
     1.5  val sel_setN = "sel_set";
     1.6  val set_emptyN = "set_empty";
     1.7 +val set_inductN = "set_induct";
     1.8  
     1.9  structure Data = Generic_Data
    1.10  (
    1.11 @@ -112,10 +113,16 @@
    1.12    fun merge data : T = Symtab.merge (K true) data;
    1.13  );
    1.14  
    1.15 -fun choose_relator Rs AB = find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) Rs;
    1.16 -fun build_the_rel ctxt Rs Ts A B = build_rel ctxt Ts (the o choose_relator Rs) (A, B);
    1.17 +fun choose_binary_fun fs AB =
    1.18 +  find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs;
    1.19 +fun build_binary_fun_app fs a b =
    1.20 +  Option.map (rapp b o rapp a) (choose_binary_fun fs (fastype_of a, fastype_of b));
    1.21 +
    1.22 +fun build_the_rel ctxt Rs Ts A B = build_rel ctxt Ts (the o choose_binary_fun Rs) (A, B);
    1.23  fun build_rel_app ctxt Rs Ts a b = build_the_rel ctxt Rs Ts (fastype_of a) (fastype_of b) $ a $ b;
    1.24  
    1.25 +val name_of_set = name_of_const "set";
    1.26 +
    1.27  fun fp_sugar_of ctxt =
    1.28    Symtab.lookup (Data.get (Context.Proof ctxt))
    1.29    #> Option.map (transfer_fp_sugar ctxt);
    1.30 @@ -759,6 +766,98 @@
    1.31       mk_coinduct_attributes fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss)
    1.32    end;
    1.33  
    1.34 +fun derive_set_induct_thms_for_types lthy nn fpTs ctrss setss dtor_set_inducts exhausts
    1.35 +    set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses =
    1.36 +  let
    1.37 +    fun mk_prems A Ps ctr_args t ctxt =
    1.38 +      (case fastype_of t of
    1.39 +        Type (type_name, xs) =>
    1.40 +        (case bnf_of ctxt type_name of
    1.41 +          NONE => ([], ctxt)
    1.42 +        | SOME bnf =>
    1.43 +          let
    1.44 +            fun seq_assm a set ctxt =
    1.45 +              let
    1.46 +                val X = HOLogic.dest_setT (range_type (fastype_of set));
    1.47 +                val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
    1.48 +                val assm = mk_Trueprop_mem (x, set $ a);
    1.49 +              in
    1.50 +                (case build_binary_fun_app Ps x a of
    1.51 +                  NONE =>
    1.52 +                  mk_prems A Ps ctr_args x ctxt'
    1.53 +                  |>> map (Logic.all x o Logic.mk_implies o pair assm)
    1.54 +                | SOME f =>
    1.55 +                  ([Logic.all x
    1.56 +                      (Logic.mk_implies (assm,
    1.57 +                         Logic.mk_implies (HOLogic.mk_Trueprop f,
    1.58 +                           HOLogic.mk_Trueprop (the (build_binary_fun_app Ps x ctr_args)))))],
    1.59 +                   ctxt'))
    1.60 +              end;
    1.61 +          in
    1.62 +            fold_map (seq_assm t o mk_set xs) (sets_of_bnf bnf) ctxt
    1.63 +            |>> flat
    1.64 +          end)
    1.65 +      | T =>
    1.66 +        if T = A then ([HOLogic.mk_Trueprop (the (build_binary_fun_app Ps t ctr_args))], ctxt)
    1.67 +        else ([], ctxt));
    1.68 +
    1.69 +    fun mk_prems_for_ctr A Ps ctr ctxt =
    1.70 +      let
    1.71 +        val (args, ctxt') = mk_Frees "arg" (binder_types (fastype_of ctr)) ctxt;
    1.72 +      in
    1.73 +        fold_map (mk_prems A Ps (list_comb (ctr, args))) args ctxt'
    1.74 +        |>> map (fold_rev Logic.all args) o flat
    1.75 +        |>> (fn prems => (prems, mk_names (length prems) (name_of_ctr ctr)))
    1.76 +      end;
    1.77 +
    1.78 +    fun mk_prems_and_concl_for_type A Ps ((fpT, ctrs), set) ctxt =
    1.79 +      let
    1.80 +        val ((x, fp), ctxt') = ctxt
    1.81 +          |> yield_singleton (mk_Frees "x") A
    1.82 +          ||>> yield_singleton (mk_Frees "a") fpT;
    1.83 +        val concl = mk_Ball (set $ fp) (Term.absfree (dest_Free x)
    1.84 +          (the (build_binary_fun_app Ps x fp)));
    1.85 +      in
    1.86 +        fold_map (mk_prems_for_ctr A Ps) ctrs ctxt'
    1.87 +        |>> split_list
    1.88 +        |>> map_prod flat flat
    1.89 +        |>> apfst (rpair concl)
    1.90 +      end;
    1.91 +
    1.92 +    fun mk_thm ctxt fpTs ctrss sets =
    1.93 +      let
    1.94 +        val A = HOLogic.dest_setT (range_type (fastype_of (hd sets)));
    1.95 +        val (Ps, ctxt') = mk_Frees "P" (map (fn fpT => A --> fpT --> HOLogic.boolT) fpTs) ctxt;
    1.96 +        val (((premises, conclusion), case_names), ctxt'') =
    1.97 +          (fold_map (mk_prems_and_concl_for_type A Ps) (fpTs ~~ ctrss ~~ sets) ctxt')
    1.98 +          |>> apfst split_list o split_list
    1.99 +          |>> apfst (apfst flat)
   1.100 +          |>> apfst (apsnd (Library.foldr1 HOLogic.mk_conj))
   1.101 +          |>> apsnd flat;
   1.102 +
   1.103 +        val thm =  Goal.prove_sorry lthy [] premises (HOLogic.mk_Trueprop conclusion)
   1.104 +          (fn {context = ctxt, prems = prems} =>
   1.105 +             mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts
   1.106 +              set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
   1.107 +          |> singleton (Proof_Context.export ctxt'' ctxt)
   1.108 +          |> Thm.close_derivation;
   1.109 +
   1.110 +        val case_names_attr =
   1.111 +          Attrib.internal (K (Rule_Cases.case_names (quasi_unambiguous_case_names case_names)));
   1.112 +        val induct_set_attrs = map (Attrib.internal o K o Induct.induct_pred o name_of_set) sets;
   1.113 +      in
   1.114 +        (thm, case_names_attr :: induct_set_attrs)
   1.115 +      end
   1.116 +    val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
   1.117 +  in
   1.118 +    map (fn Asets =>
   1.119 +      let
   1.120 +        fun massage_thm thm = rotate_prems (~1) (thm RS bspec);
   1.121 +      in
   1.122 +        mk_thm lthy fpTs ctrss Asets |> nn = 1 ? map_prod massage_thm (cons consumes_attr)
   1.123 +      end) (transpose setss)
   1.124 +  end;
   1.125 +
   1.126  fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
   1.127      dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
   1.128      kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
   1.129 @@ -1072,7 +1171,7 @@
   1.130      val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
   1.131               dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
   1.132               ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
   1.133 -             xtor_co_rec_thms, rel_xtor_co_induct_thm, ...},
   1.134 +             xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms, ...},
   1.135             lthy)) =
   1.136        fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
   1.137          (map dest_TFree killed_As) fp_eqs no_defs_lthy0
   1.138 @@ -1143,8 +1242,8 @@
   1.139  
   1.140      fun massage_simple_notes base =
   1.141        filter_out (null o #2)
   1.142 -      #> map (fn (thmN, thms, attrs) =>
   1.143 -        ((Binding.qualify true base (Binding.name thmN), attrs), [(thms, [])]));
   1.144 +      #> map (fn (thmN, thms, f_attrs) =>
   1.145 +        ((Binding.qualify true base (Binding.name thmN), []), map_index (fn (i, thm) => ([thm], f_attrs i)) thms));
   1.146  
   1.147      val massage_multi_notes =
   1.148        maps (fn (thmN, thmss, attrs) =>
   1.149 @@ -1611,17 +1710,17 @@
   1.150                  |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   1.151  
   1.152                val notes =
   1.153 -                [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
   1.154 -                 (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
   1.155 -                 (rel_casesN, [rel_cases_thm], rel_cases_attrs),
   1.156 -                 (rel_distinctN, rel_distinct_thms, simp_attrs),
   1.157 -                 (rel_injectN, rel_inject_thms, simp_attrs),
   1.158 -                 (rel_introsN, rel_intro_thms, []),
   1.159 -                 (rel_selN, rel_sel_thms, []),
   1.160 -                 (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs),
   1.161 -                 (sel_mapN, sel_map_thms, []),
   1.162 -                 (sel_setN, sel_set_thms, []),
   1.163 -                 (set_emptyN, set_empty_thms, [])]
   1.164 +                [(disc_map_iffN, disc_map_iff_thms, K simp_attrs),
   1.165 +                 (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
   1.166 +                 (rel_casesN, [rel_cases_thm], K rel_cases_attrs),
   1.167 +                 (rel_distinctN, rel_distinct_thms, K simp_attrs),
   1.168 +                 (rel_injectN, rel_inject_thms, K simp_attrs),
   1.169 +                 (rel_introsN, rel_intro_thms, K []),
   1.170 +                 (rel_selN, rel_sel_thms, K []),
   1.171 +                 (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
   1.172 +                 (sel_mapN, sel_map_thms, K []),
   1.173 +                 (sel_setN, sel_set_thms, K []),
   1.174 +                 (set_emptyN, set_empty_thms, K [])]
   1.175                  |> massage_simple_notes fp_b_name;
   1.176  
   1.177                val (noted, lthy') =
   1.178 @@ -1692,8 +1791,8 @@
   1.179  
   1.180          val common_notes =
   1.181            (if nn > 1 then
   1.182 -             [(inductN, [induct_thm], induct_attrs),
   1.183 -              (rel_inductN, common_rel_induct_thms, common_rel_induct_attrs)]
   1.184 +             [(inductN, [induct_thm], K induct_attrs),
   1.185 +              (rel_inductN, common_rel_induct_thms, K common_rel_induct_attrs)]
   1.186             else
   1.187               [])
   1.188            |> massage_simple_notes fp_common_name;
   1.189 @@ -1765,17 +1864,25 @@
   1.190                 (rel_coinduct_attrs, common_rel_coinduct_attrs))
   1.191              end;
   1.192  
   1.193 +        val (set_induct_thms, set_induct_attrss) =
   1.194 +          derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars)
   1.195 +            (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_induct_thms
   1.196 +            (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss)
   1.197 +            dtor_ctors abs_inverses
   1.198 +          |> split_list;
   1.199 +
   1.200          val simp_thmss =
   1.201            map6 mk_simp_thms ctr_sugars
   1.202              (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
   1.203              mapss rel_injectss rel_distinctss setss;
   1.204  
   1.205          val common_notes =
   1.206 +          (set_inductN, set_induct_thms, nth set_induct_attrss) ::
   1.207            (if nn > 1 then
   1.208 -            [(coinductN, [coinduct_thm], common_coinduct_attrs),
   1.209 -             (rel_coinductN, common_rel_coinduct_thms, common_rel_coinduct_attrs),
   1.210 -             (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
   1.211 -          else [])
   1.212 +            [(coinductN, [coinduct_thm], K common_coinduct_attrs),
   1.213 +             (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs),
   1.214 +             (strong_coinductN, [strong_coinduct_thm], K common_coinduct_attrs)]
   1.215 +           else [])
   1.216            |> massage_simple_notes fp_common_name;
   1.217  
   1.218          val notes =
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Jul 30 00:50:41 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Jul 30 10:50:28 2014 +0200
     2.3 @@ -39,6 +39,8 @@
     2.4    val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
     2.5    val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
     2.6    val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
     2.7 +  val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list ->
     2.8 +    thm list -> thm list -> thm list -> thm list -> tactic
     2.9  end;
    2.10  
    2.11  structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
    2.12 @@ -257,7 +259,7 @@
    2.13          HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
    2.14            (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
    2.15              THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
    2.16 -        unfold_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
    2.17 +        unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
    2.18            @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
    2.19          TRYALL (hyp_subst_tac ctxt) THEN
    2.20          unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
    2.21 @@ -306,4 +308,28 @@
    2.22      SOME (thm RS eqFalseI) handle THM _ => NONE) discs) THEN
    2.23    ALLGOALS (rtac refl ORELSE' etac FalseE);
    2.24  
    2.25 +fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors
    2.26 +    Abs_pre_inverses =
    2.27 +  let
    2.28 +    val assms_ctor_defs =
    2.29 +      map (unfold_thms ctxt (@{thm BNF_Comp.id_bnf_comp_def} :: ctor_defs)) assms;
    2.30 +    val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
    2.31 +      |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
    2.32 +  in
    2.33 +    ALLGOALS (resolve_tac dtor_set_inducts) THEN
    2.34 +    TRYALL (resolve_tac exhausts' THEN_ALL_NEW
    2.35 +      (resolve_tac (map (fn ct => refl RS
    2.36 +         cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
    2.37 +        THEN' atac THEN' hyp_subst_tac ctxt)) THEN
    2.38 +    unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
    2.39 +      @{thms BNF_Comp.id_bnf_comp_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
    2.40 +        Un_empty_left Un_empty_right empty_iff singleton_iff}) THEN
    2.41 +    REPEAT_DETERM (HEADGOAL
    2.42 +      (TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN'
    2.43 +       REPEAT_DETERM o eresolve_tac @{thms UN_E UnE singletonE} THEN'
    2.44 +       fold (curry (op ORELSE')) (map (fn thm =>
    2.45 +         funpow (length (prems_of thm)) (fn tac => tac THEN' atac) (rtac thm)) assms_ctor_defs)
    2.46 +         (etac FalseE)))
    2.47 +  end;
    2.48 +
    2.49  end;
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Jul 30 00:50:41 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Jul 30 10:50:28 2014 +0200
     3.3 @@ -463,7 +463,8 @@
     3.4          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
     3.5          xtor_co_rec_thms = xtor_co_rec_thms,
     3.6          xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
     3.7 -        rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
     3.8 +        rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
     3.9 +        dtor_set_induct_thms = []}
    3.10         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
    3.11    in
    3.12      (fp_res, lthy)
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Jul 30 00:50:41 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Jul 30 10:50:28 2014 +0200
     4.3 @@ -25,7 +25,8 @@
     4.4       xtor_rel_thms: thm list,
     4.5       xtor_co_rec_thms: thm list,
     4.6       xtor_co_rec_o_map_thms: thm list,
     4.7 -     rel_xtor_co_induct_thm: thm}
     4.8 +     rel_xtor_co_induct_thm: thm,
     4.9 +     dtor_set_induct_thms: thm list}
    4.10  
    4.11    val morph_fp_result: morphism -> fp_result -> fp_result
    4.12  
    4.13 @@ -237,11 +238,12 @@
    4.14     xtor_rel_thms: thm list,
    4.15     xtor_co_rec_thms: thm list,
    4.16     xtor_co_rec_o_map_thms: thm list,
    4.17 -   rel_xtor_co_induct_thm: thm};
    4.18 +   rel_xtor_co_induct_thm: thm,
    4.19 +   dtor_set_induct_thms: thm list};
    4.20  
    4.21  fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
    4.22      dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
    4.23 -    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} =
    4.24 +    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms} =
    4.25    {Ts = map (Morphism.typ phi) Ts,
    4.26     bnfs = map (morph_bnf phi) bnfs,
    4.27     ctors = map (Morphism.term phi) ctors,
    4.28 @@ -257,7 +259,8 @@
    4.29     xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
    4.30     xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
    4.31     xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
    4.32 -   rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
    4.33 +   rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
    4.34 +   dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *)
    4.35  
    4.36  type fp_sugar =
    4.37    {T: typ,
     5.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Jul 30 00:50:41 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Jul 30 10:50:28 2014 +0200
     5.3 @@ -1659,12 +1659,12 @@
     5.4  
     5.5      (*register new codatatypes as BNFs*)
     5.6      val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jset_thmss',
     5.7 -      dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, lthy) =
     5.8 +      dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, dtor_Jset_induct_thms, lthy) =
     5.9        if m = 0 then
    5.10          (timer, replicate n DEADID_bnf,
    5.11          map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
    5.12          replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs,
    5.13 -        mk_Jrel_DEADID_coinduct_thm (), [], lthy)
    5.14 +        mk_Jrel_DEADID_coinduct_thm (), [], [], lthy)
    5.15        else let
    5.16          val fTs = map2 (curry op -->) passiveAs passiveBs;
    5.17          val gTs = map2 (curry op -->) passiveBs passiveCs;
    5.18 @@ -2464,7 +2464,8 @@
    5.19              bs thmss)
    5.20        in
    5.21          (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jset_thmss',
    5.22 -          dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, lthy)
    5.23 +          dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, dtor_Jset_induct_thms,
    5.24 +          lthy)
    5.25        end;
    5.26  
    5.27      val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
    5.28 @@ -2526,7 +2527,8 @@
    5.29         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
    5.30         xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
    5.31         xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
    5.32 -       xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm}
    5.33 +       xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
    5.34 +       dtor_set_induct_thms = dtor_Jset_induct_thms}
    5.35        |> morph_fp_result (substitute_noted_thm noted);
    5.36    in
    5.37      timer; (fp_res, lthy')
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Jul 30 00:50:41 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Jul 30 10:50:28 2014 +0200
     6.3 @@ -1814,7 +1814,8 @@
     6.4         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
     6.5         xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
     6.6         xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
     6.7 -       xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm}
     6.8 +       xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
     6.9 +       dtor_set_induct_thms = []}
    6.10        |> morph_fp_result (substitute_noted_thm noted);
    6.11    in
    6.12      timer; (fp_res, lthy')
     7.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Jul 30 00:50:41 2014 +0200
     7.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Jul 30 10:50:28 2014 +0200
     7.3 @@ -255,12 +255,6 @@
     7.4  fun mk_disc_or_sel Ts t =
     7.5    subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
     7.6  
     7.7 -fun name_of_const what t =
     7.8 -  (case head_of t of
     7.9 -    Const (s, _) => s
    7.10 -  | Free (s, _) => s
    7.11 -  | _ => error ("Cannot extract name of " ^ what));
    7.12 -
    7.13  val name_of_ctr = name_of_const "constructor";
    7.14  
    7.15  fun name_of_disc t =
     8.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Jul 30 00:50:41 2014 +0200
     8.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Jul 30 10:50:28 2014 +0200
     8.3 @@ -39,6 +39,8 @@
     8.4      (string * sort) list * Proof.context
     8.5    val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
     8.6  
     8.7 +  val name_of_const: string -> term -> string
     8.8 +
     8.9    val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
    8.10    val subst_nonatomic_types: (typ * typ) list -> term -> term
    8.11  
    8.12 @@ -177,6 +179,12 @@
    8.13    apfst (map TFree) o
    8.14      variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
    8.15  
    8.16 +fun name_of_const what t =
    8.17 +  (case head_of t of
    8.18 +    Const (s, _) => s
    8.19 +  | Free (s, _) => s
    8.20 +  | _ => error ("Cannot extract name of " ^ what));
    8.21 +
    8.22  (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
    8.23  fun typ_subst_nonatomic [] = I
    8.24    | typ_subst_nonatomic inst =