# HG changeset patch # User wenzelm # Date 1165275038 -3600 # Node ID c07b5b0e8492514701171fa7ea36e6aa119ef931 # Parent 4af699cdfe470eeecb0a81cd911ab40afb0282b9 thm/prf: separate official name vs. additional tags; diff -r 4af699cdfe47 -r c07b5b0e8492 src/HOL/Import/xmlconv.ML --- a/src/HOL/Import/xmlconv.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/HOL/Import/xmlconv.ML Tue Dec 05 00:30:38 2006 +0100 @@ -143,7 +143,7 @@ | xml_of_proof (prf %% prf') = XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf']) | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t]) - | xml_of_proof (PThm ((s, _), _, t, optTs)) = + | xml_of_proof (PThm (s, _, t, optTs)) = XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs) | xml_of_proof (PAxm (s, t, optTs)) = XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs) diff -r 4af699cdfe47 -r c07b5b0e8492 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/HOL/Tools/datatype_package.ML Tue Dec 05 00:30:38 2006 +0100 @@ -301,7 +301,7 @@ (*Name management for ATP linkup. The suffix here must agree with the one given for notE in Clasimp.addIff*) fun name_notE th = - Thm.name_thm (Thm.name_of_thm th ^ "_iff1", th RS notE); + PureThy.put_name_hint (PureThy.get_name_hint th ^ "_iff1") (th RS notE); fun add_rules simps case_thms size_thms rec_thms inject distinct weak_case_congs cong_att = diff -r 4af699cdfe47 -r c07b5b0e8492 src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/HOL/Tools/datatype_realizer.ML Tue Dec 05 00:30:38 2006 +0100 @@ -128,7 +128,7 @@ REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i => REPEAT (etac allE i) THEN atac i)) 1)]); - val ind_name = Thm.name_of_thm induction; + val ind_name = Thm.get_name induction; val vs = map (fn i => List.nth (pnames, i)) is; val (thm', thy') = thy |> Theory.absolute_path @@ -196,7 +196,7 @@ [asm_simp_tac (HOL_basic_ss addsimps case_rewrites), resolve_tac prems, asm_simp_tac HOL_basic_ss])]); - val exh_name = Thm.name_of_thm exhaustion; + val exh_name = Thm.get_name exhaustion; val (thm', thy') = thy |> Theory.absolute_path |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), []) diff -r 4af699cdfe47 -r c07b5b0e8492 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Dec 05 00:30:38 2006 +0100 @@ -59,7 +59,7 @@ val (Const (s, _), ts) = strip_comb S; val params = map dest_Var ts; val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs); - fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr), + fun constr_of_intr intr = (Sign.base_name (Thm.get_name intr), map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @ filter_out (equal Extraction.nullT) (map (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), @@ -189,7 +189,7 @@ in if conclT = Extraction.nullT then list_abs_free (map dest_Free xs, HOLogic.unit) else list_abs_free (map dest_Free xs, list_comb - (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr), + (Free ("r" ^ Sign.base_name (Thm.get_name intr), map fastype_of (rev args) ---> conclT), rev args)) end @@ -226,7 +226,7 @@ let val r = foldr1 HOLogic.mk_prod rlzs; val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct))); - fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr); + fun name_of_fn intr = "r" ^ Sign.base_name (Thm.get_name intr); val r' = list_abs_free (List.mapPartial (fn intr => Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs, if length concls = 1 then r $ x else r) @@ -271,7 +271,7 @@ else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem, mk_prf (tl rs) prems prf)); - in (Thm.name_of_thm rule, (vs, + in (Thm.get_name rule, (vs, if rt = Extraction.nullt then rt else foldr (uncurry lambda) rt vs1, foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP @@ -349,11 +349,11 @@ val (thy3', ind_info) = thy2 |> OldInductivePackage.add_inductive_i false true "" false false false (map Logic.unvarify rlzsets) (map (fn (rintr, intr) => - ((Sign.base_name (Thm.name_of_thm intr), strip_all + ((Sign.base_name (Thm.get_name intr), strip_all (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>> Theory.absolute_path; val thy3 = PureThy.hide_thms false - (map Thm.name_of_thm (#intrs ind_info)) thy3'; + (map Thm.get_name (#intrs ind_info)) thy3'; (** realizer for induction rule **) @@ -379,7 +379,7 @@ [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac, DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); val (thm', thy') = PureThy.store_thm ((space_implode "_" - (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy + (Thm.get_name induct :: vs @ Ps @ ["correctness"]), thm), []) thy in Extraction.add_realizers_i [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy' @@ -427,7 +427,7 @@ REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN' DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); val (thm', thy') = PureThy.store_thm ((space_implode "_" - (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy + (Thm.get_name elim :: vs @ Ps @ ["correctness"]), thm), []) thy in Extraction.add_realizers_i [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy' diff -r 4af699cdfe47 -r c07b5b0e8492 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/HOL/Tools/meson.ML Tue Dec 05 00:30:38 2006 +0100 @@ -390,8 +390,7 @@ (*Use "theorem naming" to label the clauses*) fun name_thms label = let fun name1 (th, (k,ths)) = - (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths) - + (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths) in fn ths => #2 (foldr name1 (length ths, []) ths) end; (*Is the given disjunction an all-negative support clause?*) diff -r 4af699cdfe47 -r c07b5b0e8492 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/HOL/Tools/res_axioms.ML Tue Dec 05 00:30:38 2006 +0100 @@ -518,17 +518,17 @@ cls) ); -fun pairname th = (Thm.name_of_thm th, th); +fun pairname th = (PureThy.get_name_hint th, th); (*Principally for debugging*) fun cnf_name s = let val th = thm s - in cnf_axiom (Thm.name_of_thm th, th) end; + in cnf_axiom (PureThy.get_name_hint th, th) end; (**** Extract and Clausify theorems from a theory's claset and simpset ****) (*Preserve the name of "th" after the transformation "f"*) -fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th); +fun preserve_name f th = PureThy.put_name_hint (PureThy.get_name_hint th) (f th); fun rules_of_claset cs = let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs @@ -601,7 +601,7 @@ (*** meson proof methods ***) fun skolem_use_cache_thm th = - case Symtab.lookup (!clause_cache) (Thm.name_of_thm th) of + case Symtab.lookup (!clause_cache) (PureThy.get_name_hint th) of NONE => skolem_thm th | SOME (th',cls) => if eq_thm(th,th') then cls else skolem_thm th; @@ -631,7 +631,7 @@ | conj_rule ths = foldr1 conj2_rule ths; fun skolem_attr (Context.Theory thy, th) = - let val name = Thm.name_of_thm th + let val name = PureThy.get_name_hint th val (cls, thy') = skolem_cache_thm (name, th) thy in (Context.Theory thy', conj_rule cls) end | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th)); diff -r 4af699cdfe47 -r c07b5b0e8492 src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Tue Dec 05 00:30:38 2006 +0100 @@ -286,9 +286,9 @@ (** Replace congruence rules by substitution rules **) -fun strip_cong ps (PThm (("HOL.cong", _), _, _, _) % _ % _ % SOME x % SOME y %% +fun strip_cong ps (PThm ("HOL.cong", _, _, _) % _ % _ % SOME x % SOME y %% prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1 - | strip_cong ps (PThm (("HOL.refl", _), _, _, _) % SOME f) = SOME (f, ps) + | strip_cong ps (PThm ("HOL.refl", _, _, _) % SOME f) = SOME (f, ps) | strip_cong _ _ = NONE; val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst)))); @@ -310,15 +310,15 @@ fun mk_AbsP P t = AbsP ("H", P, t); -fun elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % _ % _ %% prf1 %% prf2) = +fun elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % _ % _ %% prf1 %% prf2) = Option.map (make_subst Ts prf2 []) (strip_cong [] prf1) - | elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % P % _ %% prf) = + | elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % P % _ %% prf) = Option.map (mk_AbsP P o make_subst Ts (PBound 0) []) (strip_cong [] (incr_pboundvars 1 0 prf)) - | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % _ %% prf1 %% prf2) = + | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % _ %% prf1 %% prf2) = Option.map (make_subst Ts prf2 [] o apsnd (map (make_sym Ts))) (strip_cong [] prf1) - | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % P %% prf) = + | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % P %% prf) = Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf)) | elim_cong _ _ = NONE; diff -r 4af699cdfe47 -r c07b5b0e8492 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Provers/clasimp.ML Tue Dec 05 00:30:38 2006 +0100 @@ -115,8 +115,8 @@ CHANGED o Simplifier.asm_lr_simp_tac ss)); (*Attach a suffix, provided we have a name to start with.*) -fun suffix_thm "" _ th = th - | suffix_thm a b th = Thm.name_thm (a^b, th); +fun suffix_thm "" _ = I + | suffix_thm a b = PureThy.put_name_hint (a^b); (* iffs: addition of rules to simpsets and clasets simultaneously *) @@ -129,7 +129,7 @@ fun addIff decls1 decls2 simp ((cs, ss), th) = let - val name = Thm.name_of_thm th; + val name = PureThy.get_name_hint th; val n = nprems_of th; val (elim, intro) = if n = 0 then decls1 else decls2; val zero_rotate = zero_var_indexes o rotate_prems n; diff -r 4af699cdfe47 -r c07b5b0e8492 src/Provers/classical.ML --- a/src/Provers/classical.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Provers/classical.ML Tue Dec 05 00:30:38 2006 +0100 @@ -195,7 +195,7 @@ else all_tac)) |> Seq.hd |> Drule.zero_var_indexes - |> Thm.put_name_tags (Thm.get_name_tags rule); + |> PureThy.put_name_hint (PureThy.get_name_hint rule); in if Drule.equiv_thm (rule, rule'') then rule else rule'' end else rule; @@ -424,9 +424,9 @@ if has_fewer_prems 1 th then error("Ill-formed destruction rule\n" ^ string_of_thm th) else - case Thm.name_of_thm th of + case PureThy.get_name_hint th of "" => Tactic.make_elim th - | a => Thm.name_thm (a ^ "_dest", Tactic.make_elim th); + | a => PureThy.put_name_hint (a ^ "_dest") (Tactic.make_elim th); fun cs addSDs ths = cs addSEs (map name_make_elim ths); diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/Isar/element.ML Tue Dec 05 00:30:38 2006 +0100 @@ -226,7 +226,7 @@ fun thm_name kind th prts = let val head = - (case #1 (Thm.get_name_tags th) of + (case PureThy.get_name_hint th of "" => Pretty.command kind | a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")]) in Pretty.block (Pretty.fbreaks (head :: prts)) end; diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/Isar/rule_cases.ML Tue Dec 05 00:30:38 2006 +0100 @@ -215,7 +215,7 @@ fun lookup_consumes th = let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [th]) in - (case AList.lookup (op =) (Thm.tags_of_thm th) (consumes_tagN) of + (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of NONE => NONE | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ()) | _ => err ()) @@ -249,7 +249,7 @@ PureThy.untag_rule case_names_tagN #> PureThy.tag_rule (case_names_tagN, names); -fun lookup_case_names th = AList.lookup (op =) (Thm.tags_of_thm th) case_names_tagN; +fun lookup_case_names th = AList.lookup (op =) (Thm.get_tags th) case_names_tagN; val save_case_names = add_case_names o lookup_case_names; val name = add_case_names o SOME; @@ -264,16 +264,16 @@ fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name) | is_case_concl _ _ = false; -fun add_case_concl (name, cs) = PureThy.map_tags (fn tags => +fun add_case_concl (name, cs) = Thm.map_tags (fn tags => filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]); fun get_case_concls th name = - (case find_first (is_case_concl name) (Thm.tags_of_thm th) of + (case find_first (is_case_concl name) (Thm.get_tags th) of SOME (_, _ :: cs) => cs | _ => []); fun save_case_concls th = - let val concls = Thm.tags_of_thm th |> map_filter + let val concls = Thm.get_tags th |> map_filter (fn (a, b :: cs) => if a = case_concl_tagN then SOME (b, cs) else NONE | _ => NONE) diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/Proof/extraction.ML Tue Dec 05 00:30:38 2006 +0100 @@ -314,7 +314,7 @@ val rd = ProofSyntax.read_proof thy' false in fn (thm, (vs, s1, s2)) => let - val name = Thm.name_of_thm thm; + val name = Thm.get_name thm; val _ = assert (name <> "") "add_realizers: unnamed theorem"; val prop = Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm); @@ -359,7 +359,7 @@ val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} = ExtractionData.get thy; - val name = Thm.name_of_thm thm; + val name = Thm.get_name thm; val _ = assert (name <> "") "add_expand_thms: unnamed theorem"; val is_def = @@ -555,7 +555,7 @@ (defs3, corr_prf1 % u %% corr_prf2) end - | corr d defs vs ts Ts hs (prf0 as PThm ((name, _), prf, prop, SOME Ts')) _ _ = + | corr d defs vs ts Ts hs (prf0 as PThm (name, prf, prop, SOME Ts')) _ _ = let val (vs', tye) = find_inst prop Ts ts vs; val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye; @@ -578,7 +578,7 @@ val corr_prop = Reconstruct.prop_of corr_prf; val corr_prf' = foldr forall_intr_prf (proof_combt - (PThm ((corr_name name vs', []), corr_prf, corr_prop, + (PThm (corr_name name vs', corr_prf, corr_prop, SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop)) (map (get_var_type corr_prop) (vfs_of prop)) in @@ -643,7 +643,7 @@ in (defs'', f $ t) end end - | extr d defs vs ts Ts hs (prf0 as PThm ((s, _), prf, prop, SOME Ts')) = + | extr d defs vs ts Ts hs (prf0 as PThm (s, prf, prop, SOME Ts')) = let val (vs', tye) = find_inst prop Ts ts vs; val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye @@ -687,7 +687,7 @@ val corr_prop = Reconstruct.prop_of corr_prf'; val corr_prf'' = foldr forall_intr_prf (proof_combt - (PThm ((corr_name s vs', []), corr_prf', corr_prop, + (PThm (corr_name s vs', corr_prf', corr_prop, SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop)) (map (get_var_type corr_prop) (vfs_of prop)); in @@ -719,7 +719,7 @@ fun prep_thm (thm, vs) = let val {prop, der = (_, prf), sign, ...} = rep_thm thm; - val name = Thm.name_of_thm thm; + val name = Thm.get_name thm; val _ = assert (name <> "") "extraction: unnamed theorem"; val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^ quote name ^ " has no computational content") diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Dec 05 00:30:38 2006 +0100 @@ -32,12 +32,12 @@ val equal_elim_axm = ax equal_elim_axm []; val symmetric_axm = ax symmetric_axm [propT]; - fun rew' (PThm (("ProtoPure.protectD", _), _, _, _) % _ %% - (PThm (("ProtoPure.protectI", _), _, _, _) % _ %% prf)) = SOME prf - | rew' (PThm (("ProtoPure.conjunctionD1", _), _, _, _) % _ % _ %% - (PThm (("ProtoPure.conjunctionI", _), _, _, _) % _ % _ %% prf %% _)) = SOME prf - | rew' (PThm (("ProtoPure.conjunctionD2", _), _, _, _) % _ % _ %% - (PThm (("ProtoPure.conjunctionI", _), _, _, _) % _ % _ %% _ %% prf)) = SOME prf + fun rew' (PThm ("ProtoPure.protectD", _, _, _) % _ %% + (PThm ("ProtoPure.protectI", _, _, _) % _ %% prf)) = SOME prf + | rew' (PThm ("ProtoPure.conjunctionD1", _, _, _) % _ % _ %% + (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% prf %% _)) = SOME prf + | rew' (PThm ("ProtoPure.conjunctionD2", _, _, _) % _ % _ %% + (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% _ %% prf)) = SOME prf | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% @@ -47,14 +47,14 @@ | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %% (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) % _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% - ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% prf2)) = + ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) = SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2)) | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %% (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) % _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %% - ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% prf2)) = + ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) = SOME (tg %> B %% (equal_elim_axm %> A %> B %% (symmetric_axm % ?? B % ?? A %% prf1) %% prf2)) @@ -222,7 +222,7 @@ | insert_refl defs Ts (AbsP (s, t, prf)) = AbsP (s, t, insert_refl defs Ts prf) | insert_refl defs Ts prf = (case strip_combt prf of - (PThm ((s, _), _, prop, SOME Ts), ts) => + (PThm (s, _, prop, SOME Ts), ts) => if member (op =) defs s then let val vs = vars_of prop; @@ -241,7 +241,7 @@ fun elim_defs thy r defs prf = let val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs - val defnames = map Thm.name_of_thm defs; + val defnames = map Thm.get_name defs; val f = if not r then I else let val cnames = map (fst o dest_Const o fst) defs'; diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Tue Dec 05 00:30:38 2006 +0100 @@ -108,12 +108,12 @@ | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf) | rename (prf1 %% prf2) = rename prf1 %% rename prf2 | rename (prf % t) = rename prf % t - | rename (prf' as PThm ((s, tags), prf, prop, Ts)) = + | rename (prf' as PThm (s, prf, prop, Ts)) = let val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s); val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s))) in if prop = prop' then prf' else - PThm ((s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps), tags), + PThm (s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps), prf, prop, Ts) end | rename prf = prf @@ -183,9 +183,9 @@ val mk_tyapp = fold (fn T => fn prf => Const ("Appt", [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); -fun term_of _ (PThm ((name, _), _, _, NONE)) = +fun term_of _ (PThm (name, _, _, NONE)) = Const (NameSpace.append "thm" name, proofT) - | term_of _ (PThm ((name, _), _, _, SOME Ts)) = + | term_of _ (PThm (name, _, _, SOME Ts)) = mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT)) | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT) | term_of _ (PAxm (name, _, SOME Ts)) = diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/Proof/proofchecker.ML Tue Dec 05 00:30:38 2006 +0100 @@ -45,7 +45,7 @@ Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) end; - fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) = + fun thm_of _ _ (PThm (name, _, prop', SOME Ts)) = let val thm = Drule.implies_intr_hyps (lookup name); val {prop, ...} = rep_thm thm; diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/Proof/reconstruct.ML Tue Dec 05 00:30:38 2006 +0100 @@ -151,7 +151,7 @@ val prop'' = subst_TVars (map fst tvars @ map snd fmap ~~ Ts) (forall_intr_vfs prop') handle Library.UnequalLengths => error ("Wrong number of type arguments for " ^ - quote (fst (get_name_tags [] prop prf))) + quote (get_name [] prop prf)) in (prop'', change_type (SOME Ts) prf, [], env', vTs) end; fun head_norm (prop, prf, cnstrts, env, vTs) = @@ -352,7 +352,7 @@ | expand maxidx prfs (prf % t) = let val (maxidx', prfs', prf') = expand maxidx prfs prf in (maxidx', prfs', prf' % t) end - | expand maxidx prfs (prf as PThm ((a, _), cprf, prop, SOME Ts)) = + | expand maxidx prfs (prf as PThm (a, cprf, prop, SOME Ts)) = if not (exists (fn (b, NONE) => a = b | (b, SOME prop') => a = b andalso prop = prop') thms) diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Dec 05 00:30:38 2006 +0100 @@ -338,7 +338,7 @@ (* FIXME: check this uses non-transitive closure function here *) fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () => let - val names = filter_out (equal "") (map Thm.name_of_thm ths); + val names = filter_out (equal "") (map PureThy.get_name_hint ths); val deps = filter_out (equal "") (Symtab.keys (fold Proofterm.thms_of_proof (map Thm.proof_of ths) Symtab.empty)); diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/Thy/thm_deps.ML Tue Dec 05 00:30:38 2006 +0100 @@ -25,9 +25,9 @@ fun enable () = if ! proofs = 0 then proofs := 1 else (); fun disable () = proofs := 0; -fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf) - | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], [])) - | dest_thm_axm _ = (("", []), MinProof ([], [], [])); +fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf) + | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], [])) + | dest_thm_axm _ = ("", MinProof ([], [], [])); fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf @@ -37,9 +37,9 @@ fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #> fold (make_deps_graph o Proofterm.proof_of_min_axm) axms | make_deps_graph prf = (fn p as (gra, parents) => - let val ((name, tags), prf') = dest_thm_axm prf + let val (name, prf') = dest_thm_axm prf in - if name <> "" andalso not (PureThy.has_internal tags) then + if name <> "" then if not (Symtab.defined gra name) then let val (gra', parents') = make_deps_graph prf' (gra, []); diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/display.ML --- a/src/Pure/display.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/display.ML Tue Dec 05 00:30:38 2006 +0100 @@ -77,7 +77,7 @@ val th = Thm.strip_shyps raw_th; val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th; val xshyps = Thm.extra_shyps th; - val (_, tags) = Thm.get_name_tags th; + val tags = Thm.get_tags th; val q = if quote then Pretty.quote else I; val prt_term = q o (Pretty.term pp); diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/drule.ML --- a/src/Pure/drule.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/drule.ML Tue Dec 05 00:30:38 2006 +0100 @@ -427,7 +427,7 @@ | _ => raise THM("flexflex_unique: multiple unifiers", 0, [th]); fun close_derivation thm = - if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm) + if Thm.get_name thm = "" then Thm.put_name "" thm else thm; diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/meta_simplifier.ML Tue Dec 05 00:30:38 2006 +0100 @@ -514,7 +514,7 @@ end; fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) = - maps (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms; + maps (fn thm => map (rpair (PureThy.get_name_hint thm)) (mk thm)) thms; fun extract_safe_rrules (ss, thm) = maps (orient_rrule ss) (extract_rews (ss, [thm])); diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/proof_general.ML Tue Dec 05 00:30:38 2006 +0100 @@ -481,7 +481,7 @@ (* FIXME: check this uses non-transitive closure function here *) fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () => let - val names = filter_out (equal "") (map Thm.name_of_thm ths); + val names = filter_out (equal "") (map PureThy.get_name_hint ths); val deps = filter_out (equal "") (Symtab.keys (fold Proofterm.thms_of_proof (map Thm.proof_of ths) Symtab.empty)); diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/proofterm.ML Tue Dec 05 00:30:38 2006 +0100 @@ -18,7 +18,7 @@ | % of proof * term option | %% of proof * proof | Hyp of term - | PThm of (string * (string * string list) list) * proof * term * typ list option + | PThm of string * proof * term * typ list option | PAxm of string * term * typ list option | Oracle of string * term * typ list option | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list; @@ -99,9 +99,8 @@ val equal_elim : term -> term -> proof -> proof -> proof val axm_proof : string -> term -> proof val oracle_proof : string -> term -> proof - val thm_proof : theory -> string * (string * string list) list -> - term list -> term -> proof -> proof - val get_name_tags : term list -> term -> proof -> string * (string * string list) list + val thm_proof : theory -> string -> term list -> term -> proof -> proof + val get_name : term list -> term -> proof -> string (** rewriting on proof terms **) val add_prf_rrules : (proof * proof) list -> theory -> theory @@ -112,7 +111,7 @@ val rewrite_proof_notypes : (proof * proof) list * (string * (typ list -> proof -> proof option)) list -> proof -> proof val init_data: theory -> theory - + end structure Proofterm : PROOFTERM = @@ -127,13 +126,13 @@ | op % of proof * term option | op %% of proof * proof | Hyp of term - | PThm of (string * (string * string list) list) * proof * term * typ list option + | PThm of string * proof * term * typ list option | PAxm of string * term * typ list option | Oracle of string * term * typ list option | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list; fun proof_of_min_axm (s, prop) = PAxm (s, prop, NONE); -fun proof_of_min_thm ((s, prop), prf) = PThm ((s, []), prf, prop, NONE); +fun proof_of_min_thm ((s, prop), prf) = PThm (s, prf, prop, NONE); val string_term_ord = prod_ord fast_string_ord Term.fast_term_ord; @@ -143,7 +142,7 @@ | oras_of (AbsP (_, _, prf)) = oras_of prf | oras_of (prf % _) = oras_of prf | oras_of (prf1 %% prf2) = oras_of prf1 #> oras_of prf2 - | oras_of (PThm ((name, _), prf, prop, _)) = (fn tabs as (thms, oras) => + | oras_of (PThm (name, prf, prop, _)) = (fn tabs as (thms, oras) => case Symtab.lookup thms name of NONE => oras_of prf (Symtab.update (name, [prop]) thms, oras) | SOME ps => if member (op =) ps prop then tabs else @@ -162,7 +161,7 @@ | thms_of_proof (AbsP (_, _, prf)) = thms_of_proof prf | thms_of_proof (prf1 %% prf2) = thms_of_proof prf1 #> thms_of_proof prf2 | thms_of_proof (prf % _) = thms_of_proof prf - | thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab => + | thms_of_proof (prf' as PThm (s, prf, prop, _)) = (fn tab => case Symtab.lookup tab s of NONE => thms_of_proof prf (Symtab.update (s, [(prop, prf')]) tab) | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else @@ -175,8 +174,8 @@ | thms_of_proof' (AbsP (_, _, prf)) = thms_of_proof' prf | thms_of_proof' (prf1 %% prf2) = thms_of_proof' prf1 #> thms_of_proof' prf2 | thms_of_proof' (prf % _) = thms_of_proof' prf - | thms_of_proof' (PThm (("", _), prf, prop, _)) = thms_of_proof' prf - | thms_of_proof' (prf' as PThm ((s, _), _, prop, _)) = (fn tab => + | thms_of_proof' (PThm ("", prf, prop, _)) = thms_of_proof' prf + | thms_of_proof' (prf' as PThm (s, _, prop, _)) = (fn tab => case Symtab.lookup tab s of NONE => Symtab.update (s, [(prop, prf')]) tab | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else @@ -200,7 +199,7 @@ | mk_min_proof (AbsP (_, _, prf)) = mk_min_proof prf | mk_min_proof (prf % _) = mk_min_proof prf | mk_min_proof (prf1 %% prf2) = mk_min_proof prf1 #> mk_min_proof prf2 - | mk_min_proof (PThm ((s, _), prf, prop, _)) = + | mk_min_proof (PThm (s, prf, prop, _)) = map3 (OrdList.insert (string_term_ord o pairself fst) ((s, prop), prf)) I I | mk_min_proof (PAxm (s, prop, _)) = map3 I (OrdList.insert string_term_ord (s, prop)) I @@ -239,12 +238,12 @@ val proof_combt' = Library.foldl (op %); val proof_combP = Library.foldl (op %%); -fun strip_combt prf = +fun strip_combt prf = let fun stripc (prf % t, ts) = stripc (prf, t::ts) - | stripc x = x + | stripc x = x in stripc (prf, []) end; -fun strip_combP prf = +fun strip_combP prf = let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs) | stripc x = x in stripc (prf, []) end; @@ -330,7 +329,7 @@ fun mk_abs Ts t = Library.foldl (fn (t', T) => Abs ("", T, t')) (t, Ts); -(*Abstraction of a proof term over its occurrences of v, +(*Abstraction of a proof term over its occurrences of v, which must contain no loose bound variables. The resulting proof term is ready to become the body of an Abst.*) @@ -365,17 +364,17 @@ fun incr_bv' inct tlev t = incr_bv (inct, tlev, t); fun prf_incr_bv' incP inct Plev tlev (PBound i) = - if i >= Plev then PBound (i+incP) else raise SAME + if i >= Plev then PBound (i+incP) else raise SAME | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) = (AbsP (a, apsome' (same (incr_bv' inct tlev)) t, prf_incr_bv incP inct (Plev+1) tlev body) handle SAME => AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body)) | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) = Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body) - | prf_incr_bv' incP inct Plev tlev (prf %% prf') = + | prf_incr_bv' incP inct Plev tlev (prf %% prf') = (prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf' handle SAME => prf %% prf_incr_bv' incP inct Plev tlev prf') - | prf_incr_bv' incP inct Plev tlev (prf % t) = + | prf_incr_bv' incP inct Plev tlev (prf % t) = (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t handle SAME => prf % apsome' (same (incr_bv' inct tlev)) t) | prf_incr_bv' _ _ _ _ _ = raise SAME @@ -539,7 +538,7 @@ | thaw names names' (Abs (s, T, t)) = Abs (s, thawT names' T, thaw names names' t) | thaw names names' (Const (s, T)) = Const (s, thawT names' T) - | thaw names names' (Free (s, T)) = + | thaw names names' (Free (s, T)) = let val T' = thawT names' T in case AList.lookup (op =) names s of NONE => Free (s, T') @@ -703,12 +702,12 @@ val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop); val k = length ps; - fun mk_app (b, (i, j, prf)) = + fun mk_app (b, (i, j, prf)) = if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j); fun lift Us bs i j (Const ("==>", _) $ A $ B) = AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B) - | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = + | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t) | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf, map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs))) @@ -888,7 +887,7 @@ | t' => is_p 0 t') end; -fun needed_vars prop = +fun needed_vars prop = Library.foldl (op union) ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union prop_vars prop; @@ -915,7 +914,7 @@ let val compress_typ = Compress.typ thy; val compress_term = Compress.term thy; - + fun shrink ls lev (prf as Abst (a, T, body)) = let val (b, is, ch, body') = shrink ls (lev+1) body in (b, is, ch, if ch then Abst (a, Option.map compress_typ T, body') else prf) end @@ -1029,8 +1028,7 @@ mtch Ts (i+1) j (optmatch (matcht Ts j) inst (opt, opu)) (prf1, prf2) | mtch Ts i j inst (prf1, AbsP (_, _, prf2)) = mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2) - | mtch Ts i j inst (PThm ((name1, _), _, prop1, opTs), - PThm ((name2, _), _, prop2, opUs)) = + | mtch Ts i j inst (PThm (name1, _, prop1, opTs), PThm (name2, _, prop2, opUs)) = if name1=name2 andalso prop1=prop2 then optmatch matchTs inst (opTs, opUs) else raise PMatch @@ -1070,7 +1068,7 @@ | subst _ _ t = t in subst 0 0 end; -(*A fast unification filter: true unless the two terms cannot be unified. +(*A fast unification filter: true unless the two terms cannot be unified. Terms must be NORMAL. Treats all Vars as distinct. *) fun could_unify prf1 prf2 = let @@ -1088,7 +1086,7 @@ in case (head_of prf1, head_of prf2) of (_, Hyp (Var _)) => true | (Hyp (Var _), _) => true - | (PThm ((a, _), _, propa, _), PThm ((b, _), _, propb, _)) => + | (PThm (a, _, propa, _), PThm (b, _, propb, _)) => a = b andalso propa = propb andalso matchrands prf1 prf2 | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2 | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2 @@ -1203,7 +1201,7 @@ let val r = ProofData.get thy in ProofData.put (fst r, ps @ snd r) thy end; -fun thm_proof thy (name, tags) hyps prop prf = +fun thm_proof thy name hyps prop prf = let val prop = Logic.list_implies (hyps, prop); val nvs = needed_vars prop; @@ -1215,25 +1213,23 @@ (foldr (uncurry implies_intr_proof) prf hyps))) else MinProof (mk_min_proof prf ([], [], [])); val head = (case strip_combt (fst (strip_combP prf)) of - (PThm ((old_name, _), prf', prop', NONE), args') => + (PThm (old_name, prf', prop', NONE), args') => if (old_name="" orelse old_name=name) andalso prop = prop' andalso args = args' then - PThm ((name, tags), prf', prop, NONE) + PThm (name, prf', prop, NONE) else - PThm ((name, tags), opt_prf, prop, NONE) - | _ => PThm ((name, tags), opt_prf, prop, NONE)) + PThm (name, opt_prf, prop, NONE) + | _ => PThm (name, opt_prf, prop, NONE)) in proof_combP (proof_combt' (head, args), map Hyp hyps) end; -fun get_name_tags hyps prop prf = +fun get_name hyps prop prf = let val prop = Logic.list_implies (hyps, prop) in (case strip_combt (fst (strip_combP prf)) of - (PThm ((name, tags), _, prop', _), _) => - if prop=prop' then (name, tags) else ("", []) - | (PAxm (name, prop', _), _) => - if prop=prop' then (name, []) else ("", []) - | _ => ("", [])) + (PThm (name, _, prop', _), _) => if prop=prop' then name else "" + | (PAxm (name, prop', _), _) => if prop=prop' then name else "" + | _ => "") end; end; diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/pure_thy.ML Tue Dec 05 00:30:38 2006 +0100 @@ -29,11 +29,12 @@ signature PURE_THY = sig include BASIC_PURE_THY - val map_tags: (tag list -> tag list) -> thm -> thm val tag_rule: tag -> thm -> thm val untag_rule: string -> thm -> thm val tag: tag -> attribute val untag: string -> attribute + val get_name_hint: thm -> string + val put_name_hint: string -> thm -> thm val get_kind: thm -> string val kind_rule: string -> thm -> thm val kind: string -> attribute @@ -62,7 +63,9 @@ val burrow_facts: ('a list -> 'b list) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list val name_multi: string -> 'a list -> (string * 'a) list - val name_thm: bool -> string * thm -> thm + val name_thm: bool -> bool -> string -> thm -> thm + val name_thms: bool -> bool -> string -> thm list -> thm list + val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory val smart_store_thms: (bstring * thm list) -> thm list val smart_store_thms_open: (bstring * thm list) -> thm list @@ -106,12 +109,8 @@ (* add / delete tags *) -fun map_tags f thm = - let val (name, tags) = Thm.get_name_tags thm - in Thm.put_name_tags (name, f tags) thm end; - -fun tag_rule tg = map_tags (fn tgs => if member (op =) tgs tg then tgs else tgs @ [tg]); -fun untag_rule s = map_tags (filter_out (fn (s', _) => s = s')); +fun tag_rule tg = Thm.map_tags (insert (op =) tg); +fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x; fun untag s x = Thm.rule_attribute (K (untag_rule s)) x; @@ -119,18 +118,28 @@ fun simple_tag name x = tag (name, []) x; +(* unofficial theorem names *) + +fun put_name_hint name = untag_rule "name" #> tag_rule ("name", [name]); + +fun get_name_hint thm = + (case AList.lookup (op =) (Thm.get_tags thm) "name" of + SOME (k :: _) => k + | _ => "??.unknown"); + + (* theorem kinds *) fun get_kind thm = - (case AList.lookup (op =) ((#2 o Thm.get_name_tags) thm) "kind" of + (case AList.lookup (op =) (Thm.get_tags thm) "kind" of SOME (k :: _) => k - | _ => "unknown"); + | _ => "??.unknown"); fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind"; fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x; fun kind_internal x = kind internalK x; fun has_internal tags = exists (fn ("kind", [k]) => k = internalK | _ => false) tags; -val is_internal = has_internal o Thm.tags_of_thm; +val is_internal = has_internal o Thm.get_tags; @@ -288,14 +297,14 @@ fun thms_containing_consts thy consts = thms_containing thy (consts, []) |> maps #2 - |> map (fn th => (Thm.name_of_thm th, th)); + |> map (`(get_name_hint)); (* thms_of etc. *) fun thms_of thy = let val thms = #2 (theorems_of thy) - in map (fn th => (Thm.name_of_thm th, th)) (maps snd (Symtab.dest thms)) end; + in map (`(get_name_hint)) (maps snd (Symtab.dest thms)) end; fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy); @@ -327,12 +336,15 @@ fun name_multi name [x] = [(name, x)] | name_multi name xs = gen_names 0 (length xs) name ~~ xs; -fun name_thm pre (name, thm) = - if Thm.name_of_thm thm <> "" andalso pre then thm else Thm.name_thm (name, thm); +fun name_thm pre official name thm = thm + |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) + |> (if get_name_hint thm <> "" andalso pre orelse name = "" then I else put_name_hint name); -fun name_thms pre name xs = map (name_thm pre) (name_multi name xs); +fun name_thms pre official name xs = + map (uncurry (name_thm pre official)) (name_multi name xs); -fun name_thmss name fact = burrow_fact (name_thms true name) fact; +fun name_thmss official name fact = + burrow_fact (name_thms true official name) fact; (* enter_thms *) @@ -363,7 +375,8 @@ (* add_thms(s) *) fun add_thms_atts pre_name ((bname, thms), atts) = - enter_thms pre_name (name_thms false) (foldl_map (Thm.theory_attributes atts)) (bname, thms); + enter_thms pre_name (name_thms false true) + (foldl_map (Thm.theory_attributes atts)) (bname, thms); fun gen_add_thmss pre_name = fold_map (add_thms_atts pre_name); @@ -371,8 +384,8 @@ fun gen_add_thms pre_name args = apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); -val add_thmss = gen_add_thmss (name_thms true); -val add_thms = gen_add_thms (name_thms true); +val add_thmss = gen_add_thmss (name_thms true true); +val add_thms = gen_add_thms (name_thms true true); (* note_thmss(_i) *) @@ -383,7 +396,7 @@ let fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths); val (thms, thy') = thy |> enter_thms - name_thmss (name_thms false) (apsnd flat o foldl_map app) + (name_thmss true) (name_thms false true) (apsnd flat o foldl_map app) (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind k])) ths_atts); in ((bname, thms), thy') end); @@ -405,7 +418,7 @@ (* store_thm *) fun store_thm ((bname, thm), atts) thy = - let val ([th'], thy') = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy + let val ([th'], thy') = add_thms_atts (name_thms true true) ((bname, [thm]), atts) thy in (th', thy') end; @@ -415,16 +428,18 @@ fun smart_store _ (name, []) = error ("Cannot store empty list of theorems: " ^ quote name) - | smart_store name_thm (name, [thm]) = - fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm)) - | smart_store name_thm (name, thms) = - let val thy = Theory.merge_list (map Thm.theory_of_thm thms) - in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end; + | smart_store official (name, [thm]) = + fst (enter_thms (name_thms true official) (name_thms false official) I (name, [thm]) + (Thm.theory_of_thm thm)) + | smart_store official (name, thms) = + let val thy = Theory.merge_list (map Thm.theory_of_thm thms) in + fst (enter_thms (name_thms true official) (name_thms false official) I (name, thms) thy) + end; in -val smart_store_thms = smart_store name_thms; -val smart_store_thms_open = smart_store (K (K I)); +val smart_store_thms = smart_store true; +val smart_store_thms_open = smart_store false; end; diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/thm.ML Tue Dec 05 00:30:38 2006 +0100 @@ -55,6 +55,7 @@ {thy: theory, sign: theory, (*obsolete*) der: bool * Proofterm.proof, + tags: tag list, maxidx: int, shyps: sort list, hyps: term list, @@ -64,6 +65,7 @@ {thy: theory, sign: theory, (*obsolete*) der: bool * Proofterm.proof, + tags: tag list, maxidx: int, shyps: sort list, hyps: cterm list, @@ -161,11 +163,10 @@ val maxidx_thm: thm -> int -> int val hyps_of: thm -> term list val full_prop_of: thm -> term - 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 get_name: thm -> string + val put_name: string -> thm -> thm + val get_tags: thm -> tag list + val map_tags: (tag list -> tag list) -> thm -> thm val compress: thm -> thm val adjust_maxidx_thm: int -> thm -> thm val rename_boundvars: term -> term -> thm -> thm @@ -376,17 +377,17 @@ 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*) -type tag = string * string list; - (*** Meta theorems ***) structure Pt = Proofterm; +type tag = string * string list; + datatype thm = Thm of {thy_ref: theory_ref, (*dynamic reference to theory*) der: bool * Pt.proof, (*derivation*) + tags: tag list, (*additional annotations/comments*) maxidx: int, (*maximum index of any Var or TVar*) shyps: sort list, (*sort hypotheses as ordered list*) hyps: term list, (*hypotheses as ordered list*) @@ -396,19 +397,19 @@ (*errors involving theorems*) exception THM of string * int * thm list; -fun rep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = +fun rep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = let val thy = Theory.deref thy_ref in - {thy = thy, sign = thy, der = der, maxidx = maxidx, + {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} end; (*version of rep_thm returning cterms instead of terms*) -fun crep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = +fun crep_thm (Thm {thy_ref, der, tags, 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, sorts = shyps}; in - {thy = thy, sign = thy, der = der, maxidx = maxidx, shyps = shyps, + {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps, hyps = map (cterm ~1) hyps, tpairs = map (pairself (cterm maxidx)) tpairs, prop = cterm maxidx prop} @@ -519,7 +520,7 @@ (*explicit transfer to a super theory*) fun transfer thy' thm = let - val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm; + val Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop} = thm; val thy = Theory.deref thy_ref; in if not (subthy (thy, thy')) then @@ -528,6 +529,7 @@ else Thm {thy_ref = Theory.self_ref thy', der = der, + tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, @@ -539,7 +541,7 @@ fun weaken raw_ct th = let val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct; - val Thm {der, maxidx, shyps, hyps, tpairs, prop, ...} = th; + val Thm {der, tags, maxidx, shyps, hyps, tpairs, prop, ...} = th; in if T <> propT then raise THM ("weaken: assumptions must have type prop", 0, []) @@ -548,6 +550,7 @@ else Thm {thy_ref = merge_thys1 ct th, der = der, + tags = tags, maxidx = maxidx, shyps = Sorts.union sorts shyps, hyps = insert_hyps A hyps, @@ -565,7 +568,7 @@ (*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 {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = + | strip_shyps (thm as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = let val thy = Theory.deref thy_ref; val shyps' = @@ -577,7 +580,7 @@ val witnessed = map #2 (Sign.witness_sorts thy present extra); in Sorts.subtract witnessed shyps end; in - Thm {thy_ref = thy_ref, der = der, maxidx = maxidx, + Thm {thy_ref = thy_ref, der = der, tags = tags, maxidx = maxidx, shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop} end; @@ -596,6 +599,7 @@ |> Option.map (fn prop => Thm {thy_ref = Theory.self_ref thy, der = Pt.infer_derivs' I (false, Pt.axm_proof name prop), + tags = [], maxidx = maxidx_of_term prop, shyps = may_insert_term_sorts thy prop [], hyps = [], @@ -624,30 +628,31 @@ (Symtab.dest (#2 (#axioms (Theory.rep_theory thy)))); -(* name and tags -- make proof objects more readable *) +(* official name and additional tags *) -fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) = - Pt.get_name_tags hyps prop prf; +fun get_name (Thm {hyps, prop, der = (_, prf), ...}) = + Pt.get_name 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]); +fun put_name name (Thm {thy_ref, der = (ora, prf), tags, maxidx, shyps, hyps, tpairs = [], prop}) = + Thm {thy_ref = thy_ref, + der = (ora, Pt.thm_proof (Theory.deref thy_ref) name hyps prop prf), + tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop} + | put_name _ thm = raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]); -val name_of_thm = #1 o get_name_tags; -val tags_of_thm = #2 o get_name_tags; +val get_tags = #tags o rep_thm; -fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm; +fun map_tags f (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = + Thm {thy_ref = thy_ref, der = der, tags = f tags, maxidx = maxidx, + shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; (*Compression of theorems -- a separate rule, not integrated with the others, as it could be slow.*) -fun compress (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = +fun compress (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = let val thy = Theory.deref thy_ref in Thm {thy_ref = thy_ref, der = der, + tags = tags, maxidx = maxidx, shyps = shyps, hyps = map (Compress.term thy) hyps, @@ -655,14 +660,14 @@ prop = Compress.term thy prop} end; -fun adjust_maxidx_thm i (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = +fun adjust_maxidx_thm i (th as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = if maxidx = i then th else if maxidx < i then - Thm {maxidx = i, thy_ref = thy_ref, der = der, shyps = shyps, + Thm {maxidx = i, thy_ref = thy_ref, der = der, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} else - Thm {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), - thy_ref = thy_ref, der = der, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; + Thm {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy_ref = thy_ref, + der = der, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; @@ -679,6 +684,7 @@ raise THM ("assume: variables", maxidx, []) else Thm {thy_ref = thy_ref, der = Pt.infer_derivs' I (false, Pt.Hyp prop), + tags = [], maxidx = ~1, shyps = sorts, hyps = [prop], @@ -701,6 +707,7 @@ else Thm {thy_ref = merge_thys1 ct th, der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, + tags = [], maxidx = Int.max (maxidxA, maxidx), shyps = Sorts.union sorts shyps, hyps = remove_hyps A hyps, @@ -725,6 +732,7 @@ if A aconv propA then Thm {thy_ref = merge_thys2 thAB thA, der = Pt.infer_derivs (curry Pt.%%) der derA, + tags = [], maxidx = Int.max (maxA, maxidx), shyps = Sorts.union shypsA shyps, hyps = union_hyps hypsA hyps, @@ -748,6 +756,7 @@ fun result a = Thm {thy_ref = merge_thys1 ct th, der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, + tags = [], maxidx = maxidx, shyps = Sorts.union sorts shyps, hyps = hyps, @@ -779,6 +788,7 @@ else Thm {thy_ref = merge_thys1 ct th, der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, + tags = [], maxidx = Int.max (maxidx, maxt), shyps = Sorts.union sorts shyps, hyps = hyps, @@ -795,6 +805,7 @@ fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = Thm {thy_ref = thy_ref, der = Pt.infer_derivs' I (false, Pt.reflexive), + tags = [], maxidx = maxidx, shyps = sorts, hyps = [], @@ -806,11 +817,12 @@ ------ u == t *) -fun symmetric (th as Thm {thy_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 => Thm {thy_ref = thy_ref, der = Pt.infer_derivs' Pt.symmetric der, + tags = [], maxidx = maxidx, shyps = shyps, hyps = hyps, @@ -837,6 +849,7 @@ else Thm {thy_ref = merge_thys2 th1 th2, der = Pt.infer_derivs (Pt.transitive u T) der1 der2, + tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, @@ -858,6 +871,7 @@ in Thm {thy_ref = thy_ref, der = Pt.infer_derivs' I (false, Pt.reflexive), + tags = [], maxidx = maxidx, shyps = sorts, hyps = [], @@ -868,6 +882,7 @@ fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) = Thm {thy_ref = thy_ref, der = Pt.infer_derivs' I (false, Pt.reflexive), + tags = [], maxidx = maxidx, shyps = sorts, hyps = [], @@ -882,7 +897,7 @@ *) fun abstract_rule a (Cterm {t = x, T, sorts, ...}) - (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) = + (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop, ...}) = let val string_of = Sign.string_of_term (Theory.deref thy_ref); val (t, u) = Logic.dest_equals prop @@ -890,6 +905,7 @@ val result = Thm {thy_ref = thy_ref, der = Pt.infer_derivs' (Pt.abstract_rule x a) der, + tags = [], maxidx = maxidx, shyps = Sorts.union sorts shyps, hyps = hyps, @@ -932,6 +948,7 @@ (chktypes fT tT; Thm {thy_ref = merge_thys2 th1 th2, der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2, + tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, @@ -958,6 +975,7 @@ if A aconv A' andalso B aconv B' then Thm {thy_ref = merge_thys2 th1 th2, der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, + tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, @@ -985,6 +1003,7 @@ if prop2 aconv A then Thm {thy_ref = merge_thys2 th1 th2, der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, + tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, @@ -1002,7 +1021,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 {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = +fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) = Unify.smash_unifiers (Theory.deref thy_ref) tpairs (Envir.empty maxidx) |> Seq.map (fn env => if Envir.is_empty env then th @@ -1015,6 +1034,7 @@ in Thm {thy_ref = thy_ref, der = Pt.infer_derivs' (Pt.norm_proof' env) der, + tags = [], maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'), shyps = may_insert_env_sorts (Theory.deref thy_ref) env shyps, hyps = hyps, @@ -1032,7 +1052,7 @@ fun generalize ([], []) _ th = th | generalize (tfrees, frees) idx th = let - val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = th; + val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...} = th; val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); val bad_type = if null tfrees then K false else @@ -1054,6 +1074,7 @@ Thm { thy_ref = thy_ref, der = Pt.infer_derivs' (Pt.generalize (tfrees, frees) idx) der, + tags = [], maxidx = maxidx', shyps = shyps, hyps = hyps, @@ -1126,6 +1147,7 @@ Thm {thy_ref = thy_ref', der = Pt.infer_derivs' (fn d => Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, + tags = [], maxidx = maxidx', shyps = shyps', hyps = hyps, @@ -1145,6 +1167,7 @@ else Thm {thy_ref = thy_ref, der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)), + tags = [], maxidx = maxidx, shyps = sorts, hyps = [], @@ -1159,6 +1182,7 @@ in Thm {thy_ref = thy_ref, der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])), + tags = [], maxidx = maxidx, shyps = sorts, hyps = [], @@ -1169,7 +1193,7 @@ (*Internalize sort constraints of type variable*) fun unconstrainT (Ctyp {thy_ref = thy_ref1, T, ...}) - (th as Thm {thy_ref = thy_ref2, der, maxidx, shyps, hyps, tpairs, prop}) = + (th as Thm {thy_ref = thy_ref2, der, maxidx, shyps, hyps, tpairs, prop, ...}) = let val ((x, i), S) = Term.dest_TVar T handle TYPE _ => raise THM ("unconstrainT: not a type variable", 0, [th]); @@ -1179,6 +1203,7 @@ in Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.unconstrainT", prop, SOME [])), + tags = [], maxidx = Int.max (maxidx, i), shyps = Sorts.remove_sort S shyps, hyps = hyps, @@ -1187,7 +1212,7 @@ end; (* Replace all TFrees not fixed or in the hyps by new TVars *) -fun varifyT' fixed (Thm {thy_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; @@ -1196,6 +1221,7 @@ in (al, Thm {thy_ref = thy_ref, der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, + tags = [], maxidx = Int.max (0, maxidx), shyps = shyps, hyps = hyps, @@ -1206,7 +1232,7 @@ val varifyT = #2 o varifyT' []; (* Replace all TVars by new TFrees *) -fun freezeT (Thm {thy_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; @@ -1214,6 +1240,7 @@ in Thm {thy_ref = thy_ref, der = Pt.infer_derivs' (Pt.freezeT prop1) der, + tags = [], maxidx = maxidx_of_term prop2, shyps = shyps, hyps = hyps, @@ -1246,6 +1273,7 @@ else Thm {thy_ref = merge_thys1 goal orule, der = Pt.infer_derivs' (Pt.lift_proof gprop inc prop) der, + tags = [], maxidx = maxidx + inc, shyps = Sorts.union shyps sorts, (*sic!*) hyps = hyps, @@ -1253,13 +1281,14 @@ prop = Logic.list_implies (map lift_all As, lift_all B)} end; -fun incr_indexes i (thm as Thm {thy_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 {thy_ref = thy_ref, der = Pt.infer_derivs' (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der, + tags = [], maxidx = maxidx + i, shyps = shyps, hyps = hyps, @@ -1277,6 +1306,7 @@ der = Pt.infer_derivs' ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o Pt.assumption_proof Bs Bi n) der, + tags = [], maxidx = maxidx, shyps = may_insert_env_sorts thy env shyps, hyps = hyps, @@ -1307,6 +1337,7 @@ | n => Thm {thy_ref = thy_ref, der = Pt.infer_derivs' (Pt.assumption_proof Bs Bi (n + 1)) der, + tags = [], maxidx = maxidx, shyps = shyps, hyps = hyps, @@ -1335,6 +1366,7 @@ in Thm {thy_ref = thy_ref, der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, + tags = [], maxidx = maxidx, shyps = shyps, hyps = hyps, @@ -1348,7 +1380,7 @@ number of premises. Useful with etac and underlies defer_tac*) fun permute_prems j k rl = let - val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = rl; + val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...} = rl; val prems = Logic.strip_imp_prems prop and concl = Logic.strip_imp_concl prop; val moved_prems = List.drop (prems, j) @@ -1365,6 +1397,7 @@ in Thm {thy_ref = thy_ref, der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der, + tags = [], maxidx = maxidx, shyps = shyps, hyps = hyps, @@ -1381,7 +1414,7 @@ preceding parameters may be renamed to make all params distinct.*) fun rename_params_rule (cs, i) state = let - val Thm {thy_ref, der, maxidx, shyps, hyps, ...} = state; + val Thm {thy_ref, der, tags, maxidx, shyps, hyps, ...} = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val iparams = map #1 (Logic.strip_params Bi); val short = length iparams - length cs; @@ -1399,6 +1432,7 @@ | [] => Thm {thy_ref = thy_ref, der = der, + tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, @@ -1409,12 +1443,13 @@ (*** Preservation of bound variable names ***) -fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = +fun rename_boundvars pat obj (thm as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = (case Term.rename_abs pat obj prop of NONE => thm | SOME prop' => Thm {thy_ref = thy_ref, der = der, + tags = tags, maxidx = maxidx, hyps = hyps, shyps = shyps, @@ -1535,6 +1570,7 @@ else curry op oo (Pt.norm_proof' env)) (Pt.bicompose_proof flatten Bs oldAs As A n)) rder' sder, + tags = [], maxidx = maxidx, shyps = may_insert_env_sorts thy env (Sorts.union rshyps sshyps), hyps = union_hyps rhyps shyps, @@ -1632,6 +1668,7 @@ else Thm {thy_ref = Theory.self_ref thy', der = (true, Pt.oracle_proof name prop), + tags = [], maxidx = maxidx, shyps = may_insert_term_sorts thy' prop [], hyps = [],