(* 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
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.28 Sekunden
(vorverarbeitet)
¤
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 ist noch experimentell.
