--- a/src/HOL/Tools/rewrite_hol_proof.ML Thu Jun 03 23:17:57 2010 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Thu Jun 03 23:56:05 2010 +0200
@@ -13,8 +13,6 @@
structure RewriteHOLProof : REWRITE_HOL_PROOF =
struct
-open Proofterm;
-
val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
@@ -311,14 +309,14 @@
| strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
-val subst_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of subst))));
-val sym_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of sym))));
+val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst))));
+val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of sym))));
fun make_subst Ts prf xs (_, []) = prf
| make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
let val T = fastype_of1 (Ts, x)
in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
- else change_type (SOME [T]) subst_prf %> x %> y %>
+ else Proofterm.change_type (SOME [T]) subst_prf %> x %> y %>
Abs ("z", T, list_comb (incr_boundvars 1 f,
map (incr_boundvars 1) xs @ Bound 0 ::
map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
@@ -326,7 +324,8 @@
end;
fun make_sym Ts ((x, y), (prf, clprf)) =
- ((y, x), (change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
+ ((y, x),
+ (Proofterm.change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
@@ -334,15 +333,15 @@
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
| elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
- (strip_cong [] (incr_pboundvars 1 0 prf))
+ (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
| elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 [] o
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
| elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
- apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
+ apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
| elim_cong_aux _ _ = NONE;
-fun elim_cong Ts hs prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
+fun elim_cong Ts hs prf = Option.map (rpair Proofterm.no_skel) (elim_cong_aux Ts prf);
end;
--- a/src/Pure/Proof/extraction.ML Thu Jun 03 23:17:57 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Thu Jun 03 23:56:05 2010 +0200
@@ -30,8 +30,6 @@
structure Extraction : EXTRACTION =
struct
-open Proofterm;
-
(**** tools ****)
fun add_syntax thy =
@@ -116,7 +114,7 @@
in rew end;
-val chtype = change_type o SOME;
+val chtype = Proofterm.change_type o SOME;
fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
fun corr_name s vs = extr_name s vs ^ "_correctness";
@@ -135,7 +133,7 @@
| strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
| strip_abs _ _ = error "strip_abs: not an abstraction";
-val prf_subst_TVars = map_proof_types o typ_subst_TVars;
+val prf_subst_TVars = Proofterm.map_proof_types o typ_subst_TVars;
fun relevant_vars types prop = List.foldr (fn
(Var ((a, _), T), vs) => (case strip_type T of
@@ -371,10 +369,10 @@
val xs' = map (map_types typ_map) xs
in
prf |>
- Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |>
- fold_rev implies_intr_proof' (map snd constraints) |>
- fold_rev forall_intr_proof' xs' |>
- fold_rev implies_intr_proof' constraints'
+ Same.commit (Proofterm.map_proof_same (map_types typ_map) typ_map mk_hyp) |>
+ fold_rev Proofterm.implies_intr_proof' (map snd constraints) |>
+ fold_rev Proofterm.forall_intr_proof' xs' |>
+ fold_rev Proofterm.implies_intr_proof' constraints'
end;
(** expanding theorems / definitions **)
@@ -521,7 +519,7 @@
| corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
- (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf')
+ (dummyt :: hs) cs prf (Proofterm.incr_pboundvars 1 0 prf')
(case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
in (defs', Abst (s, SOME T, corr_prf)) end
@@ -531,13 +529,15 @@
val u = if T = nullT then
(case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
- val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs)
- (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
+ val (defs', corr_prf) =
+ corr d defs vs [] (T :: Ts) (prop :: hs)
+ (prop :: cs) (Proofterm.incr_pboundvars 0 1 prf)
+ (Proofterm.incr_pboundvars 0 1 prf') u;
val rlz = Const ("realizes", T --> propT --> propT)
in (defs',
if T = nullT then AbsP ("R",
SOME (app_rlz_rews Ts vs (rlz $ nullt $ prop)),
- prf_subst_bounds [nullt] corr_prf)
+ Proofterm.prf_subst_bounds [nullt] corr_prf)
else Abst (s, SOME T, AbsP ("R",
SOME (app_rlz_rews (T :: Ts) vs
(rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
@@ -581,7 +581,7 @@
| corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
let
- val prf = join_proof body;
+ val prf = Proofterm.join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
val sprfs = mk_sprfs cs tye;
@@ -605,23 +605,26 @@
val corr_prf = mkabsp shyps corr_prf0;
val corr_prop = Reconstruct.prop_of corr_prf;
val corr_prf' =
- proof_combP (proof_combt
+ Proofterm.proof_combP (Proofterm.proof_combt
(PThm (serial (),
((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
- Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop),
+ Future.value (Proofterm.approximate_proof_body corr_prf))),
+ vfs_of corr_prop),
map PBound (length shyps - 1 downto 0)) |>
- fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
+ fold_rev Proofterm.forall_intr_proof'
+ (map (get_var_type corr_prop) (vfs_of prop)) |>
mkabsp shyps
in
((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
- proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
+ Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
end
- | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)))
+ | SOME (_, (_, prf')) =>
+ (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs)))
| SOME rs => (case find vs' rs of
- SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))
+ SOME (_, prf') => (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs))
| NONE => error ("corr: no realizer for instance of theorem " ^
quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
- (Reconstruct.prop_of (proof_combt (prf0, ts))))))
+ (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
end
| corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
@@ -633,10 +636,10 @@
realizes_null vs' prop aconv prop then (defs, prf0)
else case find vs' (Symtab.lookup_list realizers s) of
SOME (_, prf) => (defs,
- proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
+ Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
| NONE => error ("corr: no realizer for instance of axiom " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
- (Reconstruct.prop_of (proof_combt (prf0, ts)))))
+ (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
end
| corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
@@ -645,14 +648,14 @@
| extr d defs vs ts Ts hs (Abst (s, SOME T, prf)) =
let val (defs', t) = extr d defs vs []
- (T :: Ts) (dummyt :: hs) (incr_pboundvars 1 0 prf)
+ (T :: Ts) (dummyt :: hs) (Proofterm.incr_pboundvars 1 0 prf)
in (defs', Abs (s, T, t)) end
| extr d defs vs ts Ts hs (AbsP (s, SOME t, prf)) =
let
val T = etype_of thy' vs Ts t;
- val (defs', t) = extr d defs vs [] (T :: Ts) (t :: hs)
- (incr_pboundvars 0 1 prf)
+ val (defs', t) =
+ extr d defs vs [] (T :: Ts) (t :: hs) (Proofterm.incr_pboundvars 0 1 prf)
in (defs',
if T = nullT then subst_bound (nullt, t) else Abs (s, T, t))
end
@@ -677,7 +680,7 @@
| extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) =
let
- val prf = join_proof body;
+ val prf = Proofterm.join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
@@ -712,20 +715,22 @@
(Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
val corr_prf' = mkabsp shyps
- (chtype [] equal_elim_axm %> lhs %> rhs %%
- (chtype [propT] symmetric_axm %> rhs %> lhs %%
- (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
- (chtype [T --> propT] reflexive_axm %> f) %%
+ (chtype [] Proofterm.equal_elim_axm %> lhs %> rhs %%
+ (chtype [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
+ (chtype [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
+ (chtype [T --> propT] Proofterm.reflexive_axm %> f) %%
PAxm (cname ^ "_def", eqn,
SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Reconstruct.prop_of corr_prf';
val corr_prf'' =
- proof_combP (proof_combt
+ Proofterm.proof_combP (Proofterm.proof_combt
(PThm (serial (),
((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
- Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop),
+ Future.value (Proofterm.approximate_proof_body corr_prf'))),
+ vfs_of corr_prop),
map PBound (length shyps - 1 downto 0)) |>
- fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
+ fold_rev Proofterm.forall_intr_proof'
+ (map (get_var_type corr_prop) (vfs_of prop)) |>
mkabsp shyps
in
((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
@@ -736,7 +741,7 @@
SOME (t, _) => (defs, subst_TVars tye' t)
| NONE => error ("extr: no realizer for instance of theorem " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
- (Reconstruct.prop_of (proof_combt (prf0, ts))))))
+ (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
end
| extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
@@ -748,7 +753,7 @@
SOME (t, _) => (defs, subst_TVars tye' t)
| NONE => error ("extr: no realizer for instance of axiom " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
- (Reconstruct.prop_of (proof_combt (prf0, ts)))))
+ (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
end
| extr d defs vs ts Ts hs _ = error "extr: bad proof";
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 03 23:17:57 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 03 23:56:05 2010 +0200
@@ -22,8 +22,6 @@
structure ProofRewriteRules : PROOF_REWRITE_RULES =
struct
-open Proofterm;
-
fun rew b _ _ =
let
fun ?? x = if b then SOME x else NONE;
@@ -33,9 +31,9 @@
let val Type (_, [Type (_, [U, _]), _]) = T
in SOME U end
else NONE;
- val equal_intr_axm = ax equal_intr_axm [];
- val equal_elim_axm = ax equal_elim_axm [];
- val symmetric_axm = ax symmetric_axm [propT];
+ val equal_intr_axm = ax Proofterm.equal_intr_axm [];
+ val equal_elim_axm = ax Proofterm.equal_elim_axm [];
+ val symmetric_axm = ax Proofterm.symmetric_axm [propT];
fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %%
(PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf
@@ -71,9 +69,10 @@
val _ $ A $ C = Envir.beta_norm X;
val _ $ B $ D = Envir.beta_norm Y
in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B,
- equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
+ Proofterm.equal_elim_axm %> C %> D %% Proofterm.incr_pboundvars 2 0 prf2 %%
(PBound 1 %% (equal_elim_axm %> B %> A %%
- (symmetric_axm % ?? A % ?? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
+ (Proofterm.symmetric_axm % ?? A % ?? B %% Proofterm.incr_pboundvars 2 0 prf1) %%
+ PBound 0)))))
end
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
@@ -86,8 +85,9 @@
val _ $ B $ D = Envir.beta_norm X
in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A,
equal_elim_axm %> D %> C %%
- (symmetric_axm % ?? C % ?? D %% incr_pboundvars 2 0 prf2)
- %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
+ (symmetric_axm % ?? C % ?? D %% Proofterm.incr_pboundvars 2 0 prf2) %%
+ (PBound 1 %%
+ (equal_elim_axm %> A %> B %% Proofterm.incr_pboundvars 2 0 prf1 %% PBound 0)))))
end
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
@@ -99,7 +99,7 @@
val _ $ Q = Envir.beta_norm Y;
in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
- (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
+ (Proofterm.incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
end
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
@@ -114,7 +114,7 @@
val u = incr_boundvars 1 Q $ Bound 0
in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
equal_elim_axm %> t %> u %%
- (symmetric_axm % ?? u % ?? t %% (incr_pboundvars 1 1 prf %> Bound 0))
+ (symmetric_axm % ?? u % ?? t %% (Proofterm.incr_pboundvars 1 1 prf %> Bound 0))
%% (PBound 0 %> Bound 0))))
end
@@ -182,12 +182,12 @@
(PAxm ("Pure.reflexive", _, _) % _)) =
let val (U, V) = (case T of
Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
- in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
- (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t)))
+ in SOME (prf %% (ax Proofterm.combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
+ (ax Proofterm.reflexive_axm [T] % ?? eq) %% (ax Proofterm.reflexive_axm [U] % ?? t)))
end
| rew' _ = NONE;
- in rew' #> Option.map (rpair no_skel) end;
+ in rew' #> Option.map (rpair Proofterm.no_skel) end;
fun rprocs b = [rew b];
val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
@@ -231,7 +231,8 @@
(Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
| insert_refl defs Ts (AbsP (s, t, prf)) =
(AbsP (s, t, fst (insert_refl defs Ts prf)), false)
- | insert_refl defs Ts prf = (case strip_combt prf of
+ | insert_refl defs Ts prf =
+ (case Proofterm.strip_combt prf of
(PThm (_, ((s, prop, SOME Ts), _)), ts) =>
if member (op =) defs s then
let
@@ -242,11 +243,12 @@
(fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
map the ts);
in
- (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true)
+ (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')])
+ Proofterm.reflexive_axm %> rhs', true)
end
else (prf, false)
| (_, []) => (prf, false)
- | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
+ | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
fun elim_defs thy r defs prf =
let
@@ -256,7 +258,7 @@
val f = if not r then I else
let
val cnames = map (fst o dest_Const o fst) defs';
- val thms = fold_proof_atoms true
+ val thms = Proofterm.fold_proof_atoms true
(fn PThm (_, ((name, prop, _), _)) =>
if member (op =) defnames name orelse
not (exists_Const (member (op =) cnames o #1) prop)
@@ -291,7 +293,7 @@
| elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
| elim_varst t = t;
in
- map_proof_terms (fn t =>
+ Proofterm.map_proof_terms (fn t =>
if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf
end;
@@ -354,16 +356,16 @@
fun reconstruct prf prop = prf |>
Reconstruct.reconstruct_proof thy prop |>
Reconstruct.expand_proof thy [("", NONE)] |>
- Same.commit (map_proof_same Same.same Same.same hyp)
+ Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
in
map2 reconstruct
- (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
+ (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
(Logic.mk_of_sort (T, S))
end;
fun expand_of_class thy Ts hs (OfClass (T, c)) =
mk_of_sort_proof thy hs (T, [c]) |>
- hd |> rpair no_skel |> SOME
+ hd |> rpair Proofterm.no_skel |> SOME
| expand_of_class thy Ts hs _ = NONE;
end;
--- a/src/Pure/Proof/proof_syntax.ML Thu Jun 03 23:17:57 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Thu Jun 03 23:56:05 2010 +0200
@@ -23,8 +23,6 @@
structure Proof_Syntax : PROOF_SYNTAX =
struct
-open Proofterm;
-
(**** add special syntax for embedding proof terms ****)
val proofT = Type ("proof", []);
@@ -98,7 +96,7 @@
fun prf_of [] (Bound i) = PBound i
| prf_of Ts (Const (s, Type ("proof", _))) =
- change_type (if ty then SOME Ts else NONE)
+ Proofterm.change_type (if ty then SOME Ts else NONE)
(case Long_Name.explode s of
"axm" :: xs =>
let
@@ -110,14 +108,15 @@
| "thm" :: xs =>
let val name = Long_Name.implode xs;
in (case AList.lookup (op =) thms name of
- SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm))))
+ SOME thm =>
+ fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of thm))))
| NONE => error ("Unknown theorem " ^ quote name))
end
| _ => error ("Illegal proof constant name: " ^ quote s))
| prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) =
(case try Logic.class_of_const c_class of
SOME c =>
- change_type (if ty then SOME Ts else NONE)
+ Proofterm.change_type (if ty then SOME Ts else NONE)
(OfClass (TVar ((Name.aT, 0), []), c))
| NONE => error ("Bad class constant: " ^ quote c_class))
| prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
@@ -126,13 +125,13 @@
if T = proofT then
error ("Term variable abstraction may not bind proof variable " ^ quote s)
else Abst (s, if ty then SOME T else NONE,
- incr_pboundvars (~1) 0 (prf_of [] prf))
+ Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
| prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
AbsP (s, case t of
Const ("dummy_pattern", _) => NONE
| _ $ Const ("dummy_pattern", _) => NONE
| _ => SOME (mk_term t),
- incr_pboundvars 0 (~1) (prf_of [] prf))
+ Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
| prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
prf_of [] prf1 %% prf_of [] prf2
| prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
@@ -168,11 +167,11 @@
| term_of Ts (Abst (s, opT, prf)) =
let val T = the_default dummyT opT
in Const ("Abst", (T --> proofT) --> proofT) $
- Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
+ Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
end
| term_of Ts (AbsP (s, t, prf)) =
AbsPt $ the_default (Term.dummy_pattern propT) t $
- Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
+ Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
| term_of Ts (prf1 %% prf2) =
AppPt $ term_of Ts prf1 $ term_of Ts prf2
| term_of Ts (prf % opt) =
@@ -233,10 +232,10 @@
fun proof_syntax prf =
let
- val thm_names = Symtab.keys (fold_proof_atoms true
+ val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true
(fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I
| _ => I) [prf] Symtab.empty);
- val axm_names = Symtab.keys (fold_proof_atoms true
+ val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true
(fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
in
add_proof_syntax #>
@@ -249,8 +248,10 @@
val thy = Thm.theory_of_thm thm;
val prop = Thm.full_prop_of thm;
val prf = Thm.proof_of thm;
- val prf' = (case strip_combt (fst (strip_combP prf)) of
- (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else prf
+ val prf' =
+ (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of
+ (PThm (_, ((_, prop', _), body)), _) =>
+ if prop = prop' then Proofterm.join_proof body else prf
| _ => prf)
in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
--- a/src/Pure/Proof/proofchecker.ML Thu Jun 03 23:17:57 2010 +0200
+++ b/src/Pure/Proof/proofchecker.ML Thu Jun 03 23:56:05 2010 +0200
@@ -13,8 +13,6 @@
structure ProofChecker : PROOF_CHECKER =
struct
-open Proofterm;
-
(***** construct a theorem out of a proof term *****)
fun lookup_thm thy =
@@ -39,8 +37,8 @@
end;
fun pretty_prf thy vs Hs prf =
- let val prf' = prf |> prf_subst_bounds (map Free vs) |>
- prf_subst_pbounds (map (Hyp o prop_of) Hs)
+ let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
+ Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
in
(Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
--- a/src/Pure/Proof/reconstruct.ML Thu Jun 03 23:17:57 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML Thu Jun 03 23:56:05 2010 +0200
@@ -17,8 +17,6 @@
structure Reconstruct : RECONSTRUCT =
struct
-open Proofterm;
-
val quiet_mode = Unsynchronized.ref true;
fun message s = if !quiet_mode then () else writeln s;
@@ -28,7 +26,7 @@
fun forall_intr_vfs prop = fold_rev Logic.all
(vars_of prop @ frees_of prop) prop;
-fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof'
+fun forall_intr_vfs_prf prop prf = fold_rev Proofterm.forall_intr_proof'
(vars_of prop @ frees_of prop) prf;
@@ -140,8 +138,8 @@
| SOME Ts => (Ts, env));
val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
(forall_intr_vfs prop) handle Library.UnequalLengths =>
- error ("Wrong number of type arguments for " ^ quote (guess_name prf))
- in (prop', change_type (SOME Ts) prf, [], env', vTs) end;
+ error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
+ in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
fun head_norm (prop, prf, cnstrts, env, vTs) =
(Envir.head_norm env prop, prf, cnstrts, env, vTs);
@@ -285,17 +283,17 @@
fun reconstruct_proof thy prop cprf =
let
- val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop);
+ val (cprf' % SOME prop', thawf) = Proofterm.freeze_thaw_prf (cprf % SOME prop);
val _ = message "Collecting constraints...";
val (t, prf, cs, env, _) = make_constraints_cprf thy
- (Envir.empty (maxidx_proof cprf ~1)) cprf';
+ (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf';
val cs' = map (fn p => (true, p, uncurry (union (op =))
(pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
(map (pairself (Envir.norm_term env)) ((t, prop')::cs));
val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
val env' = solve thy cs' env
in
- thawf (norm_proof env' prf)
+ thawf (Proofterm.norm_proof env' prf)
end;
fun prop_of_atom prop Ts = subst_atomic_types
@@ -357,24 +355,24 @@
val _ = message ("Reconstructing proof of " ^ a);
val _ = message (Syntax.string_of_term_global thy prop);
val prf' = forall_intr_vfs_prf prop
- (reconstruct_proof thy prop (join_proof body));
+ (reconstruct_proof thy prop (Proofterm.join_proof body));
val (maxidx', prfs', prf) = expand
- (maxidx_proof prf' ~1) prfs prf'
- in (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf,
+ (Proofterm.maxidx_proof prf' ~1) prfs prf'
+ in (maxidx' + maxidx + 1, Proofterm.incr_indexes (maxidx + 1) prf,
((a, prop), (maxidx', prf)) :: prfs')
end
| SOME (maxidx', prf) => (maxidx' + maxidx + 1,
- incr_indexes (maxidx + 1) prf, prfs));
+ Proofterm.incr_indexes (maxidx + 1) prf, prfs));
val tfrees = Term.add_tfrees prop [] |> rev;
val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
(Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts;
val varify = map_type_tfree (fn p as (a, S) =>
if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
in
- (maxidx', prfs', map_proof_types (typ_subst_TVars tye o varify) prf)
+ (maxidx', prfs', Proofterm.map_proof_types (typ_subst_TVars tye o varify) prf)
end
| expand maxidx prfs prf = (maxidx, prfs, prf);
- in #3 (expand (maxidx_proof prf ~1) [] prf) end;
+ in #3 (expand (Proofterm.maxidx_proof prf ~1) [] prf) end;
end;