src/Pure/Proof/extraction.ML
changeset 37310 96e2b9a6f074
parent 37237 957753a47670
child 38761 b32975d3db3e
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Jun 03 23:17:57 2010 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu Jun 03 23:56:05 2010 +0200
     1.3 @@ -30,8 +30,6 @@
     1.4  structure Extraction : EXTRACTION =
     1.5  struct
     1.6  
     1.7 -open Proofterm;
     1.8 -
     1.9  (**** tools ****)
    1.10  
    1.11  fun add_syntax thy =
    1.12 @@ -116,7 +114,7 @@
    1.13  
    1.14    in rew end;
    1.15  
    1.16 -val chtype = change_type o SOME;
    1.17 +val chtype = Proofterm.change_type o SOME;
    1.18  
    1.19  fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
    1.20  fun corr_name s vs = extr_name s vs ^ "_correctness";
    1.21 @@ -135,7 +133,7 @@
    1.22    | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
    1.23    | strip_abs _ _ = error "strip_abs: not an abstraction";
    1.24  
    1.25 -val prf_subst_TVars = map_proof_types o typ_subst_TVars;
    1.26 +val prf_subst_TVars = Proofterm.map_proof_types o typ_subst_TVars;
    1.27  
    1.28  fun relevant_vars types prop = List.foldr (fn
    1.29        (Var ((a, _), T), vs) => (case strip_type T of
    1.30 @@ -371,10 +369,10 @@
    1.31      val xs' = map (map_types typ_map) xs
    1.32    in
    1.33      prf |>
    1.34 -    Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |>
    1.35 -    fold_rev implies_intr_proof' (map snd constraints) |>
    1.36 -    fold_rev forall_intr_proof' xs' |>
    1.37 -    fold_rev implies_intr_proof' constraints'
    1.38 +    Same.commit (Proofterm.map_proof_same (map_types typ_map) typ_map mk_hyp) |>
    1.39 +    fold_rev Proofterm.implies_intr_proof' (map snd constraints) |>
    1.40 +    fold_rev Proofterm.forall_intr_proof' xs' |>
    1.41 +    fold_rev Proofterm.implies_intr_proof' constraints'
    1.42    end;
    1.43  
    1.44  (** expanding theorems / definitions **)
    1.45 @@ -521,7 +519,7 @@
    1.46  
    1.47        | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
    1.48            let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
    1.49 -            (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf')
    1.50 +            (dummyt :: hs) cs prf (Proofterm.incr_pboundvars 1 0 prf')
    1.51              (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
    1.52            in (defs', Abst (s, SOME T, corr_prf)) end
    1.53  
    1.54 @@ -531,13 +529,15 @@
    1.55              val u = if T = nullT then 
    1.56                  (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
    1.57                else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
    1.58 -            val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs)
    1.59 -              (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
    1.60 +            val (defs', corr_prf) =
    1.61 +              corr d defs vs [] (T :: Ts) (prop :: hs)
    1.62 +                (prop :: cs) (Proofterm.incr_pboundvars 0 1 prf)
    1.63 +                (Proofterm.incr_pboundvars 0 1 prf') u;
    1.64              val rlz = Const ("realizes", T --> propT --> propT)
    1.65            in (defs',
    1.66              if T = nullT then AbsP ("R",
    1.67                SOME (app_rlz_rews Ts vs (rlz $ nullt $ prop)),
    1.68 -                prf_subst_bounds [nullt] corr_prf)
    1.69 +                Proofterm.prf_subst_bounds [nullt] corr_prf)
    1.70              else Abst (s, SOME T, AbsP ("R",
    1.71                SOME (app_rlz_rews (T :: Ts) vs
    1.72                  (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
    1.73 @@ -581,7 +581,7 @@
    1.74  
    1.75        | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
    1.76            let
    1.77 -            val prf = join_proof body;
    1.78 +            val prf = Proofterm.join_proof body;
    1.79              val (vs', tye) = find_inst prop Ts ts vs;
    1.80              val shyps = mk_shyps tye;
    1.81              val sprfs = mk_sprfs cs tye;
    1.82 @@ -605,23 +605,26 @@
    1.83                      val corr_prf = mkabsp shyps corr_prf0;
    1.84                      val corr_prop = Reconstruct.prop_of corr_prf;
    1.85                      val corr_prf' =
    1.86 -                      proof_combP (proof_combt
    1.87 +                      Proofterm.proof_combP (Proofterm.proof_combt
    1.88                           (PThm (serial (),
    1.89                            ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
    1.90 -                            Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop),
    1.91 +                            Future.value (Proofterm.approximate_proof_body corr_prf))),
    1.92 +                              vfs_of corr_prop),
    1.93                                map PBound (length shyps - 1 downto 0)) |>
    1.94 -                      fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
    1.95 +                      fold_rev Proofterm.forall_intr_proof'
    1.96 +                        (map (get_var_type corr_prop) (vfs_of prop)) |>
    1.97                        mkabsp shyps
    1.98                    in
    1.99                      ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
   1.100 -                     proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
   1.101 +                     Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
   1.102                    end
   1.103 -              | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)))
   1.104 +              | SOME (_, (_, prf')) =>
   1.105 +                  (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs)))
   1.106              | SOME rs => (case find vs' rs of
   1.107 -                SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))
   1.108 +                SOME (_, prf') => (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs))
   1.109                | NONE => error ("corr: no realizer for instance of theorem " ^
   1.110                    quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.111 -                    (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   1.112 +                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
   1.113            end
   1.114  
   1.115        | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
   1.116 @@ -633,10 +636,10 @@
   1.117                realizes_null vs' prop aconv prop then (defs, prf0)
   1.118              else case find vs' (Symtab.lookup_list realizers s) of
   1.119                SOME (_, prf) => (defs,
   1.120 -                proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
   1.121 +                Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
   1.122              | NONE => error ("corr: no realizer for instance of axiom " ^
   1.123                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.124 -                  (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   1.125 +                  (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
   1.126            end
   1.127  
   1.128        | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
   1.129 @@ -645,14 +648,14 @@
   1.130  
   1.131        | extr d defs vs ts Ts hs (Abst (s, SOME T, prf)) =
   1.132            let val (defs', t) = extr d defs vs []
   1.133 -            (T :: Ts) (dummyt :: hs) (incr_pboundvars 1 0 prf)
   1.134 +            (T :: Ts) (dummyt :: hs) (Proofterm.incr_pboundvars 1 0 prf)
   1.135            in (defs', Abs (s, T, t)) end
   1.136  
   1.137        | extr d defs vs ts Ts hs (AbsP (s, SOME t, prf)) =
   1.138            let
   1.139              val T = etype_of thy' vs Ts t;
   1.140 -            val (defs', t) = extr d defs vs [] (T :: Ts) (t :: hs)
   1.141 -              (incr_pboundvars 0 1 prf)
   1.142 +            val (defs', t) =
   1.143 +              extr d defs vs [] (T :: Ts) (t :: hs) (Proofterm.incr_pboundvars 0 1 prf)
   1.144            in (defs',
   1.145              if T = nullT then subst_bound (nullt, t) else Abs (s, T, t))
   1.146            end
   1.147 @@ -677,7 +680,7 @@
   1.148  
   1.149        | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) =
   1.150            let
   1.151 -            val prf = join_proof body;
   1.152 +            val prf = Proofterm.join_proof body;
   1.153              val (vs', tye) = find_inst prop Ts ts vs;
   1.154              val shyps = mk_shyps tye;
   1.155              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
   1.156 @@ -712,20 +715,22 @@
   1.157                        (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
   1.158  
   1.159                      val corr_prf' = mkabsp shyps
   1.160 -                      (chtype [] equal_elim_axm %> lhs %> rhs %%
   1.161 -                       (chtype [propT] symmetric_axm %> rhs %> lhs %%
   1.162 -                         (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
   1.163 -                           (chtype [T --> propT] reflexive_axm %> f) %%
   1.164 +                      (chtype [] Proofterm.equal_elim_axm %> lhs %> rhs %%
   1.165 +                       (chtype [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
   1.166 +                         (chtype [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
   1.167 +                           (chtype [T --> propT] Proofterm.reflexive_axm %> f) %%
   1.168                             PAxm (cname ^ "_def", eqn,
   1.169                               SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
   1.170                      val corr_prop = Reconstruct.prop_of corr_prf';
   1.171                      val corr_prf'' =
   1.172 -                      proof_combP (proof_combt
   1.173 +                      Proofterm.proof_combP (Proofterm.proof_combt
   1.174                          (PThm (serial (),
   1.175                           ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
   1.176 -                           Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop),
   1.177 +                           Future.value (Proofterm.approximate_proof_body corr_prf'))),
   1.178 +                            vfs_of corr_prop),
   1.179                               map PBound (length shyps - 1 downto 0)) |>
   1.180 -                      fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
   1.181 +                      fold_rev Proofterm.forall_intr_proof'
   1.182 +                        (map (get_var_type corr_prop) (vfs_of prop)) |>
   1.183                        mkabsp shyps
   1.184                    in
   1.185                      ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
   1.186 @@ -736,7 +741,7 @@
   1.187                  SOME (t, _) => (defs, subst_TVars tye' t)
   1.188                | NONE => error ("extr: no realizer for instance of theorem " ^
   1.189                    quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.190 -                    (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   1.191 +                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
   1.192            end
   1.193  
   1.194        | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
   1.195 @@ -748,7 +753,7 @@
   1.196                SOME (t, _) => (defs, subst_TVars tye' t)
   1.197              | NONE => error ("extr: no realizer for instance of axiom " ^
   1.198                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.199 -                  (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   1.200 +                  (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
   1.201            end
   1.202  
   1.203        | extr d defs vs ts Ts hs _ = error "extr: bad proof";