clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
--- 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>\<open>Reconstruct.reconstruct_proof\<close>~\<open>ctxt prop prf\<close> turns the implicit
+ \<^descr> \<^ML>\<open>Proofterm.reconstruct_proof\<close>~\<open>ctxt prop prf\<close> turns the implicit
proof term \<open>prf\<close> into a full proof of the given proposition.
Reconstruction may fail if \<open>prf\<close> is not a proof of \<open>prop\<close>, 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>\<open>Reconstruct.expand_proof\<close>~\<open>ctxt [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
+ \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<open>ctxt [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> 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.
--- 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>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
val thm =
prf
- |> Reconstruct.reconstruct_proof ctxt \<^prop>\<open>A \<and> B \<longrightarrow> B \<and> A\<close>
+ |> Proofterm.reconstruct_proof ctxt \<^prop>\<open>A \<and> B \<longrightarrow> B \<and> A\<close>
|> Proof_Checker.thm_of_proof thy
|> Drule.export_without_context;
\<close>
--- 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) =
--- 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
--- 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),
--- 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 =
--- 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
--- 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
--- 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;
--- 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";
--- 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
--- 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;