renamed ML file and module
authorblanchet
Tue Sep 09 20:51:36 2014 +0200 (2014-09-09)
changeset 58275280ede57a6a9
parent 58274 4a84e94e58a2
child 58276 aa1b6ea6a893
renamed ML file and module
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
src/HOL/Tools/datatype_realizer.ML
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4  ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
     1.5  ML_file "Tools/BNF/bnf_lfp_size.ML"
     1.6  ML_file "Tools/Function/old_size.ML"
     1.7 -ML_file "Tools/Old_Datatype/old_datatype_realizer.ML"
     1.8 +ML_file "Tools/datatype_realizer.ML"
     1.9  
    1.10  lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    1.11    by (cases b) auto
     2.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,250 +0,0 @@
     2.4 -(*  Title:      HOL/Tools/Old_Datatype/old_datatype_realizer.ML
     2.5 -    Author:     Stefan Berghofer, TU Muenchen
     2.6 -
     2.7 -Program extraction from proofs involving datatypes:
     2.8 -realizers for induction and case analysis.
     2.9 -*)
    2.10 -
    2.11 -signature OLD_DATATYPE_REALIZER =
    2.12 -sig
    2.13 -  val realizer_plugin: string
    2.14 -  val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
    2.15 -end;
    2.16 -
    2.17 -structure Old_Datatype_Realizer : OLD_DATATYPE_REALIZER =
    2.18 -struct
    2.19 -
    2.20 -val realizer_plugin = "realizer";
    2.21 -
    2.22 -fun subsets i j =
    2.23 -  if i <= j then
    2.24 -    let val is = subsets (i+1) j
    2.25 -    in map (fn ks => i::ks) is @ is end
    2.26 -  else [[]];
    2.27 -
    2.28 -fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
    2.29 -
    2.30 -fun tname_of (Type (s, _)) = s
    2.31 -  | tname_of _ = "";
    2.32 -
    2.33 -fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
    2.34 -  let
    2.35 -    val ctxt = Proof_Context.init_global thy;
    2.36 -    val cert = cterm_of thy;
    2.37 -
    2.38 -    val recTs = Old_Datatype_Aux.get_rec_types descr;
    2.39 -    val pnames =
    2.40 -      if length descr = 1 then ["P"]
    2.41 -      else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
    2.42 -
    2.43 -    val rec_result_Ts = map (fn ((i, _), P) =>
    2.44 -        if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
    2.45 -      (descr ~~ pnames);
    2.46 -
    2.47 -    fun make_pred i T U r x =
    2.48 -      if member (op =) is i then
    2.49 -        Free (nth pnames i, T --> U --> HOLogic.boolT) $ r $ x
    2.50 -      else Free (nth pnames i, U --> HOLogic.boolT) $ x;
    2.51 -
    2.52 -    fun mk_all i s T t =
    2.53 -      if member (op =) is i then Logic.all (Free (s, T)) t else t;
    2.54 -
    2.55 -    val (prems, rec_fns) = split_list (flat (fst (fold_map
    2.56 -      (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
    2.57 -        let
    2.58 -          val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
    2.59 -          val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
    2.60 -          val recs = filter (Old_Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    2.61 -          val frees = tnames ~~ Ts;
    2.62 -
    2.63 -          fun mk_prems vs [] =
    2.64 -                let
    2.65 -                  val rT = nth (rec_result_Ts) i;
    2.66 -                  val vs' = filter_out is_unit vs;
    2.67 -                  val f = Old_Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
    2.68 -                  val f' =
    2.69 -                    Envir.eta_contract (fold_rev (absfree o dest_Free) vs
    2.70 -                      (if member (op =) is i then list_comb (f, vs') else HOLogic.unit));
    2.71 -                in
    2.72 -                  (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
    2.73 -                    (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
    2.74 -                end
    2.75 -            | mk_prems vs (((dt, s), T) :: ds) =
    2.76 -                let
    2.77 -                  val k = Old_Datatype_Aux.body_index dt;
    2.78 -                  val (Us, U) = strip_type T;
    2.79 -                  val i = length Us;
    2.80 -                  val rT = nth (rec_result_Ts) k;
    2.81 -                  val r = Free ("r" ^ s, Us ---> rT);
    2.82 -                  val (p, f) = mk_prems (vs @ [r]) ds;
    2.83 -                in
    2.84 -                  (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
    2.85 -                    (Logic.list_all (map (pair "x") Us, HOLogic.mk_Trueprop
    2.86 -                      (make_pred k rT U (Old_Datatype_Aux.app_bnds r i)
    2.87 -                        (Old_Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
    2.88 -                end;
    2.89 -        in (apfst (fold_rev (Logic.all o Free) frees) (mk_prems (map Free frees) recs), j + 1) end)
    2.90 -          constrs) (descr ~~ recTs) 1)));
    2.91 -
    2.92 -    fun mk_proj _ [] t = t
    2.93 -      | mk_proj j (i :: is) t =
    2.94 -          if null is then t
    2.95 -          else if (j: int) = i then HOLogic.mk_fst t
    2.96 -          else mk_proj j is (HOLogic.mk_snd t);
    2.97 -
    2.98 -    val tnames = Old_Datatype_Prop.make_tnames recTs;
    2.99 -    val fTs = map fastype_of rec_fns;
   2.100 -    val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
   2.101 -      (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
   2.102 -        (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
   2.103 -    val r =
   2.104 -      if null is then Extraction.nullt
   2.105 -      else
   2.106 -        foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
   2.107 -          if member (op =) is i then SOME
   2.108 -            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
   2.109 -          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
   2.110 -    val concl =
   2.111 -      HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
   2.112 -        (map (fn ((((i, _), T), U), tname) =>
   2.113 -          make_pred i U T (mk_proj i is r) (Free (tname, T)))
   2.114 -            (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
   2.115 -    val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
   2.116 -      (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
   2.117 -
   2.118 -    val thm =
   2.119 -      Goal.prove_internal ctxt (map cert prems) (cert concl)
   2.120 -        (fn prems =>
   2.121 -           EVERY [
   2.122 -            rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
   2.123 -            rtac (cterm_instantiate inst induct) 1,
   2.124 -            ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
   2.125 -            rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
   2.126 -            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
   2.127 -              REPEAT (etac allE i) THEN atac i)) 1)])
   2.128 -      |> Drule.export_without_context;
   2.129 -
   2.130 -    val ind_name = Thm.derivation_name induct;
   2.131 -    val vs = map (nth pnames) is;
   2.132 -    val (thm', thy') = thy
   2.133 -      |> Sign.root_path
   2.134 -      |> Global_Theory.store_thm
   2.135 -        (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
   2.136 -      ||> Sign.restore_naming thy;
   2.137 -
   2.138 -    val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
   2.139 -    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
   2.140 -    val ivs1 = map Var (filter_out (fn (_, T) => @{type_name bool} = tname_of (body_type T)) ivs);
   2.141 -    val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
   2.142 -
   2.143 -    val prf =
   2.144 -      Extraction.abs_corr_shyps thy' induct vs ivs2
   2.145 -        (fold_rev (fn (f, p) => fn prf =>
   2.146 -            (case head_of (strip_abs_body f) of
   2.147 -              Free (s, T) =>
   2.148 -                let val T' = Logic.varifyT_global T in
   2.149 -                  Abst (s, SOME T', Proofterm.prf_abstract_over
   2.150 -                    (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
   2.151 -                end
   2.152 -            | _ => AbsP ("H", SOME p, prf)))
   2.153 -          (rec_fns ~~ prems_of thm)
   2.154 -          (Proofterm.proof_combP
   2.155 -            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
   2.156 -
   2.157 -    val r' =
   2.158 -      if null is then r
   2.159 -      else
   2.160 -        Logic.varify_global (fold_rev lambda
   2.161 -          (map Logic.unvarify_global ivs1 @ filter_out is_unit
   2.162 -              (map (head_of o strip_abs_body) rec_fns)) r);
   2.163 -
   2.164 -  in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end
   2.165 -  (* Nested new-style datatypes are not supported (unless they are registered via
   2.166 -     "datatype_compat"). *)
   2.167 -  handle Old_Datatype_Aux.Datatype => thy;
   2.168 -
   2.169 -fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
   2.170 -  let
   2.171 -    val ctxt = Proof_Context.init_global thy;
   2.172 -    val cert = cterm_of thy;
   2.173 -    val rT = TFree ("'P", @{sort type});
   2.174 -    val rT' = TVar (("'P", 0), @{sort type});
   2.175 -
   2.176 -    fun make_casedist_prem T (cname, cargs) =
   2.177 -      let
   2.178 -        val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
   2.179 -        val frees = Name.variant_list ["P", "y"] (Old_Datatype_Prop.make_tnames Ts) ~~ Ts;
   2.180 -        val free_ts = map Free frees;
   2.181 -        val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
   2.182 -      in
   2.183 -        (r, fold_rev Logic.all free_ts
   2.184 -          (Logic.mk_implies (HOLogic.mk_Trueprop
   2.185 -            (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
   2.186 -              HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
   2.187 -                list_comb (r, free_ts)))))
   2.188 -      end;
   2.189 -
   2.190 -    val SOME (_, _, constrs) = AList.lookup (op =) descr index;
   2.191 -    val T = nth (Old_Datatype_Aux.get_rec_types descr) index;
   2.192 -    val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
   2.193 -    val r = Const (case_name, map fastype_of rs ---> T --> rT);
   2.194 -
   2.195 -    val y = Var (("y", 0), Logic.varifyT_global T);
   2.196 -    val y' = Free ("y", T);
   2.197 -
   2.198 -    val thm =
   2.199 -      Goal.prove_internal ctxt (map cert prems)
   2.200 -        (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
   2.201 -        (fn prems =>
   2.202 -           EVERY [
   2.203 -            rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
   2.204 -            ALLGOALS (EVERY'
   2.205 -              [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
   2.206 -               resolve_tac prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
   2.207 -      |> Drule.export_without_context;
   2.208 -
   2.209 -    val exh_name = Thm.derivation_name exhaust;
   2.210 -    val (thm', thy') = thy
   2.211 -      |> Sign.root_path
   2.212 -      |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
   2.213 -      ||> Sign.restore_naming thy;
   2.214 -
   2.215 -    val P = Var (("P", 0), rT' --> HOLogic.boolT);
   2.216 -    val prf =
   2.217 -      Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
   2.218 -        (fold_rev (fn (p, r) => fn prf =>
   2.219 -            Proofterm.forall_intr_proof' (Logic.varify_global r)
   2.220 -              (AbsP ("H", SOME (Logic.varify_global p), prf)))
   2.221 -          (prems ~~ rs)
   2.222 -          (Proofterm.proof_combP
   2.223 -            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
   2.224 -    val prf' =
   2.225 -      Extraction.abs_corr_shyps thy' exhaust []
   2.226 -        (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
   2.227 -    val r' =
   2.228 -      Logic.varify_global (Abs ("y", T,
   2.229 -        (fold_rev (Term.abs o dest_Free) rs
   2.230 -          (list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))));
   2.231 -  in
   2.232 -    Extraction.add_realizers_i
   2.233 -      [(exh_name, (["P"], r', prf)),
   2.234 -       (exh_name, ([], Extraction.nullt, prf'))] thy'
   2.235 -  end;
   2.236 -
   2.237 -fun add_dt_realizers config names thy =
   2.238 -  if not (Proofterm.proofs_enabled ()) then thy
   2.239 -  else
   2.240 -    let
   2.241 -      val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
   2.242 -      val infos = map (BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Unfold_Nesting) names;
   2.243 -      val info :: _ = infos;
   2.244 -    in
   2.245 -      thy
   2.246 -      |> fold_rev (make_ind info) (subsets 0 (length (#descr info) - 1))
   2.247 -      |> fold_rev make_casedists infos
   2.248 -    end;
   2.249 -
   2.250 -val _ = Theory.setup (BNF_LFP_Compat.interpretation realizer_plugin BNF_LFP_Compat.Unfold_Nesting
   2.251 -  add_dt_realizers);
   2.252 -
   2.253 -end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
     3.3 @@ -0,0 +1,250 @@
     3.4 +(*  Title:      HOL/Tools/datatype_realizer.ML
     3.5 +    Author:     Stefan Berghofer, TU Muenchen
     3.6 +
     3.7 +Program extraction from proofs involving datatypes:
     3.8 +realizers for induction and case analysis.
     3.9 +*)
    3.10 +
    3.11 +signature DATATYPE_REALIZER =
    3.12 +sig
    3.13 +  val realizer_plugin: string
    3.14 +  val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
    3.15 +end;
    3.16 +
    3.17 +structure Datatype_Realizer : DATATYPE_REALIZER =
    3.18 +struct
    3.19 +
    3.20 +val realizer_plugin = "realizer";
    3.21 +
    3.22 +fun subsets i j =
    3.23 +  if i <= j then
    3.24 +    let val is = subsets (i+1) j
    3.25 +    in map (fn ks => i::ks) is @ is end
    3.26 +  else [[]];
    3.27 +
    3.28 +fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
    3.29 +
    3.30 +fun tname_of (Type (s, _)) = s
    3.31 +  | tname_of _ = "";
    3.32 +
    3.33 +fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
    3.34 +  let
    3.35 +    val ctxt = Proof_Context.init_global thy;
    3.36 +    val cert = cterm_of thy;
    3.37 +
    3.38 +    val recTs = Old_Datatype_Aux.get_rec_types descr;
    3.39 +    val pnames =
    3.40 +      if length descr = 1 then ["P"]
    3.41 +      else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
    3.42 +
    3.43 +    val rec_result_Ts = map (fn ((i, _), P) =>
    3.44 +        if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
    3.45 +      (descr ~~ pnames);
    3.46 +
    3.47 +    fun make_pred i T U r x =
    3.48 +      if member (op =) is i then
    3.49 +        Free (nth pnames i, T --> U --> HOLogic.boolT) $ r $ x
    3.50 +      else Free (nth pnames i, U --> HOLogic.boolT) $ x;
    3.51 +
    3.52 +    fun mk_all i s T t =
    3.53 +      if member (op =) is i then Logic.all (Free (s, T)) t else t;
    3.54 +
    3.55 +    val (prems, rec_fns) = split_list (flat (fst (fold_map
    3.56 +      (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
    3.57 +        let
    3.58 +          val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
    3.59 +          val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
    3.60 +          val recs = filter (Old_Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    3.61 +          val frees = tnames ~~ Ts;
    3.62 +
    3.63 +          fun mk_prems vs [] =
    3.64 +                let
    3.65 +                  val rT = nth (rec_result_Ts) i;
    3.66 +                  val vs' = filter_out is_unit vs;
    3.67 +                  val f = Old_Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
    3.68 +                  val f' =
    3.69 +                    Envir.eta_contract (fold_rev (absfree o dest_Free) vs
    3.70 +                      (if member (op =) is i then list_comb (f, vs') else HOLogic.unit));
    3.71 +                in
    3.72 +                  (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
    3.73 +                    (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
    3.74 +                end
    3.75 +            | mk_prems vs (((dt, s), T) :: ds) =
    3.76 +                let
    3.77 +                  val k = Old_Datatype_Aux.body_index dt;
    3.78 +                  val (Us, U) = strip_type T;
    3.79 +                  val i = length Us;
    3.80 +                  val rT = nth (rec_result_Ts) k;
    3.81 +                  val r = Free ("r" ^ s, Us ---> rT);
    3.82 +                  val (p, f) = mk_prems (vs @ [r]) ds;
    3.83 +                in
    3.84 +                  (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
    3.85 +                    (Logic.list_all (map (pair "x") Us, HOLogic.mk_Trueprop
    3.86 +                      (make_pred k rT U (Old_Datatype_Aux.app_bnds r i)
    3.87 +                        (Old_Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
    3.88 +                end;
    3.89 +        in (apfst (fold_rev (Logic.all o Free) frees) (mk_prems (map Free frees) recs), j + 1) end)
    3.90 +          constrs) (descr ~~ recTs) 1)));
    3.91 +
    3.92 +    fun mk_proj _ [] t = t
    3.93 +      | mk_proj j (i :: is) t =
    3.94 +          if null is then t
    3.95 +          else if (j: int) = i then HOLogic.mk_fst t
    3.96 +          else mk_proj j is (HOLogic.mk_snd t);
    3.97 +
    3.98 +    val tnames = Old_Datatype_Prop.make_tnames recTs;
    3.99 +    val fTs = map fastype_of rec_fns;
   3.100 +    val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
   3.101 +      (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
   3.102 +        (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
   3.103 +    val r =
   3.104 +      if null is then Extraction.nullt
   3.105 +      else
   3.106 +        foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
   3.107 +          if member (op =) is i then SOME
   3.108 +            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
   3.109 +          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
   3.110 +    val concl =
   3.111 +      HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
   3.112 +        (map (fn ((((i, _), T), U), tname) =>
   3.113 +          make_pred i U T (mk_proj i is r) (Free (tname, T)))
   3.114 +            (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
   3.115 +    val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
   3.116 +      (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
   3.117 +
   3.118 +    val thm =
   3.119 +      Goal.prove_internal ctxt (map cert prems) (cert concl)
   3.120 +        (fn prems =>
   3.121 +           EVERY [
   3.122 +            rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
   3.123 +            rtac (cterm_instantiate inst induct) 1,
   3.124 +            ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
   3.125 +            rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
   3.126 +            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
   3.127 +              REPEAT (etac allE i) THEN atac i)) 1)])
   3.128 +      |> Drule.export_without_context;
   3.129 +
   3.130 +    val ind_name = Thm.derivation_name induct;
   3.131 +    val vs = map (nth pnames) is;
   3.132 +    val (thm', thy') = thy
   3.133 +      |> Sign.root_path
   3.134 +      |> Global_Theory.store_thm
   3.135 +        (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
   3.136 +      ||> Sign.restore_naming thy;
   3.137 +
   3.138 +    val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
   3.139 +    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
   3.140 +    val ivs1 = map Var (filter_out (fn (_, T) => @{type_name bool} = tname_of (body_type T)) ivs);
   3.141 +    val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
   3.142 +
   3.143 +    val prf =
   3.144 +      Extraction.abs_corr_shyps thy' induct vs ivs2
   3.145 +        (fold_rev (fn (f, p) => fn prf =>
   3.146 +            (case head_of (strip_abs_body f) of
   3.147 +              Free (s, T) =>
   3.148 +                let val T' = Logic.varifyT_global T in
   3.149 +                  Abst (s, SOME T', Proofterm.prf_abstract_over
   3.150 +                    (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
   3.151 +                end
   3.152 +            | _ => AbsP ("H", SOME p, prf)))
   3.153 +          (rec_fns ~~ prems_of thm)
   3.154 +          (Proofterm.proof_combP
   3.155 +            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
   3.156 +
   3.157 +    val r' =
   3.158 +      if null is then r
   3.159 +      else
   3.160 +        Logic.varify_global (fold_rev lambda
   3.161 +          (map Logic.unvarify_global ivs1 @ filter_out is_unit
   3.162 +              (map (head_of o strip_abs_body) rec_fns)) r);
   3.163 +
   3.164 +  in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end
   3.165 +  (* Nested new-style datatypes are not supported (unless they are registered via
   3.166 +     "datatype_compat"). *)
   3.167 +  handle Old_Datatype_Aux.Datatype => thy;
   3.168 +
   3.169 +fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
   3.170 +  let
   3.171 +    val ctxt = Proof_Context.init_global thy;
   3.172 +    val cert = cterm_of thy;
   3.173 +    val rT = TFree ("'P", @{sort type});
   3.174 +    val rT' = TVar (("'P", 0), @{sort type});
   3.175 +
   3.176 +    fun make_casedist_prem T (cname, cargs) =
   3.177 +      let
   3.178 +        val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
   3.179 +        val frees = Name.variant_list ["P", "y"] (Old_Datatype_Prop.make_tnames Ts) ~~ Ts;
   3.180 +        val free_ts = map Free frees;
   3.181 +        val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
   3.182 +      in
   3.183 +        (r, fold_rev Logic.all free_ts
   3.184 +          (Logic.mk_implies (HOLogic.mk_Trueprop
   3.185 +            (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
   3.186 +              HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
   3.187 +                list_comb (r, free_ts)))))
   3.188 +      end;
   3.189 +
   3.190 +    val SOME (_, _, constrs) = AList.lookup (op =) descr index;
   3.191 +    val T = nth (Old_Datatype_Aux.get_rec_types descr) index;
   3.192 +    val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
   3.193 +    val r = Const (case_name, map fastype_of rs ---> T --> rT);
   3.194 +
   3.195 +    val y = Var (("y", 0), Logic.varifyT_global T);
   3.196 +    val y' = Free ("y", T);
   3.197 +
   3.198 +    val thm =
   3.199 +      Goal.prove_internal ctxt (map cert prems)
   3.200 +        (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
   3.201 +        (fn prems =>
   3.202 +           EVERY [
   3.203 +            rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
   3.204 +            ALLGOALS (EVERY'
   3.205 +              [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
   3.206 +               resolve_tac prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
   3.207 +      |> Drule.export_without_context;
   3.208 +
   3.209 +    val exh_name = Thm.derivation_name exhaust;
   3.210 +    val (thm', thy') = thy
   3.211 +      |> Sign.root_path
   3.212 +      |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
   3.213 +      ||> Sign.restore_naming thy;
   3.214 +
   3.215 +    val P = Var (("P", 0), rT' --> HOLogic.boolT);
   3.216 +    val prf =
   3.217 +      Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
   3.218 +        (fold_rev (fn (p, r) => fn prf =>
   3.219 +            Proofterm.forall_intr_proof' (Logic.varify_global r)
   3.220 +              (AbsP ("H", SOME (Logic.varify_global p), prf)))
   3.221 +          (prems ~~ rs)
   3.222 +          (Proofterm.proof_combP
   3.223 +            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
   3.224 +    val prf' =
   3.225 +      Extraction.abs_corr_shyps thy' exhaust []
   3.226 +        (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
   3.227 +    val r' =
   3.228 +      Logic.varify_global (Abs ("y", T,
   3.229 +        (fold_rev (Term.abs o dest_Free) rs
   3.230 +          (list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))));
   3.231 +  in
   3.232 +    Extraction.add_realizers_i
   3.233 +      [(exh_name, (["P"], r', prf)),
   3.234 +       (exh_name, ([], Extraction.nullt, prf'))] thy'
   3.235 +  end;
   3.236 +
   3.237 +fun add_dt_realizers config names thy =
   3.238 +  if not (Proofterm.proofs_enabled ()) then thy
   3.239 +  else
   3.240 +    let
   3.241 +      val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
   3.242 +      val infos = map (BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Unfold_Nesting) names;
   3.243 +      val info :: _ = infos;
   3.244 +    in
   3.245 +      thy
   3.246 +      |> fold_rev (make_ind info) (subsets 0 (length (#descr info) - 1))
   3.247 +      |> fold_rev make_casedists infos
   3.248 +    end;
   3.249 +
   3.250 +val _ = Theory.setup (BNF_LFP_Compat.interpretation realizer_plugin BNF_LFP_Compat.Unfold_Nesting
   3.251 +  add_dt_realizers);
   3.252 +
   3.253 +end;