# HG changeset patch # User wenzelm # Date 1564490129 -7200 # Node ID 755d58b48cec392a1e10a00cac0b418fb229db21 # Parent 609b10dc1a7d4e9249bf7244075eb8aaf3e7d69a clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction; diff -r 609b10dc1a7d -r 755d58b48cec src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Tue Jul 30 13:22:29 2019 +0200 +++ b/src/Doc/Implementation/Logic.thy Tue Jul 30 14:35:29 2019 +0200 @@ -1179,9 +1179,9 @@ @{index_ML_type proof} \\ @{index_ML_type proof_body} \\ @{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\ - @{index_ML Reconstruct.reconstruct_proof: + @{index_ML Proofterm.reconstruct_proof: "Proof.context -> term -> proof -> proof"} \\ - @{index_ML Reconstruct.expand_proof: "Proof.context -> + @{index_ML Proofterm.expand_proof: "Proof.context -> (string * term option) list -> proof -> proof"} \\ @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\ @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\ @@ -1213,7 +1213,7 @@ additionally records full proof terms. Officially named theorems that contribute to a result are recorded in any case. - \<^descr> \<^ML>\Reconstruct.reconstruct_proof\~\ctxt prop prf\ turns the implicit + \<^descr> \<^ML>\Proofterm.reconstruct_proof\~\ctxt prop prf\ turns the implicit proof term \prf\ into a full proof of the given proposition. Reconstruction may fail if \prf\ is not a proof of \prop\, or if it does not @@ -1221,7 +1221,7 @@ for proofs that are constructed manually, but not for those produced automatically by the inference kernel. - \<^descr> \<^ML>\Reconstruct.expand_proof\~\ctxt [thm\<^sub>1, \, thm\<^sub>n] prf\ expands and + \<^descr> \<^ML>\Proofterm.expand_proof\~\ctxt [thm\<^sub>1, \, thm\<^sub>n] prf\ expands and reconstructs the proofs of all specified theorems, with the given (full) proof. Theorems that are not unique specified via their name may be disambiguated by giving their proposition. diff -r 609b10dc1a7d -r 755d58b48cec src/HOL/Proofs/ex/Proof_Terms.thy --- a/src/HOL/Proofs/ex/Proof_Terms.thy Tue Jul 30 13:22:29 2019 +0200 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy Tue Jul 30 14:35:29 2019 +0200 @@ -60,7 +60,7 @@ \ (\<^bold>\(H: _) Ha: _. conjI \ _ \ _ \ Ha \ H))"; val thm = prf - |> Reconstruct.reconstruct_proof ctxt \<^prop>\A \ B \ B \ A\ + |> Proofterm.reconstruct_proof ctxt \<^prop>\A \ B \ B \ A\ |> Proof_Checker.thm_of_proof thy |> Drule.export_without_context; \ diff -r 609b10dc1a7d -r 755d58b48cec src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 30 13:22:29 2019 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 30 14:35:29 2019 +0200 @@ -21,7 +21,7 @@ fun prf_of ctxt thm = Thm.reconstruct_proof_of ctxt thm - |> Reconstruct.expand_proof ctxt [("", NONE)]; (* FIXME *) + |> Proofterm.expand_proof ctxt [("", NONE)]; (* FIXME *) fun subsets [] = [[]] | subsets (x::xs) = diff -r 609b10dc1a7d -r 755d58b48cec src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Jul 30 13:22:29 2019 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Tue Jul 30 14:35:29 2019 +0200 @@ -244,7 +244,7 @@ val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; in Proof_Syntax.pretty_proof ctxt - (if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf') + (if full then Proofterm.reconstruct_proof ctxt prop prf' else prf') end | SOME srcs => let diff -r 609b10dc1a7d -r 755d58b48cec src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Jul 30 13:22:29 2019 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Jul 30 14:35:29 2019 +0200 @@ -340,7 +340,7 @@ (if T = nullT then t else list_comb (t, vars')) $ prop); val r = Logic.list_implies (shyps, fold_rev Logic.all (map (get_var_type r') vars) r'); - val prf = Reconstruct.reconstruct_proof ctxt' r (rd s2); + val prf = Proofterm.reconstruct_proof ctxt' r (rd s2); in (name, (vs, (t, prf))) end end; @@ -492,7 +492,7 @@ val typroc = typeof_proc []; val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs ctxt' false (map (Thm.transfer thy) defs) o - Reconstruct.expand_proof ctxt' (map (rpair NONE) ("" :: expand)); + Proofterm.expand_proof ctxt' (map (rpair NONE) ("" :: expand)); val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); fun find_inst prop Ts ts vs = @@ -579,7 +579,7 @@ | corr d vs ts Ts hs cs t (prf1 %% prf2) (prf1' %% prf2') defs = let - val prop = Reconstruct.prop_of' hs prf2'; + val prop = Proofterm.prop_of' hs prf2'; val T = etype_of thy' vs Ts prop; val (f, u, defs1) = if T = nullT then (t, NONE, defs) else (case t of @@ -616,11 +616,11 @@ val _ = msg d ("Building correctness proof for " ^ quote name ^ (if null vs' then "" else " (relevant variables: " ^ commas_quote vs' ^ ")")); - val prf' = prep (Reconstruct.reconstruct_proof ctxt' prop prf); + val prf' = prep (Proofterm.reconstruct_proof ctxt' prop prf); val (corr_prf0, defs'') = corr (d + 1) vs' [] [] [] (rev shyps) NONE prf' prf' defs'; val corr_prf = mkabsp shyps corr_prf0; - val corr_prop = Reconstruct.prop_of corr_prf; + val corr_prop = Proofterm.prop_of corr_prf; val corr_prf' = Proofterm.proof_combP (Proofterm.proof_combt (PThm (Proofterm.proof_serial (), @@ -641,7 +641,7 @@ SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs') | NONE => error ("corr: no realizer for instance of theorem " ^ quote name ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm - (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))) + (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))) end | corr d vs ts Ts hs cs _ (prf0 as PAxm (s, prop, SOME Ts')) _ defs = @@ -656,7 +656,7 @@ defs) | NONE => error ("corr: no realizer for instance of axiom " ^ quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm - (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))) + (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))) end | corr d vs ts Ts hs _ _ _ _ defs = error "corr: bad proof" @@ -686,7 +686,7 @@ | extr d vs ts Ts hs (prf1 %% prf2) defs = let val (f, defs') = extr d vs [] Ts hs prf1 defs; - val prop = Reconstruct.prop_of' hs prf2; + val prop = Proofterm.prop_of' hs prf2; val T = etype_of thy' vs Ts prop in if T = nullT then (f, defs') else @@ -708,7 +708,7 @@ val _ = msg d ("Extracting " ^ quote s ^ (if null vs' then "" else " (relevant variables: " ^ commas_quote vs' ^ ")")); - val prf' = prep (Reconstruct.reconstruct_proof ctxt' prop prf); + val prf' = prep (Proofterm.reconstruct_proof ctxt' prop prf); val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs; val (corr_prf, defs'') = corr (d + 1) vs' [] [] [] (rev shyps) (SOME t) prf' prf' defs'; @@ -737,7 +737,7 @@ (chtypes [T --> propT] Proofterm.reflexive_axm %> f) %% PAxm (Thm.def_name cname, eqn, SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf); - val corr_prop = Reconstruct.prop_of corr_prf'; + val corr_prop = Proofterm.prop_of corr_prf'; val corr_prf'' = Proofterm.proof_combP (Proofterm.proof_combt (PThm (Proofterm.proof_serial (), @@ -757,7 +757,7 @@ SOME (t, _) => (subst_TVars tye' t, defs) | NONE => error ("extr: no realizer for instance of theorem " ^ quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm - (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))) + (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))) end | extr d vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) defs = @@ -769,7 +769,7 @@ SOME (t, _) => (subst_TVars tye' t, defs) | NONE => error ("extr: no realizer for instance of axiom " ^ quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm - (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))) + (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))) end | extr d vs ts Ts hs _ defs = error "extr: bad proof"; @@ -783,7 +783,7 @@ val _ = name <> "" orelse error "extraction: unnamed theorem"; val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^ quote name ^ " has no computational content") - in Reconstruct.reconstruct_proof ctxt' prop prf end; + in Proofterm.reconstruct_proof ctxt' prop prf end; val defs = fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm) @@ -807,7 +807,7 @@ fun add_corr (s, (vs, prf)) thy = let - val corr_prop = Reconstruct.prop_of prf; + val corr_prop = Proofterm.prop_of prf; in thy |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs), diff -r 609b10dc1a7d -r 755d58b48cec src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Tue Jul 30 13:22:29 2019 +0200 +++ b/src/Pure/Proof/proof_checker.ML Tue Jul 30 14:35:29 2019 +0200 @@ -41,7 +41,7 @@ Proofterm.prf_subst_pbounds (map (Hyp o Thm.prop_of) Hs) in (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf', - Syntax.pretty_term_global thy (Reconstruct.prop_of prf')) + Syntax.pretty_term_global thy (Proofterm.prop_of prf')) end; fun pretty_term thy vs _ t = diff -r 609b10dc1a7d -r 755d58b48cec src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Jul 30 13:22:29 2019 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Jul 30 14:35:29 2019 +0200 @@ -265,7 +265,7 @@ then I else cons (name, SOME prop) | _ => I) [prf] []; - in Reconstruct.expand_proof ctxt thms end; + in Proofterm.expand_proof ctxt thms end; in rewrite_terms (Pattern.rewrite_term (Proof_Context.theory_of ctxt) defs' []) (fst (insert_refl defnames [] (f prf))) @@ -276,7 +276,7 @@ fun elim_vars mk_default prf = let - val prop = Reconstruct.prop_of prf; + val prop = Proofterm.prop_of prf; val tv = Term.add_vars prop []; val tf = Term.add_frees prop []; @@ -354,8 +354,8 @@ ~1 => error "expand_of_class: missing class hypothesis" | i => PBound i; fun reconstruct prf prop = prf |> - Reconstruct.reconstruct_proof ctxt prop |> - Reconstruct.expand_proof ctxt [("", NONE)] |> + Proofterm.reconstruct_proof ctxt prop |> + Proofterm.expand_proof ctxt [("", NONE)] |> Same.commit (Proofterm.map_proof_same Same.same Same.same hyp) in map2 reconstruct diff -r 609b10dc1a7d -r 755d58b48cec src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Tue Jul 30 13:22:29 2019 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Tue Jul 30 14:35:29 2019 +0200 @@ -187,7 +187,7 @@ (PThm (_, ((_, prop', _, _), body)), _) => if prop = prop' then Proofterm.join_proof body else prf | _ => prf) - in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end; + in if full then Proofterm.reconstruct_proof ctxt prop prf' else prf' end; fun pretty_proof ctxt prf = Proof_Context.pretty_term_abbrev diff -r 609b10dc1a7d -r 755d58b48cec src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Tue Jul 30 13:22:29 2019 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,357 +0,0 @@ -(* Title: Pure/Proof/reconstruct.ML - Author: Stefan Berghofer, TU Muenchen - -Reconstruction of partial proof terms. -*) - -signature RECONSTRUCT = -sig - val reconstruct_proof: Proof.context -> term -> Proofterm.proof -> Proofterm.proof - val prop_of': term list -> Proofterm.proof -> term - val prop_of: Proofterm.proof -> term - val expand_proof: Proof.context -> (string * term option) list -> - Proofterm.proof -> Proofterm.proof -end; - -structure Reconstruct : RECONSTRUCT = -struct - -(* generate constraints for proof term *) - -fun mk_var env Ts T = - let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T) - in (list_comb (v, map Bound (length Ts - 1 downto 0)), env') end; - -fun mk_tvar S (Envir.Envir {maxidx, tenv, tyenv}) = - (TVar (("'t", maxidx + 1), S), - Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}); - -val mk_abs = fold (fn T => fn u => Abs ("", T, u)); - -fun unifyT ctxt env T U = - let - val Envir.Envir {maxidx, tenv, tyenv} = env; - val (tyenv', maxidx') = Sign.typ_unify (Proof_Context.theory_of ctxt) (T, U) (tyenv, maxidx); - in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end; - -fun chaseT env (T as TVar v) = - (case Type.lookup (Envir.type_env env) v of - NONE => T - | SOME T' => chaseT env T') - | chaseT _ T = T; - -fun infer_type ctxt (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs - (t as Const (s, T)) = if T = dummyT then - (case Sign.const_type (Proof_Context.theory_of ctxt) s of - NONE => error ("reconstruct_proof: No such constant: " ^ quote s) - | SOME T => - let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) - in (Const (s, T'), T', vTs, - Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}) - end) - else (t, T, vTs, env) - | infer_type _ env _ vTs (t as Free (s, T)) = - if T = dummyT then (case Symtab.lookup vTs s of - NONE => - let val (T, env') = mk_tvar [] env - in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end - | SOME T => (Free (s, T), T, vTs, env)) - else (t, T, vTs, env) - | infer_type _ _ _ _ (Var _) = error "reconstruct_proof: internal error" - | infer_type ctxt env Ts vTs (Abs (s, T, t)) = - let - val (T', env') = if T = dummyT then mk_tvar [] env else (T, env); - val (t', U, vTs', env'') = infer_type ctxt env' (T' :: Ts) vTs t - in (Abs (s, T', t'), T' --> U, vTs', env'') end - | infer_type ctxt env Ts vTs (t $ u) = - let - val (t', T, vTs1, env1) = infer_type ctxt env Ts vTs t; - val (u', U, vTs2, env2) = infer_type ctxt env1 Ts vTs1 u; - in (case chaseT env2 T of - Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT ctxt env2 U U') - | _ => - let val (V, env3) = mk_tvar [] env2 - in (t' $ u', V, vTs2, unifyT ctxt env3 T (U --> V)) end) - end - | infer_type _ env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) - handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i)); - -fun cantunify ctxt (t, u) = - error ("Non-unifiable terms:\n" ^ - Syntax.string_of_term ctxt t ^ "\n\n" ^ Syntax.string_of_term ctxt u); - -fun decompose ctxt Ts (p as (t, u)) env = - let - fun rigrig (a, T) (b, U) uT ts us = - if a <> b then cantunify ctxt p - else apfst flat (fold_map (decompose ctxt Ts) (ts ~~ us) (uT env T U)) - in - case apply2 (strip_comb o Envir.head_norm env) p of - ((Const c, ts), (Const d, us)) => rigrig c d (unifyT ctxt) ts us - | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT ctxt) ts us - | ((Bound i, ts), (Bound j, us)) => - rigrig (i, dummyT) (j, dummyT) (K o K) ts us - | ((Abs (_, T, t), []), (Abs (_, U, u), [])) => - decompose ctxt (T::Ts) (t, u) (unifyT ctxt env T U) - | ((Abs (_, T, t), []), _) => - decompose ctxt (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env - | (_, (Abs (_, T, u), [])) => - decompose ctxt (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env - | _ => ([(mk_abs Ts t, mk_abs Ts u)], env) - end; - -fun make_constraints_cprf ctxt env cprf = - let - fun add_cnstrt Ts prop prf cs env vTs (t, u) = - let - val t' = mk_abs Ts t; - val u' = mk_abs Ts u - in - (prop, prf, cs, Pattern.unify (Context.Proof ctxt) (t', u') env, vTs) - handle Pattern.Pattern => - let val (cs', env') = decompose ctxt [] (t', u') env - in (prop, prf, cs @ cs', env', vTs) end - | Pattern.Unif => - cantunify ctxt (Envir.norm_term env t', Envir.norm_term env u') - end; - - fun mk_cnstrts_atom env vTs prop opTs prf = - let - val tvars = Term.add_tvars prop [] |> rev; - val tfrees = Term.add_tfrees prop [] |> rev; - val (Ts, env') = - (case opTs of - NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env - | SOME Ts => (Ts, env)); - val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) - (Proofterm.forall_intr_vfs prop) handle ListPair.UnequalLengths => - error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf)) - in (prop', Proofterm.change_types (SOME Ts) prf, [], env', vTs) end; - - fun head_norm (prop, prf, cnstrts, env, vTs) = - (Envir.head_norm env prop, prf, cnstrts, env, vTs); - - fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs) - handle General.Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i)) - | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = - let - val (T, env') = - (case opT of - NONE => mk_tvar [] env - | SOME T => (T, env)); - val (t, prf, cnstrts, env'', vTs') = - mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; - in - (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), - cnstrts, env'', vTs') - end - | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) = - let - val (t', _, vTs', env') = infer_type ctxt env Ts vTs t; - val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf; - in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'') - end - | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) = - let - val (t, env') = mk_var env Ts propT; - val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf; - in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs') - end - | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) = - let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2 - in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of - (Const ("Pure.imp", _) $ u' $ t', prf1, cnstrts', env'', vTs'') => - add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts) - env'' vTs'' (u, u') - | (t, prf1, cnstrts', env'', vTs'') => - let val (v, env''') = mk_var env'' Ts propT - in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts) - env''' vTs'' (t, Logic.mk_implies (u, v)) - end) - end - | mk_cnstrts env Ts Hs vTs (cprf % SOME t) = - let val (t', U, vTs1, env1) = infer_type ctxt env Ts vTs t - in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of - (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, - prf, cnstrts, env2, vTs2) => - let val env3 = unifyT ctxt env2 T U - in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) - end - | (u, prf, cnstrts, env2, vTs2) => - let val (v, env3) = mk_var env2 Ts (U --> propT); - in - add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2 - (u, Const ("Pure.all", (U --> propT) --> propT) $ v) - end) - end - | mk_cnstrts env Ts Hs vTs (cprf % NONE) = - (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of - (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, - prf, cnstrts, env', vTs') => - let val (t, env'') = mk_var env' Ts T - in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs') - end - | (u, prf, cnstrts, env', vTs') => - let - val (T, env1) = mk_tvar [] env'; - val (v, env2) = mk_var env1 Ts (T --> propT); - val (t, env3) = mk_var env2 Ts T - in - add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs' - (u, Const ("Pure.all", (T --> propT) --> propT) $ v) - end) - | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs, _), _))) = - mk_cnstrts_atom env vTs prop opTs prf - | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) = - mk_cnstrts_atom env vTs prop opTs prf - | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) = - mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf - | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) = - mk_cnstrts_atom env vTs prop opTs prf - | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs) - | mk_cnstrts _ _ _ _ _ = error "reconstruct_proof: minimal proof object" - in mk_cnstrts env [] [] Symtab.empty cprf end; - - -(* update list of free variables of constraints *) - -fun upd_constrs env cs = - let - val tenv = Envir.term_env env; - val tyenv = Envir.type_env env; - val dom = [] - |> Vartab.fold (cons o #1) tenv - |> Vartab.fold (cons o #1) tyenv; - val vran = [] - |> Vartab.fold (Term.add_var_names o #2 o #2) tenv - |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv; - fun check_cs [] = [] - | check_cs ((u, p, vs) :: ps) = - let val vs' = subtract (op =) dom vs in - if vs = vs' then (u, p, vs) :: check_cs ps - else (true, p, fold (insert op =) vs' vran) :: check_cs ps - end; - in check_cs cs end; - - -(* solution of constraints *) - -fun solve _ [] bigenv = bigenv - | solve ctxt cs bigenv = - let - fun search _ [] = error ("Unsolvable constraints:\n" ^ - Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Syntax.pretty_flexpair ctxt (apply2 (Envir.norm_term bigenv) p)) cs))) - | search env ((u, p as (t1, t2), vs)::ps) = - if u then - let - val tn1 = Envir.norm_term bigenv t1; - val tn2 = Envir.norm_term bigenv t2 - in - if Pattern.pattern tn1 andalso Pattern.pattern tn2 then - (Pattern.unify (Context.Proof ctxt) (tn1, tn2) env, ps) handle Pattern.Unif => - cantunify ctxt (tn1, tn2) - else - let val (cs', env') = decompose ctxt [] (tn1, tn2) env - in if cs' = [(tn1, tn2)] then - apsnd (cons (false, (tn1, tn2), vs)) (search env ps) - else search env' (map (fn q => (true, q, vs)) cs' @ ps) - end - end - else apsnd (cons (false, p, vs)) (search env ps); - val Envir.Envir {maxidx, ...} = bigenv; - val (env, cs') = search (Envir.empty maxidx) cs; - in - solve ctxt (upd_constrs env cs') (Envir.merge (bigenv, env)) - end; - - -(* reconstruction of proofs *) - -fun reconstruct_proof ctxt prop cprf = - let - val (cprf' % SOME prop', thawf) = Proofterm.freeze_thaw_prf (cprf % SOME prop); - val (t, prf, cs, env, _) = make_constraints_cprf ctxt - (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf'; - val cs' = - map (apply2 (Envir.norm_term env)) ((t, prop') :: cs) - |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) []))); - val env' = solve ctxt cs' env - in - thawf (Proofterm.norm_proof env' prf) - end; - -fun prop_of_atom prop Ts = subst_atomic_types - (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts) - (Proofterm.forall_intr_vfs prop); - -val head_norm = Envir.head_norm Envir.init; - -fun prop_of0 Hs (PBound i) = nth Hs i - | prop_of0 Hs (Abst (s, SOME T, prf)) = - Logic.all_const T $ (Abs (s, T, prop_of0 Hs prf)) - | prop_of0 Hs (AbsP (_, SOME t, prf)) = - Logic.mk_implies (t, prop_of0 (t :: Hs) prf) - | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of - Const ("Pure.all", _) $ f => f $ t - | _ => error "prop_of: all expected") - | prop_of0 Hs (prf1 %% _) = (case head_norm (prop_of0 Hs prf1) of - Const ("Pure.imp", _) $ _ $ Q => Q - | _ => error "prop_of: ==> expected") - | prop_of0 _ (Hyp t) = t - | prop_of0 _ (PThm (_, ((_, prop, SOME Ts, _), _))) = prop_of_atom prop Ts - | prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts - | prop_of0 _ (OfClass (T, c)) = Logic.mk_of_class (T, c) - | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts - | prop_of0 _ _ = error "prop_of: partial proof object"; - -val prop_of' = Envir.beta_eta_contract oo prop_of0; -val prop_of = prop_of' []; - - -(* expand and reconstruct subproofs *) - -fun expand_proof ctxt thms prf = - let - fun expand maxidx prfs (AbsP (s, t, prf)) = - let val (maxidx', prfs', prf') = expand maxidx prfs prf - in (maxidx', prfs', AbsP (s, t, prf')) end - | expand maxidx prfs (Abst (s, T, prf)) = - let val (maxidx', prfs', prf') = expand maxidx prfs prf - in (maxidx', prfs', Abst (s, T, prf')) end - | expand maxidx prfs (prf1 %% prf2) = - let - val (maxidx', prfs', prf1') = expand maxidx prfs prf1; - val (maxidx'', prfs'', prf2') = expand maxidx' prfs' prf2; - in (maxidx'', prfs'', prf1' %% prf2') end - | expand maxidx prfs (prf % t) = - let val (maxidx', prfs', prf') = expand maxidx prfs prf - in (maxidx', prfs', prf' % t) end - | expand maxidx prfs (prf as PThm (_, ((a, prop, SOME Ts, open_proof), body))) = - if not (exists - (fn (b, NONE) => a = b - | (b, SOME prop') => a = b andalso prop = prop') thms) - then (maxidx, prfs, prf) else - let - val (maxidx', prf, prfs') = - (case AList.lookup (op =) prfs (a, prop) of - NONE => - let - val prf' = - Proofterm.join_proof body - |> open_proof - |> reconstruct_proof ctxt prop - |> Proofterm.forall_intr_vfs_prf prop; - val (maxidx', prfs', prf) = expand (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, Proofterm.incr_indexes (maxidx + 1) prf, prfs)); - in (maxidx', prfs', Proofterm.app_types (maxidx + 1) prop Ts prf) end - | expand maxidx prfs prf = (maxidx, prfs, prf); - - in #3 (expand (Proofterm.maxidx_proof prf ~1) [] prf) end; - -end; diff -r 609b10dc1a7d -r 755d58b48cec src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Jul 30 13:22:29 2019 +0200 +++ b/src/Pure/ROOT.ML Tue Jul 30 14:35:29 2019 +0200 @@ -169,7 +169,6 @@ ML_file "unify.ML"; ML_file "theory.ML"; ML_file "proofterm.ML"; -ML_file "Proof/reconstruct.ML"; ML_file "thm.ML"; ML_file "more_pattern.ML"; ML_file "more_unify.ML"; diff -r 609b10dc1a7d -r 755d58b48cec src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Tue Jul 30 13:22:29 2019 +0200 +++ b/src/Pure/more_thm.ML Tue Jul 30 14:35:29 2019 +0200 @@ -678,7 +678,7 @@ fun reconstruct_proof_of ctxt raw_thm = let val thm = Thm.transfer' ctxt raw_thm - in Reconstruct.reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end; + in Proofterm.reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end; fun clean_proof_of ctxt full raw_thm = let @@ -688,8 +688,8 @@ (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); in Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) - |> Reconstruct.reconstruct_proof ctxt prop - |> Reconstruct.expand_proof ctxt [("", NONE)] + |> Proofterm.reconstruct_proof ctxt prop + |> Proofterm.expand_proof ctxt [("", NONE)] |> Proofterm.rew_proof (Proof_Context.theory_of ctxt) |> Proofterm.no_thm_proofs |> not full ? Proofterm.shrink_proof diff -r 609b10dc1a7d -r 755d58b48cec src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Jul 30 13:22:29 2019 +0200 +++ b/src/Pure/proofterm.ML Tue Jul 30 14:35:29 2019 +0200 @@ -152,9 +152,10 @@ (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof val rew_proof: theory -> proof -> proof - val forall_intr_vfs: term -> term - val forall_intr_vfs_prf: term -> proof -> proof - val app_types: int -> term -> typ list -> proof -> proof + val reconstruct_proof: Proof.context -> term -> proof -> proof + val prop_of': term list -> proof -> term + val prop_of: proof -> term + val expand_proof: Proof.context -> (string * term option) list -> proof -> proof val proof_serial: unit -> proof_serial val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body @@ -163,7 +164,6 @@ val unconstrain_thm_proof: theory -> sort list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof val get_name: sort list -> term list -> term -> proof -> string - val guess_name: proof -> string end structure Proofterm : PROOFTERM = @@ -1589,7 +1589,8 @@ fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p)); -(* clean proof: expand unnamed PThm nodes *) + +(** reconstruction of partial proof terms **) local @@ -1597,8 +1598,6 @@ fun frees_of t = map Free (rev (Term.add_frees t [])); fun variables_of t = vars_of t @ frees_of t; -in - fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop; fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf; @@ -1610,6 +1609,354 @@ fun varify (v as (a, S)) = if member (op =) tfrees v then TVar ((a, ~1), S) else TFree v; in map_proof_types (typ_subst_TVars (vs ~~ Ts) o map_type_tfree varify) prf end; +fun guess_name (PThm (_, ((name, _, _, _), _))) = name + | guess_name (prf %% Hyp _) = guess_name prf + | guess_name (prf %% OfClass _) = guess_name prf + | guess_name (prf % NONE) = guess_name prf + | guess_name (prf % SOME (Var _)) = guess_name prf + | guess_name _ = ""; + + +(* generate constraints for proof term *) + +fun mk_var env Ts T = + let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T) + in (list_comb (v, map Bound (length Ts - 1 downto 0)), env') end; + +fun mk_tvar S (Envir.Envir {maxidx, tenv, tyenv}) = + (TVar (("'t", maxidx + 1), S), + Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}); + +val mk_abs = fold (fn T => fn u => Abs ("", T, u)); + +fun unifyT ctxt env T U = + let + val Envir.Envir {maxidx, tenv, tyenv} = env; + val (tyenv', maxidx') = Sign.typ_unify (Proof_Context.theory_of ctxt) (T, U) (tyenv, maxidx); + in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end; + +fun chaseT env (T as TVar v) = + (case Type.lookup (Envir.type_env env) v of + NONE => T + | SOME T' => chaseT env T') + | chaseT _ T = T; + +fun infer_type ctxt (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs + (t as Const (s, T)) = if T = dummyT then + (case Sign.const_type (Proof_Context.theory_of ctxt) s of + NONE => error ("reconstruct_proof: No such constant: " ^ quote s) + | SOME T => + let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) + in (Const (s, T'), T', vTs, + Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}) + end) + else (t, T, vTs, env) + | infer_type _ env _ vTs (t as Free (s, T)) = + if T = dummyT then (case Symtab.lookup vTs s of + NONE => + let val (T, env') = mk_tvar [] env + in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end + | SOME T => (Free (s, T), T, vTs, env)) + else (t, T, vTs, env) + | infer_type _ _ _ _ (Var _) = error "reconstruct_proof: internal error" + | infer_type ctxt env Ts vTs (Abs (s, T, t)) = + let + val (T', env') = if T = dummyT then mk_tvar [] env else (T, env); + val (t', U, vTs', env'') = infer_type ctxt env' (T' :: Ts) vTs t + in (Abs (s, T', t'), T' --> U, vTs', env'') end + | infer_type ctxt env Ts vTs (t $ u) = + let + val (t', T, vTs1, env1) = infer_type ctxt env Ts vTs t; + val (u', U, vTs2, env2) = infer_type ctxt env1 Ts vTs1 u; + in (case chaseT env2 T of + Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT ctxt env2 U U') + | _ => + let val (V, env3) = mk_tvar [] env2 + in (t' $ u', V, vTs2, unifyT ctxt env3 T (U --> V)) end) + end + | infer_type _ env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) + handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i)); + +fun cantunify ctxt (t, u) = + error ("Non-unifiable terms:\n" ^ + Syntax.string_of_term ctxt t ^ "\n\n" ^ Syntax.string_of_term ctxt u); + +fun decompose ctxt Ts (p as (t, u)) env = + let + fun rigrig (a, T) (b, U) uT ts us = + if a <> b then cantunify ctxt p + else apfst flat (fold_map (decompose ctxt Ts) (ts ~~ us) (uT env T U)) + in + case apply2 (strip_comb o Envir.head_norm env) p of + ((Const c, ts), (Const d, us)) => rigrig c d (unifyT ctxt) ts us + | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT ctxt) ts us + | ((Bound i, ts), (Bound j, us)) => + rigrig (i, dummyT) (j, dummyT) (K o K) ts us + | ((Abs (_, T, t), []), (Abs (_, U, u), [])) => + decompose ctxt (T::Ts) (t, u) (unifyT ctxt env T U) + | ((Abs (_, T, t), []), _) => + decompose ctxt (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env + | (_, (Abs (_, T, u), [])) => + decompose ctxt (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env + | _ => ([(mk_abs Ts t, mk_abs Ts u)], env) + end; + +fun make_constraints_cprf ctxt env cprf = + let + fun add_cnstrt Ts prop prf cs env vTs (t, u) = + let + val t' = mk_abs Ts t; + val u' = mk_abs Ts u + in + (prop, prf, cs, Pattern.unify (Context.Proof ctxt) (t', u') env, vTs) + handle Pattern.Pattern => + let val (cs', env') = decompose ctxt [] (t', u') env + in (prop, prf, cs @ cs', env', vTs) end + | Pattern.Unif => + cantunify ctxt (Envir.norm_term env t', Envir.norm_term env u') + end; + + fun mk_cnstrts_atom env vTs prop opTs prf = + let + val tvars = Term.add_tvars prop [] |> rev; + val tfrees = Term.add_tfrees prop [] |> rev; + val (Ts, env') = + (case opTs of + NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env + | SOME Ts => (Ts, env)); + val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) + (forall_intr_vfs prop) handle ListPair.UnequalLengths => + error ("Wrong number of type arguments for " ^ quote (guess_name prf)) + in (prop', change_types (SOME Ts) prf, [], env', vTs) end; + + fun head_norm (prop, prf, cnstrts, env, vTs) = + (Envir.head_norm env prop, prf, cnstrts, env, vTs); + + fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs) + handle General.Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i)) + | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = + let + val (T, env') = + (case opT of + NONE => mk_tvar [] env + | SOME T => (T, env)); + val (t, prf, cnstrts, env'', vTs') = + mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; + in + (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), + cnstrts, env'', vTs') + end + | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) = + let + val (t', _, vTs', env') = infer_type ctxt env Ts vTs t; + val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf; + in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'') + end + | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) = + let + val (t, env') = mk_var env Ts propT; + val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf; + in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs') + end + | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) = + let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2 + in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of + (Const ("Pure.imp", _) $ u' $ t', prf1, cnstrts', env'', vTs'') => + add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts) + env'' vTs'' (u, u') + | (t, prf1, cnstrts', env'', vTs'') => + let val (v, env''') = mk_var env'' Ts propT + in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts) + env''' vTs'' (t, Logic.mk_implies (u, v)) + end) + end + | mk_cnstrts env Ts Hs vTs (cprf % SOME t) = + let val (t', U, vTs1, env1) = infer_type ctxt env Ts vTs t + in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of + (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, + prf, cnstrts, env2, vTs2) => + let val env3 = unifyT ctxt env2 T U + in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) + end + | (u, prf, cnstrts, env2, vTs2) => + let val (v, env3) = mk_var env2 Ts (U --> propT); + in + add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2 + (u, Const ("Pure.all", (U --> propT) --> propT) $ v) + end) + end + | mk_cnstrts env Ts Hs vTs (cprf % NONE) = + (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of + (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, + prf, cnstrts, env', vTs') => + let val (t, env'') = mk_var env' Ts T + in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs') + end + | (u, prf, cnstrts, env', vTs') => + let + val (T, env1) = mk_tvar [] env'; + val (v, env2) = mk_var env1 Ts (T --> propT); + val (t, env3) = mk_var env2 Ts T + in + add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs' + (u, Const ("Pure.all", (T --> propT) --> propT) $ v) + end) + | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs, _), _))) = + mk_cnstrts_atom env vTs prop opTs prf + | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) = + mk_cnstrts_atom env vTs prop opTs prf + | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) = + mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf + | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) = + mk_cnstrts_atom env vTs prop opTs prf + | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs) + | mk_cnstrts _ _ _ _ _ = error "reconstruct_proof: minimal proof object" + in mk_cnstrts env [] [] Symtab.empty cprf end; + + +(* update list of free variables of constraints *) + +fun upd_constrs env cs = + let + val tenv = Envir.term_env env; + val tyenv = Envir.type_env env; + val dom = [] + |> Vartab.fold (cons o #1) tenv + |> Vartab.fold (cons o #1) tyenv; + val vran = [] + |> Vartab.fold (Term.add_var_names o #2 o #2) tenv + |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv; + fun check_cs [] = [] + | check_cs ((u, p, vs) :: ps) = + let val vs' = subtract (op =) dom vs in + if vs = vs' then (u, p, vs) :: check_cs ps + else (true, p, fold (insert op =) vs' vran) :: check_cs ps + end; + in check_cs cs end; + + +(* solution of constraints *) + +fun solve _ [] bigenv = bigenv + | solve ctxt cs bigenv = + let + fun search _ [] = error ("Unsolvable constraints:\n" ^ + Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => + Syntax.pretty_flexpair ctxt (apply2 (Envir.norm_term bigenv) p)) cs))) + | search env ((u, p as (t1, t2), vs)::ps) = + if u then + let + val tn1 = Envir.norm_term bigenv t1; + val tn2 = Envir.norm_term bigenv t2 + in + if Pattern.pattern tn1 andalso Pattern.pattern tn2 then + (Pattern.unify (Context.Proof ctxt) (tn1, tn2) env, ps) handle Pattern.Unif => + cantunify ctxt (tn1, tn2) + else + let val (cs', env') = decompose ctxt [] (tn1, tn2) env + in if cs' = [(tn1, tn2)] then + apsnd (cons (false, (tn1, tn2), vs)) (search env ps) + else search env' (map (fn q => (true, q, vs)) cs' @ ps) + end + end + else apsnd (cons (false, p, vs)) (search env ps); + val Envir.Envir {maxidx, ...} = bigenv; + val (env, cs') = search (Envir.empty maxidx) cs; + in + solve ctxt (upd_constrs env cs') (Envir.merge (bigenv, env)) + end; + +in + + +(* reconstruction of proofs *) + +fun reconstruct_proof ctxt prop cprf = + let + val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop); + val (t, prf, cs, env, _) = make_constraints_cprf ctxt + (Envir.empty (maxidx_proof cprf ~1)) cprf'; + val cs' = + map (apply2 (Envir.norm_term env)) ((t, prop') :: cs) + |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) []))); + val env' = solve ctxt cs' env + in + thawf (norm_proof env' prf) + end; + +fun prop_of_atom prop Ts = subst_atomic_types + (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts) + (forall_intr_vfs prop); + +val head_norm = Envir.head_norm Envir.init; + +fun prop_of0 Hs (PBound i) = nth Hs i + | prop_of0 Hs (Abst (s, SOME T, prf)) = + Logic.all_const T $ (Abs (s, T, prop_of0 Hs prf)) + | prop_of0 Hs (AbsP (_, SOME t, prf)) = + Logic.mk_implies (t, prop_of0 (t :: Hs) prf) + | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of + Const ("Pure.all", _) $ f => f $ t + | _ => error "prop_of: all expected") + | prop_of0 Hs (prf1 %% _) = (case head_norm (prop_of0 Hs prf1) of + Const ("Pure.imp", _) $ _ $ Q => Q + | _ => error "prop_of: ==> expected") + | prop_of0 _ (Hyp t) = t + | prop_of0 _ (PThm (_, ((_, prop, SOME Ts, _), _))) = prop_of_atom prop Ts + | prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts + | prop_of0 _ (OfClass (T, c)) = Logic.mk_of_class (T, c) + | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts + | prop_of0 _ _ = error "prop_of: partial proof object"; + +val prop_of' = Envir.beta_eta_contract oo prop_of0; +val prop_of = prop_of' []; + + +(* expand and reconstruct subproofs *) + +fun expand_proof ctxt thms prf = + let + fun expand maxidx prfs (AbsP (s, t, prf)) = + let val (maxidx', prfs', prf') = expand maxidx prfs prf + in (maxidx', prfs', AbsP (s, t, prf')) end + | expand maxidx prfs (Abst (s, T, prf)) = + let val (maxidx', prfs', prf') = expand maxidx prfs prf + in (maxidx', prfs', Abst (s, T, prf')) end + | expand maxidx prfs (prf1 %% prf2) = + let + val (maxidx', prfs', prf1') = expand maxidx prfs prf1; + val (maxidx'', prfs'', prf2') = expand maxidx' prfs' prf2; + in (maxidx'', prfs'', prf1' %% prf2') end + | expand maxidx prfs (prf % t) = + let val (maxidx', prfs', prf') = expand maxidx prfs prf + in (maxidx', prfs', prf' % t) end + | expand maxidx prfs (prf as PThm (_, ((a, prop, SOME Ts, open_proof), body))) = + if not (exists + (fn (b, NONE) => a = b + | (b, SOME prop') => a = b andalso prop = prop') thms) + then (maxidx, prfs, prf) else + let + val (maxidx', prf, prfs') = + (case AList.lookup (op =) prfs (a, prop) of + NONE => + let + val prf' = + join_proof body + |> open_proof + |> reconstruct_proof ctxt prop + |> forall_intr_vfs_prf prop; + val (maxidx', prfs', prf) = expand (maxidx_proof prf' ~1) prfs prf' + in + (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, + ((a, prop), (maxidx', prf)) :: prfs') + end + | SOME (maxidx', prf) => + (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs)); + in (maxidx', prfs', app_types (maxidx + 1) prop Ts prf) end + | expand maxidx prfs prf = (maxidx, prfs, prf); + + in #3 (expand (maxidx_proof prf ~1) [] prf) end; + end; @@ -1741,13 +2088,6 @@ | _ => "") end; -fun guess_name (PThm (_, ((name, _, _, _), _))) = name - | guess_name (prf %% Hyp _) = guess_name prf - | guess_name (prf %% OfClass _) = guess_name prf - | guess_name (prf % NONE) = guess_name prf - | guess_name (prf % SOME (Var _)) = guess_name prf - | guess_name _ = ""; - end; structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;