src/HOL/Tools/inductive_realizer.ML
author wenzelm
Wed Apr 26 22:38:05 2006 +0200 (2006-04-26)
changeset 19473 d87a8838afa4
parent 19046 bc5c6c9b114e
child 19510 29fc4e5a638c
permissions -rw-r--r--
tuned;
     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 val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
    19 
    20 fun prf_of thm =
    21   let val {sign, prop, der = (_, prf), ...} = rep_thm thm
    22   in Reconstruct.reconstruct_proof sign prop prf end;
    23 
    24 fun forall_intr_prf (t, prf) =
    25   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    26   in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    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 set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem;
    34 
    35 fun strip_all t =
    36   let
    37     fun strip used (Const ("all", _) $ Abs (s, T, t)) =
    38           let val s' = variant used s
    39           in strip (s'::used) (subst_bound (Free (s', T), t)) end
    40       | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
    41       | strip _ t = t;
    42   in strip (add_term_free_names (t, [])) t end;
    43 
    44 fun relevant_vars prop = foldr (fn
    45       (Var ((a, i), T), vs) => (case strip_type T of
    46         (_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs
    47       | _ => vs)
    48     | (_, vs) => vs) [] (term_vars prop);
    49 
    50 fun params_of intr = map (fst o fst o dest_Var) (term_vars
    51   (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
    52     (Logic.strip_imp_concl intr)))));
    53 
    54 fun dt_of_intrs thy vs intrs =
    55   let
    56     val iTs = term_tvars (prop_of (hd intrs));
    57     val Tvs = map TVar iTs;
    58     val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
    59     val (Const (s, _), ts) = strip_comb S;
    60     val params = map dest_Var ts;
    61     val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
    62     fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
    63       map (Type.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
    64         filter_out (equal Extraction.nullT) (map
    65           (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    66             NoSyn);
    67   in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
    68     map constr_of_intr intrs)
    69   end;
    70 
    71 fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
    72 
    73 (** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **)
    74 
    75 fun gen_rvar vs (t as Var ((a, 0), T)) =
    76       let val U = TVar (("'" ^ a, 0), HOLogic.typeS)
    77       in case try HOLogic.dest_setT T of
    78           NONE => if body_type T <> HOLogic.boolT then t else
    79             let
    80               val Ts = binder_types T;
    81               val i = length Ts;
    82               val xs = map (pair "x") Ts;
    83               val u = list_comb (t, map Bound (i - 1 downto 0))
    84             in 
    85               if a mem vs then
    86                 list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
    87               else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
    88             end
    89         | SOME T' => if a mem vs then
    90               Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $
    91                 (HOLogic.mk_mem (Bound 0, t))))
    92             else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $
    93               (HOLogic.mk_mem (Bound 0, t)))
    94       end
    95   | gen_rvar _ t = t;
    96 
    97 fun mk_realizes_eqn n vs intrs =
    98   let
    99     val iTs = term_tvars (prop_of (hd intrs));
   100     val Tvs = map TVar iTs;
   101     val _ $ (_ $ _ $ S) = concl_of (hd intrs);
   102     val (Const (s, T), ts') = strip_comb S;
   103     val setT = body_type T;
   104     val elT = HOLogic.dest_setT setT;
   105     val x = Var (("x", 0), elT);
   106     val rT = if n then Extraction.nullT
   107       else Type (space_implode "_" (s ^ "T" :: vs),
   108         map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
   109     val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
   110     val rvs = relevant_vars S;
   111     val vs' = map fst rvs \\ vs;
   112     val rname = space_implode "_" (s ^ "R" :: vs);
   113 
   114     fun mk_Tprem n v =
   115       let val T = (the o AList.lookup (op =) rvs) v
   116       in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
   117         Extraction.mk_typ (if n then Extraction.nullT
   118           else TVar (("'" ^ v, 0), HOLogic.typeS)))
   119       end;
   120 
   121     val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
   122     val ts = map (gen_rvar vs) ts';
   123     val argTs = map fastype_of ts;
   124 
   125   in ((prems, (Const ("typeof", setT --> Type ("Type", [])) $ S,
   126        Extraction.mk_typ rT)),
   127     (prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S),
   128        if n then
   129          HOLogic.mk_mem (x, list_comb (Const (rname, argTs ---> setT), ts))
   130        else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname,
   131          argTs ---> HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts)))))
   132   end;
   133 
   134 fun fun_of_prem thy rsets vs params rule intr =
   135   let
   136     (* add_term_vars and Term.add_vars may return variables in different order *)
   137     val args = map (Free o apfst fst o dest_Var)
   138       (add_term_vars (prop_of intr, []) \\ map Var params);
   139     val args' = map (Free o apfst fst)
   140       (Term.add_vars (prop_of intr) [] \\ params);
   141     val rule' = strip_all rule;
   142     val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
   143     val used = map (fst o dest_Free) args;
   144 
   145     fun is_rec t = not (null (term_consts t inter rsets));
   146 
   147     fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
   148       | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
   149       | is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true
   150       | is_meta _ = false;
   151 
   152     fun fun_of ts rts args used (prem :: prems) =
   153           let
   154             val T = Extraction.etype_of thy vs [] prem;
   155             val [x, r] = variantlist (["x", "r"], used)
   156           in if T = Extraction.nullT
   157             then fun_of ts rts args used prems
   158             else if is_rec prem then
   159               if is_meta prem then
   160                 let
   161                   val prem' :: prems' = prems;
   162                   val U = Extraction.etype_of thy vs [] prem';
   163                 in if U = Extraction.nullT
   164                   then fun_of (Free (x, T) :: ts)
   165                     (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
   166                     (Free (x, T) :: args) (x :: r :: used) prems'
   167                   else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
   168                     (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
   169                 end
   170               else (case strip_type T of
   171                   (Ts, Type ("*", [T1, T2])) =>
   172                     let
   173                       val fx = Free (x, Ts ---> T1);
   174                       val fr = Free (r, Ts ---> T2);
   175                       val bs = map Bound (length Ts - 1 downto 0);
   176                       val t = list_abs (map (pair "z") Ts,
   177                         HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
   178                     in fun_of (fx :: ts) (fr :: rts) (t::args)
   179                       (x :: r :: used) prems
   180                     end
   181                 | (Ts, U) => fun_of (Free (x, T) :: ts)
   182                     (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
   183                     (Free (x, T) :: args) (x :: r :: used) prems)
   184             else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args)
   185               (x :: used) prems
   186           end
   187       | fun_of ts rts args used [] =
   188           let val xs = rev (rts @ ts)
   189           in if conclT = Extraction.nullT
   190             then list_abs_free (map dest_Free xs, HOLogic.unit)
   191             else list_abs_free (map dest_Free xs, list_comb
   192               (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr),
   193                 map fastype_of (rev args) ---> conclT), rev args))
   194           end
   195 
   196   in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
   197 
   198 fun find_first f = Library.find_first f;
   199 
   200 fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
   201   let
   202     val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
   203     val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
   204       SOME (map (fn r => List.nth (prems_of raw_induct,
   205         find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
   206     val concls' = List.mapPartial (fn (s, _) => if s mem rsets then
   207         find_first (fn concl => s mem term_consts concl) concls
   208       else NONE) rss;
   209     val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
   210       let
   211         val (intrs1, intrs2) = chop (length prems) intrs;
   212         val fs = map (fn (rule, intr) =>
   213           fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
   214       in (intrs2, if dummy then Const ("arbitrary",
   215           HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
   216         else fs)
   217       end) (intrs, (premss ~~ dummies))));
   218     val frees = fold Term.add_frees fs [];
   219     val Ts = map fastype_of fs;
   220     val rlzs = List.mapPartial (fn (a, concl) =>
   221       let val T = Extraction.etype_of thy vs [] concl
   222       in if T = Extraction.nullT then NONE
   223         else SOME (list_comb (Const (a, Ts ---> T), fs))
   224       end) (rec_names ~~ concls')
   225   in if null rlzs then Extraction.nullt else
   226     let
   227       val r = foldr1 HOLogic.mk_prod rlzs;
   228       val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
   229       fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
   230       val r' = list_abs_free (List.mapPartial (fn intr =>
   231         Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
   232           if length concls = 1 then r $ x else r)
   233     in
   234       if length concls = 1 then lambda x r' else r'
   235     end
   236   end;
   237 
   238 fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
   239   if name = 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 = 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 params ((rule, rrule), rt) =
   258   let
   259     val prems = prems_of rule ~~ prems_of rrule;
   260     val rvs = map fst (relevant_vars (prop_of rule));
   261     val xs = rev (Term.add_vars (prop_of rule) []);
   262     val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
   263     val rlzvs = rev (Term.add_vars (prop_of rrule) []);
   264     val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
   265     val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
   266 
   267     fun mk_prf _ [] prf = prf
   268       | mk_prf rs ((prem, rprem) :: prems) prf =
   269           if Extraction.etype_of thy vs [] prem = Extraction.nullT
   270           then AbsP ("H", SOME rprem, mk_prf rs prems prf)
   271           else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem,
   272             mk_prf (tl rs) prems prf));
   273 
   274   in (Thm.name_of_thm rule, (vs,
   275     if rt = Extraction.nullt then rt else
   276       foldr (uncurry lambda) rt vs1,
   277     foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
   278       (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
   279   end;
   280 
   281 fun add_rule r rss =
   282   let
   283     val _ $ (_ $ _ $ S) = concl_of r;
   284     val (Const (s, _), _) = strip_comb S;
   285   in
   286     rss
   287     |> AList.default (op =) (s, [])
   288     |> AList.map_entry (op =) s (fn rs => rs @ [r])
   289   end;
   290 
   291 fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   292   let
   293     val iTs = term_tvars (prop_of (hd intrs));
   294     val ar = length vs + length iTs;
   295     val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
   296     val (_, params) = strip_comb S;
   297     val params' = map dest_Var params;
   298     val rss = [] |> Library.fold add_rule intrs;
   299     val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
   300     val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
   301 
   302     val thy1 = thy |>
   303       Theory.root_path |>
   304       Theory.add_path (NameSpace.pack prfx);
   305     val (ty_eqs, rlz_eqs) = split_list
   306       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
   307 
   308     val thy1' = thy1 |>
   309       Theory.copy |>
   310       Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
   311       Theory.add_arities_i (map (fn s =>
   312         (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) |>
   313         Extraction.add_typeof_eqns_i ty_eqs;
   314     val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
   315       SOME (dt_of_intrs thy1' vs rs) else NONE) rss;
   316 
   317     (** datatype representing computational content of inductive set **)
   318 
   319     val ((dummies, dt_info), thy2) =
   320       thy1
   321       |> add_dummies
   322            (DatatypePackage.add_datatype_i false false (map #2 dts))
   323            (map (pair false) dts) []
   324       ||> Extraction.add_typeof_eqns_i ty_eqs
   325       ||> Extraction.add_realizes_eqns_i rlz_eqs;
   326     fun get f = (these oo Option.map) f;
   327     val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
   328       HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
   329     val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
   330       if s mem rsets then
   331         let
   332           val (d :: dummies') = dummies;
   333           val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
   334         in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
   335           fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
   336         end
   337       else ((recs, dummies), replicate (length rs) Extraction.nullt))
   338         ((get #rec_thms dt_info, dummies), rss);
   339     val rintrs = map (fn (intr, c) => Envir.eta_contract
   340       (Extraction.realizes_of thy2 vs
   341         c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
   342           (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
   343             (intrs ~~ List.concat constrss);
   344     val rlzsets = distinct (op =) (map (fn rintr => snd (HOLogic.dest_mem
   345       (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
   346 
   347     (** realizability predicate **)
   348 
   349     val (thy3', ind_info) = thy2 |>
   350       InductivePackage.add_inductive_i false true "" false false false
   351         (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
   352           ((Sign.base_name (Thm.name_of_thm intr), strip_all
   353             (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
   354       Theory.absolute_path;
   355     val thy3 = PureThy.hide_thms false
   356       (map Thm.name_of_thm (#intrs ind_info)) thy3';
   357 
   358     (** realizer for induction rule **)
   359 
   360     val Ps = List.mapPartial (fn _ $ M $ P => if set_of M mem rsets then
   361       SOME (fst (fst (dest_Var (head_of P)))) else NONE)
   362         (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
   363 
   364     fun add_ind_realizer (thy, Ps) =
   365       let
   366         val r = indrule_realizer thy induct raw_induct rsets params'
   367           (vs @ Ps) rec_names rss intrs dummies;
   368         val rlz = strip_all (Logic.unvarify
   369           (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
   370         val rews = map mk_meta_eq
   371           (fst_conv :: snd_conv :: get #rec_thms dt_info);
   372         val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
   373           [if length rss = 1 then
   374              cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
   375            else EVERY [rewrite_goals_tac (rews @ all_simps),
   376              REPEAT (rtac allI 1), rtac (#induct ind_info) 1],
   377            rewrite_goals_tac rews,
   378            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   379              [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
   380               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   381         val (thm', thy') = PureThy.store_thm ((space_implode "_"
   382           (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy
   383       in
   384         Extraction.add_realizers_i
   385           [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
   386       end;
   387 
   388     (** realizer for elimination rules **)
   389 
   390     val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
   391       HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
   392 
   393     fun add_elim_realizer Ps
   394       (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
   395       let
   396         val (prem :: prems) = prems_of elim;
   397         fun reorder1 (p, intr) =
   398           Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
   399             (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
   400         fun reorder2 (intr, i) =
   401           let
   402             val fs1 = term_vars (prop_of intr) \\ params;
   403             val fs2 = Term.add_vars (prop_of intr) [] \\ params'
   404           in Library.foldl (fn (t, x) => lambda (Var x) t)
   405             (list_comb (Bound (i + length fs1), fs1), fs2)
   406           end;
   407         val p = Logic.list_implies
   408           (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
   409         val T' = Extraction.etype_of thy (vs @ Ps) [] p;
   410         val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
   411         val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
   412         val r = if null Ps then Extraction.nullt
   413           else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
   414             (if dummy then
   415                [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
   416              else []) @
   417             map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   418             [Bound (length prems)]));
   419         val rlz = strip_all (Logic.unvarify
   420           (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
   421         val rews = map mk_meta_eq case_thms;
   422         val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
   423           [cut_facts_tac [hd prems] 1,
   424            etac elimR 1,
   425            ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
   426            rewrite_goals_tac rews,
   427            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
   428              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   429         val (thm', thy') = PureThy.store_thm ((space_implode "_"
   430           (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
   431       in
   432         Extraction.add_realizers_i
   433           [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'
   434       end;
   435 
   436     (** add realizers to theory **)
   437 
   438     val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth
   439       (#intrs ind_info, find_index_eq r intrs)) rs) rss);
   440     val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
   441     val thy5 = Extraction.add_realizers_i
   442       (map (mk_realizer thy4 vs params')
   443          (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
   444             map Var (rev (Term.add_vars (prop_of rule) []) \\ params')))) 
   445               (List.concat (map snd rss) ~~ rintr_thms ~~ List.concat constrss))) thy4;
   446     val elimps = List.mapPartial (fn (s, intrs) => if s mem rsets then
   447         Option.map (rpair intrs) (find_first (fn (thm, _) =>
   448           s mem term_consts (hd (prems_of thm))) (elims ~~ #elims ind_info))
   449       else NONE) rss;
   450     val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
   451       add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
   452         (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
   453            elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
   454 
   455   in Theory.restore_naming thy thy6 end;
   456 
   457 fun add_ind_realizers name rsets thy =
   458   let
   459     val (_, {intrs, induct, raw_induct, elims, ...}) =
   460       (case InductivePackage.get_inductive thy name of
   461          NONE => error ("Unknown inductive set " ^ quote name)
   462        | SOME info => info);
   463     val _ $ (_ $ _ $ S) = concl_of (hd intrs);
   464     val vss = sort (int_ord o pairself length)
   465       (subsets (map fst (relevant_vars S)))
   466   in
   467     Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
   468   end
   469 
   470 fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.map_theory
   471   let
   472     fun err () = error "ind_realizer: bad rule";
   473     val sets =
   474       (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
   475            [_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
   476          | xs => map (set_of o fst o HOLogic.dest_imp) xs)
   477          handle TERM _ => err () | Empty => err ();
   478   in 
   479     add_ind_realizers (hd sets)
   480       (case arg of
   481         NONE => sets | SOME NONE => []
   482       | SOME (SOME sets') => sets \\ sets')
   483   end);
   484 
   485 val ind_realizer = Attrib.syntax
   486  ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
   487     Scan.option (Scan.lift (Args.colon) |--
   488       Scan.repeat1 Args.const))) >> rlz_attrib);
   489 
   490 val setup =
   491   Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
   492 
   493 end;
   494