src/HOL/Tools/inductive_realizer.ML
author wenzelm
Thu Jul 05 20:01:26 2007 +0200 (2007-07-05)
changeset 23590 ad95084a5c63
parent 23577 c5b93c69afd3
child 24157 409cd6eaa7ea
permissions -rw-r--r--
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
     1 (*  Title:      HOL/Tools/inductive_realizer.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 
     5 Porgram extraction from proofs involving inductive predicates:
     6 Realizers for induction and elimination rules
     7 *)
     8 
     9 signature INDUCTIVE_REALIZER =
    10 sig
    11   val add_ind_realizers: string -> string list -> theory -> theory
    12   val setup: theory -> theory
    13 end;
    14 
    15 structure InductiveRealizer : INDUCTIVE_REALIZER =
    16 struct
    17 
    18 (* FIXME: LocalTheory.note should return theorems with proper names! *)
    19 fun name_of_thm thm =
    20   (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of
    21      [(name, _)] => name
    22    | _ => error ("name_of_thm: bad proof of theorem\n" ^ string_of_thm thm));
    23 
    24 val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
    25 
    26 fun prf_of thm =
    27   let val {thy, prop, der = (_, prf), ...} = rep_thm thm
    28   in Reconstruct.expand_proof thy [("", NONE)] (Reconstruct.reconstruct_proof thy prop prf) end; (* FIXME *)
    29 
    30 fun forall_intr_prf (t, prf) =
    31   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    32   in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    33 
    34 fun forall_intr_term (t, u) =
    35   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    36   in all T $ Abs (a, T, abstract_over (t, u)) end;
    37 
    38 fun subsets [] = [[]]
    39   | subsets (x::xs) =
    40       let val ys = subsets xs
    41       in ys @ map (cons x) ys end;
    42 
    43 val pred_of = fst o dest_Const o head_of;
    44 
    45 fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
    46       let val (s', names') = (case names of
    47           [] => (Name.variant used s, [])
    48         | name :: names' => (name, names'))
    49       in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
    50   | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
    51       t $ strip_all' used names Q
    52   | strip_all' _ _ t = t;
    53 
    54 fun strip_all t = strip_all' (add_term_free_names (t, [])) [] t;
    55 
    56 fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
    57       (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
    58   | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
    59 
    60 fun relevant_vars prop = foldr (fn
    61       (Var ((a, i), T), vs) => (case strip_type T of
    62         (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
    63       | _ => vs)
    64     | (_, vs) => vs) [] (term_vars prop);
    65 
    66 fun dt_of_intrs thy vs nparms intrs =
    67   let
    68     val iTs = term_tvars (prop_of (hd intrs));
    69     val Tvs = map TVar iTs;
    70     val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
    71       (Logic.strip_imp_concl (prop_of (hd intrs))));
    72     val params = map dest_Var (Library.take (nparms, ts));
    73     val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
    74     fun constr_of_intr intr = (Sign.base_name (name_of_thm intr),
    75       map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
    76         filter_out (equal Extraction.nullT) (map
    77           (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    78             NoSyn);
    79   in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
    80     map constr_of_intr intrs)
    81   end;
    82 
    83 fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
    84 
    85 (** turn "P" into "%r x. realizes r (P x)" **)
    86 
    87 fun gen_rvar vs (t as Var ((a, 0), T)) =
    88       if body_type T <> HOLogic.boolT then t else
    89         let
    90           val U = TVar (("'" ^ a, 0), HOLogic.typeS)
    91           val Ts = binder_types T;
    92           val i = length Ts;
    93           val xs = map (pair "x") Ts;
    94           val u = list_comb (t, map Bound (i - 1 downto 0))
    95         in 
    96           if a mem vs then
    97             list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
    98           else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
    99         end
   100   | gen_rvar _ t = t;
   101 
   102 fun mk_realizes_eqn n vs nparms intrs =
   103   let
   104     val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
   105     val iTs = term_tvars concl;
   106     val Tvs = map TVar iTs;
   107     val (h as Const (s, T), us) = strip_comb concl;
   108     val params = List.take (us, nparms);
   109     val elTs = List.drop (binder_types T, nparms);
   110     val predT = elTs ---> HOLogic.boolT;
   111     val used = map (fst o fst o dest_Var) params;
   112     val xs = map (Var o apfst (rpair 0))
   113       (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
   114     val rT = if n then Extraction.nullT
   115       else Type (space_implode "_" (s ^ "T" :: vs),
   116         map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
   117     val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
   118     val S = list_comb (h, params @ xs);
   119     val rvs = relevant_vars S;
   120     val vs' = map fst rvs \\ vs;
   121     val rname = space_implode "_" (s ^ "R" :: vs);
   122 
   123     fun mk_Tprem n v =
   124       let val T = (the o AList.lookup (op =) rvs) v
   125       in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
   126         Extraction.mk_typ (if n then Extraction.nullT
   127           else TVar (("'" ^ v, 0), HOLogic.typeS)))
   128       end;
   129 
   130     val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
   131     val ts = map (gen_rvar vs) params;
   132     val argTs = map fastype_of ts;
   133 
   134   in ((prems, (Const ("typeof", HOLogic.boolT --> Type ("Type", [])) $ S,
   135        Extraction.mk_typ rT)),
   136     (prems, (mk_rlz rT $ r $ S,
   137        if n then list_comb (Const (rname, argTs ---> predT), ts @ xs)
   138        else list_comb (Const (rname, argTs @ [rT] ---> predT), ts @ [r] @ xs))))
   139   end;
   140 
   141 fun fun_of_prem thy rsets vs params rule ivs intr =
   142   let
   143     val ctxt = ProofContext.init thy
   144     val args = map (Free o apfst fst o dest_Var) ivs;
   145     val args' = map (Free o apfst fst)
   146       (Term.add_vars (prop_of intr) [] \\ params);
   147     val rule' = strip_all rule;
   148     val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
   149     val used = map (fst o dest_Free) args;
   150 
   151     fun is_rec t = not (null (term_consts t inter rsets));
   152 
   153     fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
   154       | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
   155       | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
   156           Const (s, _) => can (InductivePackage.the_inductive ctxt) s
   157         | _ => true)
   158       | is_meta _ = false;
   159 
   160     fun fun_of ts rts args used (prem :: prems) =
   161           let
   162             val T = Extraction.etype_of thy vs [] prem;
   163             val [x, r] = Name.variant_list used ["x", "r"]
   164           in if T = Extraction.nullT
   165             then fun_of ts rts args used prems
   166             else if is_rec prem then
   167               if is_meta prem then
   168                 let
   169                   val prem' :: prems' = prems;
   170                   val U = Extraction.etype_of thy vs [] prem';
   171                 in if U = Extraction.nullT
   172                   then fun_of (Free (x, T) :: ts)
   173                     (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
   174                     (Free (x, T) :: args) (x :: r :: used) prems'
   175                   else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
   176                     (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
   177                 end
   178               else (case strip_type T of
   179                   (Ts, Type ("*", [T1, T2])) =>
   180                     let
   181                       val fx = Free (x, Ts ---> T1);
   182                       val fr = Free (r, Ts ---> T2);
   183                       val bs = map Bound (length Ts - 1 downto 0);
   184                       val t = list_abs (map (pair "z") Ts,
   185                         HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
   186                     in fun_of (fx :: ts) (fr :: rts) (t::args)
   187                       (x :: r :: used) prems
   188                     end
   189                 | (Ts, U) => fun_of (Free (x, T) :: ts)
   190                     (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
   191                     (Free (x, T) :: args) (x :: r :: used) prems)
   192             else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args)
   193               (x :: used) prems
   194           end
   195       | fun_of ts rts args used [] =
   196           let val xs = rev (rts @ ts)
   197           in if conclT = Extraction.nullT
   198             then list_abs_free (map dest_Free xs, HOLogic.unit)
   199             else list_abs_free (map dest_Free xs, list_comb
   200               (Free ("r" ^ Sign.base_name (name_of_thm intr),
   201                 map fastype_of (rev args) ---> conclT), rev args))
   202           end
   203 
   204   in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
   205 
   206 fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
   207   let
   208     val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
   209     val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
   210       SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
   211         find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
   212     val fs = maps (fn ((intrs, prems), dummy) =>
   213       let
   214         val fs = map (fn (rule, (ivs, intr)) =>
   215           fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
   216       in if dummy then Const ("arbitrary",
   217           HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
   218         else fs
   219       end) (premss ~~ dummies);
   220     val frees = fold Term.add_frees fs [];
   221     val Ts = map fastype_of fs;
   222     fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr)
   223   in
   224     fst (fold_map (fn concl => fn names =>
   225       let val T = Extraction.etype_of thy vs [] concl
   226       in if T = Extraction.nullT then (Extraction.nullt, names) else
   227         let
   228           val Type ("fun", [U, _]) = T;
   229           val a :: names' = names
   230         in (list_abs_free (("x", U) :: List.mapPartial (fn intr =>
   231           Option.map (pair (name_of_fn intr))
   232             (AList.lookup (op =) frees (name_of_fn intr))) intrs,
   233           list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
   234         end
   235       end) concls rec_names)
   236   end;
   237 
   238 fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
   239   if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
   240   else x;
   241 
   242 fun add_dummies f [] _ thy =
   243       (([], NONE), thy)
   244   | add_dummies f dts used thy =
   245       thy
   246       |> f (map snd dts)
   247       |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
   248     handle DatatypeAux.Datatype_Empty name' =>
   249       let
   250         val name = Sign.base_name name';
   251         val dname = Name.variant used "Dummy"
   252       in
   253         thy
   254         |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
   255       end;
   256 
   257 fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
   258   let
   259     val rvs = map fst (relevant_vars (prop_of rule));
   260     val xs = rev (Term.add_vars (prop_of rule) []);
   261     val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
   262     val rlzvs = rev (Term.add_vars (prop_of rrule) []);
   263     val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
   264     val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
   265     val rlz' = foldr forall_intr_term (prop_of rrule) (vs2 @ rs);
   266     val rlz'' = foldr forall_intr_term rlz vs2
   267   in (name, (vs,
   268     if rt = Extraction.nullt then rt else
   269       foldr (uncurry lambda) rt vs1,
   270     ProofRewriteRules.un_hhf_proof rlz' rlz''
   271       (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
   272   end;
   273 
   274 fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   275   let
   276     val qualifier = NameSpace.qualifier (name_of_thm induct);
   277     val inducts = PureThy.get_thms thy (Name
   278       (NameSpace.qualified qualifier "inducts"));
   279     val iTs = term_tvars (prop_of (hd intrs));
   280     val ar = length vs + length iTs;
   281     val params = InductivePackage.params_of raw_induct;
   282     val arities = InductivePackage.arities_of raw_induct;
   283     val nparms = length params;
   284     val params' = map dest_Var params;
   285     val rss = InductivePackage.partition_rules raw_induct intrs;
   286     val rss' = map (fn (((s, rs), (_, arity)), elim) =>
   287       (s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs)))
   288         (rss ~~ arities ~~ elims);
   289     val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
   290     val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
   291 
   292     val thy1 = thy |>
   293       Theory.root_path |>
   294       Theory.add_path (NameSpace.implode prfx);
   295     val (ty_eqs, rlz_eqs) = split_list
   296       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
   297 
   298     val thy1' = thy1 |>
   299       Theory.copy |>
   300       Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
   301       fold (fn s => AxClass.axiomatize_arity_i
   302         (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   303         Extraction.add_typeof_eqns_i ty_eqs;
   304     val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
   305       SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
   306 
   307     (** datatype representing computational content of inductive set **)
   308 
   309     val ((dummies, dt_info), thy2) =
   310       thy1
   311       |> add_dummies
   312            (DatatypePackage.add_datatype_i false false (map #2 dts))
   313            (map (pair false) dts) []
   314       ||> Extraction.add_typeof_eqns_i ty_eqs
   315       ||> Extraction.add_realizes_eqns_i rlz_eqs;
   316     fun get f = (these oo Option.map) f;
   317     val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
   318       HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
   319     val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
   320       if s mem rsets then
   321         let
   322           val (d :: dummies') = dummies;
   323           val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
   324         in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
   325           fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
   326         end
   327       else ((recs, dummies), replicate (length rs) Extraction.nullt))
   328         ((get #rec_thms dt_info, dummies), rss);
   329     val rintrs = map (fn (intr, c) => Envir.eta_contract
   330       (Extraction.realizes_of thy2 vs
   331         (if c = Extraction.nullt then c else list_comb (c, map Var (rev
   332           (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
   333             (maps snd rss ~~ List.concat constrss);
   334     val (rlzpreds, rlzpreds') = split_list
   335       (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
   336         let
   337           val Const (s, T) = head_of (HOLogic.dest_Trueprop
   338             (Logic.strip_assums_concl rintr));
   339           val s' = Sign.base_name s;
   340           val T' = Logic.unvarifyT T
   341         in ((s', SOME T', NoSyn),
   342           (Const (s, T'), Free (s', T')))
   343         end) rintrs));
   344     val rlzparams = map (fn Var ((s, _), T) => (s, SOME (Logic.unvarifyT T)))
   345       (List.take (snd (strip_comb
   346         (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
   347 
   348     (** realizability predicate **)
   349 
   350     val (ind_info, thy3') = thy2 |>
   351       InductivePackage.add_inductive_global false "" false false false
   352         rlzpreds rlzparams (map (fn (rintr, intr) =>
   353           ((Sign.base_name (name_of_thm intr), []),
   354            subst_atomic rlzpreds' (Logic.unvarify rintr)))
   355              (rintrs ~~ maps snd rss)) [] ||>
   356       Theory.absolute_path;
   357     val thy3 = PureThy.hide_thms false
   358       (map name_of_thm (#intrs ind_info)) thy3';
   359 
   360     (** realizer for induction rule **)
   361 
   362     val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
   363       SOME (fst (fst (dest_Var (head_of P)))) else NONE)
   364         (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
   365 
   366     fun add_ind_realizer (thy, Ps) =
   367       let
   368         val rs = indrule_realizer thy induct raw_induct rsets params'
   369           (vs @ Ps) rec_names rss' intrs dummies;
   370         val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs @ Ps) r
   371           (prop_of ind)) (rs ~~ inducts);
   372         val used = foldr add_term_free_names [] rlzs;
   373         val rnames = Name.variant_list used (replicate (length inducts) "r");
   374         val rnames' = Name.variant_list
   375           (used @ rnames) (replicate (length intrs) "s");
   376         val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
   377           let
   378             val (P, Q) = strip_one name (Logic.unvarify rlz);
   379             val Q' = strip_all' [] rnames' Q
   380           in
   381             (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
   382           end) (rlzs ~~ rnames);
   383         val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
   384           (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
   385         val rews = map mk_meta_eq
   386           (fst_conv :: snd_conv :: get #rec_thms dt_info);
   387         val thm = Goal.prove_global thy [] prems concl (fn prems => EVERY
   388           [rtac (#raw_induct ind_info) 1,
   389            rewrite_goals_tac rews,
   390            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   391              [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
   392               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   393         val (thm', thy') = PureThy.store_thm ((space_implode "_"
   394           (NameSpace.qualified qualifier "induct" :: vs @ Ps @
   395              ["correctness"]), thm), []) thy;
   396         val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
   397           (DatatypeAux.split_conj_thm thm');
   398         val ([thms'], thy'') = PureThy.add_thmss
   399           [((space_implode "_"
   400              (NameSpace.qualified qualifier "inducts" :: vs @ Ps @
   401                ["correctness"]), thms), [])] thy';
   402         val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
   403       in
   404         Extraction.add_realizers_i
   405           (map (fn (((ind, corr), rlz), r) =>
   406               mk_realizer thy' (vs @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
   407             realizers @ (case realizers of
   408              [(((ind, corr), rlz), r)] =>
   409                [mk_realizer thy' (vs @ Ps) (NameSpace.qualified qualifier "induct",
   410                   ind, corr, rlz, r)]
   411            | _ => [])) thy''
   412       end;
   413 
   414     (** realizer for elimination rules **)
   415 
   416     val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
   417       HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
   418 
   419     fun add_elim_realizer Ps
   420       (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
   421       let
   422         val (prem :: prems) = prems_of elim;
   423         fun reorder1 (p, (_, intr)) =
   424           Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
   425             (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
   426         fun reorder2 ((ivs, intr), i) =
   427           let val fs = Term.add_vars (prop_of intr) [] \\ params'
   428           in Library.foldl (fn (t, x) => lambda (Var x) t)
   429             (list_comb (Bound (i + length ivs), ivs), fs)
   430           end;
   431         val p = Logic.list_implies
   432           (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
   433         val T' = Extraction.etype_of thy (vs @ Ps) [] p;
   434         val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
   435         val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
   436         val r = if null Ps then Extraction.nullt
   437           else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
   438             (if dummy then
   439                [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
   440              else []) @
   441             map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   442             [Bound (length prems)]));
   443         val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
   444         val rlz' = strip_all (Logic.unvarify rlz);
   445         val rews = map mk_meta_eq case_thms;
   446         val thm = Goal.prove_global thy []
   447           (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn prems => EVERY
   448           [cut_facts_tac [hd prems] 1,
   449            etac elimR 1,
   450            ALLGOALS (asm_simp_tac HOL_basic_ss),
   451            rewrite_goals_tac rews,
   452            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
   453              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   454         val (thm', thy') = PureThy.store_thm ((space_implode "_"
   455           (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
   456       in
   457         Extraction.add_realizers_i
   458           [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
   459       end;
   460 
   461     (** add realizers to theory **)
   462 
   463     val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
   464     val thy5 = Extraction.add_realizers_i
   465       (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
   466          (name_of_thm rule, rule, rrule, rlz,
   467             list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
   468               (List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~
   469                  List.concat constrss))) thy4;
   470     val elimps = List.mapPartial (fn ((s, intrs), p) =>
   471       if s mem rsets then SOME (p, intrs) else NONE)
   472         (rss' ~~ (elims ~~ #elims ind_info));
   473     val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
   474       add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
   475         (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
   476            elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
   477 
   478   in Theory.restore_naming thy thy6 end;
   479 
   480 fun add_ind_realizers name rsets thy =
   481   let
   482     val (_, {intrs, induct, raw_induct, elims, ...}) =
   483       InductivePackage.the_inductive (ProofContext.init thy) name;
   484     val vss = sort (int_ord o pairself length)
   485       (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
   486   in
   487     Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
   488   end
   489 
   490 fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
   491   let
   492     fun err () = error "ind_realizer: bad rule";
   493     val sets =
   494       (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
   495            [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
   496          | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
   497          handle TERM _ => err () | Empty => err ();
   498   in 
   499     add_ind_realizers (hd sets)
   500       (case arg of
   501         NONE => sets | SOME NONE => []
   502       | SOME (SOME sets') => sets \\ sets')
   503   end I);
   504 
   505 val ind_realizer = Attrib.syntax
   506  ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
   507     Scan.option (Scan.lift (Args.colon) |--
   508       Scan.repeat1 Args.const))) >> rlz_attrib);
   509 
   510 val setup =
   511   Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
   512 
   513 end;
   514