(* Title: Pure/proofterm.ML Author: Stefan Berghofer, TU Muenchen
LF style proof terms.
*)
infix 8 % %% %>;
signature PROOFTERM = sig type thm_header =
{serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P,
prop: term, types: typ listoption} type thm_body type thm_node datatype proof =
MinProof
| PBound of int
| Abst ofstring * typ option * proof
| AbsP ofstring * term option * proof
| % of proof * term option
| %% of proof * proof
| Hyp of term
| PAxm ofstring * term * typ listoption
| PClass of typ * class
| Oracle ofstring * term * typ listoption
| PThm of thm_header * thm_body and proof_body = PBody of
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
zboxes: ZTerm.zboxes,
zproof: zproof,
proof: proof} type oracle = (string * Position.T) * term option type thm = serial * thm_node
exception MIN_PROOF of unit val zproof_of: proof_body -> zproof val proof_of: proof_body -> proof val join_proof: proof_body future -> proof val map_proof_of: (proof -> proof) -> proof_body -> proof_body val thm_header: serial -> Position.T -> string -> Thm_Name.P -> term -> typ listoption ->
thm_header val thm_body: proof_body -> thm_body val thm_body_proof_raw: thm_body -> proof val thm_body_proof_open: thm_body -> proof val thm_node_theory_name: thm_node -> string val thm_node_name: thm_node -> Thm_Name.T val thm_node_prop: thm_node -> term val thm_node_body: thm_node -> proof_body future val thm_node_thms: thm_node -> thm list val join_thms: thm list -> proof_body list val make_thm: thm_header -> thm_body -> thm val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a val fold_body_thms:
({serial: serial, thm_name: Thm_Name.T, prop: term, body: proof_body} -> 'a -> 'a) ->
proof_body list -> 'a -> 'a val oracle_ord: oracle ord val thm_ord: thm ord val union_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T val union_thms: thm Ord_List.T -> thm Ord_List.T -> thm Ord_List.T val unions_thms: thm Ord_List.T list -> thm Ord_List.T val no_proof_body: zproof -> proof -> proof_body val no_thm_names: proof -> proof val no_thm_proofs: proof -> proof val no_body_proofs: proof -> proof
val proof_to_zproof: theory -> proof -> zproof val encode_standard_term: theory -> term XML.Encode.T val encode_standard_proof: theory -> proof XML.Encode.T val encode: theory -> proof XML.Encode.T val encode_body: theory -> proof_body XML.Encode.T val decode: theory -> proof XML.Decode.T val decode_body: theory -> proof_body XML.Decode.T
val %> : proof * term -> proof
(*primitive operations*) val zproof_enabled: int -> bool val proof_enabled: int -> bool val oracle_enabled: int -> bool val get_proofs_level: unit -> int val proofs: int Unsynchronized.ref val any_proofs_enabled: unit -> bool val proof_combt: proof * term list -> proof val proof_combt': proof * term option list -> proof val proof_combP: proof * proof list -> proof val strip_combt: proof -> proof * term optionlist val strip_combP: proof -> proof * proof list val any_head_of: proof -> proof val term_head_of: proof -> proof val proof_head_of: proof -> proof val compact_proof: proof -> bool val strip_thm_body: proof_body -> proof_body val map_proof_same: term Same.operation -> typ Same.operation
-> (typ * class -> proof) -> proof Same.operation val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation val map_proof_types_same: typ Same.operation -> proof Same.operation val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof val map_proof_types: (typ -> typ) -> proof -> proof val fold_proof_terms: (term -> 'a -> 'a) -> proof -> 'a -> 'a val fold_proof_terms_types: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a val maxidx_proof: proof -> int -> int val change_types: typ listoption -> proof -> proof val abstract_over: term -> proof -> proof val incr_bv_same: int -> int -> int -> int -> proof Same.operation val incr_bv: int -> int -> int -> int -> proof -> proof val incr_boundvars: int -> int -> proof -> proof val prf_loose_bvar1: proof -> int -> bool val prf_loose_Pbvar1: proof -> int -> bool val prf_add_loose_bnos: int -> int -> proof -> int list * int list -> int list * int list val norm_proof: Envir.env -> proof -> proof val norm_proof_remove_types: Envir.env -> proof -> proof val subst_bounds: term list -> proof -> proof val subst_pbounds: proof list -> proof -> proof val freeze_thaw_prf: proof -> proof * (proof -> proof)
(*proof terms for specific inference rules*) val trivial_proof: proof val implies_intr_proof: term -> proof -> proof val implies_intr_proof': term -> proof -> proof val forall_intr_proof: string * term -> typ option -> proof -> proof val forall_intr_proof': term -> proof -> proof val varifyT_proof: ((string * sort) * (indexname * sort)) list -> proof -> proof val legacy_freezeT: term -> proof -> proof val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof val permute_prems_proof: term list -> int -> int -> proof -> proof val generalize_proof: Names.set * Names.set -> int -> term -> proof -> proof val instantiate: typ TVars.table * term Vars.table -> proof -> proof val lift_proof: term -> int -> term list -> proof -> proof val incr_indexes: int -> proof -> proof val assumption_proof: term list -> term -> int -> proof -> proof val bicompose_proof: Envir.env -> int -> bool -> term list -> term list -> term option ->
term list -> int -> int -> proof -> proof -> proof val reflexive_axm: proof val symmetric_axm: proof val transitive_axm: proof val equal_intr_axm: proof val equal_elim_axm: proof val abstract_rule_axm: proof val combination_axm: proof val reflexive_proof: proof val symmetric_proof: proof -> proof val transitive_proof: typ -> term -> proof -> proof -> proof val equal_intr_proof: term -> term -> proof -> proof -> proof val equal_elim_proof: term -> term -> proof -> proof -> proof val abstract_rule_proof: string * term -> proof -> proof val combination_proof: term -> term -> term -> term -> proof -> proof -> proof val could_unify: proof * proof -> bool type sorts_proof = (class * class -> proof) * (string * class listlist * class -> proof) val of_sort_proof: Sorts.algebra -> sorts_proof -> (typ * class -> proof) -> typ * sort -> proof list val axiom_proof: string -> term -> proof val oracle_proof: string -> term -> proof val shrink_proof: proof -> proof
(*rewriting on proof terms*) val add_prf_rrule: proof * proof -> theory -> theory val add_prf_rproc: (typ list -> term optionlist -> proof -> (proof * proof) option) -> theory -> theory val set_preproc: (theory -> proof -> proof) -> theory -> theory val apply_preproc: theory -> proof -> proof val forall_intr_variables_term: term -> term val forall_intr_variables: term -> proof -> proof val no_skel: proof val normal_skel: proof val rewrite_proof: theory -> (proof * proof) list *
(typ list -> term optionlist -> proof -> (proof * proof) option) list -> proof -> proof val rewrite_proof_notypes: (proof * proof) list *
(typ list -> term optionlist -> proof -> (proof * proof) option) list -> proof -> proof val rew_proof: theory -> proof -> proof
val reconstruct_proof: theory -> term -> proof -> proof val prop_of': term list -> proof -> term val prop_of: proof -> term val expand_name_empty: thm_header -> Thm_Name.P option val expand_proof: theory -> (thm_header -> Thm_Name.P option) -> proof -> proof
val export_enabled: unit -> bool val export_standard_enabled: unit -> bool val export_proof_boxes_required: theory -> bool val export_proof_boxes: proof_body list -> unit val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body val thm_proof: theory -> sorts_proof -> Thm_Name.P -> sort list -> term list ->
term -> (serial * proof_body future) list -> proof_body -> proof_body val unconstrain_thm_proof: theory -> sorts_proof -> sort list ->
term -> (serial * proof_body future) list -> proof_body -> term * proof_body val get_identity: sort list -> term list -> term -> proof ->
{serial: serial, theory_name: string, thm_name: Thm_Name.P} option val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.P type thm_id = {serial: serial, theory_name: string} val make_thm_id: serial * string -> thm_id val thm_header_id: thm_header -> thm_id val thm_id: thm -> thm_id val get_id: sort list -> term list -> term -> proof -> thm_id option val this_id: thm_id option -> thm_id -> bool val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} ->
proof list -> (thm_header * proof) list(*exception MIN_PROOF*) end
structure Proofterm : PROOFTERM = struct
(** datatype proof **)
val proof_serial = Counter.make ();
type thm_header =
{serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P,
prop: term, types: typ listoption};
datatype proof =
MinProof
| PBound of int
| Abst ofstring * typ option * proof
| AbsP ofstring * term option * proof
| op % of proof * term option
| op %% of proof * proof
| Hyp of term
| PAxm ofstring * term * typ listoption
| PClass of typ * class
| Oracle ofstring * term * typ listoption
| PThm of thm_header * thm_body and proof_body = PBody of
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
zboxes: ZTerm.zboxes,
zproof: zproof,
proof: proof} and thm_body =
Thm_Body of {open_proof: proof -> proof, body: proof_body future} and thm_node =
Thm_Node of {theory_name: string, thm_name: Thm_Name.T, prop: term,
body: proof_body future, export: unit lazy, consolidate: unit lazy};
type oracle = (string * Position.T) * term option; val oracle_ord: oracle ord =
prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord);
type thm = serial * thm_node; val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
exception MIN_PROOF of unit;
fun proof_of (PBody {proof, ...}) = proof; fun zproof_of (PBody {zproof, ...}) = zproof; val join_proof = Future.join #> proof_of;
fun map_proof_of f (PBody {oracles, thms, zboxes, zproof, proof}) =
PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = f proof};
fun thm_body body = Thm_Body {open_proof = I, body = Future.value body}; fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body; fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body);
fun rep_thm_node (Thm_Node args) = args; val thm_node_theory_name = #theory_name o rep_thm_node; val thm_node_name = #thm_name o rep_thm_node; val thm_node_prop = #prop o rep_thm_node; val thm_node_body = #body o rep_thm_node; val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms); val thm_node_export = #export o rep_thm_node; val thm_node_consolidate = #consolidate o rep_thm_node;
fun join_thms (thms: thm list) =
Future.joins (map (thm_node_body o #2) thms);
fun fold_proof_atoms all f = let funapp (Abst (_, _, prf)) = app prf
| app (AbsP (_, _, prf)) = app prf
| app (prf % _) = app prf
| app (prf1 %% prf2) = app prf1 #> app prf2
| app (prf as PThm ({serial = i, ...}, Thm_Body {body, ...})) = (fn (x, seen) => if Intset.member seen i then (x, seen) else letval (x', seen') =
(ifallthenapp (join_proof body) else I) (x, Intset.insert i seen) in (f prf x', seen') end)
| app prf = (fn (x, seen) => (f prf x, seen)); in fn prfs => fn x => #1 (fold app prfs (x, Intset.empty)) end;
fun fold_body_thms f = let funapp (PBody {thms, ...}) =
tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) => if Intset.member seen i then (x, seen) else let val thm_name = thm_node_name thm_node; val prop = thm_node_prop thm_node; val body = Future.join (thm_node_body thm_node); val (x', seen') = app body (x, Intset.insert i seen); in (f {serial = i, thm_name = thm_name, prop = prop, body = body} x', seen') end); in fn bodies => fn x => #1 (fold app bodies (x, Intset.empty)) end;
(* proof body *)
val union_oracles = Ord_List.union oracle_ord; val unions_oracles = Ord_List.unions oracle_ord;
val union_thms = Ord_List.union thm_ord; val unions_thms = Ord_List.unions thm_ord;
fun no_body_proofs (Abst (x, T, prf)) = Abst (x, T, no_body_proofs prf)
| no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf)
| no_body_proofs (prf % t) = no_body_proofs prf % t
| no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2
| no_body_proofs (PThm (header, Thm_Body {open_proof, body})) = let val PBody {zproof, proof, ...} = Future.join body; val body' = Future.value (no_proof_body zproof proof); val thm_body' = Thm_Body {open_proof = open_proof, body = body'}; in PThm (header, thm_body') end
| no_body_proofs a = a;
(** XML data representation **)
(* encode as zterm/zproof *)
fun proof_to_zproof thy = let val {ztyp, zterm} = ZTerm.zterm_cache thy; val ztvar = ztyp #> (fn ZTVar v => v);
fun zproof_const name prop typargs = let val vs = rev ((fold_types o fold_atyps) (insert (op =) o ztvar) prop []); val Ts = map ztyp typargs in ZConstp ((name, zterm prop), (ZTVars.make (vs ~~ Ts), ZVars.empty)) end;
fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => PClass (typ T, c)); fun map_proof_types_same typ = map_proof_terms_same (Term.map_types_same typ) typ;
fun map_proof_terms f g =
Same.commit (map_proof_terms_same (Same.function_eq (op =) f) (Same.function_eq (op =) g));
fun map_proof_types f =
Same.commit (map_proof_types_same (Same.function_eq (op =) f));
fun fold_proof_terms f (Abst (_, _, prf)) = fold_proof_terms f prf
| fold_proof_terms f (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f prf
| fold_proof_terms f (AbsP (_, NONE, prf)) = fold_proof_terms f prf
| fold_proof_terms f (prf % SOME t) = fold_proof_terms f prf #> f t
| fold_proof_terms f (prf % NONE) = fold_proof_terms f prf
| fold_proof_terms f (prf1 %% prf2) = fold_proof_terms f prf1 #> fold_proof_terms f prf2
| fold_proof_terms _ _ = I;
fun fold_proof_terms_types f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms_types f g prf
| fold_proof_terms_types f g (Abst (_, NONE, prf)) = fold_proof_terms_types f g prf
| fold_proof_terms_types f g (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms_types f g prf
| fold_proof_terms_types f g (AbsP (_, NONE, prf)) = fold_proof_terms_types f g prf
| fold_proof_terms_types f g (prf % SOME t) = fold_proof_terms_types f g prf #> f t
| fold_proof_terms_types f g (prf % NONE) = fold_proof_terms_types f g prf
| fold_proof_terms_types f g (prf1 %% prf2) =
fold_proof_terms_types f g prf1 #> fold_proof_terms_types f g prf2
| fold_proof_terms_types _ g (PAxm (_, _, SOME Ts)) = fold g Ts
| fold_proof_terms_types _ g (PClass (T, _)) = g T
| fold_proof_terms_types _ g (Oracle (_, _, SOME Ts)) = fold g Ts
| fold_proof_terms_types _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts
| fold_proof_terms_types _ _ _ = I;
fun maxidx_proof prf = fold_proof_terms_types Term.maxidx_term Term.maxidx_typ prf;
(*Abstraction of a proof term over its occurrences of v, which must contain no loose bound variables.
The resulting proof term is ready to become the body of an Abst.*)
fun abstract_over v = let fun term lev u = if v aconv u then Bound lev else
(case u of
Abs (a, T, t) => Abs (a, T, term (lev + 1) t)
| t $ u =>
(term lev t $ Same.commit (term lev) u handle Same.SAME => t $ term lev u)
| _ => raise Same.SAME);
fun proof lev (AbsP (a, t, p)) =
(AbsP (a, Same.map_option (term lev) t, Same.commit (proof lev) p) handle Same.SAME => AbsP (a, t, proof lev p))
| proof lev (Abst (a, T, p)) = Abst (a, T, proof (lev + 1) p)
| proof lev (p %% q) = (proof lev p %% Same.commit (proof lev) q handle Same.SAME => p %% proof lev q)
| proof lev (p % t) =
(proof lev p % Option.map (Same.commit (term lev)) t handle Same.SAME => p % Same.map_option (term lev) t)
| proof _ _ = raise Same.SAME;
in Same.commit (proof 0) end;
(*increments a proof term's non-local bound variables required when moving a proof term within abstractions inc is increment for bound variables
lev is level at which a bound variable is considered 'loose'*)
fun incr_bv_same incP inct = if incP = 0 andalso inct = 0 then fn _ => fn _ => Same.same else let val term = Term.incr_bv_same inct;
fun incr_boundvars incP inct = incr_bv incP inct 0 0;
fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k
| prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k)
| prf_loose_bvar1 (_ % NONE) _ = true
| prf_loose_bvar1 (AbsP (_, SOME t, prf)) k = loose_bvar1 (t, k) orelse prf_loose_bvar1 prf k
| prf_loose_bvar1 (AbsP (_, NONE, _)) _ = true
| prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1)
| prf_loose_bvar1 _ _ = false;
fun prf_loose_Pbvar1 (PBound i) k = i = k
| prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k
| prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k
| prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1)
| prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k
| prf_loose_Pbvar1 _ _ = false;
fun prf_add_loose_bnos plev _ (PBound i) (is, js) = if i < plev then (is, js) else (insert (op =) (i-plev) is, js)
| prf_add_loose_bnos plev tlev (prf1 %% prf2) p =
prf_add_loose_bnos plev tlev prf2
(prf_add_loose_bnos plev tlev prf1 p)
| prf_add_loose_bnos plev tlev (prf % opt) (is, js) =
prf_add_loose_bnos plev tlev prf
(case opt of
NONE => (is, insert (op =) ~1 js)
| SOME t => (is, add_loose_bnos (t, tlev, js)))
| prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) =
prf_add_loose_bnos (plev+1) tlev prf
(case opt of
NONE => (is, insert (op =) ~1 js)
| SOME t => (is, add_loose_bnos (t, tlev, js)))
| prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p =
prf_add_loose_bnos plev (tlev+1) prf p
| prf_add_loose_bnos _ _ _ _ = ([], []);
(* substitutions *)
local
fun conflicting_tvarsT envT =
Term.fold_atyps
(fn T => fn instT =>
(case T of
TVar (v as (_, S)) => if TVars.defined instT v orelse can (Type.lookup envT) v then instT else TVars.add (v, Logic.dummy_tfree S) instT
| _ => instT));
fun conflicting_tvars env =
Term.fold_aterms
(fn t => fn inst =>
(case t of
Var (v as (_, T)) => if Vars.defined inst v orelse can (Envir.lookup env) v then inst else Vars.add (v, Free ("dummy", T)) inst
| _ => inst));
fun del_conflicting_tvars envT ty =
Term_Subst.instantiateT (TVars.build (conflicting_tvarsT envT ty)) ty;
fun del_conflicting_vars env tm = let val instT =
TVars.build (tm |> Term.fold_types (conflicting_tvarsT (Envir.type_env env))); val inst = Vars.build (tm |> conflicting_tvars env); in Term_Subst.instantiate (instT, inst) tm end;
in
fun norm_proof envir = let val tyenv = Envir.type_env envir; fun msg s = warning ("type conflict in norm_proof:\n" ^ s); fun norm_term_same t = Envir.norm_term_same envir t handleTYPE (s, _, _) =>
(msg s; Envir.norm_term_same envir (del_conflicting_vars envir t)); fun norm_type_same T = Envir.norm_type_same tyenv T handleTYPE (s, _, _) =>
(msg s; Envir.norm_type_same tyenv (del_conflicting_tvars tyenv T)); fun norm_types_same Ts = Envir.norm_types_same tyenv Ts handleTYPE (s, _, _) =>
(msg s; Envir.norm_types_same tyenv (map (del_conflicting_tvars tyenv) Ts));
fun thaw names names' (t $ u) =
thaw names names' t $ thaw names names' u
| thaw names names' (Abs (s, T, t)) =
Abs (s, thawT names' T, thaw names names' t)
| thaw _ names' (Const (s, T)) = Const (s, thawT names' T)
| thaw names names' (Free (s, T)) = letval T' = thawT names' T in
(case AList.lookup (op =) names s of
NONE => Free (s, T')
| SOME ixn => Var (ixn, T')) end
| thaw _ names' (Var (ixn, T)) = Var (ixn, thawT names' T)
| thaw _ _ t = t;
in
fun freeze_thaw_prf prf = let val (fs, Tfs, vs, Tvs) = fold_proof_terms_types
(fn t => fn (fs, Tfs, vs, Tvs) =>
(Term.add_free_names t fs, Term.add_tfree_names t Tfs,
Term.add_var_names t vs, Term.add_tvar_names t Tvs))
(fn T => fn (fs, Tfs, vs, Tvs) =>
(fs, Term.add_tfree_namesT T Tfs,
vs, Term.add_tvar_namesT T Tvs))
prf ([], [], [], []); val names = vs ~~ Name.variant_list fs (map fst vs); val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs); val rnames = map swap names; val rnames' = map swap names'; in
(map_proof_terms (freeze names names') (frzT names') prf,
map_proof_terms (thaw rnames rnames') (thawT rnames')) end;
end;
(** inference rules **)
(* trivial implication *)
val trivial_proof = AbsP ("H", NONE, PBound 0);
(* implication introduction *)
fun gen_implies_intr_proof f h prf = let fun abshyp i (Hyp t) = if h aconv t then PBound i elseraise Same.SAME
| abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
| abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i + 1) prf)
| abshyp i (prf % t) = abshyp i prf % t
| abshyp i (prf1 %% prf2) =
(abshyp i prf1 %% abshyph i prf2 handle Same.SAME => prf1 %% abshyp i prf2)
| abshyp _ _ = raise Same.SAME and abshyph i prf = (abshyp i prf handle Same.SAME => prf); in
AbsP ("H", f h, abshyph 0 prf) end;
val implies_intr_proof = gen_implies_intr_proof (K NONE); val implies_intr_proof' = gen_implies_intr_proof SOME;
(* forall introduction *)
fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, abstract_over v prf);
fun forall_intr_proof' v prf = letval (a, T) = (case v of Var ((a, _), T) => (a, T) | Free (a, T) => (a, T)) in forall_intr_proof (a, v) (SOME T) prf end;
(* varify *)
fun varifyT_proof names prf = if null names then prf else let val tab = TFrees.make names; val typ =
Term.map_atyps_same
(fn TFree v =>
(case TFrees.lookup tab v of
NONE => raise Same.SAME
| SOME w => TVar w)
| _ => raise Same.SAME); in Same.commit (map_proof_types_same typ) prf end;
(* freeze *)
fun legacy_freezeT t prf =
(caseType.legacy_freezeT t of
NONE => prf
| SOME f => letval frzT = map_type_tvar (Same.function f) in map_proof_terms (map_types frzT) frzT prf end);
(* rotate assumptions *)
fun rotate_proof Bs Bi' params asms m prf = let val i = length asms; val j = length Bs; in
mk_AbsP (Bs @ [Bi']) (proof_combP (prf, map PBound
(j downto 1) @ [mk_Abst params (mk_AbsP asms
(proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)), map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))])) end;
(* permute premises *)
fun permute_prems_proof prems' j k prf = letval n = length prems' in
mk_AbsP prems'
(proof_combP (prf, map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k)))) end;
(* generalization *)
fun generalize_proof (tfrees, frees) idx prop prf = let val gen = if Names.is_empty frees then [] else
fold_aterms (fn Free (x, T) => Names.defined frees x ? insert (op =) (x, T) | _ => I)
(Term_Subst.generalize (tfrees, Names.empty) idx prop) []; in
prf
|> Same.commit (map_proof_terms_same
(Term_Subst.generalize_same (tfrees, Names.empty) idx)
(Term_Subst.generalizeT_same tfrees idx))
|> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen
|> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen end;
fun mk_app b (i, j, p) = if b then (i - 1, j, p %% PBound i) else (i, j - 1, p %> Bound j);
fun lift Ts bs i j (Const ("Pure.imp", _) $ A $ B) =
AbsP ("H", NONE (*A*), lift Ts (true::bs) (i + 1) j B)
| lift Ts bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) =
Abst (a, NONE (*T*), lift (T::Ts) (false::bs) i (j + 1) t)
| lift Ts bs i j _ =
proof_combP (Same.commit (proof (rev Ts) 0) prf, map (fn k => (#3 (fold_rev mk_app bs (i - 1, j - 1, PBound k)))) (i + k - 1 downto i)); in mk_AbsP prems (lift [] [] 0 0 gprop) end;
fun incr_indexes i =
Same.commit
(map_proof_terms_same
(Logic.incr_indexes_operation {fixed = [], Ts = [], inc = i, level = 0})
(Logic.incr_tvar_same i));
(* proof by assumption *)
fun mk_asm_prf C i m = let fun imp_prf _ i 0 = PBound i
| imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
| imp_prf _ i _ = PBound i; fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
| all_prf t = imp_prf t (~i) m in all_prf C end;
fun assumption_proof Bs Bi n prf =
mk_AbsP Bs (proof_combP (prf, map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
(* composition of object rule with proof state *)
fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) =
AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k))
| flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) =
Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k))
| flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
fun bicompose_proof env smax flatten Bs As A oldAs n m rprf sprf = let val normt = Envir.norm_term env; val normp = norm_proof_remove_types env;
val lb = length Bs; val la = length As;
fun proof p =
mk_AbsP (map normt (Bs @ As)) (proof_combP (sprf, map PBound (lb + la - 1 downto la)) %%
proof_combP (p, (if n>0 then [mk_asm_prf (the A) n m] else []) @ map (if flatten then flatten_params_proof 0 0 n else PBound o snd)
(oldAs ~~ (la - 1 downto 0)))); in if Envir.is_empty env then proof rprf elseif Envir.above env smax then proof (normp rprf) else normp (proof rprf) end;
(** sort constraints within the logic **)
type sorts_proof = (class * class -> proof) * (string * class listlist * class -> proof);
fun of_sort_proof algebra (classrel_proof, arity_proof) hyps =
Sorts.of_sort_derivation algebra
{class_relation = fn _ => fn _ => fn (prf, c1) => fn c2 => if c1 = c2 then prf else classrel_proof (c1, c2) %% prf,
type_constructor = fn (a, _) => fn dom => fn c => letval Ss = map (map snd) dom and prfs = maps (map fst) dom in proof_combP (arity_proof (a, Ss, c), prfs) end,
type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)};
fun unconstrainT_proof algebra sorts_proof (ucontext: Logic.unconstrain_context) = let val typ = #typ_operation ucontext {strip_sorts = true}; val typ_sort = #typ_operation ucontext {strip_sorts = false};
fun hyps T =
(case AList.lookup (op =) (#constraints ucontext) T of
SOME t => Hyp t
| NONE => raise Fail "unconstrainT_proof: missing constraint");
fun class (T, c) = letval T' = Same.commit typ_sort T in the_single (of_sort_proof algebra sorts_proof hyps (T', [c])) end; in
Same.commit (map_proof_same (Term.map_types_same typ) typ class)
#> fold_rev (implies_intr_proof o #2) (#constraints ucontext) end;
(** axioms and theorems **)
val add_type_variables = (fold_types o fold_atyps) (insert (op =)); fun type_variables_of t = rev (add_type_variables t []);
val add_variables = fold_aterms (fn a => (is_Var a orelse is_Free a) ? insert (op =) a); fun variables_of t = rev (add_variables t []);
fun test_args _ [] = true
| test_args is (Bound i :: ts) = not (member (op =) is i) andalso test_args (i :: is) ts
| test_args _ _ = false;
fun vars_of t = map Var (build_rev (Term.add_vars t));
fun add_funvars Ts (vs, t) = if is_fun (fastype_of1 (Ts, t)) then
union (op =) vs (map_filter (fn Var (ixn, T) => if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)) else vs;
fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) =
add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u)
| add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) =
add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
| add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
| add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) and add_npvars' Ts (vs, t) =
(case strip_comb t of
(Var (ixn, _), ts) => if test_args [] ts then vs else Library.foldl (add_npvars' Ts)
(AList.update (op =) (ixn,
Library.foldl (add_funvars Ts) ((these ooo AList.lookup) (op =) vs ixn, ts)) vs, ts)
| (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
| (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
| prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t
| prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []);
fun is_proj t = let fun is_p i t =
(case strip_comb t of
(Bound _, []) => false
| (Bound j, ts) => j >= i orelse exists (is_p i) ts
| (Abs (_, _, u), _) => is_p (i+1) u
| (_, ts) => exists (is_p i) ts) in
(case strip_abs_body t of
Bound _ => true
| t' => is_p 0 t') end;
fun prop_args prop = let val needed_vars =
union (op =) (Library.foldl (uncurry (union (op =)))
([], map (uncurry (insert (op =))) (add_npvars truetrue [] ([], prop))))
(prop_vars prop); in
variables_of prop |> map
(fn var as Var (ixn, _) => if member (op =) needed_vars ixn then SOME var else NONE
| free => SOME free) end;
fun const_proof mk name prop = let val args = prop_args prop; val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop; val head = mk (name, prop1, NONE); in proof_combP (proof_combt' (head, args), map PClass outer_constraints) end;
val axiom_proof = const_proof PAxm; val oracle_proof = const_proof Oracle;
val shrink_proof = let fun shrink ls lev (prf as Abst (a, T, body)) = letval (b, is, ch, body') = shrink ls (lev+1) body in (b, is, ch, if ch then Abst (a, T, body') else prf) end
| shrink ls lev (prf as AbsP (a, t, body)) = letval (b, is, ch, body') = shrink (lev::ls) lev body in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is,
ch, if ch then AbsP (a, t, body') else prf) end
| shrink ls lev prf = letval (is, ch, _, prf') = shrink' ls lev [] [] prf in (false, is, ch, prf') end and shrink' ls lev ts prfs (prf as prf1 %% prf2) = let val p as (_, is', ch', prf') = shrink ls lev prf2; val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1 in (union (op =) is is', ch orelse ch', ts', if ch orelse ch' then prf'' %% prf'else prf) end
| shrink' ls lev ts prfs (prf as prf1 % t) = letval (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1 in (is, ch orelse ch', ts', if ch orelse ch' then prf' % t' else prf) end
| shrink' ls lev ts prfs (prf as PBound i) =
(ifexists (fn SOME (Bound j) => lev-j <= nth ls i | _ => true) ts
orelse has_duplicates (op =)
(Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
| shrink' _ _ ts _ (Hyp t) = ([], false, map (pair false) ts, Hyp t)
| shrink' _ _ ts _ (prf as MinProof) = ([], false, map (pair false) ts, prf)
| shrink' _ _ ts _ (prf as PClass _) = ([], false, map (pair false) ts, prf)
| shrink' _ _ ts prfs prf = let val prop =
(case prf of
PAxm (_, prop, _) => prop
| Oracle (_, prop, _) => prop
| PThm ({prop, ...}, _) => prop
| _ => raise Fail "shrink: proof not in normal form"); val vs = vars_of prop; val (ts', ts'') = chop (length vs) ts; val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts'; val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
insert (op =) ixn
(case AList.lookup (op =) insts ixn of
SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
| _ => union (op =) ixns ixns'))
(needed prop ts'' prfs, add_npvars falsetrue [] ([], prop)); val insts' = map
(fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
| (_, x) => (false, x)) insts in ([], false, insts' @ map (pair false) ts'', prf) end and needed (Const ("Pure.imp", _) $ t $ u) ts ((b, _, _, _)::prfs) =
union (op =) (if b thenmap (fst o dest_Var) (vars_of t) else []) (needed u ts prfs)
| needed (Var (ixn, _)) (_::_) _ = [ixn]
| needed _ _ _ = []; in fn prf => #4 (shrink [] 0 prf) end;
(** axioms for equality **)
local val thy = Sign.local_path (Context.the_global_context ()) in
fun combination_proof f g t u prf1 prf2 = let val f' = Envir.beta_norm f; val g' = Envir.beta_norm g; val ax = if check_comb prf1 then combination_axm % NONE % NONE elseif is_reflexive_proof prf1 then combination_axm %> remove_types f' % NONE else combination_axm %> remove_types f' %> remove_types g' val t' =
(case Term.head_of f' of
Abs _ => SOME (remove_types t)
| Var _ => SOME (remove_types t)
| _ => NONE); val u' =
(case Term.head_of g' of
Abs _ => SOME (remove_types u)
| Var _ => SOME (remove_types u)
| _ => NONE); in ax % t' % u' %% prf1 %% prf2 end;
(** rewriting on proof terms **)
(* simple first order matching functions for terms and proofs (see pattern.ML) *)
exception PMatch;
fun flt (i: int) = filter (fn n => n < i);
fun fomatch Ts tymatch j instsp p = let fun mtch (instsp as (tyinsts, insts)) = fn
(Var (ixn, T), t) => if j>0 andalso not (null (flt j (loose_bnos t))) thenraise PMatch else (tymatch (tyinsts, fn () => (T, fastype_of1 (Ts, t))),
(ixn, t) :: insts)
| (Free (a, T), Free (b, U)) => if a=b then (tymatch (tyinsts, K (T, U)), insts) elseraise PMatch
| (Const (a, T), Const (b, U)) => if a=b then (tymatch (tyinsts, K (T, U)), insts) elseraise PMatch
| (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
| (Bound i, Bound j) => if i=j then instsp elseraise PMatch
| _ => raise PMatch in mtch instsp (apply2 Envir.beta_eta_contract p) end;
fun match_proof Ts tymatch = let fun optmatch _ inst (NONE, _) = inst
| optmatch _ _ (SOME _, NONE) = raise PMatch
| optmatch mtch inst (SOME x, SOME y) = mtch inst (x, y)
fun matcht Ts j (pinst, tinst) (t, u) =
(pinst, fomatch Ts tymatch j tinst (t, Envir.beta_norm u)); fun matchT (pinst, (tyinsts, insts)) p =
(pinst, (tymatch (tyinsts, K p), insts)); fun matchTs inst (Ts, Us) = Library.foldl (uncurry matchT) (inst, Ts ~~ Us);
fun get_rew_data thy = letval (rules, procs) = #1 (Data.get thy) in (map #2 rules, map #2 procs) end;
fun rew_proof thy = rewrite_prf fst (get_rew_data thy);
fun add_prf_rrule r = (Data.map o apfst o apfst) (cons (stamp (), r)); fun add_prf_rproc p = (Data.map o apfst o apsnd) (cons (stamp (), p));
fun set_preproc f = (Data.map o apsnd) (K (SOME f)); fun apply_preproc thy = (case #2 (Data.get thy) of NONE => I | SOME f => f thy);
(** reconstruction of partial proof terms **)
fun forall_intr_variables_term prop = fold_rev Logic.all (variables_of prop) prop; fun forall_intr_variables prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
local
fun app_types shift prop Ts prf = let val inst = type_variables_of prop ~~ Ts; fun subst_same A =
(case AList.lookup (op =) inst A of SOME T => T | NONE => raise Same.SAME); val subst_type_same =
Term.map_atyps_same
(fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A); in Same.commit (map_proof_types_same subst_type_same) prf end;
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 (Term.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 thy 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) = letval (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'') => letval (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) = letval (t', U, vTs1, env1) = infer_type thy 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) => letval env3 = unifyT thy env2 T U in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) end
| (u, prf, cnstrts, env2, vTs2) => letval (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') => letval (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, types = 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 PClass C) =
mk_cnstrts_atom env vTs (Logic.mk_of_class 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 _ _ _ _ MinProof = raise MIN_PROOF () 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) = letval 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 thy cs bigenv = let fun search _ [] =
error ("Unsolvable constraints:\n" ^
Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
Pretty.item (Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
(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.Theory thy) (tn1, tn2) env, ps) handle Pattern.Unif => cantunify thy (tn1, tn2) else letval (cs', env') = decompose thy [] (tn1, tn2) env inif 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 thy (upd_constrs env cs') (Envir.merge (bigenv, env)) end;
in
(* reconstruction of proofs *)
fun reconstruct_proof thy prop cprf = let val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop); val (t, prf, cs, env, _) = make_constraints_cprf thy
(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 thy cs' env; in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof;
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, types = SOME Ts, ...}, _)) = prop_of_atom prop Ts
| prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
| prop_of0 _ (PClass C) = Logic.mk_of_class 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_name_empty (header: thm_header) = if Thm_Name.is_empty (#1 (#thm_name header)) then SOME Thm_Name.none else NONE;
fun expand_proof thy expand_name prf = let fun expand seen maxidx (AbsP (s, t, prf)) = letval (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', AbsP (s, t, prf')) end
| expand seen maxidx (Abst (s, T, prf)) = letval (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', Abst (s, T, prf')) end
| expand seen maxidx (prf1 %% prf2) = let val (seen', maxidx', prf1') = expand seen maxidx prf1; val (seen'', maxidx'', prf2') = expand seen' maxidx' prf2; in (seen'', maxidx'', prf1' %% prf2') end
| expand seen maxidx (prf % t) = letval (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', prf' % t) end
| expand seen maxidx (prf as PThm (header, thm_body)) = letval {serial, command_pos, theory_name, thm_name, prop, types} = header in
(case expand_name header of
SOME thm_name' => if #1 (#1 thm_name') = "" andalso is_some types then let val (seen', maxidx', prf') =
(case Inttab.lookup seen serial of
NONE => let val prf1 =
thm_body_proof_open thm_body
|> reconstruct_proof thy prop
|> forall_intr_variables prop; val (seen1, maxidx1, prf2) = expand_init seen prf1 val seen2 = seen1 |> Inttab.update (serial, (maxidx1, prf2)); in (seen2, maxidx1, prf2) end
| SOME (maxidx1, prf1) => (seen, maxidx1, prf1)); val prf'' = prf'
|> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop (the types); in (seen', maxidx' + maxidx + 1, prf'') end elseif thm_name' <> thm_name then
(seen, maxidx,
PThm (thm_header serial command_pos theory_name thm_name' prop types, thm_body)) else (seen, maxidx, prf)
| NONE => (seen, maxidx, prf)) end
| expand seen maxidx prf = (seen, maxidx, prf) and expand_init seen prf = expand seen (maxidx_proof prf ~1) prf;
in #3 (expand_init Inttab.empty prf) end;
end;
(** promises **)
fun fulfill_norm_proof thy ps body0 = let val _ = consolidate_bodies (map #2 ps @ [body0]); val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof, proof = proof0} = body0; val oracles =
unions_oracles
(fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]); val thms =
unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]); val zboxes =
ZTerm.unions_zboxes
(fold (fn (_, PBody {zboxes, ...}) => not (null zboxes) ? cons zboxes) ps [zboxes0]); val proof = rew_proof thy proof0; in
PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof} end;
fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body = let fun fulfill () =
postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)); in if null promises then Future.map postproc body elseif Future.is_finished body andalso length promises = 1 then
Future.map (fn _ => fulfill ()) (snd (hd promises)) else
(singleton o Future.forks)
{name = "Proofterm.fulfill_proof_future", group = NONE,
deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 1,
interrupts = true}
fulfill end;
(** theorems **)
(* PThm nodes *)
fun prune_body body = if Options.default_bool "prune_proofs" then Future.map no_proof body else body;
fun export_enabled () = Options.default_bool "export_proofs"; fun export_standard_enabled () = Options.default_bool "export_standard_proofs";
fun export_proof_boxes_required thy =
Context.theory_long_name thy = Context.PureN orelse
(export_enabled () andalso not (export_standard_enabled ()));
fun export_proof_boxes bodies = let fun export_thm (i, thm_node) boxes = if Inttab.defined boxes i then boxes else
boxes
|> Inttab.update (i, thm_node_export thm_node)
|> fold export_thm (thm_node_thms thm_node);
fun export_body (PBody {thms, ...}) = fold export_thm thms;
val exports = Inttab.build (fold export_body bodies) |> Inttab.dest; inList.app (Lazy.force o #2) exports end;
local
fun export_proof thy i prop0 proof0 = let val {typargs, args, prop, proof} =
ZTerm.standard_vars Name.context
(ZTerm.zterm_of thy prop0, SOME (proof_to_zproof thy (no_thm_names proof0))); val xml = (typargs, (args, (prop, the proof))) |> let open XML.Encode Term_XML.Encode; val encode_tfrees = list (pair string sort); val encode_frees = list (pair string ZTerm.encode_ztyp); val encode_term = ZTerm.encode_zterm {typed_vars = false}; val encode_proof = ZTerm.encode_zproof {typed_vars = false}; in pair encode_tfrees (pair encode_frees (pair encode_term encode_proof)) end; in
Export.export_params (Context.Theory thy)
{theory_name = Context.theory_long_name thy,
binding = Path.binding0 (Path.make ["proofs", string_of_int i]),
executable = false,
compress = true,
strict = false} xml end;
fun prepare_thm_proof unconstrain thy sorts_proof
(name, pos) shyps hyps concl promises
(PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zproof0, proof = proof0}) = let val named = not (Thm_Name.is_empty name);
val prop = Logic.list_implies (hyps, concl); val args = prop_args prop;
val (ucontext as {typ_operation, ...}, prop1) = Logic.unconstrainT shyps prop;
val proofs = get_proofs_level (); val (zproof1, zboxes1) = if zproof_enabled proofs then
ZTerm.add_box_proof {unconstrain = unconstrain} thy hyps concl zproof0 zboxes0 else (ZNop, []); val proof1 = if proof_enabled proofs then fold_rev implies_intr_proof hyps proof0 else MinProof;
fun new_prf () = let val i = proof_serial (); val unconstrainT = unconstrainT_proof (Sign.classes_of thy) sorts_proof ucontext; val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy); val body1 =
{oracles = oracles0, thms = thms0, zboxes = [], zproof = ZNop, proof = proof1}; in (i, fulfill_proof_future thy promises postproc (Future.value (PBody body1))) end;
val (i, body') = (*somewhat non-deterministic proof boxes!*) if export_enabled () then new_prf () else
(case strip_combt (proof_head_of proof0) of
(PThm ({serial = ser, thm_name = (a, _), prop = prop', types = NONE, ...}, thm_body'), args') => if (#1 a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then let val Thm_Body {body = body', ...} = thm_body'; val i = if #1 a = "" andalso named then proof_serial () else ser; in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end else new_prf ()
| _ => new_prf ());
val exp_proof = Future.map proof_of body'; val open_proof = not named ? rew_proof thy; fun export_body () =
Future.join exp_proof
|> open_proof
|> reconstruct_proof thy prop1
|> apply_preproc thy
|> export_proof thy i prop1;
val export = if export_enabled () then
Lazy.lazy (fn () =>
(case Exn.capture_body export_body of
Exn.Res res => res
| Exn.Exn exn => if Exn.is_interrupt_breakdown exn then raise Fail ("Resource problems while exporting proof " ^ string_of_int i) else Exn.reraise exn)) else no_export;
val thm_body = prune_body body'; val theory_name = Context.theory_long_name thy; val thm = (i, make_thm_node theory_name name prop1 thm_body export);
val header = thm_header i (Position.thread_data ()) theory_name (name, pos) prop1 NONE; val head = PThm (header, Thm_Body {open_proof = open_proof, body = thm_body}); val argst = if unconstrain then
(Same.commit o Same.map o Same.map_option o Term.map_types_same)
(typ_operation {strip_sorts = true}) args else args; val argsP = if unconstrain then [] elsemap PClass (#outer_constraints ucontext) @ map Hyp hyps; val proof2 = proof_combP (proof_combt' (head, argst), argsP);
fun proof_boxes {included, excluded} proofs = let fun boxes_of (Abst (_, _, prf)) = boxes_of prf
| boxes_of (AbsP (_, _, prf)) = boxes_of prf
| boxes_of (prf % _) = boxes_of prf
| boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2
| boxes_of (PThm (header as {serial = i, ...}, thm_body)) =
(fn boxes => letval thm_id = thm_header_id header in if Inttab.defined boxes i orelse (excluded thm_id andalso not (included thm_id)) then boxes else let val prf' = thm_body_proof_open thm_body; val boxes' = Inttab.update (i, (header, prf')) boxes; in boxes_of prf' boxes'end end)
| boxes_of MinProof = raise MIN_PROOF ()
| boxes_of _ = I; in Inttab.fold_rev (cons o #2) (Inttab.build (fold boxes_of proofs)) [] end;
end;
structure Basic_Proofterm = struct datatype proof = datatype Proofterm.proof datatype proof_body = datatype Proofterm.proof_body val op %> = Proofterm.%> end;
open Basic_Proofterm;
Messung V0.5 in Prozent
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.36Bemerkung:
(vorverarbeitet am 2026-04-27)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
