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.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.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.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.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.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.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.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.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.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.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.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.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.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