New package for constructing realizers for introduction and elimination
authorberghofe
Wed Nov 13 15:32:41 2002 +0100 (2002-11-13)
changeset 1371075bec2c1bfd5
parent 13709 ec00ba43aee8
child 13711 5ace1cccb612
New package for constructing realizers for introduction and elimination
rules of inductive predicates.
src/HOL/Tools/inductive_realizer.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Nov 13 15:32:41 2002 +0100
     1.3 @@ -0,0 +1,493 @@
     1.4 +(*  Title:      HOL/Tools/inductive_realizer.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Porgram extraction from proofs involving inductive predicates:
    1.10 +Realizers for induction and elimination rules
    1.11 +*)
    1.12 +
    1.13 +signature INDUCTIVE_REALIZER =
    1.14 +sig
    1.15 +  val add_ind_realizers: string -> string list -> theory -> theory
    1.16 +  val setup: (theory -> theory) list
    1.17 +end;
    1.18 +
    1.19 +structure InductiveRealizer : INDUCTIVE_REALIZER =
    1.20 +struct
    1.21 +
    1.22 +val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
    1.23 +
    1.24 +fun prf_of thm =
    1.25 +  let val {sign, prop, der = (_, prf), ...} = rep_thm thm
    1.26 +  in Reconstruct.reconstruct_proof sign prop prf end;
    1.27 +
    1.28 +fun forall_intr_prf (t, prf) =
    1.29 +  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    1.30 +  in Abst (a, Some T, Proofterm.prf_abstract_over t prf) end;
    1.31 +
    1.32 +fun subsets [] = [[]]
    1.33 +  | subsets (x::xs) =
    1.34 +      let val ys = subsets xs
    1.35 +      in ys @ map (cons x) ys end;
    1.36 +
    1.37 +val set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem;
    1.38 +
    1.39 +fun strip_all t =
    1.40 +  let
    1.41 +    fun strip used (Const ("all", _) $ Abs (s, T, t)) =
    1.42 +          let val s' = variant used s
    1.43 +          in strip (s'::used) (subst_bound (Free (s', T), t)) end
    1.44 +      | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
    1.45 +      | strip _ t = t;
    1.46 +  in strip (add_term_free_names (t, [])) t end;
    1.47 +
    1.48 +fun relevant_vars prop = foldr (fn
    1.49 +      (Var ((a, i), T), vs) => (case strip_type T of
    1.50 +        (_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs
    1.51 +      | _ => vs)
    1.52 +    | (_, vs) => vs) (term_vars prop, []);
    1.53 +
    1.54 +fun params_of intr = map (fst o fst o dest_Var) (term_vars
    1.55 +  (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
    1.56 +    (Logic.strip_imp_concl intr)))));
    1.57 +
    1.58 +fun dt_of_intrs thy vs intrs =
    1.59 +  let
    1.60 +    val iTs = term_tvars (prop_of (hd intrs));
    1.61 +    val Tvs = map TVar iTs;
    1.62 +    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
    1.63 +    val (Const (s, _), ts) = strip_comb S;
    1.64 +    val params = map dest_Var ts;
    1.65 +    val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
    1.66 +    fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
    1.67 +      map (Type.unvarifyT o snd) (rev (Term.add_vars ([], prop_of intr)) \\ params) @
    1.68 +        filter_out (equal Extraction.nullT) (map
    1.69 +          (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    1.70 +            NoSyn);
    1.71 +  in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
    1.72 +    map constr_of_intr intrs)
    1.73 +  end;
    1.74 +
    1.75 +fun gen_realizes (Const ("realizes", Type ("fun", [T, _])) $ t $
    1.76 +      (Const ("op :", Type ("fun", [U, _])) $ x $ Var (ixn, _))) =
    1.77 +        Var (ixn, [T, U] ---> HOLogic.boolT) $ t $ x
    1.78 +  | gen_realizes (Const ("op :", Type ("fun", [U, _])) $ x $ Var (ixn, _)) =
    1.79 +      Var (ixn, U --> HOLogic.boolT) $ x
    1.80 +  | gen_realizes (bla as Const ("realizes", Type ("fun", [T, _])) $ t $ P) =
    1.81 +      if T = Extraction.nullT then P
    1.82 +      else (case strip_comb P of
    1.83 +          (Var (ixn, U), ts) => list_comb (Var (ixn, T --> U), t :: ts)
    1.84 +        | _ => error "gen_realizes: variable expected")
    1.85 +  | gen_realizes (t $ u) = gen_realizes t $ gen_realizes u
    1.86 +  | gen_realizes (Abs (s, T, t)) = Abs (s, T, gen_realizes t)
    1.87 +  | gen_realizes t = t;
    1.88 +
    1.89 +fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
    1.90 +fun mk_rlz' T = Const ("realizes", [T, propT] ---> propT);
    1.91 +
    1.92 +(** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **)
    1.93 +
    1.94 +fun gen_rvar vs (t as Var ((a, 0), T)) =
    1.95 +      let val U = TVar (("'" ^ a, 0), HOLogic.typeS)
    1.96 +      in case try HOLogic.dest_setT T of
    1.97 +          None => if body_type T <> HOLogic.boolT then t else
    1.98 +            let
    1.99 +              val Ts = binder_types T;
   1.100 +              val i = length Ts;
   1.101 +              val xs = map (pair "x") Ts;
   1.102 +              val u = list_comb (t, map Bound (i - 1 downto 0))
   1.103 +            in 
   1.104 +              if a mem vs then
   1.105 +                list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
   1.106 +              else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
   1.107 +            end
   1.108 +        | Some T' => if a mem vs then
   1.109 +              Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $
   1.110 +                (HOLogic.mk_mem (Bound 0, t))))
   1.111 +            else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $
   1.112 +              (HOLogic.mk_mem (Bound 0, t)))
   1.113 +      end
   1.114 +  | gen_rvar _ t = t;
   1.115 +
   1.116 +fun mk_realizes_eqn n vs intrs =
   1.117 +  let
   1.118 +    val iTs = term_tvars (prop_of (hd intrs));
   1.119 +    val Tvs = map TVar iTs;
   1.120 +    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
   1.121 +    val (Const (s, T), ts') = strip_comb S;
   1.122 +    val setT = body_type T;
   1.123 +    val elT = HOLogic.dest_setT setT;
   1.124 +    val x = Var (("x", 0), elT);
   1.125 +    val rT = if n then Extraction.nullT
   1.126 +      else Type (space_implode "_" (s ^ "T" :: vs),
   1.127 +        map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
   1.128 +    val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
   1.129 +    val rvs = relevant_vars S;
   1.130 +    val vs' = map fst rvs \\ vs;
   1.131 +    val rname = space_implode "_" (s ^ "R" :: vs);
   1.132 +
   1.133 +    fun mk_Tprem n v =
   1.134 +      let val Some T = assoc (rvs, v)
   1.135 +      in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
   1.136 +        Extraction.mk_typ (if n then Extraction.nullT
   1.137 +          else TVar (("'" ^ v, 0), HOLogic.typeS)))
   1.138 +      end;
   1.139 +
   1.140 +    val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
   1.141 +    val ts = map (gen_rvar vs) ts';
   1.142 +    val argTs = map fastype_of ts;
   1.143 +
   1.144 +  in ((prems, (Const ("typeof", setT --> Type ("Type", [])) $ S,
   1.145 +       Extraction.mk_typ rT)),
   1.146 +    (prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S),
   1.147 +       if n then
   1.148 +         HOLogic.mk_mem (x, list_comb (Const (rname, argTs ---> setT), ts))
   1.149 +       else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname,
   1.150 +         argTs ---> HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts)))))
   1.151 +  end;
   1.152 +
   1.153 +fun fun_of_prem thy rsets vs params rule intr =
   1.154 +  let
   1.155 +    (* add_term_vars and Term.add_vars may return variables in different order *)
   1.156 +    val args = map (Free o apfst fst o dest_Var)
   1.157 +      (add_term_vars (prop_of intr, []) \\ map Var params);
   1.158 +    val args' = map (Free o apfst fst)
   1.159 +      (Term.add_vars ([], prop_of intr) \\ params);
   1.160 +    val rule' = strip_all rule;
   1.161 +    val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
   1.162 +    val used = map (fst o dest_Free) args;
   1.163 +
   1.164 +    fun is_rec t = not (null (term_consts t inter rsets));
   1.165 +
   1.166 +    fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
   1.167 +      | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
   1.168 +      | is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true
   1.169 +      | is_meta _ = false;
   1.170 +
   1.171 +    fun fun_of ts rts args used (prem :: prems) =
   1.172 +          let
   1.173 +            val T = Extraction.etype_of thy vs [] prem;
   1.174 +            val [x, r] = variantlist (["x", "r"], used)
   1.175 +          in if T = Extraction.nullT
   1.176 +            then fun_of ts rts args used prems
   1.177 +            else if is_rec prem then
   1.178 +              if is_meta prem then
   1.179 +                let
   1.180 +                  val prem' :: prems' = prems;
   1.181 +                  val U = Extraction.etype_of thy vs [] prem';
   1.182 +                in if U = Extraction.nullT
   1.183 +                  then fun_of (Free (x, T) :: ts)
   1.184 +                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
   1.185 +                    (Free (x, T) :: args) (x :: r :: used) prems'
   1.186 +                  else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
   1.187 +                    (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
   1.188 +                end
   1.189 +              else (case strip_type T of
   1.190 +                  (Ts, Type ("*", [T1, T2])) =>
   1.191 +                    let
   1.192 +                      val fx = Free (x, Ts ---> T1);
   1.193 +                      val fr = Free (r, Ts ---> T2);
   1.194 +                      val bs = map Bound (length Ts - 1 downto 0);
   1.195 +                      val t = list_abs (map (pair "z") Ts,
   1.196 +                        HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
   1.197 +                    in fun_of (fx :: ts) (fr :: rts) (t::args)
   1.198 +                      (x :: r :: used) prems
   1.199 +                    end
   1.200 +                | (Ts, U) => fun_of (Free (x, T) :: ts)
   1.201 +                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
   1.202 +                    (Free (x, T) :: args) (x :: r :: used) prems)
   1.203 +            else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args)
   1.204 +              (x :: used) prems
   1.205 +          end
   1.206 +      | fun_of ts rts args used [] =
   1.207 +          let val xs = rev (rts @ ts)
   1.208 +          in if conclT = Extraction.nullT
   1.209 +            then list_abs_free (map dest_Free xs, HOLogic.unit)
   1.210 +            else list_abs_free (map dest_Free xs, list_comb
   1.211 +              (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr),
   1.212 +                map fastype_of (rev args) ---> conclT), rev args))
   1.213 +          end
   1.214 +
   1.215 +  in fun_of (rev args) [] args' used (Logic.strip_imp_prems rule') end;
   1.216 +
   1.217 +fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
   1.218 +  let
   1.219 +    val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
   1.220 +    val premss = mapfilter (fn (s, rs) => if s mem rsets then
   1.221 +      Some (map (fn r => nth_elem (find_index_eq (prop_of r) (map prop_of intrs),
   1.222 +        prems_of raw_induct)) rs) else None) rss;
   1.223 +    val concls' = mapfilter (fn (s, _) => if s mem rsets then
   1.224 +        find_first (fn concl => s mem term_consts concl) concls
   1.225 +      else None) rss;
   1.226 +    val fs = flat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
   1.227 +      let
   1.228 +        val (intrs1, intrs2) = splitAt (length prems, intrs);
   1.229 +        val fs = map (fn (rule, intr) =>
   1.230 +          fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
   1.231 +      in (intrs2, if dummy then Const ("arbitrary",
   1.232 +          HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
   1.233 +        else fs)
   1.234 +      end) (intrs, (premss ~~ dummies))));
   1.235 +    val frees = foldl Term.add_frees ([], fs);
   1.236 +    val Ts = map fastype_of fs;
   1.237 +    val rlzs = mapfilter (fn (a, concl) =>
   1.238 +      let val T = Extraction.etype_of thy vs [] concl
   1.239 +      in if T = Extraction.nullT then None
   1.240 +        else Some (list_comb (Const (a, Ts ---> T), fs))
   1.241 +      end) (rec_names ~~ concls')
   1.242 +  in if null rlzs then Extraction.nullt else
   1.243 +    let
   1.244 +      val r = foldr1 HOLogic.mk_prod rlzs;
   1.245 +      val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
   1.246 +      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
   1.247 +      val r' = list_abs_free (mapfilter (fn intr =>
   1.248 +        apsome (pair (name_of_fn intr)) (assoc (frees, name_of_fn intr))) intrs,
   1.249 +          if length concls = 1 then r $ x else r)
   1.250 +    in
   1.251 +      if length concls = 1 then lambda x r' else r'
   1.252 +    end
   1.253 +  end;
   1.254 +
   1.255 +val nonempty_msg = explode "Nonemptiness check failed for datatype ";
   1.256 +
   1.257 +fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
   1.258 +  if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
   1.259 +  else x;
   1.260 +
   1.261 +fun add_dummies f dts used thy =
   1.262 +  apsnd (pair (map fst dts)) (transform_error (f (map snd dts)) thy)
   1.263 +  handle ERROR_MESSAGE msg => if nonempty_msg prefix explode msg then
   1.264 +      let
   1.265 +        val name = Sign.base_name
   1.266 +          (implode (drop (length nonempty_msg, explode msg)));
   1.267 +        val dname = variant used "Dummy"
   1.268 +      in add_dummies f (map (add_dummy name dname) dts) (dname :: used) thy
   1.269 +      end
   1.270 +    else error msg;
   1.271 +
   1.272 +fun mk_realizer thy vs params ((rule, rrule), rt) =
   1.273 +  let
   1.274 +    val prems = prems_of rule;
   1.275 +    val xs = rev (Term.add_vars ([], prop_of rule));
   1.276 +    val rs = gen_rems (op = o pairself fst)
   1.277 +      (rev (Term.add_vars ([], prop_of rrule)), xs);
   1.278 +
   1.279 +    fun mk_prf _ [] prf = prf
   1.280 +      | mk_prf rs (prem :: prems) prf =
   1.281 +          let val T = Extraction.etype_of thy vs [] prem
   1.282 +          in if T = Extraction.nullT
   1.283 +            then AbsP ("H", Some (mk_rlz' T $ Extraction.nullt $ prem),
   1.284 +              mk_prf rs prems prf)
   1.285 +            else forall_intr_prf (Var (hd rs), AbsP ("H", Some (mk_rlz' T $
   1.286 +              Var (hd rs) $ prem), mk_prf (tl rs) prems prf))
   1.287 +          end;
   1.288 +
   1.289 +    val subst = map (fn v as (ixn, _) => (ixn, gen_rvar vs (Var v))) xs;
   1.290 +    val prf = Proofterm.map_proof_terms
   1.291 +      (subst_vars ([], subst)) I (prf_of rrule);
   1.292 +
   1.293 +  in (Thm.name_of_thm rule, (vs,
   1.294 +    if rt = Extraction.nullt then rt else
   1.295 +      foldr (uncurry lambda) (map Var xs, rt),
   1.296 +    foldr forall_intr_prf (map Var xs, mk_prf rs prems (Proofterm.proof_combP
   1.297 +      (prf, map PBound (length prems - 1 downto 0))))))
   1.298 +  end;
   1.299 +
   1.300 +fun add_rule (rss, r) =
   1.301 +  let
   1.302 +    val _ $ (_ $ _ $ S) = concl_of r;
   1.303 +    val (Const (s, _), _) = strip_comb S;
   1.304 +    val rs = if_none (assoc (rss, s)) [];
   1.305 +  in overwrite (rss, (s, rs @ [r])) end;
   1.306 +
   1.307 +fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   1.308 +  let
   1.309 +    val iTs = term_tvars (prop_of (hd intrs));
   1.310 +    val ar = length vs + length iTs;
   1.311 +    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
   1.312 +    val (_, params) = strip_comb S;
   1.313 +    val params' = map dest_Var params;
   1.314 +    val rss = foldl add_rule ([], intrs);
   1.315 +    val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
   1.316 +    val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
   1.317 +    val {path, ...} = Sign.rep_sg (sign_of thy);
   1.318 +    val thy1 = thy |>
   1.319 +      Theory.root_path |>
   1.320 +      Theory.add_path (NameSpace.pack prfx);
   1.321 +    val (ty_eqs, rlz_eqs) = split_list
   1.322 +      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
   1.323 +
   1.324 +    val thy1' = thy1 |>
   1.325 +      Theory.copy |>
   1.326 +      Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
   1.327 +      Theory.add_arities_i (map (fn s =>
   1.328 +        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) |>
   1.329 +        Extraction.add_typeof_eqns_i ty_eqs;
   1.330 +    val dts = mapfilter (fn (s, rs) => if s mem rsets then
   1.331 +      Some (dt_of_intrs thy1' vs rs) else None) rss;
   1.332 +
   1.333 +    (** datatype representing computational content of inductive set **)
   1.334 +
   1.335 +    val (thy2, (dummies, dt_info)) = thy1 |>
   1.336 +      (if null dts then rpair ([], None) else
   1.337 +        apsnd (apsnd Some) o add_dummies (DatatypePackage.add_datatype_i false
   1.338 +          (map #2 dts)) (map (pair false) dts) []) |>>
   1.339 +      Extraction.add_typeof_eqns_i ty_eqs |>>
   1.340 +      Extraction.add_realizes_eqns_i rlz_eqs;
   1.341 +    fun get f x = if_none (apsome f x) [];
   1.342 +    val rec_names = distinct (map (fst o dest_Const o head_of o fst o
   1.343 +      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
   1.344 +    val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
   1.345 +      if s mem rsets then
   1.346 +        let
   1.347 +          val (d :: dummies') = dummies;
   1.348 +          val (recs1, recs2) = splitAt (length rs, if d then tl recs else recs)
   1.349 +        in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
   1.350 +          fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
   1.351 +        end
   1.352 +      else ((recs, dummies), replicate (length rs) Extraction.nullt))
   1.353 +        ((get #rec_thms dt_info, dummies), rss);
   1.354 +    val rintrs = map (fn (intr, c) => Pattern.eta_contract (gen_realizes
   1.355 +      (Extraction.realizes_of thy2 vs
   1.356 +        c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
   1.357 +          (rev (Term.add_vars ([], prop_of intr)) \\ params')) intr)))))
   1.358 +            (intrs ~~ flat constrss);
   1.359 +    val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem
   1.360 +      (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
   1.361 +
   1.362 +    (** realizability predicate **)
   1.363 +
   1.364 +    val (thy3', ind_info) = thy2 |>
   1.365 +      InductivePackage.add_inductive_i false true "" false false false
   1.366 +        (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
   1.367 +          ((Sign.base_name (Thm.name_of_thm intr), strip_all
   1.368 +            (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
   1.369 +      Theory.absolute_path;
   1.370 +    val thy3 = PureThy.hide_thms false
   1.371 +      (map Thm.name_of_thm (#intrs ind_info)) thy3';
   1.372 +
   1.373 +    (** realizer for induction rule **)
   1.374 +
   1.375 +    val Ps = mapfilter (fn _ $ M $ P => if set_of M mem rsets then
   1.376 +      Some (fst (fst (dest_Var (head_of P)))) else None)
   1.377 +        (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
   1.378 +
   1.379 +    fun add_ind_realizer (thy, Ps) =
   1.380 +      let
   1.381 +        val r = indrule_realizer thy induct raw_induct rsets params'
   1.382 +          (vs @ Ps) rec_names rss intrs dummies;
   1.383 +        val rlz = strip_all (Logic.unvarify (gen_realizes
   1.384 +          (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct))));
   1.385 +        val rews = map mk_meta_eq
   1.386 +          (fst_conv :: snd_conv :: get #rec_thms dt_info);
   1.387 +        val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
   1.388 +          [if length rss = 1 then
   1.389 +             cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
   1.390 +           else EVERY [rewrite_goals_tac (rews @ all_simps),
   1.391 +             REPEAT (rtac allI 1), rtac (#induct ind_info) 1],
   1.392 +           rewrite_goals_tac rews,
   1.393 +           REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   1.394 +             [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
   1.395 +              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   1.396 +        val (thy', thm') = PureThy.store_thm ((space_implode "_"
   1.397 +          (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy
   1.398 +      in
   1.399 +        Extraction.add_realizers_i
   1.400 +          [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
   1.401 +      end;
   1.402 +
   1.403 +    (** realizer for elimination rules **)
   1.404 +
   1.405 +    val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
   1.406 +      HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
   1.407 +
   1.408 +    fun add_elim_realizer Ps ((((elim, elimR), case_thms), case_name), dummy) thy =
   1.409 +      let
   1.410 +        val (prem :: prems) = prems_of elim;
   1.411 +        val p = Logic.list_implies (prems @ [prem], concl_of elim);
   1.412 +        val T' = Extraction.etype_of thy (vs @ Ps) [] p;
   1.413 +        val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
   1.414 +        val Ts = filter_out (equal Extraction.nullT)
   1.415 +          (map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim));
   1.416 +        val r = if null Ps then Extraction.nullt
   1.417 +          else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
   1.418 +            (if dummy then
   1.419 +               [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
   1.420 +             else []) @
   1.421 +            map Bound ((length prems - 1 downto 0) @ [length prems])));
   1.422 +        val rlz = strip_all (Logic.unvarify (gen_realizes
   1.423 +          (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim))));
   1.424 +        val rews = map mk_meta_eq case_thms;
   1.425 +        val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
   1.426 +          [cut_facts_tac [hd prems] 1,
   1.427 +           etac elimR 1,
   1.428 +           ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
   1.429 +           rewrite_goals_tac rews,
   1.430 +           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
   1.431 +             DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   1.432 +        val (thy', thm') = PureThy.store_thm ((space_implode "_"
   1.433 +          (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
   1.434 +      in
   1.435 +        Extraction.add_realizers_i
   1.436 +          [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'
   1.437 +      end;
   1.438 +
   1.439 +    (** add realizers to theory **)
   1.440 +
   1.441 +    val rintr_thms = flat (map (fn (_, rs) => map (fn r => nth_elem
   1.442 +      (find_index_eq r intrs, #intrs ind_info)) rs) rss);
   1.443 +    val thy4 = foldl add_ind_realizer (thy3, subsets Ps);
   1.444 +    val thy5 = Extraction.add_realizers_i
   1.445 +      (map (mk_realizer thy4 vs params')
   1.446 +         (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
   1.447 +            map Var (rev (Term.add_vars ([], prop_of rule)) \\ params')))) 
   1.448 +              (flat (map snd rss) ~~ rintr_thms ~~ flat constrss))) thy4;
   1.449 +    val elimps = mapfilter (fn (s, _) => if s mem rsets then
   1.450 +        find_first (fn (thm, _) => s mem term_consts (hd (prems_of thm)))
   1.451 +          (elims ~~ #elims ind_info)
   1.452 +      else None) rss;
   1.453 +    val thy6 = foldl (fn (thy, p as ((((elim, _), _), _), _)) => thy |>
   1.454 +      add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
   1.455 +        (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
   1.456 +           elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
   1.457 +
   1.458 +  in Theory.add_path (NameSpace.pack (if_none path [])) thy6 end;
   1.459 +
   1.460 +fun add_ind_realizers name rsets thy =
   1.461 +  let
   1.462 +    val (_, {intrs, induct, raw_induct, elims, ...}) =
   1.463 +      (case InductivePackage.get_inductive thy name of
   1.464 +         None => error ("Unknown inductive set " ^ quote name)
   1.465 +       | Some info => info);
   1.466 +    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
   1.467 +    val vss = sort (int_ord o pairself length)
   1.468 +      (subsets (map fst (relevant_vars S)))
   1.469 +  in
   1.470 +    foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
   1.471 +  end
   1.472 +
   1.473 +fun rlz_attrib arg (thy, thm) =
   1.474 +  let
   1.475 +    fun err () = error "ind_realizer: bad rule";
   1.476 +    val sets =
   1.477 +      (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
   1.478 +           [_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
   1.479 +         | xs => map (set_of o fst o HOLogic.dest_imp) xs)
   1.480 +         handle TERM _ => err () | LIST _ => err ();
   1.481 +  in 
   1.482 +    (add_ind_realizers (hd sets) (case arg of
   1.483 +        None => sets | Some None => []
   1.484 +      | Some (Some sets') => sets \\ map (Sign.intern_const (sign_of thy)) sets')
   1.485 +      thy, thm)
   1.486 +  end;
   1.487 +
   1.488 +val rlz_attrib_global = Attrib.syntax (Scan.lift
   1.489 +  (Scan.option (Args.$$$ "irrelevant" |--
   1.490 +    Scan.option (Args.colon |-- Scan.repeat1 Args.name))) >> rlz_attrib);
   1.491 +
   1.492 +val setup = [Attrib.add_attributes [("ind_realizer",
   1.493 +  (rlz_attrib_global, K Attrib.undef_local_attribute),
   1.494 +  "add realizers for inductive set")]];
   1.495 +
   1.496 +end;