# HG changeset patch # User wenzelm # Date 1275602165 -7200 # Node ID 96e2b9a6f074c5ebeaf16e9ba85aefff3920f561 # Parent 38ce84c83738e0901a9d7a2533d3484b0bfc6638 do not open Proofterm, which is very ould style; diff -r 38ce84c83738 -r 96e2b9a6f074 src/HOL/Tools/rewrite_hol_proof.ML --- 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; diff -r 38ce84c83738 -r 96e2b9a6f074 src/Pure/Proof/extraction.ML --- 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"; diff -r 38ce84c83738 -r 96e2b9a6f074 src/Pure/Proof/proof_rewrite_rules.ML --- 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; diff -r 38ce84c83738 -r 96e2b9a6f074 src/Pure/Proof/proof_syntax.ML --- 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; diff -r 38ce84c83738 -r 96e2b9a6f074 src/Pure/Proof/proofchecker.ML --- 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')) diff -r 38ce84c83738 -r 96e2b9a6f074 src/Pure/Proof/reconstruct.ML --- 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;