--- a/src/Pure/drule.ML Fri Jun 17 18:33:05 2005 +0200
+++ b/src/Pure/drule.ML Fri Jun 17 18:33:08 2005 +0200
@@ -20,7 +20,7 @@
val cterm_fun : (term -> term) -> (cterm -> cterm)
val ctyp_fun : (typ -> typ) -> (ctyp -> ctyp)
val read_insts :
- Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
+ theory -> (indexname -> typ option) * (indexname -> sort option)
-> (indexname -> typ option) * (indexname -> sort option)
-> string list -> (indexname * string) list
-> (ctyp * ctyp) list * (cterm * cterm) list
@@ -54,10 +54,10 @@
val OF : thm * thm list -> thm
val compose : thm * int * thm -> thm list
val COMP : thm * thm -> thm
- val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
+ val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
val read_instantiate : (string*string)list -> thm -> thm
val cterm_instantiate : (cterm*cterm)list -> thm -> thm
- val eq_thm_sg : thm * thm -> bool
+ val eq_thm_thy : thm * thm -> bool
val eq_thm_prop : thm * thm -> bool
val weak_eq_thm : thm * thm -> bool
val size_of_thm : thm -> int
@@ -123,7 +123,7 @@
val fconv_rule : (cterm -> thm) -> thm -> thm
val norm_hhf_eq: thm
val is_norm_hhf: term -> bool
- val norm_hhf: Sign.sg -> term -> term
+ val norm_hhf: theory -> term -> term
val triv_goal: thm
val rev_triv_goal: thm
val implies_intr_goals: cterm list -> thm -> thm
@@ -146,7 +146,7 @@
val conj_elim_precise: int -> thm -> thm list
val conj_intr_thm: thm
val abs_def: thm -> thm
- val read_instantiate_sg': Sign.sg -> (indexname * string) list -> thm -> thm
+ val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm
val read_instantiate': (indexname * string) list -> thm -> thm
end;
@@ -190,16 +190,14 @@
val cprems_of = strip_imp_prems o cprop_of;
fun cterm_fun f ct =
- let val {t, sign, ...} = Thm.rep_cterm ct
- in Thm.cterm_of sign (f t) end;
+ let val {t, thy, ...} = Thm.rep_cterm ct
+ in Thm.cterm_of thy (f t) end;
fun ctyp_fun f cT =
- let val {T, sign, ...} = Thm.rep_ctyp cT
- in Thm.ctyp_of sign (f T) end;
+ let val {T, thy, ...} = Thm.rep_ctyp cT
+ in Thm.ctyp_of thy (f T) end;
-val proto_sign = Theory.sign_of ProtoPure.thy;
-
-val implies = cterm_of proto_sign Term.implies;
+val implies = cterm_of ProtoPure.thy Term.implies;
(*cterm version of mk_implies*)
fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B;
@@ -259,7 +257,7 @@
fun inst_failure ixn =
error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
-fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
+fun read_insts thy (rtypes,rsorts) (types,sorts) used insts =
let
fun is_tv ((a, _), _) =
(case Symbol.explode a of "'" :: _ => true | _ => false);
@@ -267,8 +265,8 @@
fun sort_of ixn = case rsorts ixn of SOME S => S | NONE => absent ixn;
fun readT (ixn, st) =
let val S = sort_of ixn;
- val T = Sign.read_typ (sign,sorts) st;
- in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
+ val T = Sign.read_typ (thy,sorts) st;
+ in if Sign.typ_instance thy (T, TVar(ixn,S)) then (ixn,T)
else inst_failure ixn
end
val tye = map readT tvs;
@@ -278,13 +276,13 @@
val ixnsTs = map mkty vs;
val ixns = map fst ixnsTs
and sTs = map snd ixnsTs
- val (cts,tye2) = read_def_cterms(sign,types,sorts) used false sTs;
+ val (cts,tye2) = read_def_cterms(thy,types,sorts) used false sTs;
fun mkcVar(ixn,T) =
let val U = typ_subst_TVars tye2 T
- in cterm_of sign (Var(ixn,U)) end
+ in cterm_of thy (Var(ixn,U)) end
val ixnTs = ListPair.zip(ixns, map snd sTs)
-in (map (fn (ixn, T) => (ctyp_of sign (TVar (ixn, sort_of ixn)),
- ctyp_of sign T)) (tye2 @ tye),
+in (map (fn (ixn, T) => (ctyp_of thy (TVar (ixn, sort_of ixn)),
+ ctyp_of thy T)) (tye2 @ tye),
ListPair.zip(map mkcVar ixnTs,cts))
end;
@@ -362,7 +360,7 @@
(*Strip extraneous shyps as far as possible*)
fun strip_shyps_warning thm =
let
- val str_of_sort = Pretty.str_of o Sign.pretty_sort (Thm.sign_of_thm thm);
+ val str_of_sort = Pretty.str_of o Sign.pretty_sort (Thm.theory_of_thm thm);
val thm' = Thm.strip_shyps thm;
val xshyps = Thm.extra_shyps thm';
in
@@ -379,9 +377,9 @@
(*Generalization over all suitable Free variables*)
fun forall_intr_frees th =
- let val {prop,sign,...} = rep_thm th
+ let val {prop,thy,...} = rep_thm th
in forall_intr_list
- (map (cterm_of sign) (sort (make_ord atless) (term_frees prop)))
+ (map (cterm_of thy) (sort (make_ord atless) (term_frees prop)))
th
end;
@@ -390,8 +388,8 @@
fun gen_all thm =
let
- val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
- fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of sign (Var ((x, maxidx + 1), T))) th;
+ val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
+ fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of thy (Var ((x, maxidx + 1), T))) th;
val vs = Term.strip_all_vars prop;
in Library.foldl elim (thm, Term.variantlist (map #1 vs, []) ~~ map #2 vs) end;
@@ -415,7 +413,7 @@
(*Reset Var indexes to zero, renaming to preserve distinctness*)
fun zero_var_indexes th =
- let val {prop,sign,tpairs,...} = rep_thm th;
+ let val {prop,thy,tpairs,...} = rep_thm th;
val (tpair_l, tpair_r) = Library.split_list tpairs;
val vars = foldr add_term_vars
(foldr add_term_vars (term_vars prop) tpair_l) tpair_r;
@@ -426,12 +424,12 @@
val nms' = rev(Library.foldl add_new_id ([], map (#1 o #1) inrs));
val tye = ListPair.map (fn ((v, rs), a) => (TVar (v, rs), TVar ((a, 0), rs)))
(inrs, nms')
- val ctye = map (pairself (ctyp_of sign)) tye;
+ val ctye = map (pairself (ctyp_of thy)) tye;
fun varpairs([],[]) = []
| varpairs((var as Var(v,T)) :: vars, b::bs) =
let val T' = typ_subst_atomic tye T
- in (cterm_of sign (Var(v,T')),
- cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
+ in (cterm_of thy (Var(v,T')),
+ cterm_of thy (Var((b,0),T'))) :: varpairs(vars,bs)
end
| varpairs _ = raise TERM("varpairs", []);
in Thm.instantiate (ctye, varpairs(vars,rev bs)) th end;
@@ -474,7 +472,7 @@
fun freeze_thaw_robust th =
let val fth = freezeT th
- val {prop, tpairs, sign, ...} = rep_thm fth
+ val {prop, tpairs, thy, ...} = rep_thm fth
in
case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
[] => (fth, fn i => fn x => x) (*No vars: nothing to do!*)
@@ -484,8 +482,8 @@
in ((ix,v)::pairs) end;
val alist = foldr newName [] vars
fun mk_inst (Var(v,T)) =
- (cterm_of sign (Var(v,T)),
- cterm_of sign (Free(valOf (assoc(alist,v)), T)))
+ (cterm_of thy (Var(v,T)),
+ cterm_of thy (Free(valOf (assoc(alist,v)), T)))
val insts = map mk_inst vars
fun thaw i th' = (*i is non-negative increment for Var indexes*)
th' |> forall_intr_list (map #2 insts)
@@ -497,7 +495,7 @@
The Frees created from Vars have nice names.*)
fun freeze_thaw th =
let val fth = freezeT th
- val {prop, tpairs, sign, ...} = rep_thm fth
+ val {prop, tpairs, thy, ...} = rep_thm fth
in
case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
[] => (fth, fn x => x)
@@ -508,8 +506,8 @@
val (alist, _) = foldr newName ([], Library.foldr add_term_names
(prop :: Thm.terms_of_tpairs tpairs, [])) vars
fun mk_inst (Var(v,T)) =
- (cterm_of sign (Var(v,T)),
- cterm_of sign (Free(valOf (assoc(alist,v)), T)))
+ (cterm_of thy (Var(v,T)),
+ cterm_of thy (Free(valOf (assoc(alist,v)), T)))
val insts = map mk_inst vars
fun thaw th' =
th' |> forall_intr_list (map #2 insts)
@@ -536,9 +534,8 @@
Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
[ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ] *)
fun assume_ax thy sP =
- let val sign = Theory.sign_of thy
- val prop = Logic.close_form (term_of (read_cterm sign (sP, propT)))
- in forall_elim_vars 0 (assume (cterm_of sign prop)) end;
+ let val prop = Logic.close_form (term_of (read_cterm thy (sP, propT)))
+ in forall_elim_vars 0 (Thm.assume (cterm_of thy prop)) end;
(*Resolution: exactly one resolvent must be produced.*)
fun tha RSN (i,thb) =
@@ -594,8 +591,8 @@
(** theorem equality **)
-(*True if the two theorems have the same signature.*)
-val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
+(*True if the two theorems have the same theory.*)
+val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm;
(*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
val eq_thm_prop = op aconv o pairself Thm.prop_of;
@@ -622,16 +619,16 @@
| term_vars' _ = [];
fun forall_intr_vars th =
- let val {prop,sign,...} = rep_thm th;
+ let val {prop,thy,...} = rep_thm th;
val vars = distinct (term_vars' prop);
- in forall_intr_list (map (cterm_of sign) vars) th end;
+ in forall_intr_list (map (cterm_of thy) vars) th end;
val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT);
(*** Meta-Rewriting Rules ***)
-fun read_prop s = read_cterm proto_sign (s, propT);
+fun read_prop s = read_cterm ProtoPure.thy (s, propT);
fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
fun store_standard_thm name thm = store_thm name (standard thm);
@@ -639,7 +636,7 @@
fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
val reflexive_thm =
- let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),[])))
+ let val cx = cterm_of ProtoPure.thy (Var(("x",0),TVar(("'a",0),[])))
in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
val symmetric_thm =
@@ -768,7 +765,7 @@
val triv_forall_equality =
let val V = read_prop "PROP V"
and QV = read_prop "!!x::'a. PROP V"
- and x = read_cterm proto_sign ("x", TypeInfer.logicT);
+ and x = read_cterm ProtoPure.thy ("x", TypeInfer.logicT);
in
store_standard_thm_open "triv_forall_equality"
(equal_intr (implies_intr QV (forall_elim x (assume QV)))
@@ -823,7 +820,7 @@
val norm_hhf_eq =
let
- val cert = Thm.cterm_of proto_sign;
+ val cert = Thm.cterm_of ProtoPure.thy;
val aT = TFree ("'a", []);
val all = Term.all aT;
val x = Free ("x", aT);
@@ -857,53 +854,53 @@
| is_norm _ = true;
in is_norm (Pattern.beta_eta_contract tm) end;
-fun norm_hhf sg t =
+fun norm_hhf thy t =
if is_norm_hhf t then t
- else Pattern.rewrite_term (Sign.tsig_of sg) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
+ else Pattern.rewrite_term (Sign.tsig_of thy) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
-(*** Instantiate theorem th, reading instantiations under signature sg ****)
+(*** Instantiate theorem th, reading instantiations in theory thy ****)
(*Version that normalizes the result: Thm.instantiate no longer does that*)
fun instantiate instpair th = Thm.instantiate instpair th COMP asm_rl;
-fun read_instantiate_sg' sg sinsts th =
+fun read_instantiate_sg' thy sinsts th =
let val ts = types_sorts th;
val used = add_used th [];
- in instantiate (read_insts sg ts ts used sinsts) th end;
+ in instantiate (read_insts thy ts ts used sinsts) th end;
-fun read_instantiate_sg sg sinsts th =
- read_instantiate_sg' sg (map (apfst Syntax.indexname) sinsts) th;
+fun read_instantiate_sg thy sinsts th =
+ read_instantiate_sg' thy (map (apfst Syntax.indexname) sinsts) th;
(*Instantiate theorem th, reading instantiations under theory of th*)
fun read_instantiate sinsts th =
- read_instantiate_sg (Thm.sign_of_thm th) sinsts th;
+ read_instantiate_sg (Thm.theory_of_thm th) sinsts th;
fun read_instantiate' sinsts th =
- read_instantiate_sg' (Thm.sign_of_thm th) sinsts th;
+ read_instantiate_sg' (Thm.theory_of_thm th) sinsts th;
(*Left-to-right replacements: tpairs = [...,(vi,ti),...].
Instantiates distinct Vars by terms, inferring type instantiations. *)
local
- fun add_types ((ct,cu), (sign,tye,maxidx)) =
- let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
- and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
+ fun add_types ((ct,cu), (thy,tye,maxidx)) =
+ let val {thy=thyt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
+ and {thy=thyu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
val maxi = Int.max(maxidx, Int.max(maxt, maxu));
- val sign' = Sign.merge(sign, Sign.merge(signt, signu))
- val (tye',maxi') = Type.unify (Sign.tsig_of sign') (tye, maxi) (T, U)
+ val thy' = Theory.merge(thy, Theory.merge(thyt, thyu))
+ val (tye',maxi') = Type.unify (Sign.tsig_of thy') (tye, maxi) (T, U)
handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
- in (sign', tye', maxi') end;
+ in (thy', tye', maxi') end;
in
fun cterm_instantiate ctpairs0 th =
- let val (sign,tye,_) = foldr add_types (Thm.sign_of_thm th, Vartab.empty, 0) ctpairs0
+ let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
fun instT(ct,cu) =
- let val inst = cterm_of sign o Envir.subst_TVars tye o term_of
+ let val inst = cterm_of thy o Envir.subst_TVars tye o term_of
in (inst ct, inst cu) end
- fun ctyp2 (ixn, (S, T)) = (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)
+ fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
in instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end
handle TERM _ =>
- raise THM("cterm_instantiate: incompatible signatures",0,[th])
+ raise THM("cterm_instantiate: incompatible theories",0,[th])
| TYPE (msg, _, _) => raise THM(msg, 0, [th])
end;
@@ -912,11 +909,11 @@
(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
fun equal_abs_elim ca eqth =
- let val {sign=signa, t=a, ...} = rep_cterm ca
+ let val {thy=thya, t=a, ...} = rep_cterm ca
and combth = combination eqth (reflexive ca)
- val {sign,prop,...} = rep_thm eqth
+ val {thy,prop,...} = rep_thm eqth
val (abst,absu) = Logic.dest_equals prop
- val cterm = cterm_of (Sign.merge (sign,signa))
+ val cterm = cterm_of (Theory.merge (thy,thya))
in transitive (symmetric (beta_conversion false (cterm (abst$a))))
(transitive combth (beta_conversion false (cterm (absu$a))))
end
@@ -929,7 +926,7 @@
(*** Goal (PROP A) <==> PROP A ***)
local
- val cert = Thm.cterm_of proto_sign;
+ val cert = Thm.cterm_of ProtoPure.thy;
val A = Free ("A", propT);
val G = Logic.mk_goal A;
val (G_def, _) = freeze_thaw ProtoPure.Goal_def;
@@ -940,7 +937,7 @@
(Thm.equal_elim G_def (Thm.assume (cert G)))));
end;
-val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const);
+val mk_cgoal = Thm.capply (Thm.cterm_of ProtoPure.thy Logic.goal_const);
fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal;
fun implies_intr_goals cprops thm =
@@ -952,7 +949,7 @@
(** variations on instantiate **)
(*shorthand for instantiating just one variable in the current theory*)
-fun inst x t = read_instantiate_sg (sign_of (the_context())) [(x,t)];
+fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
(* collect vars in left-to-right order *)
@@ -974,11 +971,11 @@
List.mapPartial (Option.map Thm.term_of) cts);
fun inst_of (v, ct) =
- (Thm.cterm_of (#sign (Thm.rep_cterm ct)) (Var v), ct)
+ (Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct)
handle TYPE (msg, _, _) => err msg;
fun tyinst_of (v, cT) =
- (Thm.ctyp_of (#sign (Thm.rep_ctyp cT)) (TVar v), cT)
+ (Thm.ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT)
handle TYPE (msg, _, _) => err msg;
fun zip_vars _ [] = []
@@ -1005,18 +1002,18 @@
fun rename_bvars [] thm = thm
| rename_bvars vs thm =
let
- val {sign, prop, ...} = rep_thm thm;
+ val {thy, prop, ...} = rep_thm thm;
fun ren (Abs (x, T, t)) = Abs (getOpt (assoc (vs, x), x), T, ren t)
| ren (t $ u) = ren t $ ren u
| ren t = t;
- in equal_elim (reflexive (cterm_of sign (ren prop))) thm end;
+ in equal_elim (reflexive (cterm_of thy (ren prop))) thm end;
(* renaming in left-to-right order *)
fun rename_bvars' xs thm =
let
- val {sign, prop, ...} = rep_thm thm;
+ val {thy, prop, ...} = rep_thm thm;
fun rename [] t = ([], t)
| rename (x' :: xs) (Abs (x, T, t)) =
let val (xs', t') = rename xs t
@@ -1028,7 +1025,7 @@
in (xs'', t' $ u') end
| rename xs t = (xs, t);
in case rename xs prop of
- ([], prop') => equal_elim (reflexive (cterm_of sign prop')) thm
+ ([], prop') => equal_elim (reflexive (cterm_of thy prop')) thm
| _ => error "More names than abstractions in theorem"
end;
@@ -1040,14 +1037,14 @@
fun unvarifyT thm =
let
- val cT = Thm.ctyp_of (Thm.sign_of_thm thm);
+ val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (tvars_of thm);
in instantiate' tfrees [] thm end;
fun unvarify raw_thm =
let
val thm = unvarifyT raw_thm;
- val ct = Thm.cterm_of (Thm.sign_of_thm thm);
+ val ct = Thm.cterm_of (Thm.theory_of_thm thm);
val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (vars_of thm);
in instantiate' [] frees thm end;
@@ -1083,14 +1080,14 @@
(case tvars_of thm of
[] => thm
| tvars =>
- let val cert = Thm.ctyp_of (Thm.sign_of_thm thm)
+ let val cert = Thm.ctyp_of (Thm.theory_of_thm thm)
in instantiate' (map (fn ((x, _), S) => SOME (cert (TFree (x, S)))) tvars) [] thm end);
fun freeze_all_Vars thm =
(case vars_of thm of
[] => thm
| vars =>
- let val cert = Thm.cterm_of (Thm.sign_of_thm thm)
+ let val cert = Thm.cterm_of (Thm.theory_of_thm thm)
in instantiate' [] (map (fn ((x, _), T) => SOME (cert (Free (x, T)))) vars) thm end);
val freeze_all = freeze_all_Vars o freeze_all_TVars;
--- a/src/Pure/thm.ML Fri Jun 17 18:33:05 2005 +0200
+++ b/src/Pure/thm.ML Fri Jun 17 18:33:08 2005 +0200
@@ -3,137 +3,143 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-The core of Isabelle's Meta Logic: certified types and terms, meta
-theorems, meta rules (including lifting and resolution).
+The very core of Isabelle's Meta Logic: certified types and terms,
+meta theorems, meta rules (including lifting and resolution).
*)
signature BASIC_THM =
sig
(*certified types*)
type ctyp
- val rep_ctyp : ctyp -> {sign: Sign.sg, T: typ}
- val typ_of : ctyp -> typ
- val ctyp_of : Sign.sg -> typ -> ctyp
- val read_ctyp : Sign.sg -> string -> ctyp
+ val rep_ctyp: ctyp -> {thy: theory, sign: theory, T: typ}
+ val theory_of_ctyp: ctyp -> theory
+ val typ_of: ctyp -> typ
+ val ctyp_of: theory -> typ -> ctyp
+ val read_ctyp: theory -> string -> ctyp
(*certified terms*)
type cterm
exception CTERM of string
- val rep_cterm : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
- val crep_cterm : cterm -> {sign: Sign.sg, t: term, T: ctyp, maxidx: int}
- val sign_of_cterm : cterm -> Sign.sg
- val term_of : cterm -> term
- val cterm_of : Sign.sg -> term -> cterm
- val ctyp_of_term : cterm -> ctyp
- val read_cterm : Sign.sg -> string * typ -> cterm
- val adjust_maxidx : cterm -> cterm
- val read_def_cterm :
- Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
+ val rep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: typ, maxidx: int}
+ val crep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int}
+ val theory_of_cterm: cterm -> theory
+ val sign_of_cterm: cterm -> theory (*obsolete*)
+ val term_of: cterm -> term
+ val cterm_of: theory -> term -> cterm
+ val ctyp_of_term: cterm -> ctyp
+ val read_cterm: theory -> string * typ -> cterm
+ val adjust_maxidx: cterm -> cterm
+ val read_def_cterm:
+ theory * (indexname -> typ option) * (indexname -> sort option) ->
string list -> bool -> string * typ -> cterm * (indexname * typ) list
- val read_def_cterms :
- Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
+ val read_def_cterms:
+ theory * (indexname -> typ option) * (indexname -> sort option) ->
string list -> bool -> (string * typ)list
-> cterm list * (indexname * typ)list
- type tag (* = string * string list *)
+ type tag (* = string * string list *)
(*meta theorems*)
type thm
- val rep_thm : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int,
- shyps: sort list, hyps: term list,
- tpairs: (term * term) list, prop: term}
- val crep_thm : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int,
- shyps: sort list, hyps: cterm list,
- tpairs: (cterm * cterm) list, prop: cterm}
+ val rep_thm: thm ->
+ {thy: theory, sign: theory,
+ der: bool * Proofterm.proof,
+ maxidx: int,
+ shyps: sort list,
+ hyps: term list,
+ tpairs: (term * term) list,
+ prop: term}
+ val crep_thm: thm ->
+ {thy: theory, sign: theory,
+ der: bool * Proofterm.proof,
+ maxidx: int,
+ shyps: sort list,
+ hyps: cterm list,
+ tpairs: (cterm * cterm) list,
+ prop: cterm}
exception THM of string * int * thm list
- type 'a attribute (* = 'a * thm -> 'a * thm *)
- val eq_thm : thm * thm -> bool
- val eq_thms : thm list * thm list -> bool
- val sign_of_thm : thm -> Sign.sg
- val prop_of : thm -> term
- val proof_of : thm -> Proofterm.proof
- val transfer_sg : Sign.sg -> thm -> thm
- val transfer : theory -> thm -> thm
- val tpairs_of : thm -> (term * term) list
- val prems_of : thm -> term list
- val nprems_of : thm -> int
- val concl_of : thm -> term
- val cprop_of : thm -> cterm
- val extra_shyps : thm -> sort list
- val strip_shyps : thm -> thm
- val get_axiom_i : theory -> string -> thm
- val get_axiom : theory -> xstring -> thm
- val def_name : string -> string
- val get_def : theory -> xstring -> thm
- val axioms_of : theory -> (string * thm) list
+ type 'a attribute (* = 'a * thm -> 'a * thm *)
+ val eq_thm: thm * thm -> bool
+ val eq_thms: thm list * thm list -> bool
+ val theory_of_thm: thm -> theory
+ val sign_of_thm: thm -> theory (*obsolete*)
+ val prop_of: thm -> term
+ val proof_of: thm -> Proofterm.proof
+ val transfer: theory -> thm -> thm
+ val tpairs_of: thm -> (term * term) list
+ val prems_of: thm -> term list
+ val nprems_of: thm -> int
+ val concl_of: thm -> term
+ val cprop_of: thm -> cterm
+ val extra_shyps: thm -> sort list
+ val strip_shyps: thm -> thm
+ val get_axiom_i: theory -> string -> thm
+ val get_axiom: theory -> xstring -> thm
+ val def_name: string -> string
+ val get_def: theory -> xstring -> thm
+ val axioms_of: theory -> (string * thm) list
(*meta rules*)
- val assume : cterm -> thm
- val compress : thm -> thm
- 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 -> cterm -> thm
- val eta_conversion : cterm -> thm
- 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 implies_intr_hyps : thm -> thm
- val flexflex_rule : thm -> thm Seq.seq
- val instantiate :
- (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
- val trivial : cterm -> thm
- val class_triv : Sign.sg -> class -> thm
- val varifyT : thm -> thm
- val varifyT' : (string * sort) list -> thm -> thm * ((string * sort) * indexname) list
- val freezeT : thm -> thm
- val dest_state : thm * int ->
- (term * term) list * term list * term * term
- val lift_rule : (thm * int) -> thm -> thm
- val incr_indexes : int -> thm -> thm
- val assumption : 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 assume: cterm -> thm
+ val compress: thm -> thm
+ 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 -> cterm -> thm
+ val eta_conversion: cterm -> thm
+ 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 implies_intr_hyps: thm -> thm
+ val flexflex_rule: thm -> thm Seq.seq
+ val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
+ val trivial: cterm -> thm
+ val class_triv: theory -> class -> thm
+ val varifyT: thm -> thm
+ val varifyT': (string * sort) list -> thm -> thm * ((string * sort) * indexname) list
+ val freezeT: thm -> thm
+ val dest_state: thm * int -> (term * term) list * term list * term * term
+ val lift_rule: (thm * int) -> thm -> thm
+ val incr_indexes: int -> thm -> thm
+ val assumption: 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 rename_params_rule: string list * int -> thm -> thm
- val bicompose : bool -> bool * thm * int ->
- int -> thm -> thm Seq.seq
- val biresolution : bool -> (bool * thm) list ->
- int -> thm -> thm Seq.seq
- val invoke_oracle_i : theory -> string -> Sign.sg * Object.T -> thm
- val invoke_oracle : theory -> xstring -> Sign.sg * Object.T -> thm
+ val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
+ val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
+ val invoke_oracle: theory -> xstring -> theory * Object.T -> thm
+ val invoke_oracle_i: theory -> string -> theory * Object.T -> thm
end;
signature THM =
sig
include BASIC_THM
- val dest_ctyp : ctyp -> ctyp list
- val dest_comb : cterm -> cterm * cterm
- val dest_abs : string option -> cterm -> cterm * cterm
- val capply : cterm -> cterm -> cterm
- val cabs : cterm -> cterm -> cterm
- val major_prem_of : thm -> term
- val no_prems : thm -> bool
- val no_attributes : 'a -> 'a * 'b attribute list
- val apply_attributes : ('a * thm) * 'a attribute list -> ('a * thm)
- val applys_attributes : ('a * thm list) * 'a attribute list -> ('a * thm list)
- val get_name_tags : thm -> string * tag list
- val put_name_tags : string * tag list -> thm -> thm
- val name_of_thm : thm -> string
- val tags_of_thm : thm -> tag list
- val name_thm : string * thm -> thm
- val rename_boundvars : term -> term -> thm -> thm
- val cterm_match : cterm * cterm ->
- (ctyp * ctyp) list * (cterm * cterm) list
- val cterm_first_order_match : cterm * cterm ->
- (ctyp * ctyp) list * (cterm * cterm) list
- val cterm_incr_indexes : int -> cterm -> cterm
- val terms_of_tpairs : (term * term) list -> term list
+ val dest_ctyp: ctyp -> ctyp list
+ val dest_comb: cterm -> cterm * cterm
+ val dest_abs: string option -> cterm -> cterm * cterm
+ val capply: cterm -> cterm -> cterm
+ val cabs: cterm -> cterm -> cterm
+ val major_prem_of: thm -> term
+ val no_prems: thm -> bool
+ val no_attributes: 'a -> 'a * 'b attribute list
+ val apply_attributes: ('a * thm) * 'a attribute list -> ('a * thm)
+ val applys_attributes: ('a * thm list) * 'a attribute list -> ('a * thm list)
+ val get_name_tags: thm -> string * tag list
+ val put_name_tags: string * tag list -> thm -> thm
+ val name_of_thm: thm -> string
+ val tags_of_thm: thm -> tag list
+ val name_thm: string * thm -> thm
+ val rename_boundvars: term -> term -> thm -> thm
+ val cterm_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
+ val cterm_first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
+ val cterm_incr_indexes: int -> cterm -> cterm
+ val terms_of_tpairs: (term * term) list -> term list
end;
structure Thm: THM =
@@ -143,111 +149,116 @@
(** certified types **)
-(*certified typs under a signature*)
+datatype ctyp = Ctyp of {thy_ref: theory_ref, T: typ};
-datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};
+fun rep_ctyp (Ctyp {thy_ref, T}) =
+ let val thy = Theory.deref thy_ref
+ in {thy = thy, sign = thy, T = T} end;
-fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
+val theory_of_ctyp = #thy o rep_ctyp;
+
fun typ_of (Ctyp {T, ...}) = T;
-fun ctyp_of sign T =
- Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T};
+fun ctyp_of thy T =
+ Ctyp {thy_ref = Theory.self_ref thy, T = Sign.certify_typ thy T};
-fun read_ctyp sign s =
- Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K NONE) s};
+fun read_ctyp thy s =
+ Ctyp {thy_ref = Theory.self_ref thy, T = Sign.read_typ (thy, K NONE) s};
-fun dest_ctyp (Ctyp {sign_ref, T = Type (s, Ts)}) =
- map (fn T => Ctyp {sign_ref = sign_ref, T = T}) Ts
+fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts)}) =
+ map (fn T => Ctyp {thy_ref = thy_ref, T = T}) Ts
| dest_ctyp ct = [ct];
(** certified terms **)
-(*certified terms under a signature, with checked typ and maxidx of Vars*)
+(*certified terms with checked typ and maxidx of Vars/TVars*)
+
+datatype cterm = Cterm of {thy_ref: theory_ref, t: term, T: typ, maxidx: int};
-datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};
+fun rep_cterm (Cterm {thy_ref, t, T, maxidx}) =
+ let val thy = Theory.deref thy_ref
+ in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx} end;
-fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
- {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};
+fun crep_cterm (Cterm {thy_ref, t, T, maxidx}) =
+ let val thy = Theory.deref thy_ref in
+ {thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T}, maxidx = maxidx}
+ end;
-fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) =
- {sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T},
- maxidx = maxidx};
-
-fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref;
+fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref;
+val sign_of_cterm = theory_of_cterm;
fun term_of (Cterm {t, ...}) = t;
-fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};
+fun ctyp_of_term (Cterm {thy_ref, T, ...}) = Ctyp {thy_ref = thy_ref, T = T};
-(*create a cterm by checking a "raw" term with respect to a signature*)
-fun cterm_of sign tm =
- let val (t, T, maxidx) = Sign.certify_term (Sign.pp sign) sign tm
- in Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
+fun cterm_of thy tm =
+ let val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm
+ in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx}
end;
exception CTERM of string;
(*Destruct application in cterms*)
-fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) =
+fun dest_comb (Cterm {thy_ref, T, maxidx, t = A $ B}) =
let val typeA = fastype_of A;
val typeB =
case typeA of Type("fun",[S,T]) => S
| _ => error "Function type expected in dest_comb";
in
- (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA},
- Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB})
+ (Cterm {thy_ref=thy_ref, maxidx=maxidx, t=A, T=typeA},
+ Cterm {thy_ref=thy_ref, maxidx=maxidx, t=B, T=typeB})
end
| dest_comb _ = raise CTERM "dest_comb";
(*Destruct abstraction in cterms*)
-fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) =
- let val (y,N) = variant_abs (getOpt (a,x),ty,M)
- in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)},
- Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N})
+fun dest_abs a (Cterm {thy_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) =
+ let val (y,N) = variant_abs (if_none a x, ty, M)
+ in (Cterm {thy_ref = thy_ref, T = ty, maxidx = 0, t = Free(y,ty)},
+ Cterm {thy_ref = thy_ref, T = S, maxidx = maxidx, t = N})
end
| dest_abs _ _ = raise CTERM "dest_abs";
(*Makes maxidx precise: it is often too big*)
-fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) =
- if maxidx = ~1 then ct
- else Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t};
+fun adjust_maxidx (ct as Cterm {thy_ref, T, t, maxidx, ...}) =
+ if maxidx = ~1 then ct
+ else Cterm {thy_ref = thy_ref, T = T, maxidx = maxidx_of_term t, t = t};
(*Form cterm out of a function and an argument*)
-fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
- (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
+fun capply (Cterm {t=f, thy_ref=thy_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
+ (Cterm {t=x, thy_ref=thy_ref2, T, maxidx=maxidx2}) =
if T = dty then
Cterm{t = f $ x,
- sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
+ thy_ref=Theory.merge_refs(thy_ref1,thy_ref2), T=rty,
maxidx=Int.max(maxidx1, maxidx2)}
else raise CTERM "capply: types don't agree"
| capply _ _ = raise CTERM "capply: first arg is not a function"
-fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
- (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
- Cterm {t = lambda t1 t2, sign_ref = Sign.merge_refs (sign_ref1,sign_ref2),
+fun cabs (Cterm {t=t1, thy_ref=thy_ref1, T=T1, maxidx=maxidx1})
+ (Cterm {t=t2, thy_ref=thy_ref2, T=T2, maxidx=maxidx2}) =
+ Cterm {t = lambda t1 t2, thy_ref = Theory.merge_refs (thy_ref1,thy_ref2),
T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)}
handle TERM _ => raise CTERM "cabs: first arg is not a variable";
(*Matching of cterms*)
fun gen_cterm_match mtch
- (Cterm {sign_ref = sign_ref1, maxidx = maxidx1, t = t1, ...},
- Cterm {sign_ref = sign_ref2, maxidx = maxidx2, t = t2, ...}) =
+ (Cterm {thy_ref = thy_ref1, maxidx = maxidx1, t = t1, ...},
+ Cterm {thy_ref = thy_ref2, maxidx = maxidx2, t = t2, ...}) =
let
- val sign_ref = Sign.merge_refs (sign_ref1, sign_ref2);
- val tsig = Sign.tsig_of (Sign.deref sign_ref);
+ val thy_ref = Theory.merge_refs (thy_ref1, thy_ref2);
+ val tsig = Sign.tsig_of (Theory.deref thy_ref);
val (Tinsts, tinsts) = mtch tsig (t1, t2);
val maxidx = Int.max (maxidx1, maxidx2);
fun mk_cTinsts (ixn, (S, T)) =
- (Ctyp {sign_ref = sign_ref, T = TVar (ixn, S)},
- Ctyp {sign_ref = sign_ref, T = T});
+ (Ctyp {thy_ref = thy_ref, T = TVar (ixn, S)},
+ Ctyp {thy_ref = thy_ref, T = T});
fun mk_ctinsts (ixn, (T, t)) =
let val T = Envir.typ_subst_TVars Tinsts T
in
- (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
- Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t})
+ (Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
+ Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = t})
end;
in (map mk_cTinsts (Vartab.dest Tinsts),
map mk_ctinsts (Vartab.dest tinsts))
@@ -257,10 +268,10 @@
val cterm_first_order_match = gen_cterm_match Pattern.first_order_match;
(*Incrementing indexes*)
-fun cterm_incr_indexes i (ct as Cterm {sign_ref, maxidx, t, T}) =
- if i < 0 then raise CTERM "negative increment" else
+fun cterm_incr_indexes i (ct as Cterm {thy_ref, maxidx, t, T}) =
+ if i < 0 then raise CTERM "negative increment" else
if i = 0 then ct else
- Cterm {sign_ref = sign_ref, maxidx = maxidx + i,
+ Cterm {thy_ref = thy_ref, maxidx = maxidx + i,
t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T};
@@ -268,10 +279,10 @@
(** read cterms **) (*exception ERROR*)
(*read terms, infer types, certify terms*)
-fun read_def_cterms (sign, types, sorts) used freeze sTs =
+fun read_def_cterms (thy, types, sorts) used freeze sTs =
let
- val (ts', tye) = Sign.read_def_terms (sign, types, sorts) used freeze sTs;
- val cts = map (cterm_of sign) ts'
+ val (ts', tye) = Sign.read_def_terms (thy, types, sorts) used freeze sTs;
+ val cts = map (cterm_of thy) ts'
handle TYPE (msg, _, _) => error msg
| TERM (msg, _) => error msg;
in (cts, tye) end;
@@ -281,7 +292,7 @@
let val ([ct],tye) = read_def_cterms args used freeze [aT]
in (ct,tye) end;
-fun read_cterm sign = #1 o read_def_cterm (sign, K NONE, K NONE) [] true;
+fun read_cterm thy = #1 o read_def_cterm (thy, K NONE, K NONE) [] true;
(*tags provide additional comment, apart from the axiom/theorem name*)
@@ -293,7 +304,7 @@
structure Pt = Proofterm;
datatype thm = Thm of
- {sign_ref: Sign.sg_ref, (*mutable reference to signature*)
+ {thy_ref: theory_ref, (*dynamic reference to theory*)
der: bool * Pt.proof, (*derivation*)
maxidx: int, (*maximum index of any Var or TVar*)
shyps: sort list, (*sort hypotheses*)
@@ -306,23 +317,28 @@
fun attach_tpairs tpairs prop =
Logic.list_implies (map Logic.mk_equals tpairs, prop);
-fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
- {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
- shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
+fun rep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+ let val thy = Theory.deref thy_ref in
+ {thy = thy, sign = thy, der = der, maxidx = maxidx,
+ shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
+ end;
-(*Version of rep_thm returning cterms instead of terms*)
-fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
- let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max};
- in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps,
- hyps = map (ctermf ~1) hyps,
- tpairs = map (pairself (ctermf maxidx)) tpairs,
- prop = ctermf maxidx prop}
+(*version of rep_thm returning cterms instead of terms*)
+fun crep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+ let
+ val thy = Theory.deref thy_ref;
+ fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max};
+ in
+ {thy = thy, sign = thy, der = der, maxidx = maxidx, shyps = shyps,
+ hyps = map (cterm ~1) hyps,
+ tpairs = map (pairself (cterm maxidx)) tpairs,
+ prop = cterm maxidx prop}
end;
(*errors involving theorems*)
exception THM of string * int * thm list;
-(*attributes subsume any kind of rules or addXXXs modifiers*)
+(*attributes subsume any kind of rules or context modifiers*)
type 'a attribute = 'a * thm -> 'a * thm;
fun no_attributes x = (x, []);
@@ -331,12 +347,12 @@
fun eq_thm (th1, th2) =
let
- val {sign = sg1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} =
+ val {thy = thy1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} =
rep_thm th1;
- val {sign = sg2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} =
+ val {thy = thy2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} =
rep_thm th2;
in
- Sign.joinable (sg1, sg2) andalso
+ (subthy (thy1, thy2) orelse subthy (thy2, thy1)) andalso
Sorts.eq_set_sort (shyps1, shyps2) andalso
aconvs (hyps1, hyps2) andalso
aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso
@@ -345,30 +361,30 @@
val eq_thms = Library.equal_lists eq_thm;
-fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
+fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref;
+val sign_of_thm = theory_of_thm;
+
fun prop_of (Thm {prop, ...}) = prop;
fun proof_of (Thm {der = (_, proof), ...}) = proof;
-(*merge signatures of two theorems; raise exception if incompatible*)
-fun merge_thm_sgs
- (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
- Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
+(*merge theories of two theorems; raise exception if incompatible*)
+fun merge_thm_thys
+ (th1 as Thm {thy_ref = r1, ...}, th2 as Thm {thy_ref = r2, ...}) =
+ Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
(*transfer thm to super theory (non-destructive)*)
-fun transfer_sg sign' thm =
+fun transfer thy' thm =
let
- val Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm;
- val sign = Sign.deref sign_ref;
+ val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm;
+ val thy = Theory.deref thy_ref;
in
- if Sign.eq_sg (sign, sign') then thm
- else if Sign.subsig (sign, sign') then
- Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
+ if eq_thy (thy, thy') then thm
+ else if subthy (thy, thy') then
+ Thm {thy_ref = Theory.self_ref thy', der = der, maxidx = maxidx,
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
else raise THM ("transfer: not a super theory", 0, [thm])
end;
-val transfer = transfer_sg o Theory.sign_of;
-
(*maps object-rule to tpairs*)
fun tpairs_of (Thm {tpairs, ...}) = tpairs;
@@ -391,8 +407,8 @@
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
(*the statement of any thm is a cterm*)
-fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) =
- Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop};
+fun cprop_of (Thm {thy_ref, maxidx, prop, ...}) =
+ Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop};
@@ -443,16 +459,16 @@
(* fix_shyps *)
-fun all_sorts_nonempty sign_ref = isSome (Sign.universal_witness (Sign.deref sign_ref));
+val all_sorts_nonempty = is_some o Sign.universal_witness o Theory.deref;
(*preserve sort contexts of rule premises and substituted types*)
-fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, tpairs, prop, ...}) =
+fun fix_shyps thms Ts (thm as Thm {thy_ref, der, maxidx, hyps, tpairs, prop, ...}) =
Thm
- {sign_ref = sign_ref,
+ {thy_ref = thy_ref,
der = der, (*no new derivation, as other rules call this*)
maxidx = maxidx,
shyps =
- if all_sorts_nonempty sign_ref then []
+ if all_sorts_nonempty thy_ref then []
else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))),
hyps = hyps, tpairs = tpairs, prop = prop}
@@ -461,15 +477,14 @@
(*remove extra sorts that are non-empty by virtue of type signature information*)
fun strip_shyps (thm as Thm {shyps = [], ...}) = thm
- | strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+ | strip_shyps (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
let
- val sign = Sign.deref sign_ref;
-
+ val thy = Theory.deref thy_ref;
val present_sorts = add_thm_sorts (thm, []);
val extra_shyps = Sorts.rems_sort (shyps, present_sorts);
- val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps;
+ val witnessed_shyps = Sign.witness_sorts thy present_sorts extra_shyps;
in
- Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
+ Thm {thy_ref = thy_ref, der = der, maxidx = maxidx,
shyps = Sorts.rems_sort (shyps, map #2 witnessed_shyps),
hyps = hyps, tpairs = tpairs, prop = prop}
end;
@@ -478,33 +493,28 @@
(** Axioms **)
-(*look up the named axiom in the theory*)
+(*look up the named axiom in the theory or its ancestors*)
fun get_axiom_i theory name =
let
- fun get_ax [] = NONE
- | get_ax (thy :: thys) =
- let val {sign, axioms = (_, axioms), ...} = Theory.rep_theory thy in
- (case Symtab.lookup (axioms, name) of
- SOME t =>
- SOME (fix_shyps [] []
- (Thm {sign_ref = Sign.self_ref sign,
- der = Pt.infer_derivs' I
- (false, Pt.axm_proof name t),
- maxidx = maxidx_of_term t,
- shyps = [],
- hyps = [],
- tpairs = [],
- prop = t}))
- | NONE => get_ax thys)
- end;
+ fun get_ax thy =
+ Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name)
+ |> Option.map (fn t =>
+ fix_shyps [] []
+ (Thm {thy_ref = Theory.self_ref thy,
+ der = Pt.infer_derivs' I (false, Pt.axm_proof name t),
+ maxidx = maxidx_of_term t,
+ shyps = [],
+ hyps = [],
+ tpairs = [],
+ prop = t}));
in
- (case get_ax (theory :: Theory.ancestors_of theory) of
+ (case get_first get_ax (theory :: Theory.ancestors_of theory) of
SOME thm => thm
| NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
end;
fun get_axiom thy =
- get_axiom_i thy o NameSpace.intern (#1 (#axioms (Theory.rep_theory thy)));
+ get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy);
fun def_name name = name ^ "_def";
fun get_def thy = get_axiom thy o def_name;
@@ -521,9 +531,9 @@
fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) =
Pt.get_name_tags hyps prop prf;
-fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx,
- shyps, hyps, tpairs = [], prop}) = Thm {sign_ref = sign_ref,
- der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf),
+fun put_name_tags x (Thm {thy_ref, der = (ora, prf), maxidx,
+ shyps, hyps, tpairs = [], prop}) = Thm {thy_ref = thy_ref,
+ der = (ora, Pt.thm_proof (Theory.deref thy_ref) x hyps prop prf),
maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop}
| put_name_tags _ thm =
raise THM ("put_name_tags: unsolved flex-flex constraints", 0, [thm]);
@@ -536,12 +546,12 @@
(*Compression of theorems -- a separate rule, not integrated with the others,
as it could be slow.*)
-fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
- Thm {sign_ref = sign_ref,
+fun compress (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+ Thm {thy_ref = thy_ref,
der = der, (*No derivation recorded!*)
maxidx = maxidx,
- shyps = shyps,
- hyps = map Term.compress_term hyps,
+ shyps = shyps,
+ hyps = map Term.compress_term hyps,
tpairs = map (pairself Term.compress_term) tpairs,
prop = Term.compress_term prop};
@@ -556,17 +566,17 @@
(*The assumption rule A|-A in a theory*)
fun assume raw_ct : thm =
- let val ct as Cterm {sign_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
+ let val ct as Cterm {thy_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
in if T<>propT then
raise THM("assume: assumptions must have type prop", 0, [])
else if maxidx <> ~1 then
raise THM("assume: assumptions may not contain scheme variables",
maxidx, [])
- else Thm{sign_ref = sign_ref,
+ else Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' I (false, Pt.Hyp prop),
- maxidx = ~1,
- shyps = add_term_sorts(prop,[]),
- hyps = [prop],
+ maxidx = ~1,
+ shyps = add_term_sorts(prop,[]),
+ hyps = [prop],
tpairs = [],
prop = prop}
end;
@@ -578,12 +588,12 @@
-------
A ==> B
*)
-fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs,prop}) : thm =
- let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA
+fun implies_intr cA (thB as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs,prop}) : thm =
+ let val Cterm {thy_ref=thy_refA, t=A, T, maxidx=maxidxA} = cA
in if T<>propT then
raise THM("implies_intr: assumptions must have type prop", 0, [thB])
else
- Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA),
+ Thm{thy_ref = Theory.merge_refs (thy_ref,thy_refA),
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
maxidx = Int.max(maxidxA, maxidx),
shyps = add_term_sorts (A, shyps),
@@ -591,7 +601,7 @@
tpairs = tpairs,
prop = implies$A$prop}
handle TERM _ =>
- raise THM("implies_intr: incompatible signatures", 0, [thB])
+ raise THM("implies_intr: incompatible theories", 0, [thB])
end;
@@ -608,7 +618,7 @@
imp$A$B =>
if imp=implies andalso A aconv propA
then
- Thm{sign_ref= merge_thm_sgs(thAB,thA),
+ Thm{thy_ref= merge_thm_thys (thAB, thA),
der = Pt.infer_derivs (curry Pt.%%) der derA,
maxidx = Int.max(maxA,maxidx),
shyps = Sorts.union_sort (shypsA, shyps),
@@ -624,10 +634,10 @@
-----
!!x.A
*)
-fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,tpairs,prop,...}) =
+fun forall_intr cx (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) =
let val x = term_of cx;
fun result a T = fix_shyps [th] []
- (Thm{sign_ref = sign_ref,
+ (Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der,
maxidx = maxidx,
shyps = [],
@@ -649,35 +659,35 @@
------
A[t/x]
*)
-fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,tpairs,prop,...}) : thm =
- let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct
+fun forall_elim ct (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) : thm =
+ let val Cterm {thy_ref=thy_reft, t, T, maxidx=maxt} = ct
in case prop of
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
if T<>qary then
raise THM("forall_elim: type mismatch", 0, [th])
else fix_shyps [th] []
- (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
+ (Thm{thy_ref= Theory.merge_refs(thy_ref,thy_reft),
der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
maxidx = Int.max(maxidx, maxt),
shyps = [],
- hyps = hyps,
+ hyps = hyps,
tpairs = tpairs,
prop = betapply(A,t)})
| _ => raise THM("forall_elim: not quantified", 0, [th])
end
handle TERM _ =>
- raise THM("forall_elim: incompatible signatures", 0, [th]);
+ raise THM("forall_elim: incompatible theories", 0, [th]);
(* Equality *)
(*The reflexivity rule: maps t to the theorem t==t *)
fun reflexive ct =
- let val Cterm {sign_ref, t, T, maxidx} = ct
- in Thm{sign_ref= sign_ref,
+ let val Cterm {thy_ref, t, T, maxidx} = ct
+ in Thm{thy_ref= thy_ref,
der = Pt.infer_derivs' I (false, Pt.reflexive),
shyps = add_term_sorts (t, []),
- hyps = [],
+ hyps = [],
maxidx = maxidx,
tpairs = [],
prop = Logic.mk_equals(t,t)}
@@ -688,11 +698,11 @@
----
u==t
*)
-fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
+fun symmetric (th as Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
case prop of
(eq as Const("==", Type (_, [T, _]))) $ t $ u =>
(*no fix_shyps*)
- Thm{sign_ref = sign_ref,
+ Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' Pt.symmetric der,
maxidx = maxidx,
shyps = shyps,
@@ -709,14 +719,14 @@
fun transitive th1 th2 =
let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, tpairs=tpairs1, prop=prop1,...} = th1
and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, tpairs=tpairs2, prop=prop2,...} = th2;
- fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
+ fun err msg = raise THM("transitive: "^msg, 0, [th1,th2])
in case (prop1,prop2) of
((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) =>
if not (u aconv u') then err"middle term"
else
- Thm{sign_ref= merge_thm_sgs(th1,th2),
+ Thm{thy_ref= merge_thm_thys (th1, th2),
der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
- maxidx = Int.max(max1,max2),
+ maxidx = Int.max(max1,max2),
shyps = Sorts.union_sort (shyps1, shyps2),
hyps = union_term(hyps1,hyps2),
tpairs = tpairs1 @ tpairs2,
@@ -728,9 +738,9 @@
Fully beta-reduces the term if full=true
*)
fun beta_conversion full ct =
- let val Cterm {sign_ref, t, T, maxidx} = ct
+ let val Cterm {thy_ref, t, T, maxidx} = ct
in Thm
- {sign_ref = sign_ref,
+ {thy_ref = thy_ref,
der = Pt.infer_derivs' I (false, Pt.reflexive),
maxidx = maxidx,
shyps = add_term_sorts (t, []),
@@ -743,9 +753,9 @@
end;
fun eta_conversion ct =
- let val Cterm {sign_ref, t, T, maxidx} = ct
+ let val Cterm {thy_ref, t, T, maxidx} = ct
in Thm
- {sign_ref = sign_ref,
+ {thy_ref = thy_ref,
der = Pt.infer_derivs' I (false, Pt.reflexive),
maxidx = maxidx,
shyps = add_term_sorts (t, []),
@@ -760,16 +770,16 @@
------------
%x.t == %x.u
*)
-fun abstract_rule a cx (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs,prop}) =
+fun abstract_rule a cx (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs,prop}) =
let val x = term_of cx;
val (t,u) = Logic.dest_equals prop
handle TERM _ =>
raise THM("abstract_rule: premise not an equality", 0, [th])
fun result T =
- Thm{sign_ref = sign_ref,
+ Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' (Pt.abstract_rule x a) der,
- maxidx = maxidx,
- shyps = add_typ_sorts (T, shyps),
+ maxidx = maxidx,
+ shyps = add_typ_sorts (T, shyps),
hyps = hyps,
tpairs = tpairs,
prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
@@ -790,27 +800,27 @@
f(t) == g(u)
*)
fun combination th1 th2 =
- let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
+ let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
tpairs=tpairs1, prop=prop1,...} = th1
- and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2,
+ and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2,
tpairs=tpairs2, prop=prop2,...} = th2
fun chktypes fT tT =
(case fT of
- Type("fun",[T1,T2]) =>
+ Type("fun",[T1,T2]) =>
if T1 <> tT then
raise THM("combination: types", 0, [th1,th2])
else ()
- | _ => raise THM("combination: not function type", 0,
+ | _ => raise THM("combination: not function type", 0,
[th1,th2]))
in case (prop1,prop2) of
(Const ("==", Type ("fun", [fT, _])) $ f $ g,
Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
(chktypes fT tT;
(*no fix_shyps*)
- Thm{sign_ref = merge_thm_sgs(th1,th2),
+ Thm{thy_ref = merge_thm_thys(th1,th2),
der = Pt.infer_derivs
(Pt.combination f g t u fT) der1 der2,
- maxidx = Int.max(max1,max2),
+ maxidx = Int.max(max1,max2),
shyps = Sorts.union_sort(shyps1,shyps2),
hyps = union_term(hyps1,hyps2),
tpairs = tpairs1 @ tpairs2,
@@ -825,9 +835,9 @@
A == B
*)
fun equal_intr th1 th2 =
- let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
+ let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
tpairs=tpairs1, prop=prop1,...} = th1
- and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2,
+ and Thm{der=der2, maxidx=max2, 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
@@ -835,7 +845,7 @@
if A aconv A' andalso B aconv B'
then
(*no fix_shyps*)
- Thm{sign_ref = merge_thm_sgs(th1,th2),
+ Thm{thy_ref = merge_thm_thys(th1,th2),
der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
maxidx = Int.max(max1,max2),
shyps = Sorts.union_sort(shyps1,shyps2),
@@ -860,7 +870,7 @@
Const("==",_) $ A $ B =>
if not (prop2 aconv A) then err"not equal" else
fix_shyps [th1, th2] []
- (Thm{sign_ref= merge_thm_sgs(th1,th2),
+ (Thm{thy_ref= merge_thm_thys(th1,th2),
der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2,
maxidx = Int.max(max1,max2),
shyps = [],
@@ -876,13 +886,13 @@
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps.
Repeated hypotheses are discharged only once; fold cannot do this*)
-fun implies_intr_hyps (Thm{sign_ref, der, maxidx, shyps, hyps=A::As, tpairs, prop}) =
+fun implies_intr_hyps (Thm{thy_ref, der, maxidx, shyps, hyps=A::As, tpairs, prop}) =
implies_intr_hyps (*no fix_shyps*)
- (Thm{sign_ref = sign_ref,
+ (Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
- maxidx = maxidx,
+ maxidx = maxidx,
shyps = shyps,
- hyps = disch(As,A),
+ hyps = disch(As,A),
tpairs = tpairs,
prop = implies$A$prop})
| implies_intr_hyps th = th;
@@ -891,7 +901,7 @@
Instantiates the theorem and deletes trivial tpairs.
Resulting sequence may contain multiple elements if the tpairs are
not all flex-flex. *)
-fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, tpairs, prop, ...}) =
+fun flexflex_rule (th as Thm{thy_ref, der, maxidx, hyps, tpairs, prop, ...}) =
let fun newthm env =
if Envir.is_empty env then th
else
@@ -900,17 +910,17 @@
(*Remove trivial tpairs, of the form t=t*)
val distpairs = List.filter (not o op aconv) ntpairs
in fix_shyps [th] (env_codT env)
- (Thm{sign_ref = sign_ref,
+ (Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' (Pt.norm_proof' env) der,
maxidx = maxidx_of_terms (newprop ::
terms_of_tpairs distpairs),
- shyps = [],
+ shyps = [],
hyps = hyps,
tpairs = distpairs,
prop = newprop})
end;
in Seq.map newthm
- (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
+ (Unify.smash_unifiers(Theory.deref thy_ref, Envir.empty maxidx, tpairs))
end;
(*Instantiation of Vars
@@ -924,42 +934,39 @@
(*Check that all the terms are Vars and are distinct*)
fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
-fun prt_typing sg_ref t T =
- let val sg = Sign.deref sg_ref in
- Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T]
- end;
-
-fun prt_type sg_ref T = Sign.pretty_typ (Sign.deref sg_ref) T;
+fun pretty_typing thy t T =
+ Pretty.block [Sign.pretty_term thy t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ thy T];
(*For instantiate: process pair of cterms, merge theories*)
-fun add_ctpair ((ct,cu), (sign_ref,tpairs)) =
+fun add_ctpair ((ct,cu), (thy_ref,tpairs)) =
let
- val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct
- and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu;
- val sign_ref_merged = Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu));
+ val Cterm {thy_ref=thy_reft, t=t, T= T, ...} = ct
+ and Cterm {thy_ref=thy_refu, t=u, T= U, ...} = cu;
+ val thy_ref_merged = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_reft, thy_refu));
+ val thy_merged = Theory.deref thy_ref_merged;
in
- if T=U then (sign_ref_merged, (t,u)::tpairs)
+ if T=U then (thy_ref_merged, (t,u)::tpairs)
else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict",
- Pretty.fbrk, prt_typing sign_ref_merged t T,
- Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u])
+ Pretty.fbrk, pretty_typing thy_merged t T,
+ Pretty.fbrk, pretty_typing thy_merged u U]), [T,U], [t,u])
end;
-fun add_ctyp ((Ctyp {T = T as TVar (_, S), sign_ref = sign_refT},
- Ctyp {T = U, sign_ref = sign_refU}), (sign_ref, vTs)) =
+fun add_ctyp ((Ctyp {T = T as TVar (_, S), thy_ref = thy_refT},
+ Ctyp {T = U, thy_ref = thy_refU}), (thy_ref, vTs)) =
let
- val sign_ref_merged = Sign.merge_refs
- (sign_ref, Sign.merge_refs (sign_refT, sign_refU));
- val sign = Sign.deref sign_ref_merged
+ val thy_ref_merged = Theory.merge_refs
+ (thy_ref, Theory.merge_refs (thy_refT, thy_refU));
+ val thy_merged = Theory.deref thy_ref_merged
in
- if Type.of_sort (Sign.tsig_of sign) (U, S) then
- (sign_ref_merged, (T, U) :: vTs)
+ if Type.of_sort (Sign.tsig_of thy_merged) (U, S) then
+ (thy_ref_merged, (T, U) :: vTs)
else raise TYPE ("Type not of sort " ^
- Sign.string_of_sort sign S, [U], [])
+ Sign.string_of_sort thy_merged S, [U], [])
end
- | add_ctyp ((Ctyp {T, sign_ref}, _), _) =
+ | add_ctyp ((Ctyp {T, thy_ref}, _), _) =
raise TYPE (Pretty.string_of (Pretty.block
[Pretty.str "instantiate: not a type variable",
- Pretty.fbrk, prt_type sign_ref T]), [T], []);
+ Pretty.fbrk, Sign.pretty_typ (Theory.deref thy_ref) T]), [T], []);
in
@@ -967,18 +974,18 @@
Instantiates distinct Vars by terms of same type.
No longer normalizes the new theorem! *)
fun instantiate ([], []) th = th
- | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) =
- let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs;
- val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs;
+ | instantiate (vcTs,ctpairs) (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) =
+ let val (newthy_ref,tpairs) = foldr add_ctpair (thy_ref,[]) ctpairs;
+ val (newthy_ref,vTs) = foldr add_ctyp (newthy_ref,[]) vcTs;
fun subst t =
subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t);
val newprop = subst prop;
val newdpairs = map (pairself subst) dpairs;
val newth =
- (Thm{sign_ref = newsign_ref,
+ (Thm{thy_ref = newthy_ref,
der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der,
maxidx = maxidx_of_terms (newprop ::
- terms_of_tpairs newdpairs),
+ terms_of_tpairs newdpairs),
shyps = add_insts_sorts ((vTs, tpairs), shyps),
hyps = hyps,
tpairs = newdpairs,
@@ -989,7 +996,7 @@
then raise THM("instantiate: type variables not distinct", 0, [th])
else newth
end
- handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th])
+ handle TERM _ => raise THM("instantiate: incompatible theories", 0, [th])
| TYPE (msg, _, _) => raise THM (msg, 0, [th]);
end;
@@ -998,49 +1005,49 @@
(*The trivial implication A==>A, justified by assume and forall rules.
A can contain Vars, not so for assume! *)
fun trivial ct : thm =
- let val Cterm {sign_ref, t=A, T, maxidx} = ct
+ let val Cterm {thy_ref, t=A, T, maxidx} = ct
in if T<>propT then
raise THM("trivial: the term must have type prop", 0, [])
else fix_shyps [] []
- (Thm{sign_ref = sign_ref,
+ (Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)),
- maxidx = maxidx,
- shyps = [],
+ maxidx = maxidx,
+ shyps = [],
hyps = [],
tpairs = [],
prop = implies$A$A})
end;
(*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
-fun class_triv sign c =
- let val Cterm {sign_ref, t, maxidx, ...} =
- cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
+fun class_triv thy c =
+ let val Cterm {thy_ref, t, maxidx, ...} =
+ cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
in
fix_shyps [] []
- (Thm {sign_ref = sign_ref,
+ (Thm {thy_ref = thy_ref,
der = Pt.infer_derivs' I
(false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])),
- maxidx = maxidx,
- shyps = [],
- hyps = [],
+ maxidx = maxidx,
+ shyps = [],
+ hyps = [],
tpairs = [],
prop = t})
end;
(* Replace all TFrees not fixed or in the hyps by new TVars *)
-fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
+fun varifyT' fixed (Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
let
val tfrees = foldr add_term_tfrees fixed hyps;
val prop1 = attach_tpairs tpairs prop;
val (prop2, al) = Type.varify (prop1, tfrees);
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
in (*no fix_shyps*)
- (Thm{sign_ref = sign_ref,
+ (Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
- maxidx = Int.max(0,maxidx),
- shyps = shyps,
+ maxidx = Int.max(0,maxidx),
+ shyps = shyps,
hyps = hyps,
tpairs = rev (map Logic.dest_equals ts),
prop = prop3}, al)
@@ -1049,13 +1056,13 @@
val varifyT = #1 o varifyT' [];
(* Replace all TVars by new TFrees *)
-fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
+fun freezeT(Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
let
val prop1 = attach_tpairs tpairs prop;
val prop2 = Type.freeze prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
in (*no fix_shyps*)
- Thm{sign_ref = sign_ref,
+ Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' (Pt.freezeT prop1) der,
maxidx = maxidx_of_term prop2,
shyps = shyps,
@@ -1077,27 +1084,27 @@
(*Increment variables and parameters of orule as required for
resolution with goal i of state. *)
fun lift_rule (state, i) orule =
- let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state
+ let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, thy_ref=sthy_ref,...} = state
val (Bi::_, _) = Logic.strip_prems(i, [], sprop)
handle TERM _ => raise THM("lift_rule", i, [orule,state])
- val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi}
+ val ct_Bi = Cterm {thy_ref=sthy_ref, maxidx=smax, T=propT, t=Bi}
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1)
- val (Thm{sign_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule
+ val (Thm{thy_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule
val (As, B) = Logic.strip_horn prop
in (*no fix_shyps*)
- Thm{sign_ref = merge_thm_sgs(state,orule),
+ Thm{thy_ref = merge_thm_thys(state,orule),
der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der,
maxidx = maxidx+smax+1,
- shyps = Sorts.union_sort(sshyps,shyps),
- hyps = hyps,
+ shyps = Sorts.union_sort(sshyps,shyps),
+ hyps = hyps,
tpairs = map (pairself lift_abs) tpairs,
prop = Logic.list_implies (map lift_all As, lift_all B)}
end;
-fun incr_indexes i (thm as Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
if i < 0 then raise THM ("negative increment", 0, [thm]) else
if i = 0 then thm else
- Thm {sign_ref = sign_ref,
+ Thm {thy_ref = thy_ref,
der = Pt.infer_derivs' (Pt.map_proof_terms
(Logic.incr_indexes ([], i)) (incr_tvar i)) der,
maxidx = maxidx + i,
@@ -1108,11 +1115,11 @@
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
fun assumption i state =
- let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
+ let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state;
val (tpairs, Bs, Bi, C) = dest_state(state,i)
fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) =
fix_shyps [state] (env_codT env)
- (Thm{sign_ref = sign_ref,
+ (Thm{thy_ref = thy_ref,
der = Pt.infer_derivs'
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
Pt.assumption_proof Bs Bi n) der,
@@ -1121,7 +1128,7 @@
hyps = hyps,
tpairs = if Envir.is_empty env then tpairs else
map (pairself (Envir.norm_term env)) tpairs,
- prop =
+ prop =
if Envir.is_empty env then (*avoid wasted normalizations*)
Logic.list_implies (Bs, C)
else (*normalize the new rule fully*)
@@ -1129,19 +1136,19 @@
fun addprfs [] _ = Seq.empty
| addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull
(Seq.mapp (newth n)
- (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
+ (Unify.unifiers(Theory.deref thy_ref,Envir.empty maxidx, (t,u)::tpairs))
(addprfs apairs (n+1))))
in addprfs (Logic.assum_pairs (~1,Bi)) 1 end;
(*Solve subgoal Bi of proof state B1...Bn/C by assumption.
Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
fun eq_assumption i state =
- let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
+ let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state;
val (tpairs, Bs, Bi, C) = dest_state(state,i)
in (case find_index (op aconv) (Logic.assum_pairs (~1,Bi)) of
(~1) => raise THM("eq_assumption", 0, [state])
| n => fix_shyps [state] []
- (Thm{sign_ref = sign_ref,
+ (Thm{thy_ref = thy_ref,
der = Pt.infer_derivs'
(Pt.assumption_proof Bs Bi (n+1)) der,
maxidx = maxidx,
@@ -1154,7 +1161,7 @@
(*For rotate_tac: fast rotation of assumptions of subgoal i*)
fun rotate_rule k i state =
- let val Thm{sign_ref,der,maxidx,hyps,prop,shyps,...} = state;
+ let val Thm{thy_ref,der,maxidx,hyps,prop,shyps,...} = state;
val (tpairs, Bs, Bi, C) = dest_state(state,i)
val params = Term.strip_all_vars Bi
and rest = Term.strip_all_body Bi
@@ -1163,19 +1170,19 @@
val n = length asms
val m = if k<0 then n+k else k
val Bi' = if 0=m orelse m=n then Bi
- else if 0<m andalso m<n
- then let val (ps,qs) = splitAt(m,asms)
+ else if 0<m andalso m<n
+ then let val (ps,qs) = splitAt(m,asms)
in list_all(params, Logic.list_implies(qs @ ps, concl))
- end
- else raise THM("rotate_rule", k, [state])
+ end
+ else raise THM("rotate_rule", k, [state])
in (*no fix_shyps*)
- Thm{sign_ref = sign_ref,
+ Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
- maxidx = maxidx,
- shyps = shyps,
- hyps = hyps,
+ maxidx = maxidx,
+ shyps = shyps,
+ hyps = hyps,
tpairs = tpairs,
- prop = Logic.list_implies (Bs @ [Bi'], C)}
+ prop = Logic.list_implies (Bs @ [Bi'], C)}
end;
@@ -1183,7 +1190,7 @@
unchanged. Does nothing if k=0 or if k equals n-j, where n is the
number of premises. Useful with etac and underlies tactic/defer_tac*)
fun permute_prems j k rl =
- let val Thm{sign_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl
+ let val Thm{thy_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl
val prems = Logic.strip_imp_prems prop
and concl = Logic.strip_imp_concl prop
val moved_prems = List.drop(prems, j)
@@ -1192,18 +1199,18 @@
val n_j = length moved_prems
val m = if k<0 then n_j + k else k
val prop' = if 0 = m orelse m = n_j then prop
- else if 0<m andalso m<n_j
- then let val (ps,qs) = splitAt(m,moved_prems)
- in Logic.list_implies(fixed_prems @ qs @ ps, concl) end
- else raise THM("permute_prems:k", k, [rl])
+ else if 0<m andalso m<n_j
+ then let val (ps,qs) = splitAt(m,moved_prems)
+ in Logic.list_implies(fixed_prems @ qs @ ps, concl) end
+ else raise THM("permute_prems:k", k, [rl])
in (*no fix_shyps*)
- Thm{sign_ref = sign_ref,
+ Thm{thy_ref = thy_ref,
der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
- maxidx = maxidx,
- shyps = shyps,
- hyps = hyps,
+ maxidx = maxidx,
+ shyps = shyps,
+ hyps = hyps,
tpairs = tpairs,
- prop = prop'}
+ prop = prop'}
end;
@@ -1214,7 +1221,7 @@
The names in cs, if distinct, are used for the innermost parameters;
preceding parameters may be renamed to make all params distinct.*)
fun rename_params_rule (cs, i) state =
- let val Thm{sign_ref,der,maxidx,hyps,shyps,...} = state
+ let val Thm{thy_ref,der,maxidx,hyps,shyps,...} = state
val (tpairs, Bs, Bi, C) = dest_state(state,i)
val iparams = map #1 (Logic.strip_params Bi)
val short = length iparams - length cs
@@ -1225,12 +1232,12 @@
val newBi = Logic.list_rename_params (newnames, Bi)
in
case findrep cs of
- c::_ => (warning ("Can't rename. Bound variables not distinct: " ^ c);
- state)
+ c::_ => (warning ("Can't rename. Bound variables not distinct: " ^ c);
+ state)
| [] => (case cs inter_string freenames of
- a::_ => (warning ("Can't rename. Bound/Free variable clash: " ^ a);
- state)
- | [] => Thm{sign_ref = sign_ref,
+ a::_ => (warning ("Can't rename. Bound/Free variable clash: " ^ a);
+ state)
+ | [] => Thm{thy_ref = thy_ref,
der = der,
maxidx = maxidx,
shyps = shyps,
@@ -1242,11 +1249,11 @@
(*** Preservation of bound variable names ***)
-fun rename_boundvars pat obj (thm as Thm {sign_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
+fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
(case Term.rename_abs pat obj prop of
NONE => thm
| SOME prop' => Thm
- {sign_ref = sign_ref,
+ {thy_ref = thy_ref,
der = der,
maxidx = maxidx,
hyps = hyps,
@@ -1280,7 +1287,7 @@
else Var((y,i),T)
| NONE=> t)
| rename(Abs(x,T,t)) =
- Abs(getOpt(assoc_string(al,x),x), T, rename t)
+ Abs (if_none (assoc_string (al, x)) x, T, rename t)
| rename(f$t) = rename f $ rename t
| rename(t) = t;
fun strip_ren Ai = strip_apply rename (Ai,B)
@@ -1332,13 +1339,13 @@
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
(eres_flg, orule, nsubgoal) =
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state
- and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps,
+ and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps,
tpairs=rtpairs, prop=rprop,...} = orule
(*How many hyps to skip over during normalization*)
and nlift = Logic.count_prems(strip_all_body Bi,
if eres_flg then ~1 else 0)
- val sign_ref = merge_thm_sgs(state,orule);
- val sign = Sign.deref sign_ref;
+ val thy_ref = merge_thm_thys(state,orule);
+ val thy = Theory.deref thy_ref;
(** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
let val normt = Envir.norm_term env;
@@ -1357,7 +1364,7 @@
(ntps, (map normt (Bs @ As), normt C))
end
val th = (*tuned fix_shyps*)
- Thm{sign_ref = sign_ref,
+ Thm{thy_ref = thy_ref,
der = Pt.infer_derivs
((if Envir.is_empty env then I
else if Envir.above (smax, env) then
@@ -1390,12 +1397,12 @@
(*elim-resolution: try each assumption in turn. Initially n=1*)
fun tryasms (_, _, _, []) = Seq.empty
| tryasms (A, As, n, (t,u)::apairs) =
- (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of
- NONE => tryasms (A, As, n+1, apairs)
- | cell as SOME((_,tpairs),_) =>
- Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
- (Seq.make(fn()=> cell),
- Seq.make(fn()=> Seq.pull (tryasms(A, As, n+1, apairs)))))
+ (case Seq.pull(Unify.unifiers(thy, env, (t,u)::dpairs)) of
+ NONE => tryasms (A, As, n+1, apairs)
+ | cell as SOME((_,tpairs),_) =>
+ Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
+ (Seq.make(fn()=> cell),
+ Seq.make(fn()=> Seq.pull (tryasms(A, As, n+1, apairs)))))
fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
| eres (A1::As) = tryasms(SOME A1, As, 1, Logic.assum_pairs(nlift+1,A1))
(*ordinary resolution*)
@@ -1404,7 +1411,7 @@
Seq.it_right (addth NONE (newAs(rev rAs, 0, [BBi], tpairs)))
(Seq.make (fn()=> cell), Seq.empty)
in if eres_flg then eres(rev rAs)
- else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
+ else res(Seq.pull(Unify.unifiers(thy, env, dpairs)))
end;
end;
@@ -1442,36 +1449,34 @@
(*** Oracles ***)
-fun invoke_oracle_i thy name =
+fun invoke_oracle_i thy1 name =
let
- val {sign = sg, oracles = (_, oracles), ...} = Theory.rep_theory thy;
val oracle =
- (case Symtab.lookup (oracles, name) of
+ (case Symtab.lookup (#2 (#oracles (Theory.rep_theory thy1)), name) of
NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
| SOME (f, _) => f);
in
- fn (sign, exn) =>
+ fn (thy2, data) =>
let
- val sign_ref' = Sign.merge_refs (Sign.self_ref sg, Sign.self_ref sign);
- val sign' = Sign.deref sign_ref';
+ val thy' = Theory.merge (thy1, thy2);
val (prop, T, maxidx) =
- Sign.certify_term (Sign.pp sign') sign' (oracle (sign', exn));
+ Sign.certify_term (Sign.pp thy') thy' (oracle (thy', data));
in
if T <> propT then
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else fix_shyps [] []
- (Thm {sign_ref = sign_ref',
+ (Thm {thy_ref = Theory.self_ref thy',
der = (true, Pt.oracle_proof name prop),
maxidx = maxidx,
- shyps = [],
- hyps = [],
+ shyps = [],
+ hyps = [],
tpairs = [],
prop = prop})
end
end;
fun invoke_oracle thy =
- invoke_oracle_i thy o NameSpace.intern (#1 (#oracles (Theory.rep_theory thy)));
+ invoke_oracle_i thy o NameSpace.intern (Theory.oracle_space thy);
end;