--- 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;