# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 280ede57a6a99cb1a1f18802b3f7f6e9f5e0c2eb
# Parent  4a84e94e58a24f14d536b5de693374bcec986eff
renamed ML file and module

diff -r 4a84e94e58a2 -r 280ede57a6a9 src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -235,7 +235,7 @@
 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
 ML_file "Tools/BNF/bnf_lfp_size.ML"
 ML_file "Tools/Function/old_size.ML"
-ML_file "Tools/Old_Datatype/old_datatype_realizer.ML"
+ML_file "Tools/datatype_realizer.ML"
 
 lemma size_bool[code]: "size (b\<Colon>bool) = 0"
   by (cases b) auto
diff -r 4a84e94e58a2 -r 280ede57a6a9 src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,250 +0,0 @@
-(*  Title:      HOL/Tools/Old_Datatype/old_datatype_realizer.ML
-    Author:     Stefan Berghofer, TU Muenchen
-
-Program extraction from proofs involving datatypes:
-realizers for induction and case analysis.
-*)
-
-signature OLD_DATATYPE_REALIZER =
-sig
-  val realizer_plugin: string
-  val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
-end;
-
-structure Old_Datatype_Realizer : OLD_DATATYPE_REALIZER =
-struct
-
-val realizer_plugin = "realizer";
-
-fun subsets i j =
-  if i <= j then
-    let val is = subsets (i+1) j
-    in map (fn ks => i::ks) is @ is end
-  else [[]];
-
-fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
-
-fun tname_of (Type (s, _)) = s
-  | tname_of _ = "";
-
-fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
-  let
-    val ctxt = Proof_Context.init_global thy;
-    val cert = cterm_of thy;
-
-    val recTs = Old_Datatype_Aux.get_rec_types descr;
-    val pnames =
-      if length descr = 1 then ["P"]
-      else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
-
-    val rec_result_Ts = map (fn ((i, _), P) =>
-        if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
-      (descr ~~ pnames);
-
-    fun make_pred i T U r x =
-      if member (op =) is i then
-        Free (nth pnames i, T --> U --> HOLogic.boolT) $ r $ x
-      else Free (nth pnames i, U --> HOLogic.boolT) $ x;
-
-    fun mk_all i s T t =
-      if member (op =) is i then Logic.all (Free (s, T)) t else t;
-
-    val (prems, rec_fns) = split_list (flat (fst (fold_map
-      (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
-        let
-          val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
-          val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
-          val recs = filter (Old_Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
-          val frees = tnames ~~ Ts;
-
-          fun mk_prems vs [] =
-                let
-                  val rT = nth (rec_result_Ts) i;
-                  val vs' = filter_out is_unit vs;
-                  val f = Old_Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
-                  val f' =
-                    Envir.eta_contract (fold_rev (absfree o dest_Free) vs
-                      (if member (op =) is i then list_comb (f, vs') else HOLogic.unit));
-                in
-                  (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
-                    (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
-                end
-            | mk_prems vs (((dt, s), T) :: ds) =
-                let
-                  val k = Old_Datatype_Aux.body_index dt;
-                  val (Us, U) = strip_type T;
-                  val i = length Us;
-                  val rT = nth (rec_result_Ts) k;
-                  val r = Free ("r" ^ s, Us ---> rT);
-                  val (p, f) = mk_prems (vs @ [r]) ds;
-                in
-                  (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
-                    (Logic.list_all (map (pair "x") Us, HOLogic.mk_Trueprop
-                      (make_pred k rT U (Old_Datatype_Aux.app_bnds r i)
-                        (Old_Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
-                end;
-        in (apfst (fold_rev (Logic.all o Free) frees) (mk_prems (map Free frees) recs), j + 1) end)
-          constrs) (descr ~~ recTs) 1)));
-
-    fun mk_proj _ [] t = t
-      | mk_proj j (i :: is) t =
-          if null is then t
-          else if (j: int) = i then HOLogic.mk_fst t
-          else mk_proj j is (HOLogic.mk_snd t);
-
-    val tnames = Old_Datatype_Prop.make_tnames recTs;
-    val fTs = map fastype_of rec_fns;
-    val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
-      (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
-        (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
-    val r =
-      if null is then Extraction.nullt
-      else
-        foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
-          if member (op =) is i then SOME
-            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
-          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
-    val concl =
-      HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
-        (map (fn ((((i, _), T), U), tname) =>
-          make_pred i U T (mk_proj i is r) (Free (tname, T)))
-            (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
-    val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
-      (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
-
-    val thm =
-      Goal.prove_internal ctxt (map cert prems) (cert concl)
-        (fn prems =>
-           EVERY [
-            rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
-            rtac (cterm_instantiate inst induct) 1,
-            ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
-            rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
-            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
-              REPEAT (etac allE i) THEN atac i)) 1)])
-      |> Drule.export_without_context;
-
-    val ind_name = Thm.derivation_name induct;
-    val vs = map (nth pnames) is;
-    val (thm', thy') = thy
-      |> Sign.root_path
-      |> Global_Theory.store_thm
-        (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
-      ||> Sign.restore_naming thy;
-
-    val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
-    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
-    val ivs1 = map Var (filter_out (fn (_, T) => @{type_name bool} = tname_of (body_type T)) ivs);
-    val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
-
-    val prf =
-      Extraction.abs_corr_shyps thy' induct vs ivs2
-        (fold_rev (fn (f, p) => fn prf =>
-            (case head_of (strip_abs_body f) of
-              Free (s, T) =>
-                let val T' = Logic.varifyT_global T in
-                  Abst (s, SOME T', Proofterm.prf_abstract_over
-                    (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
-                end
-            | _ => AbsP ("H", SOME p, prf)))
-          (rec_fns ~~ prems_of thm)
-          (Proofterm.proof_combP
-            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
-
-    val r' =
-      if null is then r
-      else
-        Logic.varify_global (fold_rev lambda
-          (map Logic.unvarify_global ivs1 @ filter_out is_unit
-              (map (head_of o strip_abs_body) rec_fns)) r);
-
-  in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end
-  (* Nested new-style datatypes are not supported (unless they are registered via
-     "datatype_compat"). *)
-  handle Old_Datatype_Aux.Datatype => thy;
-
-fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
-  let
-    val ctxt = Proof_Context.init_global thy;
-    val cert = cterm_of thy;
-    val rT = TFree ("'P", @{sort type});
-    val rT' = TVar (("'P", 0), @{sort type});
-
-    fun make_casedist_prem T (cname, cargs) =
-      let
-        val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
-        val frees = Name.variant_list ["P", "y"] (Old_Datatype_Prop.make_tnames Ts) ~~ Ts;
-        val free_ts = map Free frees;
-        val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
-      in
-        (r, fold_rev Logic.all free_ts
-          (Logic.mk_implies (HOLogic.mk_Trueprop
-            (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
-              HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
-                list_comb (r, free_ts)))))
-      end;
-
-    val SOME (_, _, constrs) = AList.lookup (op =) descr index;
-    val T = nth (Old_Datatype_Aux.get_rec_types descr) index;
-    val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
-    val r = Const (case_name, map fastype_of rs ---> T --> rT);
-
-    val y = Var (("y", 0), Logic.varifyT_global T);
-    val y' = Free ("y", T);
-
-    val thm =
-      Goal.prove_internal ctxt (map cert prems)
-        (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
-        (fn prems =>
-           EVERY [
-            rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
-            ALLGOALS (EVERY'
-              [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
-               resolve_tac prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
-      |> Drule.export_without_context;
-
-    val exh_name = Thm.derivation_name exhaust;
-    val (thm', thy') = thy
-      |> Sign.root_path
-      |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
-      ||> Sign.restore_naming thy;
-
-    val P = Var (("P", 0), rT' --> HOLogic.boolT);
-    val prf =
-      Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
-        (fold_rev (fn (p, r) => fn prf =>
-            Proofterm.forall_intr_proof' (Logic.varify_global r)
-              (AbsP ("H", SOME (Logic.varify_global p), prf)))
-          (prems ~~ rs)
-          (Proofterm.proof_combP
-            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
-    val prf' =
-      Extraction.abs_corr_shyps thy' exhaust []
-        (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
-    val r' =
-      Logic.varify_global (Abs ("y", T,
-        (fold_rev (Term.abs o dest_Free) rs
-          (list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))));
-  in
-    Extraction.add_realizers_i
-      [(exh_name, (["P"], r', prf)),
-       (exh_name, ([], Extraction.nullt, prf'))] thy'
-  end;
-
-fun add_dt_realizers config names thy =
-  if not (Proofterm.proofs_enabled ()) then thy
-  else
-    let
-      val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
-      val infos = map (BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Unfold_Nesting) names;
-      val info :: _ = infos;
-    in
-      thy
-      |> fold_rev (make_ind info) (subsets 0 (length (#descr info) - 1))
-      |> fold_rev make_casedists infos
-    end;
-
-val _ = Theory.setup (BNF_LFP_Compat.interpretation realizer_plugin BNF_LFP_Compat.Unfold_Nesting
-  add_dt_realizers);
-
-end;
diff -r 4a84e94e58a2 -r 280ede57a6a9 src/HOL/Tools/datatype_realizer.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -0,0 +1,250 @@
+(*  Title:      HOL/Tools/datatype_realizer.ML
+    Author:     Stefan Berghofer, TU Muenchen
+
+Program extraction from proofs involving datatypes:
+realizers for induction and case analysis.
+*)
+
+signature DATATYPE_REALIZER =
+sig
+  val realizer_plugin: string
+  val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
+end;
+
+structure Datatype_Realizer : DATATYPE_REALIZER =
+struct
+
+val realizer_plugin = "realizer";
+
+fun subsets i j =
+  if i <= j then
+    let val is = subsets (i+1) j
+    in map (fn ks => i::ks) is @ is end
+  else [[]];
+
+fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
+
+fun tname_of (Type (s, _)) = s
+  | tname_of _ = "";
+
+fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
+  let
+    val ctxt = Proof_Context.init_global thy;
+    val cert = cterm_of thy;
+
+    val recTs = Old_Datatype_Aux.get_rec_types descr;
+    val pnames =
+      if length descr = 1 then ["P"]
+      else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
+
+    val rec_result_Ts = map (fn ((i, _), P) =>
+        if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
+      (descr ~~ pnames);
+
+    fun make_pred i T U r x =
+      if member (op =) is i then
+        Free (nth pnames i, T --> U --> HOLogic.boolT) $ r $ x
+      else Free (nth pnames i, U --> HOLogic.boolT) $ x;
+
+    fun mk_all i s T t =
+      if member (op =) is i then Logic.all (Free (s, T)) t else t;
+
+    val (prems, rec_fns) = split_list (flat (fst (fold_map
+      (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
+        let
+          val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
+          val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
+          val recs = filter (Old_Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
+          val frees = tnames ~~ Ts;
+
+          fun mk_prems vs [] =
+                let
+                  val rT = nth (rec_result_Ts) i;
+                  val vs' = filter_out is_unit vs;
+                  val f = Old_Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
+                  val f' =
+                    Envir.eta_contract (fold_rev (absfree o dest_Free) vs
+                      (if member (op =) is i then list_comb (f, vs') else HOLogic.unit));
+                in
+                  (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
+                    (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
+                end
+            | mk_prems vs (((dt, s), T) :: ds) =
+                let
+                  val k = Old_Datatype_Aux.body_index dt;
+                  val (Us, U) = strip_type T;
+                  val i = length Us;
+                  val rT = nth (rec_result_Ts) k;
+                  val r = Free ("r" ^ s, Us ---> rT);
+                  val (p, f) = mk_prems (vs @ [r]) ds;
+                in
+                  (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
+                    (Logic.list_all (map (pair "x") Us, HOLogic.mk_Trueprop
+                      (make_pred k rT U (Old_Datatype_Aux.app_bnds r i)
+                        (Old_Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
+                end;
+        in (apfst (fold_rev (Logic.all o Free) frees) (mk_prems (map Free frees) recs), j + 1) end)
+          constrs) (descr ~~ recTs) 1)));
+
+    fun mk_proj _ [] t = t
+      | mk_proj j (i :: is) t =
+          if null is then t
+          else if (j: int) = i then HOLogic.mk_fst t
+          else mk_proj j is (HOLogic.mk_snd t);
+
+    val tnames = Old_Datatype_Prop.make_tnames recTs;
+    val fTs = map fastype_of rec_fns;
+    val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
+      (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
+        (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
+    val r =
+      if null is then Extraction.nullt
+      else
+        foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
+          if member (op =) is i then SOME
+            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
+          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
+    val concl =
+      HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
+        (map (fn ((((i, _), T), U), tname) =>
+          make_pred i U T (mk_proj i is r) (Free (tname, T)))
+            (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
+    val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
+      (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
+
+    val thm =
+      Goal.prove_internal ctxt (map cert prems) (cert concl)
+        (fn prems =>
+           EVERY [
+            rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
+            rtac (cterm_instantiate inst induct) 1,
+            ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
+            rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
+            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
+              REPEAT (etac allE i) THEN atac i)) 1)])
+      |> Drule.export_without_context;
+
+    val ind_name = Thm.derivation_name induct;
+    val vs = map (nth pnames) is;
+    val (thm', thy') = thy
+      |> Sign.root_path
+      |> Global_Theory.store_thm
+        (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
+      ||> Sign.restore_naming thy;
+
+    val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
+    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
+    val ivs1 = map Var (filter_out (fn (_, T) => @{type_name bool} = tname_of (body_type T)) ivs);
+    val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
+
+    val prf =
+      Extraction.abs_corr_shyps thy' induct vs ivs2
+        (fold_rev (fn (f, p) => fn prf =>
+            (case head_of (strip_abs_body f) of
+              Free (s, T) =>
+                let val T' = Logic.varifyT_global T in
+                  Abst (s, SOME T', Proofterm.prf_abstract_over
+                    (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
+                end
+            | _ => AbsP ("H", SOME p, prf)))
+          (rec_fns ~~ prems_of thm)
+          (Proofterm.proof_combP
+            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+
+    val r' =
+      if null is then r
+      else
+        Logic.varify_global (fold_rev lambda
+          (map Logic.unvarify_global ivs1 @ filter_out is_unit
+              (map (head_of o strip_abs_body) rec_fns)) r);
+
+  in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end
+  (* Nested new-style datatypes are not supported (unless they are registered via
+     "datatype_compat"). *)
+  handle Old_Datatype_Aux.Datatype => thy;
+
+fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
+  let
+    val ctxt = Proof_Context.init_global thy;
+    val cert = cterm_of thy;
+    val rT = TFree ("'P", @{sort type});
+    val rT' = TVar (("'P", 0), @{sort type});
+
+    fun make_casedist_prem T (cname, cargs) =
+      let
+        val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
+        val frees = Name.variant_list ["P", "y"] (Old_Datatype_Prop.make_tnames Ts) ~~ Ts;
+        val free_ts = map Free frees;
+        val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
+      in
+        (r, fold_rev Logic.all free_ts
+          (Logic.mk_implies (HOLogic.mk_Trueprop
+            (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
+              HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
+                list_comb (r, free_ts)))))
+      end;
+
+    val SOME (_, _, constrs) = AList.lookup (op =) descr index;
+    val T = nth (Old_Datatype_Aux.get_rec_types descr) index;
+    val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
+    val r = Const (case_name, map fastype_of rs ---> T --> rT);
+
+    val y = Var (("y", 0), Logic.varifyT_global T);
+    val y' = Free ("y", T);
+
+    val thm =
+      Goal.prove_internal ctxt (map cert prems)
+        (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
+        (fn prems =>
+           EVERY [
+            rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
+            ALLGOALS (EVERY'
+              [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
+               resolve_tac prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
+      |> Drule.export_without_context;
+
+    val exh_name = Thm.derivation_name exhaust;
+    val (thm', thy') = thy
+      |> Sign.root_path
+      |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
+      ||> Sign.restore_naming thy;
+
+    val P = Var (("P", 0), rT' --> HOLogic.boolT);
+    val prf =
+      Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
+        (fold_rev (fn (p, r) => fn prf =>
+            Proofterm.forall_intr_proof' (Logic.varify_global r)
+              (AbsP ("H", SOME (Logic.varify_global p), prf)))
+          (prems ~~ rs)
+          (Proofterm.proof_combP
+            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+    val prf' =
+      Extraction.abs_corr_shyps thy' exhaust []
+        (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
+    val r' =
+      Logic.varify_global (Abs ("y", T,
+        (fold_rev (Term.abs o dest_Free) rs
+          (list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))));
+  in
+    Extraction.add_realizers_i
+      [(exh_name, (["P"], r', prf)),
+       (exh_name, ([], Extraction.nullt, prf'))] thy'
+  end;
+
+fun add_dt_realizers config names thy =
+  if not (Proofterm.proofs_enabled ()) then thy
+  else
+    let
+      val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
+      val infos = map (BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Unfold_Nesting) names;
+      val info :: _ = infos;
+    in
+      thy
+      |> fold_rev (make_ind info) (subsets 0 (length (#descr info) - 1))
+      |> fold_rev make_casedists infos
+    end;
+
+val _ = Theory.setup (BNF_LFP_Compat.interpretation realizer_plugin BNF_LFP_Compat.Unfold_Nesting
+  add_dt_realizers);
+
+end;