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