src/Pure/Proof/extraction.ML
changeset 49960 1167c1157a5b
parent 48704 85a3de10567d
child 52788 da1fdbfebd39
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun Oct 21 08:39:41 2012 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Oct 21 16:43:08 2012 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4          | _ => nullT))
     1.5    | typeof_proc _ _ _ = NONE;
     1.6  
     1.7 -fun rlz_proc (Const ("realizes", Type (_, [Type ("Null", []), _])) $ r $ t) = SOME t
     1.8 +fun rlz_proc (Const ("realizes", Type (_, [Type ("Null", []), _])) $ _ $ t) = SOME t
     1.9    | rlz_proc (Const ("realizes", Type (_, [T, _])) $ r $ t) =
    1.10        (case strip_comb t of
    1.11           (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T --> U), r :: ts))
    1.12 @@ -370,7 +370,6 @@
    1.13        (rev (Term.add_vars prop' []));
    1.14      val cs = maps (fn T => map (pair T) S) Ts;
    1.15      val constraints' = map Logic.mk_of_class cs;
    1.16 -    val cs' = rev (cs @ map (Logic.dest_of_class o snd) constraints);
    1.17      fun typ_map T = Type.strip_sorts
    1.18        (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
    1.19      fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
    1.20 @@ -524,40 +523,41 @@
    1.21      fun realizes_null vs prop = app_rlz_rews [] vs
    1.22        (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
    1.23  
    1.24 -    fun corr d defs vs ts Ts hs cs (PBound i) _ _ = (defs, PBound i)
    1.25 +    fun corr d vs ts Ts hs cs _ (PBound i) _ defs = (PBound i, defs)
    1.26  
    1.27 -      | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
    1.28 -          let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
    1.29 -            (dummyt :: hs) cs prf (Proofterm.incr_pboundvars 1 0 prf')
    1.30 -            (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
    1.31 -          in (defs', Abst (s, SOME T, corr_prf)) end
    1.32 +      | corr d vs ts Ts hs cs t (Abst (s, SOME T, prf)) (Abst (_, _, prf')) defs =
    1.33 +          let val (corr_prf, defs') = corr d vs [] (T :: Ts)
    1.34 +            (dummyt :: hs) cs (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
    1.35 +            prf (Proofterm.incr_pboundvars 1 0 prf') defs
    1.36 +          in (Abst (s, SOME T, corr_prf), defs') end
    1.37  
    1.38 -      | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
    1.39 +      | corr d vs ts Ts hs cs t (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) defs =
    1.40            let
    1.41              val T = etype_of thy' vs Ts prop;
    1.42              val u = if T = nullT then
    1.43                  (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
    1.44                else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
    1.45 -            val (defs', corr_prf) =
    1.46 -              corr d defs vs [] (T :: Ts) (prop :: hs)
    1.47 -                (prop :: cs) (Proofterm.incr_pboundvars 0 1 prf)
    1.48 -                (Proofterm.incr_pboundvars 0 1 prf') u;
    1.49 +            val (corr_prf, defs') =
    1.50 +              corr d vs [] (T :: Ts) (prop :: hs)
    1.51 +                (prop :: cs) u (Proofterm.incr_pboundvars 0 1 prf)
    1.52 +                (Proofterm.incr_pboundvars 0 1 prf') defs;
    1.53              val rlz = Const ("realizes", T --> propT --> propT)
    1.54 -          in (defs',
    1.55 +          in (
    1.56              if T = nullT then AbsP ("R",
    1.57                SOME (app_rlz_rews Ts vs (rlz $ nullt $ prop)),
    1.58                  Proofterm.prf_subst_bounds [nullt] corr_prf)
    1.59              else Abst (s, SOME T, AbsP ("R",
    1.60                SOME (app_rlz_rews (T :: Ts) vs
    1.61 -                (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
    1.62 +                (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)), defs')
    1.63            end
    1.64  
    1.65 -      | corr d defs vs ts Ts hs cs (prf % SOME t) (prf' % _) t' =
    1.66 +      | corr d vs ts Ts hs cs t' (prf % SOME t) (prf' % _) defs =
    1.67            let
    1.68              val (Us, T) = strip_type (fastype_of1 (Ts, t));
    1.69 -            val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs cs prf prf'
    1.70 +            val (corr_prf, defs') = corr d vs (t :: ts) Ts hs cs
    1.71                (if member (op =) rtypes (tname_of T) then t'
    1.72 -               else (case t' of SOME (u $ _) => SOME u | _ => NONE));
    1.73 +               else (case t' of SOME (u $ _) => SOME u | _ => NONE))
    1.74 +               prf prf' defs;
    1.75              val u = if not (member (op =) rtypes (tname_of T)) then t else
    1.76                let
    1.77                  val eT = etype_of thy' vs Ts t;
    1.78 @@ -569,26 +569,28 @@
    1.79                      SOME ((_, SOME f)) => f r eT u T
    1.80                    | _ => Const ("realizes", eT --> T --> T) $ r $ u)
    1.81                in app_rlz_rews Ts vs (fold_rev (Term.abs o pair "x") Us' u') end
    1.82 -          in (defs', corr_prf % SOME u) end
    1.83 +          in (corr_prf % SOME u, defs') end
    1.84  
    1.85 -      | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
    1.86 +      | corr d vs ts Ts hs cs t (prf1 %% prf2) (prf1' %% prf2') defs =
    1.87            let
    1.88              val prop = Reconstruct.prop_of' hs prf2';
    1.89              val T = etype_of thy' vs Ts prop;
    1.90 -            val (defs1, f, u) = if T = nullT then (defs, t, NONE) else
    1.91 +            val (f, u, defs1) = if T = nullT then (t, NONE, defs) else
    1.92                (case t of
    1.93 -                 SOME (f $ u) => (defs, SOME f, SOME u)
    1.94 +                 SOME (f $ u) => (SOME f, SOME u, defs)
    1.95                 | _ =>
    1.96 -                 let val (defs1, u) = extr d defs vs [] Ts hs prf2'
    1.97 -                 in (defs1, NONE, SOME u) end)
    1.98 -            val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs cs prf1 prf1' f;
    1.99 -            val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs cs prf2 prf2' u;
   1.100 +                 let val (u, defs1) = extr d vs [] Ts hs prf2' defs
   1.101 +                 in (NONE, SOME u, defs1) end)
   1.102 +            val ((corr_prf1, corr_prf2), defs2) =
   1.103 +              defs1
   1.104 +              |> corr d vs [] Ts hs cs f prf1 prf1'
   1.105 +              ||>> corr d vs [] Ts hs cs u prf2 prf2';
   1.106            in
   1.107 -            if T = nullT then (defs3, corr_prf1 %% corr_prf2) else
   1.108 -              (defs3, corr_prf1 % u %% corr_prf2)
   1.109 +            if T = nullT then (corr_prf1 %% corr_prf2, defs2) else
   1.110 +              (corr_prf1 % u %% corr_prf2, defs2)
   1.111            end
   1.112  
   1.113 -      | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
   1.114 +      | corr d vs ts Ts hs cs _ (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ defs =
   1.115            let
   1.116              val prf = Proofterm.join_proof body;
   1.117              val (vs', tye) = find_inst prop Ts ts vs;
   1.118 @@ -597,10 +599,10 @@
   1.119              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
   1.120              val T = etype_of thy' vs' [] prop;
   1.121              val defs' = if T = nullT then defs
   1.122 -              else fst (extr d defs vs ts Ts hs prf0)
   1.123 +              else snd (extr d vs ts Ts hs prf0 defs)
   1.124            in
   1.125 -            if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0)
   1.126 -            else case Symtab.lookup realizers name of
   1.127 +            if T = nullT andalso realizes_null vs' prop aconv prop then (prf0, defs)
   1.128 +            else (case Symtab.lookup realizers name of
   1.129                NONE => (case find vs' (find' name defs') of
   1.130                  NONE =>
   1.131                    let
   1.132 @@ -609,8 +611,8 @@
   1.133                        (if null vs' then ""
   1.134                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   1.135                      val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   1.136 -                    val (defs'', corr_prf0) = corr (d + 1) defs' vs' [] [] []
   1.137 -                      (rev shyps) prf' prf' NONE;
   1.138 +                    val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
   1.139 +                      (rev shyps) NONE prf' prf' defs';
   1.140                      val corr_prf = mkabsp shyps corr_prf0;
   1.141                      val corr_prop = Reconstruct.prop_of corr_prf;
   1.142                      val corr_prf' =
   1.143 @@ -624,70 +626,69 @@
   1.144                          (map (get_var_type corr_prop) (vfs_of prop)) |>
   1.145                        mkabsp shyps
   1.146                    in
   1.147 -                    ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
   1.148 -                     Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
   1.149 +                    (Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs),
   1.150 +                      (name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
   1.151                    end
   1.152                | SOME (_, (_, prf')) =>
   1.153 -                  (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs)))
   1.154 +                  (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs'))
   1.155              | SOME rs => (case find vs' rs of
   1.156 -                SOME (_, prf') => (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs))
   1.157 +                SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
   1.158                | NONE => error ("corr: no realizer for instance of theorem " ^
   1.159                    quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.160 -                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
   1.161 +                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))))
   1.162            end
   1.163  
   1.164 -      | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
   1.165 +      | corr d vs ts Ts hs cs _ (prf0 as PAxm (s, prop, SOME Ts')) _ defs =
   1.166            let
   1.167              val (vs', tye) = find_inst prop Ts ts vs;
   1.168              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
   1.169            in
   1.170              if etype_of thy' vs' [] prop = nullT andalso
   1.171 -              realizes_null vs' prop aconv prop then (defs, prf0)
   1.172 +              realizes_null vs' prop aconv prop then (prf0, defs)
   1.173              else case find vs' (Symtab.lookup_list realizers s) of
   1.174 -              SOME (_, prf) => (defs,
   1.175 -                Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
   1.176 +              SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
   1.177 +                defs)
   1.178              | NONE => error ("corr: no realizer for instance of axiom " ^
   1.179                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.180                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
   1.181            end
   1.182  
   1.183 -      | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
   1.184 +      | corr d vs ts Ts hs _ _ _ _ defs = error "corr: bad proof"
   1.185  
   1.186 -    and extr d defs vs ts Ts hs (PBound i) = (defs, Bound i)
   1.187 +    and extr d vs ts Ts hs (PBound i) defs = (Bound i, defs)
   1.188  
   1.189 -      | extr d defs vs ts Ts hs (Abst (s, SOME T, prf)) =
   1.190 -          let val (defs', t) = extr d defs vs []
   1.191 -            (T :: Ts) (dummyt :: hs) (Proofterm.incr_pboundvars 1 0 prf)
   1.192 -          in (defs', Abs (s, T, t)) end
   1.193 +      | extr d vs ts Ts hs (Abst (s, SOME T, prf)) defs =
   1.194 +          let val (t, defs') = extr d vs []
   1.195 +            (T :: Ts) (dummyt :: hs) (Proofterm.incr_pboundvars 1 0 prf) defs
   1.196 +          in (Abs (s, T, t), defs') end
   1.197  
   1.198 -      | extr d defs vs ts Ts hs (AbsP (s, SOME t, prf)) =
   1.199 +      | extr d vs ts Ts hs (AbsP (s, SOME t, prf)) defs =
   1.200            let
   1.201              val T = etype_of thy' vs Ts t;
   1.202 -            val (defs', t) =
   1.203 -              extr d defs vs [] (T :: Ts) (t :: hs) (Proofterm.incr_pboundvars 0 1 prf)
   1.204 -          in (defs',
   1.205 -            if T = nullT then subst_bound (nullt, t) else Abs (s, T, t))
   1.206 +            val (t, defs') =
   1.207 +              extr d vs [] (T :: Ts) (t :: hs) (Proofterm.incr_pboundvars 0 1 prf) defs
   1.208 +          in
   1.209 +            (if T = nullT then subst_bound (nullt, t) else Abs (s, T, t), defs')
   1.210            end
   1.211  
   1.212 -      | extr d defs vs ts Ts hs (prf % SOME t) =
   1.213 -          let val (defs', u) = extr d defs vs (t :: ts) Ts hs prf
   1.214 -          in (defs',
   1.215 -            if member (op =) rtypes (tname_of (body_type (fastype_of1 (Ts, t)))) then u
   1.216 -            else u $ t)
   1.217 +      | extr d vs ts Ts hs (prf % SOME t) defs =
   1.218 +          let val (u, defs') = extr d vs (t :: ts) Ts hs prf defs
   1.219 +          in (if member (op =) rtypes (tname_of (body_type (fastype_of1 (Ts, t)))) then u
   1.220 +            else u $ t, defs')
   1.221            end
   1.222  
   1.223 -      | extr d defs vs ts Ts hs (prf1 %% prf2) =
   1.224 +      | extr d vs ts Ts hs (prf1 %% prf2) defs =
   1.225            let
   1.226 -            val (defs', f) = extr d defs vs [] Ts hs prf1;
   1.227 +            val (f, defs') = extr d vs [] Ts hs prf1 defs;
   1.228              val prop = Reconstruct.prop_of' hs prf2;
   1.229              val T = etype_of thy' vs Ts prop
   1.230            in
   1.231 -            if T = nullT then (defs', f) else
   1.232 -              let val (defs'', t) = extr d defs' vs [] Ts hs prf2
   1.233 -              in (defs'', f $ t) end
   1.234 +            if T = nullT then (f, defs') else
   1.235 +              let val (t, defs'') = extr d vs [] Ts hs prf2 defs'
   1.236 +              in (f $ t, defs'') end
   1.237            end
   1.238  
   1.239 -      | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) =
   1.240 +      | extr d vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) defs =
   1.241            let
   1.242              val prf = Proofterm.join_proof body;
   1.243              val (vs', tye) = find_inst prop Ts ts vs;
   1.244 @@ -702,9 +703,9 @@
   1.245                        (if null vs' then ""
   1.246                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   1.247                      val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   1.248 -                    val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
   1.249 -                    val (defs'', corr_prf) = corr (d + 1) defs' vs' [] [] []
   1.250 -                      (rev shyps) prf' prf' (SOME t);
   1.251 +                    val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
   1.252 +                    val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
   1.253 +                      (rev shyps) (SOME t) prf' prf' defs';
   1.254  
   1.255                      val nt = Envir.beta_norm t;
   1.256                      val args = filter_out (fn v => member (op =) rtypes
   1.257 @@ -742,30 +743,30 @@
   1.258                          (map (get_var_type corr_prop) (vfs_of prop)) |>
   1.259                        mkabsp shyps
   1.260                    in
   1.261 -                    ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
   1.262 -                     subst_TVars tye' u)
   1.263 +                    (subst_TVars tye' u,
   1.264 +                      (s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
   1.265                    end
   1.266 -              | SOME ((_, u), _) => (defs, subst_TVars tye' u))
   1.267 +              | SOME ((_, u), _) => (subst_TVars tye' u, defs))
   1.268              | SOME rs => (case find vs' rs of
   1.269 -                SOME (t, _) => (defs, subst_TVars tye' t)
   1.270 +                SOME (t, _) => (subst_TVars tye' t, defs)
   1.271                | NONE => error ("extr: no realizer for instance of theorem " ^
   1.272                    quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.273                      (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
   1.274            end
   1.275  
   1.276 -      | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
   1.277 +      | extr d vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) defs =
   1.278            let
   1.279              val (vs', tye) = find_inst prop Ts ts vs;
   1.280              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
   1.281            in
   1.282              case find vs' (Symtab.lookup_list realizers s) of
   1.283 -              SOME (t, _) => (defs, subst_TVars tye' t)
   1.284 +              SOME (t, _) => (subst_TVars tye' t, defs)
   1.285              | NONE => error ("extr: no realizer for instance of axiom " ^
   1.286                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.287                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
   1.288            end
   1.289  
   1.290 -      | extr d defs vs ts Ts hs _ = error "extr: bad proof";
   1.291 +      | extr d vs ts Ts hs _ defs = error "extr: bad proof";
   1.292  
   1.293      fun prep_thm (thm, vs) =
   1.294        let
   1.295 @@ -779,7 +780,7 @@
   1.296        in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
   1.297  
   1.298      val defs =
   1.299 -      fold (fn (prf, vs) => fn defs => fst (extr 0 defs vs [] [] [] prf))
   1.300 +      fold (fn (prf, vs) => snd o extr 0 vs [] [] [] prf)
   1.301          (map prep_thm thms) [];
   1.302  
   1.303      fun add_def (s, (vs, ((t, u), (prf, _)))) thy =