# HG changeset patch # User wenzelm # Date 1119025988 -7200 # Node ID 2427be27cc60eb6a7289ef6d6246bb4d2d8fc0e7 # Parent 18a07ad8fea81ecc72d2370ebbe485b4ac14d81f accomodate identification of type Sign.sg and theory; diff -r 18a07ad8fea8 -r 2427be27cc60 TFL/casesplit.ML --- a/TFL/casesplit.ML Fri Jun 17 18:33:05 2005 +0200 +++ b/TFL/casesplit.ML Fri Jun 17 18:33:08 2005 +0200 @@ -121,7 +121,7 @@ (* get the case_thm (my version) from a type *) fun case_thm_of_ty sgn ty = let - val dtypestab = DatatypePackage.get_datatypes_sg sgn; + val dtypestab = DatatypePackage.get_datatypes sgn; val ty_str = case ty of Type(ty_str, _) => ty_str | TFree(s,_) => raise ERROR_MESSAGE diff -r 18a07ad8fea8 -r 2427be27cc60 src/HOLCF/IOA/Modelcheck/MuIOA.ML --- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML Fri Jun 17 18:33:05 2005 +0200 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML Fri Jun 17 18:33:08 2005 +0200 @@ -164,7 +164,7 @@ fun mk_sim_oracle (sign, SimOracleExn (subgoal,thl)) = (let - val weak_case_congs = DatatypePackage.weak_case_congs_of_sg sign; + val weak_case_congs = DatatypePackage.weak_case_congs_of sign; val concl = (Logic.strip_imp_concl subgoal); diff -r 18a07ad8fea8 -r 2427be27cc60 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Fri Jun 17 18:33:05 2005 +0200 +++ b/src/Pure/Isar/isar_thy.ML Fri Jun 17 18:33:08 2005 +0200 @@ -186,9 +186,8 @@ (case assoc_string (kinds, kind) of SOME (intern, check, hide) => let - val sg = Theory.sign_of thy; - val names = if int then map (intern sg) xnames else xnames; - val bads = filter_out (check sg) names; + val names = if int then map (intern thy) xnames else xnames; + val bads = filter_out (check thy) names; in if null bads then hide true names thy else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads) @@ -313,6 +312,8 @@ fun pretty_results ctxt ((kind, ""), facts) = Pretty.block (Pretty.str kind :: Pretty.brk 1 :: prt_facts ctxt facts) + | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1, + [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact]) | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1, [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Pretty.blk (1, Pretty.str "(" :: prt_facts ctxt facts @ [Pretty.str ")"])]); @@ -385,8 +386,8 @@ fun locale_multi_theorem k locale (name, atts) elems concl int thy = global_statement (Proof.multi_theorem k I ProofContext.export_standard (SOME (locale, - (map (Attrib.intern_src (Theory.sign_of thy)) atts, - map (map (Attrib.intern_src (Theory.sign_of thy)) o snd o fst) concl))) + (map (Attrib.intern_src thy) atts, + map (map (Attrib.intern_src thy) o snd o fst) concl))) (name, []) (map (Locale.intern_attrib_elem_expr thy) elems)) (map (apfst (apsnd (K []))) concl) int thy; @@ -554,7 +555,7 @@ (* translation functions *) fun advancedT false = "" - | advancedT true = "Sign.sg -> "; + | advancedT true = "theory -> "; fun advancedN false = "" | advancedN true = "advanced_"; @@ -610,7 +611,7 @@ fun add_oracle (name, txt) = Context.use_let - "val oracle: bstring * (Sign.sg * Object.T -> term)" + "val oracle: bstring * (theory * Object.T -> term)" "Theory.add_oracle oracle" ("(" ^ Library.quote name ^ ", " ^ txt ^ ")"); @@ -635,8 +636,8 @@ in multi_theorem_i Drule.internalK activate ProofContext.export_plain ("", []) [] - (map (fn ((n, ps), props) => - ((NameSpace.base n, [witness (n, map Logic.varify ps)]), + (map (fn ((n, ps), props) => + ((NameSpace.base n, [witness (n, map Logic.varify ps)]), map (fn prop => (prop, ([], []))) props)) propss) int thy' end; @@ -659,16 +660,20 @@ (* theory init and exit *) fun gen_begin_theory upd name parents files = - let val ml_filename = Path.pack (ThyLoad.ml_path name); - val () = if exists (equal ml_filename o #1) files - then error ((quote ml_filename) ^ " not allowed in files section for theory " ^ name) - else () - in ThyInfo.begin_theory Present.begin_theory upd name parents (map (apfst Path.unpack) files) end; + let + val ml_filename = Path.pack (ThyLoad.ml_path name); + (* FIXME unreliable test -- better make ThyInfo manage dependencies properly *) + val _ = conditional (exists (equal ml_filename o #1) files) (fn () => + error ((quote ml_filename) ^ " not allowed in files section for theory " ^ name)); + in + ThyInfo.begin_theory Present.begin_theory upd name parents + (map (apfst Path.unpack) files) + end; val begin_theory = gen_begin_theory false; fun end_theory thy = - if ThyInfo.check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy + if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy; val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; @@ -677,7 +682,8 @@ fun bg_theory (name, parents, files) int = gen_begin_theory int name parents files; fun en_theory thy = (end_theory thy; ()); -fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory (kill_theory o PureThy.get_name); +fun theory spec = + Toplevel.init_theory (bg_theory spec) en_theory (kill_theory o Context.theory_name); (* context switch *) diff -r 18a07ad8fea8 -r 2427be27cc60 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Fri Jun 17 18:33:05 2005 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Fri Jun 17 18:33:08 2005 +0200 @@ -8,7 +8,7 @@ signature PROOF_SYNTAX = sig val proofT : typ - val add_proof_syntax : Sign.sg -> Sign.sg + val add_proof_syntax : theory -> theory val disambiguate_names : theory -> Proofterm.proof -> Proofterm.proof * Proofterm.proof Symtab.table val proof_of_term : theory -> Proofterm.proof Symtab.table -> @@ -17,7 +17,7 @@ val cterm_of_proof : theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) val read_term : theory -> typ -> string -> term val read_proof : theory -> bool -> string -> Proofterm.proof - val pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T + val pretty_proof : theory -> Proofterm.proof -> Pretty.T val pretty_proof_of : bool -> thm -> Pretty.T val print_proof_of : bool -> thm -> unit end; @@ -37,20 +37,20 @@ (** constants for theorems and axioms **) -fun add_proof_atom_consts names sg = - sg - |> Sign.add_path "//" - |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names); +fun add_proof_atom_consts names thy = + thy + |> Theory.absolute_path + |> Theory.add_consts_i (map (fn name => (name, proofT, NoSyn)) names); (** constants for application and abstraction **) -fun add_proof_syntax sg = - sg - |> Sign.copy - |> Sign.add_path "/" - |> Sign.add_defsort_i [] - |> Sign.add_types [("proof", 0, NoSyn)] - |> Sign.add_consts_i +fun add_proof_syntax thy = + thy + |> Theory.copy + |> Theory.root_path + |> Theory.add_defsort_i [] + |> Theory.add_types [("proof", 0, NoSyn)] + |> Theory.add_consts_i [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)), ("Abst", (aT --> proofT) --> proofT, NoSyn), @@ -58,8 +58,8 @@ ("Hyp", propT --> proofT, NoSyn), ("Oracle", propT --> proofT, NoSyn), ("MinProof", proofT, Delimfix "?")] - |> Sign.add_nonterminals ["param", "params"] - |> Sign.add_syntax_i + |> Theory.add_nonterminals ["param", "params"] + |> Theory.add_syntax_i [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), @@ -67,13 +67,13 @@ ("", paramT --> paramT, Delimfix "'(_')"), ("", idtT --> paramsT, Delimfix "_"), ("", paramT --> paramsT, Delimfix "_")] - |> Sign.add_modesyntax_i (("xsymbols", true), + |> Theory.add_modesyntax_i ("xsymbols", true) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\_./ _)", [0, 3], 3)), ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), - ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))]) - |> Sign.add_modesyntax_i (("latex", false), - [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [0, 3], 3))]) - |> Sign.add_trrules_i (map Syntax.ParsePrintRule + ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] + |> Theory.add_modesyntax_i ("latex", false) + [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [0, 3], 3))] + |> Theory.add_trrules_i (map Syntax.ParsePrintRule [(Syntax.mk_appl (Constant "_Lam") [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"], Syntax.mk_appl (Constant "_Lam") @@ -167,7 +167,7 @@ | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t)) | prf_of _ t = error ("Not a proof term:\n" ^ - Sign.string_of_term (sign_of thy) t) + Sign.string_of_term thy t) in prf_of [] end; @@ -217,12 +217,12 @@ val thm_names = filter_out (equal "") (map fst (PureThy.all_thms_of thy) @ map fst (Symtab.dest tab)); val axm_names = map fst (Theory.all_axioms_of thy); - val sg = sign_of thy |> - add_proof_syntax |> - add_proof_atom_consts + val thy' = thy + |> add_proof_syntax + |> add_proof_atom_consts (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names) in - (cterm_of sg (term_of_proof prf'), + (cterm_of thy' (term_of_proof prf'), proof_of_term thy tab true o Thm.term_of) end; @@ -230,12 +230,12 @@ let val thm_names = filter_out (equal "") (map fst (PureThy.all_thms_of thy)); val axm_names = map fst (Theory.all_axioms_of thy); - val sg = sign_of thy |> - add_proof_syntax |> - add_proof_atom_consts + val thy' = thy + |> add_proof_syntax + |> add_proof_atom_consts (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names) in - (fn T => fn s => Thm.term_of (read_cterm sg (s, T))) + fn T => fn s => Thm.term_of (read_cterm thy' (s, T)) end; fun read_proof thy = @@ -244,27 +244,27 @@ (fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s))) end; -fun pretty_proof sg prf = +fun pretty_proof thy prf = let val thm_names = map fst (Symtab.dest (thms_of_proof Symtab.empty prf)) \ ""; val axm_names = map fst (Symtab.dest (axms_of_proof Symtab.empty prf)); - val sg' = sg |> + val thy' = thy |> add_proof_syntax |> add_proof_atom_consts (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names) in - Sign.pretty_term sg' (term_of_proof prf) + Sign.pretty_term thy' (term_of_proof prf) end; fun pretty_proof_of full thm = let - val {sign, der = (_, prf), prop, ...} = rep_thm thm; + val {thy, der = (_, prf), prop, ...} = rep_thm thm; val prf' = (case strip_combt (fst (strip_combP prf)) of (PThm (_, prf', prop', _), _) => if prop=prop' then prf' else prf | _ => prf) in - pretty_proof sign - (if full then Reconstruct.reconstruct_proof sign prop prf' else prf') + pretty_proof thy + (if full then Reconstruct.reconstruct_proof thy prop prf' else prf') end; val print_proof_of = Pretty.writeln oo pretty_proof_of; diff -r 18a07ad8fea8 -r 2427be27cc60 src/Pure/drule.ML --- 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; diff -r 18a07ad8fea8 -r 2427be27cc60 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Fri Jun 17 18:33:05 2005 +0200 +++ b/src/Pure/tactic.ML Fri Jun 17 18:33:08 2005 +0200 @@ -111,15 +111,15 @@ val simplify: bool -> thm list -> thm -> thm val conjunction_tac: tactic val smart_conjunction_tac: int -> tactic - val prove_multi_plain: Sign.sg -> string list -> term list -> term list -> + val prove_multi_plain: theory -> string list -> term list -> term list -> (thm list -> tactic) -> thm list - val prove_multi: Sign.sg -> string list -> term list -> term list -> + val prove_multi: theory -> string list -> term list -> term list -> (thm list -> tactic) -> thm list - val prove_multi_standard: Sign.sg -> string list -> term list -> term list -> + val prove_multi_standard: theory -> string list -> term list -> term list -> (thm list -> tactic) -> thm list - val prove_plain: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm - val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm - val prove_standard: Sign.sg -> string list -> term list -> term -> + val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm + val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm + val prove_standard: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) -> int -> tactic @@ -237,16 +237,16 @@ let val (_, _, Bi, _) = dest_state(st,i) val params = Logic.strip_params Bi in rev(rename_wrt_term Bi params) end; - + (*read instantiations with respect to subgoal i of proof state st*) fun read_insts_in_state (st, i, sinsts, rule) = - let val {sign,...} = rep_thm st - and params = params_of_state st i - and rts = types_sorts rule and (types,sorts) = types_sorts st - fun types'(a,~1) = (case assoc(params,a) of NONE => types(a,~1) | sm => sm) - | types'(ixn) = types ixn; - val used = Drule.add_used rule (Drule.add_used st []); - in read_insts sign rts (types',sorts) used sinsts end; + let val thy = Thm.theory_of_thm st + and params = params_of_state st i + and rts = types_sorts rule and (types,sorts) = types_sorts st + fun types'(a, ~1) = (case assoc_string (params, a) of NONE => types (a, ~1) | sm => sm) + | types' ixn = types ixn; + val used = Drule.add_used rule (Drule.add_used st []); + in read_insts thy rts (types',sorts) used sinsts end; (*Lift and instantiate a rule wrt the given state and subgoal number *) fun lift_inst_rule' (st, i, sinsts, rule) = @@ -285,15 +285,15 @@ i.e. Tinsts is not applied to insts. *) fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = -let val {maxidx,sign,...} = rep_thm st +let val {maxidx,thy,...} = rep_thm st val paramTs = map #2 (params_of_state st i) and inc = maxidx+1 fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T) (*lift only Var, not term, which must be lifted already*) - fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t) + fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t) fun liftTpair (((a, i), S), T) = - (ctyp_of sign (TVar ((a, i + inc), S)), - ctyp_of sign (incr_tvar inc T)) + (ctyp_of thy (TVar ((a, i + inc), S)), + ctyp_of thy (incr_tvar inc T)) in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) (lift_rule (st,i) rule) end; @@ -338,7 +338,7 @@ increment revcut_rl instead.*) fun make_elim_preserve rl = let val {maxidx,...} = rep_thm rl - fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT)); + fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT)); val revcut_rl' = instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl @@ -596,11 +596,11 @@ fun rename_params_tac xs i = case Library.find_first (not o Syntax.is_identifier) xs of SOME x => error ("Not an identifier: " ^ x) - | NONE => + | NONE => (if !Logic.auto_rename - then (warning "Resetting Logic.auto_rename"; - Logic.auto_rename := false) - else (); PRIMITIVE (rename_params_rule (xs, i))); + then (warning "Resetting Logic.auto_rename"; + Logic.auto_rename := false) + else (); PRIMITIVE (rename_params_rule (xs, i))); fun rename_tac str i = let val cs = Symbol.explode str in @@ -652,7 +652,7 @@ (fn st => compose_tac (false, Drule.incr_indexes_wrt [] [] [] [st] Drule.conj_intr_thm, 2) i st) | _ => no_tac); - + val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac); fun smart_conjunction_tac 0 = assume_tac 1 @@ -662,7 +662,7 @@ (** minimal goal interface for programmed proofs *) -fun gen_prove_multi finish_thm sign xs asms props tac = +fun gen_prove_multi finish_thm thy xs asms props tac = let val prop = Logic.mk_conjunction_list props; val statement = Logic.list_implies (asms, prop); @@ -673,9 +673,9 @@ fun err msg = raise ERROR_MESSAGE (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^ - Sign.string_of_term sign (Term.list_all_free (params, statement))); + Sign.string_of_term thy (Term.list_all_free (params, statement))); - fun cert_safe t = Thm.cterm_of sign (Envir.beta_norm t) + fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t) handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; val _ = cert_safe statement; @@ -696,8 +696,8 @@ val raw_result = goal' RS Drule.rev_triv_goal; val prop' = prop_of raw_result; - val _ = conditional (not (Pattern.matches (Sign.tsig_of sign) (prop, prop'))) (fn () => - err ("Proved a different theorem: " ^ Sign.string_of_term sign prop')); + val _ = conditional (not (Pattern.matches (Sign.tsig_of thy) (prop, prop'))) (fn () => + err ("Proved a different theorem: " ^ Sign.string_of_term thy prop')); in Drule.conj_elim_precise (length props) raw_result |> map (fn res => res @@ -706,18 +706,18 @@ |> finish_thm fixed_tfrees) end; -fun prove_multi_plain sign xs asms prop tac = - gen_prove_multi (K norm_hhf_plain) sign xs asms prop tac; -fun prove_multi sign xs asms prop tac = +fun prove_multi_plain thy xs asms prop tac = + gen_prove_multi (K norm_hhf_plain) thy xs asms prop tac; +fun prove_multi thy xs asms prop tac = gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule) - sign xs asms prop tac; -fun prove_multi_standard sign xs asms prop tac = - map Drule.standard (prove_multi sign xs asms prop tac); + thy xs asms prop tac; +fun prove_multi_standard thy xs asms prop tac = + map Drule.standard (prove_multi thy xs asms prop tac); -fun prove_plain sign xs asms prop tac = hd (prove_multi_plain sign xs asms [prop] tac); -fun prove sign xs asms prop tac = hd (prove_multi sign xs asms [prop] tac); -fun prove_standard sign xs asms prop tac = Drule.standard (prove sign xs asms prop tac); +fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac); +fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac); +fun prove_standard thy xs asms prop tac = Drule.standard (prove thy xs asms prop tac); end; diff -r 18a07ad8fea8 -r 2427be27cc60 src/Pure/thm.ML --- 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 (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; diff -r 18a07ad8fea8 -r 2427be27cc60 src/Pure/unify.ML --- a/src/Pure/unify.ML Fri Jun 17 18:33:05 2005 +0200 +++ b/src/Pure/unify.ML Fri Jun 17 18:33:08 2005 +0200 @@ -1,33 +1,31 @@ (* Title: Pure/unify.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright Cambridge University 1992 -Higher-Order Unification +Higher-Order Unification. -Types as well as terms are unified. The outermost functions assume the -terms to be unified already have the same type. In resolution, this is -assured because both have type "prop". +Types as well as terms are unified. The outermost functions assume +the terms to be unified already have the same type. In resolution, +this is assured because both have type "prop". *) - -signature UNIFY = - sig +signature UNIFY = +sig (*references for control and tracing*) val trace_bound: int ref val trace_simp: bool ref val trace_types: bool ref val search_bound: int ref (*other exports*) - val combound : (term*int*int) -> term - val rlist_abs: (string*typ)list * term -> term - val smash_unifiers : Sign.sg * Envir.env * (term*term)list - -> (Envir.env Seq.seq) - val unifiers: Sign.sg * Envir.env * ((term*term)list) - -> (Envir.env * (term * term)list) Seq.seq - end; + val combound: term * int * int -> term + val rlist_abs: (string * typ) list * term -> term + val smash_unifiers: theory * Envir.env * (term * term) list -> Envir.env Seq.seq + val unifiers: theory * Envir.env * ((term * term) list) -> + (Envir.env * (term * term) list) Seq.seq +end -structure Unify : UNIFY = +structure Unify : UNIFY = struct (*Unification options*) @@ -38,7 +36,8 @@ and trace_types = ref false (*announce potential incompleteness of type unification*) -val sgr = ref(Sign.pre_pure); +val thy_ref = ref (NONE: theory option); +fun thy () = the (! thy_ref); type binderlist = (string*typ) list; @@ -180,12 +179,12 @@ fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) = if T=U then env - else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (!sgr)) (iTs, maxidx) (U, T) + else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (thy ())) (iTs, maxidx) (U, T) in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end handle Type.TUNIFY => raise CANTUNIFY; fun test_unify_types(args as (T,U,_)) = -let val sot = Sign.string_of_typ (!sgr); +let val sot = Sign.string_of_typ (thy ()); fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T); val env' = unify_types(args) in if is_TVar(T) orelse is_TVar(U) then warn() else (); @@ -556,7 +555,7 @@ t is always flexible.*) fun print_dpairs msg (env,dpairs) = let fun pdp (rbinder,t,u) = - let fun termT t = Sign.pretty_term (!sgr) + let fun termT t = Sign.pretty_term (thy ()) (Envir.norm_term env (rlist_abs(rbinder,t))) val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, termT t]; @@ -567,7 +566,7 @@ (*Unify the dpairs in the environment. Returns flex-flex disagreement pairs NOT IN normal form. SIMPL may raise exception CANTUNIFY. *) -fun hounifiers (sg,env, tus : (term*term)list) +fun hounifiers (thy,env, tus : (term*term)list) : (Envir.env * (term*term)list)Seq.seq = let fun add_unify tdepth ((env,dpairs), reseq) = Seq.make (fn()=> @@ -591,14 +590,13 @@ (if tdepth > !trace_bound then tracing"Failure node" else (); Seq.pull reseq)); val dps = map (fn(t,u)=> ([],t,u)) tus - in sgr := sg; - add_unify 1 ((env,dps), Seq.empty) - end; + val _ = thy_ref := SOME thy; + in add_unify 1 ((env, dps), Seq.empty) end; -fun unifiers(params) = - Seq.cons((Pattern.unify(params), []), Seq.empty) - handle Pattern.Unif => Seq.empty - | Pattern.Pattern => hounifiers(params); +fun unifiers params = + Seq.cons ((Pattern.unify params, []), Seq.empty) + handle Pattern.Unif => Seq.empty + | Pattern.Pattern => hounifiers params; (*For smash_flexflex1*) @@ -630,7 +628,7 @@ foldr smash_flexflex1 env tpairs; (*Returns unifiers with no remaining disagreement pairs*) -fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq = - Seq.map smash_flexflex (unifiers(sg,env,tus)); +fun smash_unifiers (thy, env, tus) : Envir.env Seq.seq = + Seq.map smash_flexflex (unifiers(thy,env,tus)); end; diff -r 18a07ad8fea8 -r 2427be27cc60 src/ZF/Datatype.ML --- a/src/ZF/Datatype.ML Fri Jun 17 18:33:05 2005 +0200 +++ b/src/ZF/Datatype.ML Fri Jun 17 18:33:08 2005 +0200 @@ -73,9 +73,9 @@ and (rhead, rargs) = strip_comb rhs val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; - val lcon_info = valOf (Symtab.lookup (ConstructorsData.get_sg sg, lname)) + val lcon_info = valOf (Symtab.lookup (ConstructorsData.get sg, lname)) handle Option => raise Match; - val rcon_info = valOf (Symtab.lookup (ConstructorsData.get_sg sg, rname)) + val rcon_info = valOf (Symtab.lookup (ConstructorsData.get sg, rname)) handle Option => raise Match; val new = if #big_rec_name lcon_info = #big_rec_name rcon_info