src/HOL/Tools/inductive_realizer.ML
changeset 22271 51a80e238b29
parent 21858 05f57309170c
child 22596 d0d2af4db18f
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Feb 07 17:41:11 2007 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Feb 07 17:44:07 2007 +0100
     1.3 @@ -15,51 +15,103 @@
     1.4  structure InductiveRealizer : INDUCTIVE_REALIZER =
     1.5  struct
     1.6  
     1.7 +(* FIXME: LocalTheory.note should return theorems with proper names! *)
     1.8 +fun name_of_thm thm = (case Proofterm.strip_combt (fst (Proofterm.strip_combP
     1.9 +    (Proofterm.rewrite_proof (theory_of_thm thm) ([], []) (proof_of thm)))) of
    1.10 +    (PThm (name, _, _, _), _) => name
    1.11 +  | _ => error "name_of_thm: bad proof");
    1.12 +
    1.13 +(* infer order of variables in intro rules from order of quantifiers in elim rule *)
    1.14 +fun infer_intro_vars elim arity intros =
    1.15 +  let
    1.16 +    val thy = theory_of_thm elim;
    1.17 +    val _ :: cases = prems_of elim;
    1.18 +    val used = map (fst o fst) (Term.add_vars (prop_of elim) []);
    1.19 +    fun mtch (t, u) =
    1.20 +      let
    1.21 +        val params = Logic.strip_params t;
    1.22 +        val vars = map (Var o apfst (rpair 0))
    1.23 +          (Name.variant_list used (map fst params) ~~ map snd params);
    1.24 +        val ts = map (curry subst_bounds (rev vars))
    1.25 +          (List.drop (Logic.strip_assums_hyp t, arity));
    1.26 +        val us = Logic.strip_imp_prems u;
    1.27 +        val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
    1.28 +          (Vartab.empty, Vartab.empty);
    1.29 +      in
    1.30 +        map (Envir.subst_vars tab) vars
    1.31 +      end
    1.32 +  in
    1.33 +    map (mtch o apsnd prop_of) (cases ~~ intros)
    1.34 +  end;
    1.35 +
    1.36 +(* read off arities of inductive predicates from raw induction rule *)
    1.37 +fun arities_of induct =
    1.38 +  map (fn (_ $ t $ u) =>
    1.39 +      (fst (dest_Const (head_of t)), length (snd (strip_comb u))))
    1.40 +    (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.41 +
    1.42 +(* read off parameters of inductive predicate from raw induction rule *)
    1.43 +fun params_of induct =
    1.44 +  let
    1.45 +    val (_ $ t $ u :: _) =
    1.46 +      HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
    1.47 +    val (_, ts) = strip_comb t;
    1.48 +    val (_, us) = strip_comb u
    1.49 +  in
    1.50 +    List.take (ts, length ts - length us)
    1.51 +  end;
    1.52 +
    1.53  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
    1.54  
    1.55  fun prf_of thm =
    1.56    let val {sign, prop, der = (_, prf), ...} = rep_thm thm
    1.57 -  in Reconstruct.reconstruct_proof sign prop prf end;
    1.58 +  in Reconstruct.expand_proof sign [("", NONE)] (Reconstruct.reconstruct_proof sign prop prf) end; (* FIXME *)
    1.59  
    1.60  fun forall_intr_prf (t, prf) =
    1.61    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    1.62    in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    1.63  
    1.64 +fun forall_intr_term (t, u) =
    1.65 +  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    1.66 +  in all T $ Abs (a, T, abstract_over (t, u)) end;
    1.67 +
    1.68  fun subsets [] = [[]]
    1.69    | subsets (x::xs) =
    1.70        let val ys = subsets xs
    1.71        in ys @ map (cons x) ys end;
    1.72  
    1.73 -val set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem;
    1.74 +val pred_of = fst o dest_Const o head_of;
    1.75  
    1.76 -fun strip_all t =
    1.77 -  let
    1.78 -    fun strip used (Const ("all", _) $ Abs (s, T, t)) =
    1.79 -          let val s' = Name.variant used s
    1.80 -          in strip (s'::used) (subst_bound (Free (s', T), t)) end
    1.81 -      | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
    1.82 -      | strip _ t = t;
    1.83 -  in strip (add_term_free_names (t, [])) t end;
    1.84 +fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
    1.85 +      let val (s', names') = (case names of
    1.86 +          [] => (Name.variant used s, [])
    1.87 +        | name :: names' => (name, names'))
    1.88 +      in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
    1.89 +  | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
    1.90 +      t $ strip_all' used names Q
    1.91 +  | strip_all' _ _ t = t;
    1.92 +
    1.93 +fun strip_all t = strip_all' (add_term_free_names (t, [])) [] t;
    1.94 +
    1.95 +fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
    1.96 +      (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
    1.97 +  | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
    1.98  
    1.99  fun relevant_vars prop = foldr (fn
   1.100        (Var ((a, i), T), vs) => (case strip_type T of
   1.101 -        (_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs
   1.102 +        (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
   1.103        | _ => vs)
   1.104      | (_, vs) => vs) [] (term_vars prop);
   1.105  
   1.106 -fun params_of intr = map (fst o fst o dest_Var) (term_vars
   1.107 -  (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
   1.108 -    (Logic.strip_imp_concl intr)))));
   1.109 -
   1.110 -fun dt_of_intrs thy vs intrs =
   1.111 +fun dt_of_intrs thy vs nparms intrs =
   1.112    let
   1.113      val iTs = term_tvars (prop_of (hd intrs));
   1.114      val Tvs = map TVar iTs;
   1.115 -    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
   1.116 -    val (Const (s, _), ts) = strip_comb S;
   1.117 -    val params = map dest_Var ts;
   1.118 +    val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
   1.119 +      (Logic.strip_imp_concl (prop_of (hd intrs))));
   1.120 +    val params = map dest_Var (Library.take (nparms, ts));
   1.121      val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
   1.122 -    fun constr_of_intr intr = (Sign.base_name (Thm.get_name intr),
   1.123 +    fun constr_of_intr intr = (Sign.base_name (name_of_thm intr),
   1.124        map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
   1.125          filter_out (equal Extraction.nullT) (map
   1.126            (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
   1.127 @@ -70,43 +122,40 @@
   1.128  
   1.129  fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
   1.130  
   1.131 -(** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **)
   1.132 +(** turn "P" into "%r x. realizes r (P x)" **)
   1.133  
   1.134  fun gen_rvar vs (t as Var ((a, 0), T)) =
   1.135 -      let val U = TVar (("'" ^ a, 0), HOLogic.typeS)
   1.136 -      in case try HOLogic.dest_setT T of
   1.137 -          NONE => if body_type T <> HOLogic.boolT then t else
   1.138 -            let
   1.139 -              val Ts = binder_types T;
   1.140 -              val i = length Ts;
   1.141 -              val xs = map (pair "x") Ts;
   1.142 -              val u = list_comb (t, map Bound (i - 1 downto 0))
   1.143 -            in 
   1.144 -              if a mem vs then
   1.145 -                list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
   1.146 -              else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
   1.147 -            end
   1.148 -        | SOME T' => if a mem vs then
   1.149 -              Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $
   1.150 -                (HOLogic.mk_mem (Bound 0, t))))
   1.151 -            else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $
   1.152 -              (HOLogic.mk_mem (Bound 0, t)))
   1.153 -      end
   1.154 +      if body_type T <> HOLogic.boolT then t else
   1.155 +        let
   1.156 +          val U = TVar (("'" ^ a, 0), HOLogic.typeS)
   1.157 +          val Ts = binder_types T;
   1.158 +          val i = length Ts;
   1.159 +          val xs = map (pair "x") Ts;
   1.160 +          val u = list_comb (t, map Bound (i - 1 downto 0))
   1.161 +        in 
   1.162 +          if a mem vs then
   1.163 +            list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
   1.164 +          else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
   1.165 +        end
   1.166    | gen_rvar _ t = t;
   1.167  
   1.168 -fun mk_realizes_eqn n vs intrs =
   1.169 +fun mk_realizes_eqn n vs nparms intrs =
   1.170    let
   1.171 -    val iTs = term_tvars (prop_of (hd intrs));
   1.172 +    val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
   1.173 +    val iTs = term_tvars concl;
   1.174      val Tvs = map TVar iTs;
   1.175 -    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
   1.176 -    val (Const (s, T), ts') = strip_comb S;
   1.177 -    val setT = body_type T;
   1.178 -    val elT = HOLogic.dest_setT setT;
   1.179 -    val x = Var (("x", 0), elT);
   1.180 +    val (h as Const (s, T), us) = strip_comb concl;
   1.181 +    val params = List.take (us, nparms);
   1.182 +    val elTs = List.drop (binder_types T, nparms);
   1.183 +    val predT = elTs ---> HOLogic.boolT;
   1.184 +    val used = map (fst o fst o dest_Var) params;
   1.185 +    val xs = map (Var o apfst (rpair 0))
   1.186 +      (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
   1.187      val rT = if n then Extraction.nullT
   1.188        else Type (space_implode "_" (s ^ "T" :: vs),
   1.189          map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
   1.190      val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
   1.191 +    val S = list_comb (h, params @ xs);
   1.192      val rvs = relevant_vars S;
   1.193      val vs' = map fst rvs \\ vs;
   1.194      val rname = space_implode "_" (s ^ "R" :: vs);
   1.195 @@ -119,23 +168,20 @@
   1.196        end;
   1.197  
   1.198      val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
   1.199 -    val ts = map (gen_rvar vs) ts';
   1.200 +    val ts = map (gen_rvar vs) params;
   1.201      val argTs = map fastype_of ts;
   1.202  
   1.203 -  in ((prems, (Const ("typeof", setT --> Type ("Type", [])) $ S,
   1.204 +  in ((prems, (Const ("typeof", HOLogic.boolT --> Type ("Type", [])) $ S,
   1.205         Extraction.mk_typ rT)),
   1.206 -    (prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S),
   1.207 -       if n then
   1.208 -         HOLogic.mk_mem (x, list_comb (Const (rname, argTs ---> setT), ts))
   1.209 -       else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname,
   1.210 -         argTs ---> HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts)))))
   1.211 +    (prems, (mk_rlz rT $ r $ S,
   1.212 +       if n then list_comb (Const (rname, argTs ---> predT), ts @ xs)
   1.213 +       else list_comb (Const (rname, argTs @ [rT] ---> predT), ts @ [r] @ xs))))
   1.214    end;
   1.215  
   1.216 -fun fun_of_prem thy rsets vs params rule intr =
   1.217 +fun fun_of_prem thy rsets vs params rule ivs intr =
   1.218    let
   1.219 -    (* add_term_vars and Term.add_vars may return variables in different order *)
   1.220 -    val args = map (Free o apfst fst o dest_Var)
   1.221 -      (add_term_vars (prop_of intr, []) \\ map Var params);
   1.222 +    val ctxt = ProofContext.init thy
   1.223 +    val args = map (Free o apfst fst o dest_Var) ivs;
   1.224      val args' = map (Free o apfst fst)
   1.225        (Term.add_vars (prop_of intr) [] \\ params);
   1.226      val rule' = strip_all rule;
   1.227 @@ -146,7 +192,9 @@
   1.228  
   1.229      fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
   1.230        | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
   1.231 -      | is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true
   1.232 +      | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
   1.233 +          Const (s, _) => can (InductivePackage.the_inductive ctxt) s
   1.234 +        | _ => true)
   1.235        | is_meta _ = false;
   1.236  
   1.237      fun fun_of ts rts args used (prem :: prems) =
   1.238 @@ -189,50 +237,42 @@
   1.239            in if conclT = Extraction.nullT
   1.240              then list_abs_free (map dest_Free xs, HOLogic.unit)
   1.241              else list_abs_free (map dest_Free xs, list_comb
   1.242 -              (Free ("r" ^ Sign.base_name (Thm.get_name intr),
   1.243 +              (Free ("r" ^ Sign.base_name (name_of_thm intr),
   1.244                  map fastype_of (rev args) ---> conclT), rev args))
   1.245            end
   1.246  
   1.247    in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
   1.248  
   1.249 -fun find_first f = Library.find_first f;
   1.250 -
   1.251  fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
   1.252    let
   1.253      val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
   1.254      val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
   1.255 -      SOME (map (fn r => List.nth (prems_of raw_induct,
   1.256 +      SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
   1.257          find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
   1.258 -    val concls' = List.mapPartial (fn (s, _) => if s mem rsets then
   1.259 -        find_first (fn concl => s mem term_consts concl) concls
   1.260 -      else NONE) rss;
   1.261 -    val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
   1.262 +    val fs = maps (fn ((intrs, prems), dummy) =>
   1.263        let
   1.264 -        val (intrs1, intrs2) = chop (length prems) intrs;
   1.265 -        val fs = map (fn (rule, intr) =>
   1.266 -          fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
   1.267 -      in (intrs2, if dummy then Const ("arbitrary",
   1.268 +        val fs = map (fn (rule, (ivs, intr)) =>
   1.269 +          fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
   1.270 +      in if dummy then Const ("arbitrary",
   1.271            HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
   1.272 -        else fs)
   1.273 -      end) (intrs, (premss ~~ dummies))));
   1.274 +        else fs
   1.275 +      end) (premss ~~ dummies);
   1.276      val frees = fold Term.add_frees fs [];
   1.277      val Ts = map fastype_of fs;
   1.278 -    val rlzs = List.mapPartial (fn (a, concl) =>
   1.279 +    fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr)
   1.280 +  in
   1.281 +    fst (fold_map (fn concl => fn names =>
   1.282        let val T = Extraction.etype_of thy vs [] concl
   1.283 -      in if T = Extraction.nullT then NONE
   1.284 -        else SOME (list_comb (Const (a, Ts ---> T), fs))
   1.285 -      end) (rec_names ~~ concls')
   1.286 -  in if null rlzs then Extraction.nullt else
   1.287 -    let
   1.288 -      val r = foldr1 HOLogic.mk_prod rlzs;
   1.289 -      val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
   1.290 -      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.get_name intr);
   1.291 -      val r' = list_abs_free (List.mapPartial (fn intr =>
   1.292 -        Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
   1.293 -          if length concls = 1 then r $ x else r)
   1.294 -    in
   1.295 -      if length concls = 1 then lambda x r' else r'
   1.296 -    end
   1.297 +      in if T = Extraction.nullT then (Extraction.nullt, names) else
   1.298 +        let
   1.299 +          val Type ("fun", [U, _]) = T;
   1.300 +          val a :: names' = names
   1.301 +        in (list_abs_free (("x", U) :: List.mapPartial (fn intr =>
   1.302 +          Option.map (pair (name_of_fn intr))
   1.303 +            (AList.lookup (op =) frees (name_of_fn intr))) intrs,
   1.304 +          list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
   1.305 +        end
   1.306 +      end) concls rec_names)
   1.307    end;
   1.308  
   1.309  fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
   1.310 @@ -254,48 +294,47 @@
   1.311          |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
   1.312        end;
   1.313  
   1.314 -fun mk_realizer thy vs params ((rule, rrule), rt) =
   1.315 +fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
   1.316    let
   1.317 -    val prems = prems_of rule ~~ prems_of rrule;
   1.318      val rvs = map fst (relevant_vars (prop_of rule));
   1.319      val xs = rev (Term.add_vars (prop_of rule) []);
   1.320      val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
   1.321      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
   1.322      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
   1.323 -    val rs = subtract (op = o pairself fst) xs rlzvs;
   1.324 -
   1.325 -    fun mk_prf _ [] prf = prf
   1.326 -      | mk_prf rs ((prem, rprem) :: prems) prf =
   1.327 -          if Extraction.etype_of thy vs [] prem = Extraction.nullT
   1.328 -          then AbsP ("H", SOME rprem, mk_prf rs prems prf)
   1.329 -          else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem,
   1.330 -            mk_prf (tl rs) prems prf));
   1.331 -
   1.332 -  in (Thm.get_name rule, (vs,
   1.333 +    val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
   1.334 +    val rlz' = foldr forall_intr_term (prop_of rrule) (vs2 @ rs);
   1.335 +    val rlz'' = foldr forall_intr_term rlz vs2
   1.336 +  in (name, (vs,
   1.337      if rt = Extraction.nullt then rt else
   1.338        foldr (uncurry lambda) rt vs1,
   1.339 -    foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
   1.340 -      (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
   1.341 +    ProofRewriteRules.un_hhf_proof rlz' rlz''
   1.342 +      (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
   1.343    end;
   1.344  
   1.345 -fun add_rule r rss =
   1.346 +fun partition_rules induct intrs =
   1.347    let
   1.348 -    val _ $ (_ $ _ $ S) = concl_of r;
   1.349 -    val (Const (s, _), _) = strip_comb S;
   1.350 +    fun name_of t = fst (dest_Const (head_of t));
   1.351 +    val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
   1.352 +    val sets = map (name_of o fst o HOLogic.dest_imp) ts;
   1.353    in
   1.354 -    rss
   1.355 -    |> AList.default (op =) (s, [])
   1.356 -    |> AList.map_entry (op =) s (fn rs => rs @ [r])
   1.357 +    map (fn s => (s, filter
   1.358 +      (equal s o name_of o HOLogic.dest_Trueprop o concl_of) intrs)) sets
   1.359    end;
   1.360  
   1.361  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   1.362    let
   1.363 +    val qualifier = NameSpace.qualifier (name_of_thm induct);
   1.364 +    val inducts = PureThy.get_thms thy (Name
   1.365 +      (NameSpace.qualified qualifier "inducts"));
   1.366      val iTs = term_tvars (prop_of (hd intrs));
   1.367      val ar = length vs + length iTs;
   1.368 -    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
   1.369 -    val (_, params) = strip_comb S;
   1.370 +    val params = params_of raw_induct;
   1.371 +    val arities = arities_of raw_induct;
   1.372 +    val nparms = length params;
   1.373      val params' = map dest_Var params;
   1.374 -    val rss = [] |> fold add_rule intrs;
   1.375 +    val rss = partition_rules raw_induct intrs;
   1.376 +    val rss' = map (fn (((s, rs), (_, arity)), elim) =>
   1.377 +      (s, (infer_intro_vars elim arity rs ~~ rs))) (rss ~~ arities ~~ elims);
   1.378      val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
   1.379      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
   1.380  
   1.381 @@ -303,7 +342,7 @@
   1.382        Theory.root_path |>
   1.383        Theory.add_path (NameSpace.implode prfx);
   1.384      val (ty_eqs, rlz_eqs) = split_list
   1.385 -      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
   1.386 +      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
   1.387  
   1.388      val thy1' = thy1 |>
   1.389        Theory.copy |>
   1.390 @@ -312,7 +351,7 @@
   1.391          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   1.392          Extraction.add_typeof_eqns_i ty_eqs;
   1.393      val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
   1.394 -      SOME (dt_of_intrs thy1' vs rs) else NONE) rss;
   1.395 +      SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
   1.396  
   1.397      (** datatype representing computational content of inductive set **)
   1.398  
   1.399 @@ -338,51 +377,89 @@
   1.400          ((get #rec_thms dt_info, dummies), rss);
   1.401      val rintrs = map (fn (intr, c) => Envir.eta_contract
   1.402        (Extraction.realizes_of thy2 vs
   1.403 -        c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
   1.404 -          (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
   1.405 -            (intrs ~~ List.concat constrss);
   1.406 -    val rlzsets = distinct (op =) (map (fn rintr => snd (HOLogic.dest_mem
   1.407 -      (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
   1.408 +        (if c = Extraction.nullt then c else list_comb (c, map Var (rev
   1.409 +          (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
   1.410 +            (maps snd rss ~~ List.concat constrss);
   1.411 +    val (rlzpreds, rlzpreds') = split_list
   1.412 +      (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
   1.413 +        let
   1.414 +          val Const (s, T) = head_of (HOLogic.dest_Trueprop
   1.415 +            (Logic.strip_assums_concl rintr));
   1.416 +          val s' = Sign.base_name s;
   1.417 +          val T' = Logic.unvarifyT T
   1.418 +        in ((s', SOME T', NoSyn),
   1.419 +          (Const (s, T'), Free (s', T')))
   1.420 +        end) rintrs));
   1.421 +    val rlzparams = map (fn Var ((s, _), T) => (s, SOME (Logic.unvarifyT T)))
   1.422 +      (List.take (snd (strip_comb
   1.423 +        (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
   1.424  
   1.425      (** realizability predicate **)
   1.426  
   1.427 -    val (thy3', ind_info) = thy2 |>
   1.428 -      OldInductivePackage.add_inductive_i false true "" false false false
   1.429 -        (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
   1.430 -          ((Sign.base_name (Thm.get_name intr), strip_all
   1.431 -            (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
   1.432 +    val (ind_info, thy3') = thy2 |>
   1.433 +      TheoryTarget.init NONE |>
   1.434 +      InductivePackage.add_inductive_i false "" false false false
   1.435 +        rlzpreds rlzparams (map (fn (rintr, intr) =>
   1.436 +          ((Sign.base_name (name_of_thm intr), []),
   1.437 +           subst_atomic rlzpreds' (Logic.unvarify rintr)))
   1.438 +             (rintrs ~~ maps snd rss)) [] ||>
   1.439 +      ProofContext.theory_of o LocalTheory.exit ||>
   1.440        Theory.absolute_path;
   1.441      val thy3 = PureThy.hide_thms false
   1.442 -      (map Thm.get_name (#intrs ind_info)) thy3';
   1.443 +      (map name_of_thm (#intrs ind_info)) thy3';
   1.444  
   1.445      (** realizer for induction rule **)
   1.446  
   1.447 -    val Ps = List.mapPartial (fn _ $ M $ P => if set_of M mem rsets then
   1.448 +    val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
   1.449        SOME (fst (fst (dest_Var (head_of P)))) else NONE)
   1.450          (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
   1.451  
   1.452      fun add_ind_realizer (thy, Ps) =
   1.453        let
   1.454 -        val r = indrule_realizer thy induct raw_induct rsets params'
   1.455 -          (vs @ Ps) rec_names rss intrs dummies;
   1.456 -        val rlz = strip_all (Logic.unvarify
   1.457 -          (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
   1.458 +        val rs = indrule_realizer thy induct raw_induct rsets params'
   1.459 +          (vs @ Ps) rec_names rss' intrs dummies;
   1.460 +        val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs @ Ps) r
   1.461 +          (prop_of ind)) (rs ~~ inducts);
   1.462 +        val used = foldr add_term_free_names [] rlzs;
   1.463 +        val rnames = Name.variant_list used (replicate (length inducts) "r");
   1.464 +        val rnames' = Name.variant_list
   1.465 +          (used @ rnames) (replicate (length intrs) "s");
   1.466 +        val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
   1.467 +          let
   1.468 +            val (P, Q) = strip_one name (Logic.unvarify rlz);
   1.469 +            val Q' = strip_all' [] rnames' Q
   1.470 +          in
   1.471 +            (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
   1.472 +          end) (rlzs ~~ rnames);
   1.473 +        val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
   1.474 +          (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
   1.475          val rews = map mk_meta_eq
   1.476            (fst_conv :: snd_conv :: get #rec_thms dt_info);
   1.477 -        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
   1.478 -          [if length rss = 1 then
   1.479 -             cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
   1.480 -           else EVERY [rewrite_goals_tac (rews @ all_simps),
   1.481 -             REPEAT (rtac allI 1), rtac (#induct ind_info) 1],
   1.482 +        val thm = Goal.prove_global thy [] prems concl (fn prems => EVERY
   1.483 +          [rtac (#raw_induct ind_info) 1,
   1.484             rewrite_goals_tac rews,
   1.485             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   1.486               [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
   1.487                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   1.488          val (thm', thy') = PureThy.store_thm ((space_implode "_"
   1.489 -          (Thm.get_name induct :: vs @ Ps @ ["correctness"]), thm), []) thy
   1.490 +          (NameSpace.qualified qualifier "induct" :: vs @ Ps @
   1.491 +             ["correctness"]), thm), []) thy;
   1.492 +        val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
   1.493 +          (DatatypeAux.split_conj_thm thm');
   1.494 +        val ([thms'], thy'') = PureThy.add_thmss
   1.495 +          [((space_implode "_"
   1.496 +             (NameSpace.qualified qualifier "inducts" :: vs @ Ps @
   1.497 +               ["correctness"]), thms), [])] thy';
   1.498 +        val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
   1.499        in
   1.500          Extraction.add_realizers_i
   1.501 -          [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
   1.502 +          (map (fn (((ind, corr), rlz), r) =>
   1.503 +              mk_realizer thy' (vs @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
   1.504 +            realizers @ (case realizers of
   1.505 +             [(((ind, corr), rlz), r)] =>
   1.506 +               [mk_realizer thy' (vs @ Ps) (NameSpace.qualified qualifier "induct",
   1.507 +                  ind, corr, rlz, r)]
   1.508 +           | _ => [])) thy''
   1.509        end;
   1.510  
   1.511      (** realizer for elimination rules **)
   1.512 @@ -394,15 +471,13 @@
   1.513        (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
   1.514        let
   1.515          val (prem :: prems) = prems_of elim;
   1.516 -        fun reorder1 (p, intr) =
   1.517 +        fun reorder1 (p, (_, intr)) =
   1.518            Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
   1.519              (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
   1.520 -        fun reorder2 (intr, i) =
   1.521 -          let
   1.522 -            val fs1 = term_vars (prop_of intr) \\ params;
   1.523 -            val fs2 = Term.add_vars (prop_of intr) [] \\ params'
   1.524 +        fun reorder2 ((ivs, intr), i) =
   1.525 +          let val fs = Term.add_vars (prop_of intr) [] \\ params'
   1.526            in Library.foldl (fn (t, x) => lambda (Var x) t)
   1.527 -            (list_comb (Bound (i + length fs1), fs1), fs2)
   1.528 +            (list_comb (Bound (i + length ivs), ivs), fs)
   1.529            end;
   1.530          val p = Logic.list_implies
   1.531            (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
   1.532 @@ -416,37 +491,36 @@
   1.533               else []) @
   1.534              map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   1.535              [Bound (length prems)]));
   1.536 -        val rlz = strip_all (Logic.unvarify
   1.537 -          (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
   1.538 +        val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
   1.539 +        val rlz' = strip_all (Logic.unvarify rlz);
   1.540          val rews = map mk_meta_eq case_thms;
   1.541 -        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
   1.542 +        val thm = Goal.prove_global thy []
   1.543 +          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn prems => EVERY
   1.544            [cut_facts_tac [hd prems] 1,
   1.545             etac elimR 1,
   1.546 -           ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
   1.547 +           ALLGOALS (asm_simp_tac HOL_basic_ss),
   1.548             rewrite_goals_tac rews,
   1.549             REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
   1.550               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   1.551          val (thm', thy') = PureThy.store_thm ((space_implode "_"
   1.552 -          (Thm.get_name elim :: vs @ Ps @ ["correctness"]), thm), []) thy
   1.553 +          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
   1.554        in
   1.555          Extraction.add_realizers_i
   1.556 -          [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'
   1.557 +          [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
   1.558        end;
   1.559  
   1.560      (** add realizers to theory **)
   1.561  
   1.562 -    val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth
   1.563 -      (#intrs ind_info, find_index (fn th => eq_thm (th, r)) intrs)) rs) rss);
   1.564      val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
   1.565      val thy5 = Extraction.add_realizers_i
   1.566 -      (map (mk_realizer thy4 vs params')
   1.567 -         (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
   1.568 -            map Var (rev (Term.add_vars (prop_of rule) []) \\ params')))) 
   1.569 -              (List.concat (map snd rss) ~~ rintr_thms ~~ List.concat constrss))) thy4;
   1.570 -    val elimps = List.mapPartial (fn (s, intrs) => if s mem rsets then
   1.571 -        Option.map (rpair intrs) (find_first (fn (thm, _) =>
   1.572 -          s mem term_consts (hd (prems_of thm))) (elims ~~ #elims ind_info))
   1.573 -      else NONE) rss;
   1.574 +      (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
   1.575 +         (name_of_thm rule, rule, rrule, rlz,
   1.576 +            list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
   1.577 +              (List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~
   1.578 +                 List.concat constrss))) thy4;
   1.579 +    val elimps = List.mapPartial (fn ((s, intrs), p) =>
   1.580 +      if s mem rsets then SOME (p, intrs) else NONE)
   1.581 +        (rss' ~~ (elims ~~ #elims ind_info));
   1.582      val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
   1.583        add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
   1.584          (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
   1.585 @@ -457,12 +531,9 @@
   1.586  fun add_ind_realizers name rsets thy =
   1.587    let
   1.588      val (_, {intrs, induct, raw_induct, elims, ...}) =
   1.589 -      (case OldInductivePackage.get_inductive thy name of
   1.590 -         NONE => error ("Unknown inductive set " ^ quote name)
   1.591 -       | SOME info => info);
   1.592 -    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
   1.593 +      InductivePackage.the_inductive (ProofContext.init thy) name;
   1.594      val vss = sort (int_ord o pairself length)
   1.595 -      (subsets (map fst (relevant_vars S)))
   1.596 +      (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
   1.597    in
   1.598      Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
   1.599    end
   1.600 @@ -472,8 +543,8 @@
   1.601      fun err () = error "ind_realizer: bad rule";
   1.602      val sets =
   1.603        (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
   1.604 -           [_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
   1.605 -         | xs => map (set_of o fst o HOLogic.dest_imp) xs)
   1.606 +           [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
   1.607 +         | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
   1.608           handle TERM _ => err () | Empty => err ();
   1.609    in 
   1.610      add_ind_realizers (hd sets)