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