src/Pure/Proof/extraction.ML
changeset 13732 f8badfef5cf2
parent 13719 44fed7d0c305
child 13793 c02c81fd11b8
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Nov 27 17:22:18 2002 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Nov 27 17:23:19 2002 +0100
     1.3 @@ -18,7 +18,9 @@
     1.4    val add_realizers : (thm * (string list * string * string)) list
     1.5      -> theory -> theory
     1.6    val add_expand_thms : thm list -> theory -> theory
     1.7 -  val extract : thm list -> theory -> theory
     1.8 +  val add_types : (xstring * ((term -> term option) list *
     1.9 +    (term -> typ -> term -> typ -> term) option)) list -> theory -> theory
    1.10 +  val extract : (thm * string list) list -> theory -> theory
    1.11    val nullT : typ
    1.12    val nullt : term
    1.13    val mk_typ : typ -> term
    1.14 @@ -63,13 +65,14 @@
    1.15          | _ => nullT))
    1.16    | typeof_proc _ _ _ = None;
    1.17  
    1.18 -fun rlz_proc (Const ("realizes", Type (_, [Type ("Null", []), _])) $ _ $ t) =
    1.19 -  (case strip_comb t of (Const _, _) => Some t | _ => None)
    1.20 +fun rlz_proc (Const ("realizes", Type (_, [Type ("Null", []), _])) $ r $ t) = Some t
    1.21 +  | rlz_proc (Const ("realizes", Type (_, [T, _])) $ r $ t) =
    1.22 +      (case strip_comb t of
    1.23 +         (Var (ixn, U), ts) => Some (list_comb (Var (ixn, T --> U), r :: ts))
    1.24 +       | (Free (s, U), ts) => Some (list_comb (Free (s, T --> U), r :: ts))
    1.25 +       | _ => None)
    1.26    | rlz_proc _ = None;
    1.27  
    1.28 -fun rlz_proc' (Const ("realizes", _) $ _ $ t) = Some t
    1.29 -  | rlz_proc' _ = None;
    1.30 -
    1.31  val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
    1.32    take_prefix (not o equal ":") o explode;
    1.33  
    1.34 @@ -116,6 +119,11 @@
    1.35  
    1.36  fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);
    1.37  
    1.38 +fun corr_name s vs =
    1.39 +  add_prefix "extr" (space_implode "_" (s :: vs)) ^ "_correctness";
    1.40 +
    1.41 +fun extr_name s vs = add_prefix "extr" (space_implode "_" (s :: vs));
    1.42 +
    1.43  fun msg d s = priority (implode (replicate d " ") ^ s);
    1.44  
    1.45  fun vars_of t = rev (foldl_aterms
    1.46 @@ -133,21 +141,36 @@
    1.47  
    1.48  val mkabs = foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
    1.49  
    1.50 +fun strip_abs 0 t = t
    1.51 +  | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
    1.52 +  | strip_abs _ _ = error "strip_abs: not an abstraction";
    1.53 +
    1.54  fun prf_subst_TVars tye =
    1.55    map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
    1.56  
    1.57 -fun add_types (Const ("typeof", Type (_, [T, _])), xs) =
    1.58 -      (case strip_type T of (_, Type (s, _)) => s ins xs | _ => xs)
    1.59 -  | add_types (t $ u, xs) = add_types (t, add_types (u, xs))
    1.60 -  | add_types (Abs (_, _, t), xs) = add_types (t, xs)
    1.61 -  | add_types (_, xs) = xs;
    1.62 -
    1.63  fun relevant_vars types prop = foldr (fn
    1.64        (Var ((a, i), T), vs) => (case strip_type T of
    1.65          (_, Type (s, _)) => if s mem types then a :: vs else vs
    1.66        | _ => vs)
    1.67      | (_, vs) => vs) (vars_of prop, []);
    1.68  
    1.69 +fun tname_of (Type (s, _)) = s
    1.70 +  | tname_of _ = "";
    1.71 +
    1.72 +fun get_var_type t =
    1.73 +  let
    1.74 +    val vs = Term.add_vars ([], t);
    1.75 +    val fs = Term.add_frees ([], t)
    1.76 +  in fn 
    1.77 +      Var (ixn, _) => (case assoc (Term.add_vars ([], t), ixn) of
    1.78 +          None => error "get_var_type: no such variable in term"
    1.79 +        | Some T => Var (ixn, T))
    1.80 +    | Free (s, _) => (case assoc (Term.add_frees ([], t), s) of
    1.81 +          None => error "get_var_type: no such variable in term"
    1.82 +        | Some T => Free (s, T))
    1.83 +    | _ => error "get_var_type: not a variable"
    1.84 +  end;
    1.85 +
    1.86  
    1.87  (**** theory data ****)
    1.88  
    1.89 @@ -159,7 +182,8 @@
    1.90    type T =
    1.91      {realizes_eqns : rules,
    1.92       typeof_eqns : rules,
    1.93 -     types : string list,
    1.94 +     types : (string * ((term -> term option) list *
    1.95 +       (term -> typ -> term -> typ -> term) option)) list,
    1.96       realizers : (string list * (term * proof)) list Symtab.table,
    1.97       defs : thm list,
    1.98       expand : (string * term) list,
    1.99 @@ -183,7 +207,7 @@
   1.100         realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
   1.101      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
   1.102       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
   1.103 -     types = types1 union types2,
   1.104 +     types = merge_alists types1 types2,
   1.105       realizers = Symtab.merge_multi' (eq_set o pairself #1)
   1.106         (realizers1, realizers2),
   1.107       defs = gen_merge_lists eq_thm defs1 defs2,
   1.108 @@ -236,15 +260,12 @@
   1.109    let
   1.110      val {realizes_eqns, typeof_eqns, types, realizers,
   1.111        defs, expand, prep} = ExtractionData.get thy;
   1.112 -    val eqns' = map (prep_eq thy) eqns;
   1.113 -    val ts = flat (flat
   1.114 -      (map (fn (ps, p) => map (fn (x, y) => [x, y]) (p :: ps)) eqns'))
   1.115 +    val eqns' = map (prep_eq thy) eqns
   1.116    in
   1.117      ExtractionData.put
   1.118        {realizes_eqns = realizes_eqns, realizers = realizers,
   1.119         typeof_eqns = foldr add_rule (eqns', typeof_eqns),
   1.120 -       types = foldr add_types (ts, types),
   1.121 -       defs = defs, expand = expand, prep = prep} thy
   1.122 +       types = types, defs = defs, expand = expand, prep = prep} thy
   1.123    end
   1.124  
   1.125  val add_typeof_eqns_i = gen_add_typeof_eqns (K I);
   1.126 @@ -266,10 +287,9 @@
   1.127    let
   1.128      val {typeof_eqns, ...} = ExtractionData.get_sg sg;
   1.129      fun err () = error ("Unable to determine type of extracted program for\n" ^
   1.130 -      Sign.string_of_term sg t);
   1.131 -    val abs = foldr (fn (T, u) => Abs ("x", T, u))
   1.132 +      Sign.string_of_term sg t)
   1.133    in case strip_abs_body (freeze_thaw (condrew sg (#net typeof_eqns)
   1.134 -    [typeof_proc (Sign.defaultS sg) vs]) (abs (Ts,
   1.135 +    [typeof_proc (Sign.defaultS sg) vs]) (list_abs (map (pair "x") (rev Ts),
   1.136        Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
   1.137        Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
   1.138      | _ => err ()
   1.139 @@ -290,8 +310,10 @@
   1.140  
   1.141  fun prep_realizer thy =
   1.142    let
   1.143 -    val {realizes_eqns, typeof_eqns, defs, ...} =
   1.144 +    val {realizes_eqns, typeof_eqns, defs, types, ...} =
   1.145        ExtractionData.get thy;
   1.146 +    val procs = flat (map (fst o snd) types);
   1.147 +    val rtypes = map fst types;
   1.148      val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
   1.149      val thy' = add_syntax thy;
   1.150      val sign = sign_of thy';
   1.151 @@ -304,14 +326,17 @@
   1.152        val prop = Pattern.rewrite_term tsg
   1.153          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
   1.154        val vars = vars_of prop;
   1.155 +      val vars' = filter_out (fn v =>
   1.156 +        tname_of (body_type (fastype_of v)) mem rtypes) vars;
   1.157        val T = etype_of sign vs [] prop;
   1.158        val (T', thw) = Type.freeze_thaw_type
   1.159 -        (if T = nullT then nullT else map fastype_of vars ---> T);
   1.160 +        (if T = nullT then nullT else map fastype_of vars' ---> T);
   1.161        val t = map_term_types thw (term_of (read_cterm sign (s1, T')));
   1.162 -      val r = foldr forall_intr (vars, freeze_thaw
   1.163 -        (condrew sign eqns [typeof_proc (Sign.defaultS sign) vs, rlz_proc])
   1.164 +      val r' = freeze_thaw (condrew sign eqns
   1.165 +        (procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
   1.166            (Const ("realizes", T --> propT --> propT) $
   1.167 -            (if T = nullT then t else list_comb (t, vars)) $ prop));
   1.168 +            (if T = nullT then t else list_comb (t, vars')) $ prop);
   1.169 +      val r = foldr forall_intr (map (get_var_type r') vars, r');
   1.170        val prf = Reconstruct.reconstruct_proof sign r (rd s2);
   1.171      in (name, (vs, (t, prf))) end
   1.172    end;
   1.173 @@ -324,13 +349,14 @@
   1.174    let
   1.175      val thy' = add_syntax thy;
   1.176      val sign = sign_of thy';
   1.177 -    val {realizes_eqns, typeof_eqns, defs, ...} =
   1.178 +    val {realizes_eqns, typeof_eqns, defs, types, ...} =
   1.179        ExtractionData.get thy';
   1.180 +    val procs = flat (map (fst o snd) types);
   1.181      val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
   1.182      val prop' = Pattern.rewrite_term (Sign.tsig_of sign)
   1.183        (map (Logic.dest_equals o prop_of) defs) [] prop;
   1.184 -  in freeze_thaw
   1.185 -    (condrew sign eqns [typeof_proc (Sign.defaultS sign) vs, rlz_proc])
   1.186 +  in freeze_thaw (condrew sign eqns
   1.187 +    (procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
   1.188        (Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
   1.189    end;
   1.190  
   1.191 @@ -370,6 +396,18 @@
   1.192  
   1.193  fun add_expand_thms thms thy = foldl (fst o add_expand_thm) (thy, thms);
   1.194  
   1.195 +(** types with computational content **)
   1.196 +
   1.197 +fun add_types tys thy =
   1.198 +  let val {realizes_eqns, typeof_eqns, types, realizers,
   1.199 +    defs, expand, prep} = ExtractionData.get thy;
   1.200 +  in
   1.201 +    ExtractionData.put
   1.202 +      {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns,
   1.203 +       types = map (apfst (Sign.intern_tycon (sign_of thy))) tys @ types,
   1.204 +       realizers = realizers, defs = defs, expand = expand, prep = prep} thy
   1.205 +  end;
   1.206 +
   1.207  
   1.208  (**** extract program ****)
   1.209  
   1.210 @@ -381,6 +419,8 @@
   1.211      val tsg = Sign.tsig_of sg;
   1.212      val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
   1.213        ExtractionData.get thy;
   1.214 +    val procs = flat (map (fst o snd) types);
   1.215 +    val rtypes = map fst types;
   1.216      val typroc = typeof_proc (Sign.defaultS sg);
   1.217      val prep = if_none prep (K I) sg o ProofRewriteRules.elim_defs sg false defs o
   1.218        Reconstruct.expand_proof sg (("", None) :: map (apsnd Some) expand);
   1.219 @@ -388,7 +428,7 @@
   1.220  
   1.221      fun find_inst prop Ts ts vs =
   1.222        let
   1.223 -        val rvs = relevant_vars types prop;
   1.224 +        val rvs = relevant_vars rtypes prop;
   1.225          val vars = vars_of prop;
   1.226          val n = Int.min (length vars, length ts);
   1.227  
   1.228 @@ -405,9 +445,12 @@
   1.229      fun find vs = apsome snd o find_first (curry eq_set vs o fst);
   1.230      fun find' s = map snd o filter (equal s o fst)
   1.231  
   1.232 -    fun realizes_null vs prop =
   1.233 -      freeze_thaw (condrew sg rrews [typroc vs, rlz_proc])
   1.234 -        (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
   1.235 +    fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
   1.236 +      (condrew sg rrews (procs @ [typroc vs, rlz_proc])) (list_abs
   1.237 +        (map (pair "x") (rev Ts), t)));
   1.238 +
   1.239 +    fun realizes_null vs prop = app_rlz_rews [] vs
   1.240 +      (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
   1.241  
   1.242      fun corr d defs vs ts Ts hs (PBound i) _ _ = (defs, PBound i)
   1.243  
   1.244 @@ -427,16 +470,32 @@
   1.245                (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
   1.246              val rlz = Const ("realizes", T --> propT --> propT)
   1.247            in (defs',
   1.248 -            if T = nullT then AbsP ("R", Some (rlz $ nullt $ prop),
   1.249 -              prf_subst_bounds [nullt] corr_prf)
   1.250 +            if T = nullT then AbsP ("R",
   1.251 +              Some (app_rlz_rews Ts vs (rlz $ nullt $ prop)),
   1.252 +                prf_subst_bounds [nullt] corr_prf)
   1.253              else Abst (s, Some T, AbsP ("R",
   1.254 -              Some (rlz $ Bound 0 $ incr_boundvars 1 prop), corr_prf)))
   1.255 +              Some (app_rlz_rews (T :: Ts) vs
   1.256 +                (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
   1.257            end
   1.258  
   1.259        | corr d defs vs ts Ts hs (prf % Some t) (prf' % _) t' =
   1.260 -          let val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
   1.261 -            (case t' of Some (u $ _) => Some u | _ => None)
   1.262 -          in (defs', corr_prf % Some t) end
   1.263 +          let
   1.264 +            val (Us, T) = strip_type (fastype_of1 (Ts, t));
   1.265 +            val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
   1.266 +              (if tname_of T mem rtypes then t'
   1.267 +               else (case t' of Some (u $ _) => Some u | _ => None));
   1.268 +            val u = if not (tname_of T mem rtypes) then t else
   1.269 +              let
   1.270 +                val eT = etype_of sg vs Ts t;
   1.271 +                val (r, Us') = if eT = nullT then (nullt, Us) else
   1.272 +                  (Bound (length Us), eT :: Us);
   1.273 +                val u = list_comb (incr_boundvars (length Us') t,
   1.274 +                  map Bound (length Us - 1 downto 0));
   1.275 +                val u' = (case assoc (types, tname_of T) of
   1.276 +                    Some ((_, Some f)) => f r eT u T
   1.277 +                  | _ => Const ("realizes", eT --> T --> T) $ r $ u)
   1.278 +              in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
   1.279 +          in (defs', corr_prf % Some u) end
   1.280  
   1.281        | corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t =
   1.282            let
   1.283 @@ -475,13 +534,16 @@
   1.284                      val prf' = prep (Reconstruct.reconstruct_proof sg prop prf);
   1.285                      val (defs'', corr_prf) =
   1.286                        corr (d + 1) defs' vs' [] [] [] prf' prf' None;
   1.287 -                    val args = vfs_of prop;
   1.288 -                    val corr_prf' = foldr forall_intr_prf (args, corr_prf);
   1.289 +                    val corr_prop = Reconstruct.prop_of corr_prf;
   1.290 +                    val corr_prf' = foldr forall_intr_prf
   1.291 +                      (map (get_var_type corr_prop) (vfs_of prop), proof_combt
   1.292 +                         (PThm ((corr_name name vs, []), corr_prf, corr_prop,
   1.293 +                             Some (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
   1.294                    in
   1.295 -                    ((name, (vs', ((nullt, nullt), corr_prf'))) :: defs'',
   1.296 +                    ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
   1.297                       prf_subst_TVars tye' corr_prf')
   1.298                    end
   1.299 -              | Some (_, prf') => (defs', prf_subst_TVars tye' prf'))
   1.300 +              | Some (_, (_, prf')) => (defs', prf_subst_TVars tye' prf'))
   1.301              | Some rs => (case find vs' rs of
   1.302                  Some (_, prf') => (defs', prf_subst_TVars tye' prf')
   1.303                | None => error ("corr: no realizer for instance of theorem " ^
   1.304 @@ -523,7 +585,10 @@
   1.305  
   1.306        | extr d defs vs ts Ts hs (prf % Some t) =
   1.307            let val (defs', u) = extr d defs vs (t :: ts) Ts hs prf
   1.308 -          in (defs', u $ t) end
   1.309 +          in (defs',
   1.310 +            if tname_of (body_type (fastype_of1 (Ts, t))) mem rtypes then u
   1.311 +            else u $ t)
   1.312 +          end
   1.313  
   1.314        | extr d defs vs ts Ts hs (prf1 %% prf2) =
   1.315            let
   1.316 @@ -554,33 +619,36 @@
   1.317                        corr (d + 1) defs' vs' [] [] [] prf' prf' (Some t);
   1.318  
   1.319                      val nt = Envir.beta_norm t;
   1.320 -                    val args = vfs_of prop;
   1.321 +                    val args = filter_out (fn v => tname_of (body_type
   1.322 +                      (fastype_of v)) mem rtypes) (vfs_of prop);
   1.323                      val args' = filter (fn v => Logic.occs (v, nt)) args;
   1.324                      val t' = mkabs (args', nt);
   1.325                      val T = fastype_of t';
   1.326 -                    val cname = add_prefix "extr" (space_implode "_" (s :: vs'));
   1.327 +                    val cname = extr_name s vs';
   1.328                      val c = Const (cname, T);
   1.329                      val u = mkabs (args, list_comb (c, args'));
   1.330                      val eqn = Logic.mk_equals (c, t');
   1.331                      val rlz =
   1.332                        Const ("realizes", fastype_of nt --> propT --> propT);
   1.333 -                    val lhs = rlz $ nt $ prop;
   1.334 -                    val rhs = rlz $ list_comb (c, args') $ prop;
   1.335 -                    val f = Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop);
   1.336 +                    val lhs = app_rlz_rews [] vs' (rlz $ nt $ prop);
   1.337 +                    val rhs = app_rlz_rews [] vs' (rlz $ list_comb (c, args') $ prop);
   1.338 +                    val f = app_rlz_rews [] vs'
   1.339 +                      (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
   1.340  
   1.341 -                    val corr_prf' = foldr forall_intr_prf (args,
   1.342 -                      ProofRewriteRules.rewrite_terms
   1.343 -                        (freeze_thaw (condrew sg rrews [typroc vs', rlz_proc]))
   1.344 -                        (Proofterm.rewrite_proof_notypes ([], [])
   1.345 -                          (chtype [] equal_elim_axm %> lhs %> rhs %%
   1.346 -                            (chtype [propT] symmetric_axm %> rhs %> lhs %%
   1.347 -                              (chtype [propT, T] combination_axm %> f %> f %> c %> t' %%
   1.348 -                                (chtype [T --> propT] reflexive_axm %> f) %%
   1.349 -                                PAxm (cname ^ "_def", eqn,
   1.350 -                                  Some (map TVar (term_tvars eqn))))) %%
   1.351 -                            corr_prf)))
   1.352 +                    val corr_prf' =
   1.353 +                      chtype [] equal_elim_axm %> lhs %> rhs %%
   1.354 +                       (chtype [propT] symmetric_axm %> rhs %> lhs %%
   1.355 +                         (chtype [propT, T] combination_axm %> f %> f %> c %> t' %%
   1.356 +                           (chtype [T --> propT] reflexive_axm %> f) %%
   1.357 +                           PAxm (cname ^ "_def", eqn,
   1.358 +                             Some (map TVar (term_tvars eqn))))) %% corr_prf;
   1.359 +                    val corr_prop = Reconstruct.prop_of corr_prf';
   1.360 +                    val corr_prf'' = foldr forall_intr_prf
   1.361 +                      (map (get_var_type corr_prop) (vfs_of prop), proof_combt
   1.362 +                        (PThm ((corr_name s vs', []), corr_prf', corr_prop,
   1.363 +                          Some (map TVar (term_tvars corr_prop))), vfs_of corr_prop));
   1.364                    in
   1.365 -                    ((s, (vs', ((t', u), corr_prf'))) :: defs'',
   1.366 +                    ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
   1.367                       subst_TVars tye' u)
   1.368                    end
   1.369                | Some ((_, u), _) => (defs, subst_TVars tye' u))
   1.370 @@ -605,44 +673,42 @@
   1.371  
   1.372        | extr d defs vs ts Ts hs _ = error "extr: bad proof";
   1.373  
   1.374 -    fun prep_thm thm =
   1.375 +    fun prep_thm (thm, vs) =
   1.376        let
   1.377          val {prop, der = (_, prf), sign, ...} = rep_thm thm;
   1.378          val name = Thm.name_of_thm thm;
   1.379          val _ = assert (name <> "") "extraction: unnamed theorem";
   1.380 -        val _ = assert (etype_of sg [] [] prop <> nullT) ("theorem " ^
   1.381 +        val _ = assert (etype_of sg vs [] prop <> nullT) ("theorem " ^
   1.382            quote name ^ " has no computational content")
   1.383 -      in (name, Reconstruct.reconstruct_proof sign prop prf) end;
   1.384 +      in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
   1.385  
   1.386 -    val (names, prfs) = ListPair.unzip (map prep_thm thms);
   1.387 -    val defs = foldl (fn (defs, prf) =>
   1.388 -      fst (extr 0 defs [] [] [] [] prf)) ([], prfs);
   1.389 +    val defs = foldl (fn (defs, (prf, vs)) =>
   1.390 +      fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);
   1.391      val {path, ...} = Sign.rep_sg sg;
   1.392  
   1.393 -    fun add_def ((s, (vs, ((t, u), _))), thy) = 
   1.394 -      let
   1.395 -        val ft = fst (Type.freeze_thaw t);
   1.396 -        val fu = fst (Type.freeze_thaw u);
   1.397 -        val name = add_prefix "extr" (space_implode "_" (s :: vs))
   1.398 -      in case Sign.const_type (sign_of thy) name of
   1.399 -          None => if t = nullt then thy else thy |>
   1.400 -            Theory.add_consts_i [(name, fastype_of ft, NoSyn)] |>
   1.401 -            fst o PureThy.add_defs_i false [((name ^ "_def",
   1.402 -              Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
   1.403 -        | Some _ => thy
   1.404 -      end;
   1.405 -
   1.406 -    fun add_thm ((s, (vs, (_, prf))), thy) = fst (PureThy.store_thm
   1.407 -          ((add_prefix "extr" (space_implode "_" (s :: vs)) ^
   1.408 -            "_correctness", standard (gen_all (ProofChecker.thm_of_proof thy
   1.409 -              (fst (Proofterm.freeze_thaw_prf (ProofRewriteRules.rewrite_terms
   1.410 -                (Pattern.rewrite_term (Sign.tsig_of (sign_of thy)) []
   1.411 -                  [rlz_proc']) prf)))))), []) thy)
   1.412 +    fun add_def ((s, (vs, ((t, u), (prf, _)))), thy) =
   1.413 +      (case Sign.const_type (sign_of thy) (extr_name s vs) of
   1.414 +         None =>
   1.415 +           let
   1.416 +             val corr_prop = Reconstruct.prop_of prf;
   1.417 +             val ft = fst (Type.freeze_thaw t);
   1.418 +             val fu = fst (Type.freeze_thaw u);
   1.419 +             val thy' = if t = nullt then thy else thy |>
   1.420 +               Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] |>
   1.421 +               fst o PureThy.add_defs_i false [((extr_name s vs ^ "_def",
   1.422 +                 Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])];
   1.423 +           in
   1.424 +             fst (PureThy.store_thm ((corr_name s vs,
   1.425 +               Thm.varifyT (funpow (length (term_vars corr_prop))
   1.426 +                 (forall_elim_var 0) (forall_intr_frees
   1.427 +                   (ProofChecker.thm_of_proof thy'
   1.428 +                     (fst (Proofterm.freeze_thaw_prf prf)))))), []) thy')
   1.429 +           end
   1.430 +       | Some _ => thy);
   1.431  
   1.432    in thy |>
   1.433      Theory.absolute_path |>
   1.434      curry (foldr add_def) defs |>
   1.435 -    curry (foldr add_thm) (filter (fn (s, _) => s mem names) defs) |>
   1.436      Theory.add_path (NameSpace.pack (if_none path []))
   1.437    end;
   1.438  
   1.439 @@ -651,13 +717,13 @@
   1.440  
   1.441  structure P = OuterParse and K = OuterSyntax.Keyword;
   1.442  
   1.443 +val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
   1.444 +
   1.445  val realizersP =
   1.446    OuterSyntax.command "realizers"
   1.447    "specify realizers for primitive axioms / theorems, together with correctness proof"
   1.448    K.thy_decl
   1.449 -    (Scan.repeat1 (P.xname --
   1.450 -       Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [] --|
   1.451 -       P.$$$ ":" -- P.string -- P.string) >>
   1.452 +    (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
   1.453       (fn xs => Toplevel.theory (fn thy => add_realizers
   1.454         (map (fn (((a, vs), s1), s2) =>
   1.455           (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
   1.456 @@ -674,14 +740,16 @@
   1.457  
   1.458  val extractP =
   1.459    OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
   1.460 -    (Scan.repeat1 P.xname >> (fn xs => Toplevel.theory
   1.461 -      (fn thy => extract (map (PureThy.get_thm thy) xs) thy)));
   1.462 +    (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
   1.463 +      (fn thy => extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
   1.464  
   1.465  val parsers = [realizersP, realizabilityP, typeofP, extractP];
   1.466  
   1.467  val setup =
   1.468    [ExtractionData.init,
   1.469  
   1.470 +   add_types [("prop", ([], None))],
   1.471 +
   1.472     add_typeof_eqns
   1.473       ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
   1.474      \  (typeof (PROP Q)) == (Type (TYPE('Q))) ==>  \