(* Title: Pure/thm.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Makarius
The very core of Isabelle's Meta Logic: certified types and terms, derivations, theorems, inference rules (including lifting and resolution), oracles.
*)
infix 0 RS RSN;
signature BASIC_THM = sig type ctyp type cterm
exception CTERM ofstring * cterm list type thm type conv = cterm -> thm
exception THM ofstring * int * thm list val RSN: thm * (int * thm) -> thm val RS: thm * thm -> thm end;
signature THM = sig
include BASIC_THM (*certified types*) val typ_of: ctyp -> typ val global_ctyp_of: theory -> typ -> ctyp val ctyp_of: Proof.context -> typ -> ctyp val dest_ctyp: ctyp -> ctyp list val dest_ctypN: int -> ctyp -> ctyp val make_ctyp: ctyp -> ctyp list -> ctyp val maxidx_of_ctyp: ctyp -> int (*certified terms*) val term_of: cterm -> term val typ_of_cterm: cterm -> typ val ctyp_of_cterm: cterm -> ctyp val maxidx_of_cterm: cterm -> int val global_cterm_of: theory -> term -> cterm val cterm_of: Proof.context -> term -> cterm val renamed_term: term -> cterm -> cterm val fast_term_ord: cterm ord val term_ord: cterm ord val dest_comb: cterm -> cterm * cterm val dest_fun: cterm -> cterm val dest_arg: cterm -> cterm val dest_fun2: cterm -> cterm val dest_arg1: cterm -> cterm val dest_abs_fresh: string -> cterm -> cterm * cterm val dest_abs_global: cterm -> cterm * cterm val rename_tvar: indexname -> ctyp -> ctyp val free: string * ctyp -> cterm val var: indexname * ctyp -> cterm val apply: cterm -> cterm -> cterm val lambda_name: string * cterm -> cterm -> cterm val lambda: cterm -> cterm -> cterm val adjust_maxidx_cterm: int -> cterm -> cterm val incr_indexes_cterm: int -> cterm -> cterm valmatch: cterm * cterm -> ctyp TVars.table * cterm Vars.table val first_order_match: cterm * cterm -> ctyp TVars.table * cterm Vars.table (*theorems*) val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_ctyps: {hyps: bool} ->
('a -> typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_cterms: {hyps: bool} ->
('a -> term -> bool) -> (cterm -> 'a -> 'a) -> thm -> 'a -> 'a val terms_of_tpairs: (term * term) list -> term list val full_prop_of: thm -> term val theory_id: thm -> Context.theory_id val theory_name: {long: bool} -> thm -> string val theory_long_name: thm -> string val theory_base_name: thm -> string val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int val shyps_of: thm -> sort Ord_List.T val hyps_of: thm -> term list val prop_of: thm -> term val tpairs_of: thm -> (term * term) list val concl_of: thm -> term val prems_of: thm -> term list val take_prems_of: int -> thm -> term list val nprems_of: thm -> int val no_prems: thm -> bool val one_prem: thm -> bool val prem_of: thm -> int -> term val major_prem_of: thm -> term val cprop_of: thm -> cterm val cprem_of: thm -> int -> cterm val cconcl_of: thm -> cterm val cprems_of: thm -> cterm list val take_cprems_of: int -> thm -> cterm list val chyps_of: thm -> cterm list val thm_ord: thm ord
exception CONTEXT ofstring * ctyp list * cterm list * thm list * Context.generic option val theory_of_cterm: cterm -> theory val theory_of_thm: thm -> theory val trim_context_ctyp: ctyp -> ctyp val trim_context_cterm: cterm -> cterm val transfer_ctyp: theory -> ctyp -> ctyp val transfer_ctyp': Proof.context -> ctyp -> ctyp val transfer_ctyp'': Context.generic -> ctyp -> ctyp val transfer_cterm: theory -> cterm -> cterm val transfer_cterm': Proof.context -> cterm -> cterm val transfer_cterm'': Context.generic -> cterm -> cterm val transfer: theory -> thm -> thm val transfer': Proof.context -> thm -> thm val transfer'': Context.generic -> thm -> thm val join_transfer: theory -> thm -> thm val join_transfer_context: Proof.context * thm -> Proof.context * thm val renamed_prop: term -> thm -> thm val weaken: cterm -> thm -> thm val weaken_sorts: sort list -> cterm -> cterm val proof_bodies_of: thm list -> proof_body list val proof_body_of: thm -> proof_body val zproof_of: thm -> zproof val proof_of: thm -> proof val reconstruct_proof_of: thm -> Proofterm.proof val consolidate: thm list -> unit val expose_proofs: theory -> thm list -> unit val expose_proof: theory -> thm -> unit val future: thm future -> cterm -> thm val thm_deps: thm -> Proofterm.thm Ord_List.T val extra_shyps: thm -> sort list val strip_shyps: thm -> thm val derivation_closed: thm -> bool val derivation_name: thm -> Thm_Name.T val derivation_id: thm -> Proofterm.thm_id option val raw_derivation_name: thm -> Thm_Name.P val expand_name: thm -> Proofterm.thm_header -> Thm_Name.P option val name_derivation: Thm_Name.P -> thm -> thm val close_derivation: Position.T -> thm -> thm val trim_context: thm -> thm val axiom: theory -> string -> thm val all_axioms_of: theory -> (string * thm) list val get_tags: thm -> Properties.T val map_tags: (Properties.T -> Properties.T) -> thm -> thm val norm_proof: thm -> thm val adjust_maxidx_thm: int -> thm -> thm (*type classes*) val the_classrel: theory -> class * class -> thm val the_arity: theory -> string * sort list * class -> thm val sorts_zproof: theory -> ZTerm.sorts_proof val sorts_proof: theory -> Proofterm.sorts_proof (*oracles*) val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory val oracle_space: theory -> Name_Space.T val pretty_oracle: Proof.context -> string -> Pretty.T val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list val check_oracle: Proof.context -> xstring * Position.T -> string (*inference rules*) val assume: cterm -> thm (*exception THM*) val assume_cterm: cterm -> thm (*exception CTERM*) val implies_intr: cterm -> thm -> thm val implies_elim: thm -> thm -> thm val forall_intr: cterm -> thm -> thm val forall_elim: cterm -> thm -> thm val reflexive: cterm -> thm val symmetric: thm -> thm val transitive: thm -> thm -> thm val beta_conversion: bool -> conv val eta_conversion: conv val eta_long_conversion: conv val abstract_rule: string -> cterm -> thm -> thm val combination: thm -> thm -> thm val equal_intr: thm -> thm -> thm val equal_elim: thm -> thm -> thm val solve_constraints: thm -> thm val flexflex_rule: Proof.context option -> thm -> thm Seq.seq val generalize: Names.set * Names.set -> int -> thm -> thm val generalize_cterm: Names.set * Names.set -> int -> cterm -> cterm val generalize_ctyp: Names.set -> int -> ctyp -> ctyp val instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm val instantiate_beta: ctyp TVars.table * cterm Vars.table -> thm -> thm val instantiate_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm val instantiate_beta_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm val trivial: cterm -> thm val of_class: ctyp * class -> thm val unconstrainT: thm -> thm val varifyT_global': TFrees.set -> thm -> ((string * sort) * (indexname * sort)) list * thm val varifyT_global: thm -> thm val legacy_freezeT: thm -> thm val plain_prop_of: thm -> term val get_zproof_serials: theory -> serial list val get_zproof: theory -> serial ->
{name: Thm_Name.P, thm: thm, zboxes: ZTerm.zboxes, zproof: zproof} option val store_zproof: Thm_Name.P -> thm -> theory -> thm * theory val dest_state: thm * int -> (term * term) list * term list * term * term val lift_rule: cterm -> thm -> thm val incr_indexes: int -> thm -> thm val assumption: Proof.context option -> int -> thm -> thm Seq.seq val eq_assumption: int -> thm -> thm val rotate_rule: int -> int -> thm -> thm val permute_prems: int -> int -> thm -> thm val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} -> bool * thm * int -> int -> thm -> thm Seq.seq val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq val theory_names_of_arity: {long: bool} -> theory -> string * class -> stringlist val add_classrel: thm -> theory -> theory val add_arity: thm -> theory -> theory end;
fun global_ctyp_of thy raw_T = let val T = Sign.certify_typ thy raw_T; val maxidx = Term.maxidx_of_typ T; val sorts = Sorts.insert_typ T []; in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end;
val ctyp_of = global_ctyp_of o Proof_Context.theory_of;
fun dest_ctyp (Ctyp {cert, T = Type (_, Ts), maxidx, sorts}) = map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts
| dest_ctyp cT = raiseTYPE ("dest_ctyp", [typ_of cT], []);
fun dest_ctypN n (Ctyp {cert, T, maxidx, sorts}) = letfun err () = raiseTYPE ("dest_ctypN", [T], []) in
(case T of Type (_, Ts) =>
Ctyp {cert = cert, T = nth Ts n handle General.Subscript => err (),
maxidx = maxidx, sorts = sorts}
| _ => err ()) end;
fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert); fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts; fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx);
fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs = let val As = map typ_of cargs; fun err () = raiseTYPE ("make_ctyp", T :: As, []); in
(case T of Type (a, args) =>
Ctyp {
cert = fold join_certificate_ctyp cargs cert,
maxidx = fold maxidx_ctyp cargs ~1,
sorts = fold union_sorts_ctyp cargs [],
T = if length args = length cargs thenType (a, As) else err ()}
| _ => err ()) end;
(** certified terms **)
(*certified terms with checked typ, maxidx, and sorts*) datatype cterm =
Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T};
fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx;
fun global_cterm_of thy tm = let val (t, T) = Sign.certify_term thy tm; val maxidx = Term.maxidx_of_term t; val sorts = Sorts.insert_term t []; in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
val cterm_of = global_cterm_of o Proof_Context.theory_of;
fun renamed_term t' (Cterm {cert, t, T, maxidx, sorts}) = if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts} elseraise TERM ("renamed_term: terms disagree", [t, t']);
val fast_term_ord = Term_Ord.fast_term_ord o apply2 term_of; val term_ord = Term_Ord.term_ord o apply2 term_of;
(* destructors *)
fun dest_comb (Cterm {t = c $ a, T, cert, maxidx, sorts}) = letval A = Term.argument_type_of c 0 in
(Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts},
Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts}) end
| dest_comb ct = raise CTERM ("dest_comb", [ct]);
fun dest_fun (Cterm {t = c $ _, T, cert, maxidx, sorts}) = letval A = Term.argument_type_of c 0 in Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts} end
| dest_fun ct = raise CTERM ("dest_fun", [ct]);
fun dest_arg (Cterm {t = c $ a, T = _, cert, maxidx, sorts}) = letval A = Term.argument_type_of c 0 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end
| dest_arg ct = raise CTERM ("dest_arg", [ct]);
fun dest_fun2 (Cterm {t = c $ _ $ _, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0; val B = Term.argument_type_of c 1; in Cterm {t = c, T = A --> B --> T, cert = cert, maxidx = maxidx, sorts = sorts} end
| dest_fun2 ct = raise CTERM ("dest_fun2", [ct]);
fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) = letval A = Term.argument_type_of c 0 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end
| dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);
fun gen_dest_abs dest ct =
(case ct of
Cterm {t = t as Abs _, T = Type ("fun", [_, U]), cert, maxidx, sorts} => let val ((x', T), t') = dest t; val v = Cterm {t = Free (x', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts}; val body = Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts}; in (v, body) end
| _ => raise CTERM ("dest_abs", [ct]));
val dest_abs_fresh = gen_dest_abs o Term.dest_abs_fresh; val dest_abs_global = gen_dest_abs Term.dest_abs_global;
(* constructors *)
fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) = let val S =
(case T of
TFree (_, S) => S
| TVar (_, S) => S
| _ => raiseTYPE ("rename_tvar: no variable", [T], [])); val _ = if i < 0 thenraiseTYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else (); in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end;
fun free (x, Ctyp {cert, T, maxidx, sorts}) =
Cterm {cert = cert, t = Free (x, T), T = T, maxidx = maxidx, sorts = sorts};
fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) = if i < 0 thenraise TERM ("var: bad index", [Var ((x, i), T)]) else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts};
fun apply
(cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
(cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) = if T = dty then
Cterm {cert = join_certificate0 (cf, cx),
t = f $ x,
T = rty,
maxidx = Int.max (maxidx1, maxidx2),
sorts = Sorts.union sorts1 sorts2} elseraise CTERM ("apply: types don't agree", [cf, cx])
| apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]);
fun lambda_name
(x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
(ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) = letval t = Term.lambda_name (x, t1) t2 in
Cterm {cert = join_certificate0 (ct1, ct2),
t = t, T = T1 --> T2,
maxidx = Int.max (maxidx1, maxidx2),
sorts = Sorts.union sorts1 sorts2} end;
fun lambda t u = lambda_name ("", t) u;
(* indexes *)
fun adjust_maxidx_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = if maxidx = i then ct elseif maxidx < i then
Cterm {maxidx = i, cert = cert, t = t, T = T, sorts = sorts} else
Cterm {maxidx = Int.max (maxidx_of_term t, i), cert = cert, t = t, T = T, sorts = sorts};
fun incr_indexes_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = if i < 0 thenraise CTERM ("negative increment", [ct]) elseif i = 0 then ct else Cterm {cert = cert, t = Logic.incr_indexes ([], i) t,
T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
(*** Derivations and Theorems ***)
(* sort constraints *)
type constraint = {theory: theory, typ: typ, sort: sort};
local
val constraint_ord : constraint ord =
Context.theory_id_ord o apply2 (Context.theory_id o #theory)
||| Term_Ord.typ_ord o apply2 #typ
||| Term_Ord.sort_ord o apply2 #sort;
val smash_atyps =
map_atyps (fn TVar (_, S) => Term.aT S | TFree (_, S) => Term.aT S | T => T);
in
val union_constraints = Ord_List.union constraint_ord;
fun insert_constraints _ (_, []) = I
| insert_constraints thy (T, S) = let val ignored =
(case T of
TFree (_, S') => S = S'
| TVar (_, S') => S = S'
| _ => false); in if ignored then I else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S} end;
fun insert_constraints_env thy env = let val tyenv = Envir.type_env env; val normT = Envir.norm_type tyenv; fun insert ([], _) = I
| insert (S, T) = insert_constraints thy (normT T, S); in tyenv |> Vartab.fold (insert o #2) end;
end;
(* datatype thm *)
datatype thm = Thm of
deriv * (*derivation*)
{cert: Context.certificate, (*background theory certificate*)
tags: Properties.T, (*additional annotations/comments*)
maxidx: int, (*maximum index of any Var or TVar*)
constraints: constraint Ord_List.T, (*implicit proof obligations for sort constraints*)
shyps: sort Ord_List.T, (*sort hypotheses*)
hyps: term Ord_List.T, (*hypotheses*)
tpairs: (term * term) list, (*flex-flex pairs*)
prop: term} (*conclusion*) and deriv = Deriv of
{promises: (serial * thm future) Ord_List.T,
body: Proofterm.proof_body};
fun fold_terms h f (Thm (_, {tpairs, prop, hyps, ...})) =
fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps;
fun fold_atomic_ctyps h g f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps}; fun apply T a = if g a T then f (ctyp T) a else a; in (fold_terms h o fold_types o fold_atyps) apply th end;
fun fold_atomic_cterms h g f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps}; fun apply t T a = if g a t then f (cterm t T) a else a; in
(fold_terms h o fold_aterms)
(fn t as Const (_, T) => apply t T
| t as Free (_, T) => apply t T
| t as Var (_, T) => apply t T
| _ => I) th end;
fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u'; fun union_tpairs ts us = Library.merge eq_tpairs (ts, us); val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u);
fun attach_tpairs tpairs prop =
Logic.list_implies (map Logic.mk_equals tpairs, prop);
val union_hyps = Ord_List.union Term_Ord.fast_term_ord; val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord; val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
val cert_of = #cert o rep_thm; val theory_id = Context.certificate_theory_id o cert_of;
fun theory_name long = Context.theory_id_name long o theory_id; val theory_long_name = theory_name {long = true}; val theory_base_name = theory_name {long = false};
val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); val shyps_of = #shyps o rep_thm; val hyps_of = #hyps o rep_thm; val prop_of = #prop o rep_thm; val tpairs_of = #tpairs o rep_thm;
val concl_of = Logic.strip_imp_concl o prop_of; val prems_of = Logic.strip_imp_prems o prop_of; fun take_prems_of n = Logic.take_imp_prems n o prop_of; val nprems_of = Logic.count_prems o prop_of; val no_prems = Logic.no_prems o prop_of; val one_prem = Logic.one_prem o prop_of;
fun prem_of th i =
Logic.nth_prem (i, prop_of th) handle TERM _ => raise THM ("prem_of", i, [th]);
fun major_prem_of th =
(case take_prems_of 1 th of
prem :: _ => Logic.strip_assums_concl prem
| [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));
fun cprop_of (Thm (_, {cert, maxidx, shyps, prop, ...})) =
Cterm {cert = cert, maxidx = maxidx, T = propT, t = prop, sorts = shyps};
fun cprem_of (th as Thm (_, {cert, maxidx, shyps, prop, ...})) i =
Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps,
t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};
fun cconcl_of (th as Thm (_, {cert, maxidx, shyps, ...})) =
Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = concl_of th};
fun cprems_of (th as Thm (_, {cert, maxidx, shyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
(prems_of th);
fun take_cprems_of n (th as Thm (_, {cert, maxidx, shyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
(take_prems_of n th);
fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;
(* thm order: ignores theory context! *)
val thm_ord =
pointer_eq_ord
(Term_Ord.fast_term_ord o apply2 prop_of
||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 tpairs_of
||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of
||| list_ord Term_Ord.sort_ord o apply2 shyps_of);
(* implicit theory context *)
exception CONTEXT ofstring * ctyp list * cterm list * thm list * Context.generic option;
fun transfer_ctyp thy' cT = let val Ctyp {cert, T, maxidx, sorts} = cT; val _ =
Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [cT], [], [],
SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then cT else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts} end;
val transfer_ctyp' = transfer_ctyp o Proof_Context.theory_of; val transfer_ctyp'' = transfer_ctyp o Context.theory_of;
fun transfer_cterm thy' ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; val _ =
Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [], [ct], [],
SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then ct else Cterm {cert = cert', t = t, T = T, maxidx = maxidx, sorts = sorts} end;
val transfer_cterm' = transfer_cterm o Proof_Context.theory_of; val transfer_cterm'' = transfer_cterm o Context.theory_of;
fun transfer thy' th = let val Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) = th; val _ =
Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [], [], [th],
SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then th else
Thm (der,
{cert = cert',
tags = tags,
maxidx = maxidx,
constraints = constraints,
shyps = shyps,
hyps = hyps,
tpairs = tpairs,
prop = prop}) end;
val transfer' = transfer o Proof_Context.theory_of; val transfer'' = transfer o Context.theory_of;
fun join_transfer thy th =
(Context.subthy_id (theory_id th, Context.theory_id thy) ? transfer thy) th;
fun join_transfer_context (ctxt, th) = if Context.subthy_id (theory_id th, Context.theory_id (Proof_Context.theory_of ctxt)) then (ctxt, transfer' ctxt th) else (Context.raw_transfer (theory_of_thm th) ctxt, th);
(* matching *)
local
fun gen_match match
(ct1 as Cterm {t = t1, sorts = sorts1, ...},
ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = let val cert = join_certificate0 (ct1, ct2); val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE); val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) =
(((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts}); fun mk_ctinst ((x, i), (U, t)) = letval T = Envir.subst_type Tinsts U in
(((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts}) end; in
(TVars.build (Vartab.fold (TVars.add o mk_cTinst) Tinsts),
Vars.build (Vartab.fold (Vars.add o mk_ctinst) tinsts)) end;
in
valmatch = gen_match Pattern.match; val first_order_match = gen_match Pattern.first_order_match;
fun make_context ths NONE cert =
(Context.Theory (Context.certificate_theory cert) handle ERROR msg => raise CONTEXT (msg, [], [], ths, NONE))
| make_context ths (SOME ctxt) cert = let val thy_id = Context.certificate_theory_id cert; val thy_id' = Context.theory_id (Proof_Context.theory_of ctxt); in if Context.subthy_id (thy_id, thy_id') then Context.Proof ctxt elseraise CONTEXT ("Bad context", [], [], ths, SOME (Context.Proof ctxt)) end;
fun make_context_certificate ths opt_ctxt cert = let val context = make_context ths opt_ctxt cert; val cert' = Context.Certificate (Context.theory_of context); in (context, cert') end;
(*explicit weakening: maps |- B to A |- B*) fun weaken raw_ct th = let val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct; val Thm (der, {tags, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; in if T <> propT then raise THM ("weaken: assumptions must have type prop", 0, []) elseif maxidxA <> ~1 then raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, []) else
Thm (der,
{cert = join_certificate1 (ct, th),
tags = tags,
maxidx = maxidx,
constraints = constraints,
shyps = Sorts.union sorts shyps,
hyps = insert_hyps A hyps,
tpairs = tpairs,
prop = prop}) end;
fun weaken_sorts raw_sorts ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; val thy = theory_of_cterm ct; val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); val sorts' = Sorts.union sorts more_sorts; in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
(** derivations and promised proofs **)
fun make_deriv0 promises body = Deriv {promises = promises, body = body};
val oracles' = Proofterm.union_oracles oracles1 oracles2; val thms' = Proofterm.union_thms thms1 thms2; val zboxes' = ZTerm.union_zboxes zboxes1 zboxes2;
val proofs = Proofterm.get_proofs_level (); val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZNop; val proof' = if Proofterm.proof_enabled proofs then proof prf1 prf2 else MinProof; in make_deriv ps' oracles' thms' zboxes' zproof' proof'end;
val empty_classes = make_classes (Symreltab.empty, Aritytab.empty);
(*see Theory.at_begin hook for transitive closure of classrels and arity completion*) fun merge_classes
(Classes {classrels = classrels1, arities = arities1},
Classes {classrels = classrels2, arities = arities2}) = let val classrels' = Symreltab.merge (K true) (classrels1, classrels2); val arities' = Aritytab.merge (K true) (arities1, arities2); in make_classes (classrels', arities') end;
(* data *)
structure Data = Theory_Data
( type T =
{name: Thm_Name.P, thm: thm} Inttab.table * (*stored zproof thms*)
unit Name_Space.table * (*oracles: authentic derivation names*)
classes; (*type classes within the logic*)
val empty : T = (Inttab.empty, Name_Space.empty_table Markup.oracleN, empty_classes); fun merge ((_, oracles1, sorts1), (_, oracles2, sorts2)) : T =
(Inttab.empty,
Name_Space.merge_tables (oracles1, oracles2),
merge_classes (sorts1, sorts2));
);
val get_zproofs = #1 o Data.get; fun map_zproofs f = Data.map (fn (a, b, c) => (f a, b, c));
val get_oracles = #2 o Data.get; fun map_oracles f = Data.map (fn (a, b, c) => (a, f b, c));
val get_classes = (fn (_, _, Classes args) => args) o Data.get; val get_classrels = #classrels o get_classes; val get_arities = #arities o get_classes;
fun map_classes f =
Data.map (fn (a, b, Classes {classrels, arities}) =>
(a, b, make_classes (f (classrels, arities)))); fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities)); fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities));
val _ =
(Theory.setup o Theory.at_begin) (fn thy => if Inttab.is_empty (get_zproofs thy) then NONE else SOME (map_zproofs (K Inttab.empty) thy));
(* type classes *)
fun the_classrel thy (c1, c2) =
(case Symreltab.lookup (get_classrels thy) (c1, c2) of
SOME thm => transfer thy thm
| NONE => error ("Unproven class relation " ^
Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2]));
fun the_arity thy (a, Ss, c) =
(case Aritytab.lookup (get_arities thy) (a, Ss, c) of
SOME (thm, _, _) => transfer thy thm
| NONE => error ("Unproven type arity " ^
Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));
fun sorts_zproof thy = (zproof_of o the_classrel thy, zproof_of o the_arity thy); fun sorts_proof thy = (proof_of o the_classrel thy, proof_of o the_arity thy);
fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
Sorts.of_sort_derivation (Sign.classes_of thy)
{class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 => if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
type_constructor = fn (a, _) => fn dom => fn c => letval arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c)) in (fold o fold) (union_digest o #1) dom arity_digest end,
type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)}
(typ, sort);
fun bad_constraint_theory cert ({theory = thy, ...}: constraint) = if Context.eq_thy_id (Context.certificate_theory_id cert, Context.theory_id thy) then NONE else SOME thy;
in
fun solve_constraints (thm as Thm (der, args)) = let val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args;
val bad_thys = map_filter (bad_constraint_theory cert) constraints; val _ = if null bad_thys then () else raise THEORY ("solve_constraints: bad theories for theorem\n" ^
Syntax.string_of_term_global (hd bad_thys) (prop_of thm), bad_thys);
(*Dangling sort constraints of a thm*) fun extra_shyps (th as Thm (_, {shyps, ...})) =
Sorts.subtract (fold_terms {hyps = true} Sorts.insert_term th []) shyps;
(*Remove extra sorts that are witnessed by type signature information*) fun strip_shyps thm =
(case thm of
Thm (_, {shyps = [], ...}) => thm
| Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) => let val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
val thy = theory_of_thm thm; val algebra = Sign.classes_of thy; val le = Sorts.sort_le algebra; fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1)); fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
val present_set = Types.build (thm |> fold_terms {hyps = true} Types.add_atyps); val {present, extra} = Logic.present_sorts shyps present_set;
val (witnessed, non_witnessed) =
Sign.witness_sorts thy present extra ||> map (`(Sorts.minimize_sort algebra));
val extra' =
non_witnessed |> map_filter (fn (S, _) => if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S)
|> Sorts.make;
val non_witnessed_constraints =
non_witnessed |> maps (fn (S1, S2) => letval S0 = the (find_first (fn S => le (S, S1)) extra') in rel (S0, S1) @ rel (S1, S2) end);
val shyps' = fold (Sorts.insert_sort o #2) present extra';
val types = present @ witnessed @ map (`Logic.dummy_tfree) extra'; fun get_type S = types |> get_first (fn (T', S') => if le (S', S) then SOME T'else NONE); val map_atyp =
Same.function_eq (op =) (fn T => if Types.defined present_set T thenraise Same.SAME else
(case get_type (Type.sort_of_atyp T) of
SOME T' => T'
| NONE => raise Fail "strip_shyps: bad type variable in proof term")); val map_ztyp =
ZTypes.apply_unsynchronized_cache
(ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = let val self_id =
(case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of
NONE => K false
| SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header); fun expand header = if self_id header orelse Thm_Name.is_empty (#1 (#thm_name header)) then SOME Thm_Name.none else NONE; in expand end;
(*deterministic name of finished proof*) fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
#1 (Proofterm.get_approximative_name shyps hyps prop (proof_of thm));
(*identified PThm node*) fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
Proofterm.get_id shyps hyps prop (proof_of thm);
(*dependencies of PThm node*) fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) =
(case (derivation_id thm, thms) of
(SOME {serial = i, ...}, [(j, thm_node)]) => if i = j then Proofterm.thm_node_thms thm_node else thms
| _ => thms)
| thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]);
fun name_derivation name_pos =
strip_shyps #> (fn thm as Thm (der, args) => let val thy = theory_of_thm thm;
val Deriv {promises, body} = der; val {shyps, hyps, prop, tpairs, ...} = args;
val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);
val ps = map (apsnd (Future.map fulfill_body)) promises; val body' = Proofterm.thm_proof thy (sorts_proof thy) name_pos shyps hyps prop ps body; in Thm (make_deriv0 [] body', args) end);
val trim_context = solve_constraints #> trim_context_thm;
(*** Oracles ***)
fun add_oracle (b, oracle_fn) thy1 = let val (name, oracles') = Name_Space.define (Context.Theory thy1) true (b, ()) (get_oracles thy1); val thy2 = map_oracles (K oracles') thy1; val cert2 = Context.Certificate_Id (Context.theory_id thy2); fun invoke_oracle arg = letval ct as Cterm {cert = cert3, t = prop, T, maxidx, sorts} = oracle_fn arg in if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else let val cert = Context.join_certificate (cert2, cert3); val proofs = Proofterm.get_proofs_level (); val oracle = if Proofterm.oracle_enabled proofs then ((name, Position.thread_data ()), SOME prop) else ((name, Position.none), NONE); val proof = if Proofterm.proof_enabled proofs then Proofterm.oracle_proof name prop else MinProof; val zproof = if Proofterm.zproof_enabled proofs then let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); in ZTerm.oracle_proof thy name prop end else ZNop; in
Thm (make_deriv [] [oracle] [] [] zproof proof,
{cert = cert,
tags = [],
maxidx = maxidx,
constraints = [],
shyps = sorts,
hyps = [],
tpairs = [],
prop = prop}) end end; in ((name, invoke_oracle), thy2) end;
val oracle_space = Name_Space.space_of_table o get_oracles;
fun pretty_oracle ctxt =
Name_Space.pretty ctxt (oracle_space (Proof_Context.theory_of ctxt));
(*The assumption rule A |- A*) fun assume raw_ct = letval ct as Cterm {cert, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in if T <> propT then raise THM ("assume: prop", 0, []) elseif maxidx <> ~1 then raise THM ("assume: variables", maxidx, []) else let fun zproof () = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); in ZTerm.assume_proof thy prop end; fun proof () = Proofterm.Hyp prop; in
Thm (deriv_rule0 zproof proof,
{cert = cert,
tags = [],
maxidx = ~1,
constraints = [],
shyps = sorts,
hyps = [prop],
tpairs = [],
prop = prop}) end end;
fun assume_cterm A = assume A handle THM (msg, _, _) => raise CTERM (msg, [A]);
(*Implication introduction [A] : B ------- A \<Longrightarrow> B
*) fun implies_intr
(ct as Cterm {t = A, T, maxidx = maxidx1, sorts, ...})
(th as Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...})) = if T <> propT then raise THM ("implies_intr: assumptions must have type prop", 0, [th]) else let val cert = join_certificate1 (ct, th); fun zproof p = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [th], NONE); in ZTerm.implies_intr_proof thy A p end fun proof p = Proofterm.implies_intr_proof A p; in
Thm (deriv_rule1 zproof proof der,
{cert = cert,
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = constraints,
shyps = Sorts.union sorts shyps,
hyps = remove_hyps A hyps,
tpairs = tpairs,
prop = Logic.mk_implies (A, prop)}) end;
(*Implication elimination A \<Longrightarrow> B A ------------ B
*) fun implies_elim thAB thA = let val Thm (derA,
{maxidx = maxidx1, hyps = hypsA, constraints = constraintsA, shyps = shypsA,
tpairs = tpairsA, prop = propA, ...}) = thA and Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...}) = thAB; fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]); in
(case prop of Const ("Pure.imp", _) $ A $ B => if A aconv propA then
Thm (deriv_rule2 (curry ZAppp) (curry Proofterm.%%) der derA,
{cert = join_certificate2 (thAB, thA),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraintsA constraints,
shyps = Sorts.union shypsA shyps,
hyps = union_hyps hypsA hyps,
tpairs = union_tpairs tpairsA tpairs,
prop = B}) else err ()
| _ => err ()) end;
(*Forall introduction. The Free or Var x must not be free in the hypotheses. [x] : A ------ \<And>x. A
*) fun occs x ts tpairs = letfun occs t = Logic.occs (x, t) inexists occs ts orelse exists (occs o fst) tpairs orelse exists (occs o snd) tpairs end;
fun forall_intr
(ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...})
(th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) = let fun check_result a ts = if occs x ts tpairs then raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th]) else let val cert = join_certificate1 (ct, th); fun zproof p = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [th], NONE); in ZTerm.forall_intr_proof thy T (a, x) p end; fun proof p = Proofterm.forall_intr_proof (a, x) NONE p; in
Thm (deriv_rule1 zproof proof der,
{cert = cert,
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = constraints,
shyps = Sorts.union sorts shyps,
hyps = hyps,
tpairs = tpairs,
prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))}) end; in
(case x of
Free (a, _) => check_result a hyps
| Var ((a, _), _) => check_result a []
| _ => raise THM ("forall_intr: not a variable", 0, [th])) end;
(*Forall elimination \<And>x. A ------ A[t/x]
*) fun forall_elim
(ct as Cterm {t, T, maxidx = maxidx1, sorts, ...})
(th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) =
(case prop of Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => if T <> qary then raise THM ("forall_elim: type mismatch", 0, [th]) else let val cert = join_certificate1 (ct, th); fun zproof p = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [th], NONE); in ZTerm.forall_elim_proof thy t p end; fun proof p = p % SOME t; in
Thm (deriv_rule1 zproof proof der,
{cert = cert,
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = constraints,
shyps = Sorts.union sorts shyps,
hyps = hyps,
tpairs = tpairs,
prop = Term.betapply (A, t)}) end
| _ => raise THM ("forall_elim: not quantified", 0, [th]));
(* Equality *)
(*Reflexivity t \<equiv> t
*) fun reflexive (ct as Cterm {cert, t, T, maxidx, sorts}) = let fun zproof () = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); in ZTerm.reflexive_proof thy T t end; fun proof () = Proofterm.reflexive_proof; in
Thm (deriv_rule0 zproof proof,
{cert = cert,
tags = [],
maxidx = maxidx,
constraints = [],
shyps = sorts,
hyps = [],
tpairs = [],
prop = Logic.mk_equals (t, t)}) end;
(*Symmetry t \<equiv> u ------ u \<equiv> t
*) fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
(case prop of
(eq as Const ("Pure.eq", Type ("fun", [T, _]))) $ t $ u => let fun zproof p = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE); in ZTerm.symmetric_proof thy T t u p end; in
Thm (deriv_rule1 zproof Proofterm.symmetric_proof der,
{cert = cert,
tags = [],
maxidx = maxidx,
constraints = constraints,
shyps = shyps,
hyps = hyps,
tpairs = tpairs,
prop = eq $ u $ t}) end
| _ => raise THM ("symmetric", 0, [th]));
(*Transitivity t1 \<equiv> u u \<equiv> t2 ------------------ t1 \<equiv> t2
*) fun transitive th1 th2 = let val Thm (der1, {maxidx = maxidx1, hyps = hyps1, constraints = constraints1, shyps = shyps1,
tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, hyps = hyps2, constraints = constraints2, shyps = shyps2,
tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]); in case (prop1, prop2) of
((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) => ifnot (u aconv u') then err "middle term" else let val cert = join_certificate2 (th1, th2); fun zproof p q = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [], [th1, th2], NONE); in ZTerm.transitive_proof thy T t1 u t2 p q end; fun proof p = Proofterm.transitive_proof T u p; in
Thm (deriv_rule2 zproof proof der1 der2,
{cert = cert,
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraints1 constraints2,
shyps = Sorts.union shyps1 shyps2,
hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = eq $ t1 $ t2}) end
| _ => err "premises" end;
(*Beta-conversion (\<lambda>x. t) u \<equiv> t[u/x] fully beta-reduces the term if full = true
*) fun beta_conversion full (ct as Cterm {cert, t, T, maxidx, sorts}) = let val t' = if full then Envir.beta_norm t else
(case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
| _ => raise THM ("beta_conversion: not a redex", 0, [])); fun zproof () = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); in ZTerm.reflexive_proof thy T t end; fun proof () = Proofterm.reflexive_proof; in
Thm (deriv_rule0 zproof proof,
{cert = cert,
tags = [],
maxidx = maxidx,
constraints = [],
shyps = sorts,
hyps = [],
tpairs = [],
prop = Logic.mk_equals (t, t')}) end;
fun eta_conversion (ct as Cterm {cert, t, T, maxidx, sorts}) = let fun zproof () = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); in ZTerm.reflexive_proof thy T t end; fun proof () = Proofterm.reflexive_proof; in
Thm (deriv_rule0 zproof proof,
{cert = cert,
tags = [],
maxidx = maxidx,
constraints = [],
shyps = sorts,
hyps = [],
tpairs = [],
prop = Logic.mk_equals (t, Envir.eta_contract t)}) end;
fun eta_long_conversion (ct as Cterm {cert, t, T, maxidx, sorts}) = let fun zproof () = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); in ZTerm.reflexive_proof thy T t end; fun proof () = Proofterm.reflexive_proof; in
Thm (deriv_rule0 zproof proof,
{cert = cert,
tags = [],
maxidx = maxidx,
constraints = [],
shyps = sorts,
hyps = [],
tpairs = [],
prop = Logic.mk_equals (t, Envir.eta_long [] t)}) end;
(*The abstraction rule. The Free or Var x must not be free in the hypotheses. The bound variable will be named "a" (since x will be something like x320) t \<equiv> u -------------- \<lambda>x. t \<equiv> \<lambda>x. u
*) fun abstract_rule b
(ct as Cterm {t = x, T, sorts, ...})
(th as Thm (der, {cert, maxidx, hyps, constraints, shyps, tpairs, prop, ...})) = let val (U, t, u) =
(case prop of Const ("Pure.eq", Type ("fun", [U, _])) $ t $ u => (U, t, u)
| _ => raise THM ("abstract_rule: premise not an equality", 0, [th])); fun check_result a ts = if occs x ts tpairs then raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th]) else let val f = Abs (b, T, abstract_over (x, t)); val g = Abs (b, T, abstract_over (x, u)); fun zproof p = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [th], NONE); in ZTerm.abstract_rule_proof thy T U (b, x) f g p end; fun proof p = Proofterm.abstract_rule_proof (b, x) p in
Thm (deriv_rule1 zproof proof der,
{cert = cert,
tags = [],
maxidx = maxidx,
constraints = constraints,
shyps = Sorts.union sorts shyps,
hyps = hyps,
tpairs = tpairs,
prop = Logic.mk_equals (f, g)}) end; in
(case x of
Free (a, _) => check_result a hyps
| Var ((a, _), _) => check_result a []
| _ => raise THM ("abstract_rule: not a variable", 0, [th])) end;
(*The combination rule f \<equiv> g t \<equiv> u ------------- f t \<equiv> g u
*) fun combination th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1,
hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; in
(case (prop1, prop2) of
(Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g, Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) => let val U =
(case fT of Type ("fun", [T1, U]) => if T1 = tT then U elseraise THM ("combination: types", 0, [th1, th2])
| _ => raise THM ("combination: not function type", 0, [th1, th2])); val cert = join_certificate2 (th1, th2); fun zproof p q = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [], [th1, th2], NONE); in ZTerm.combination_proof thy fT U f g t u p q end; fun proof p q = Proofterm.combination_proof f g t u p q; in
Thm (deriv_rule2 zproof proof der1 der2,
{cert = cert,
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraints1 constraints2,
shyps = Sorts.union shyps1 shyps2,
hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = Logic.mk_equals (f $ t, g $ u)}) end
| _ => raise THM ("combination: premises", 0, [th1, th2])) end;
(*Equality introduction A \<Longrightarrow> B B \<Longrightarrow> A ---------------- A \<equiv> B
*) fun equal_intr th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1,
hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); in
(case (prop1, prop2) of
(Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') => if A aconv A' andalso B aconv B'then let val cert = join_certificate2 (th1, th2); fun proof p q = Proofterm.equal_intr_proof A B p q; fun zproof p q = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [], [th1, th2], NONE); in ZTerm.equal_intr_proof thy A B p q end; in
Thm (deriv_rule2 zproof proof der1 der2,
{cert = cert,
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraints1 constraints2,
shyps = Sorts.union shyps1 shyps2,
hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = Logic.mk_equals (A, B)}) end else err "not equal"
| _ => err "premises") end;
(*The equal propositions rule A \<equiv> B A --------- B
*) fun equal_elim th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1,
hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); in
(case prop1 of Const ("Pure.eq", _) $ A $ B => if prop2 aconv A then let val cert = join_certificate2 (th1, th2); fun proof p q = Proofterm.equal_elim_proof A B p q; fun zproof p q = let val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [], [th1, th2], NONE); in ZTerm.equal_elim_proof thy A B p q end; in
Thm (deriv_rule2 zproof proof der1 der2,
{cert = cert,
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraints1 constraints2,
shyps = Sorts.union shyps1 shyps2,
hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = B}) end else err "not equal"
| _ => err "major premise") end;
(**** Derived rules ****)
(*Smash unifies the list of term pairs leaving no flex-flex pairs. Instantiates the theorem and deletes trivial tpairs. Resulting sequence may contain multiple elements if the tpairs are not all
flex-flex.*) fun flexflex_rule opt_ctxt =
solve_constraints #> (fn th => let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; val (context, cert') = make_context_certificate [th] opt_ctxt cert; in
Unify.smash_unifiers context tpairs (Envir.empty maxidx)
|> Seq.map (fn env => if Envir.is_empty env then th else let val tpairs' = tpairs |> map (apply2 (Envir.norm_term env)) (*remove trivial tpairs, of the form t \<equiv> t*)
|> filter_out (op aconv); val prop' = Envir.norm_term env prop; val thy' = Context.certificate_theory cert'handle ERROR msg => raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);
(*Generalization of fixed variables A -------------------- A[?'a/'a, ?x/x, ...]
*)
fun generalize (tfrees, frees) idx th = if Names.is_empty tfrees andalso Names.is_empty frees then th else let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
val bad_type = if Names.is_empty tfrees then K false else Term.exists_subtype (fn TFree (a, _) => Names.defined tfrees a | _ => false);
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.24 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.
