# HG changeset patch # User wenzelm # Date 1185712194 -7200 # Node ID 273698405054f16182a1692051e50695d299f9e2 # Parent 18182c4aec9e22bd603e17d1af6fe147b9594934 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms; diff -r 18182c4aec9e -r 273698405054 src/HOL/Hyperreal/transfer.ML --- a/src/HOL/Hyperreal/transfer.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/HOL/Hyperreal/transfer.ML Sun Jul 29 14:29:54 2007 +0200 @@ -30,14 +30,12 @@ refolds = refolds1, consts = consts1}, {intros = intros2, unfolds = unfolds2, refolds = refolds2, consts = consts2}) = - {intros = Drule.merge_rules (intros1, intros2), - unfolds = Drule.merge_rules (unfolds1, unfolds2), - refolds = Drule.merge_rules (refolds1, refolds2), + {intros = Thm.merge_thms (intros1, intros2), + unfolds = Thm.merge_thms (unfolds1, unfolds2), + refolds = Thm.merge_thms (refolds1, refolds2), consts = Library.merge (op =) (consts1, consts2)} : T; ); -val transfer_start = thm "transfer_start" - fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts) | unstar_typ T = T @@ -48,7 +46,7 @@ else (Const(a,unstar_typ T) $ unstar t) | unstar (f $ t) = unstar f $ unstar t | unstar (Const(a,T)) = Const(a,unstar_typ T) - | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) + | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) | unstar t = t in unstar term @@ -67,7 +65,7 @@ rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN ALLGOALS ObjectLogic.full_atomize_tac THEN match_tac [transitive_thm] 1 THEN - resolve_tac [transfer_start] 1 THEN + resolve_tac [@{thm transfer_start}] 1 THEN REPEAT_ALL_NEW (resolve_tac intros) 1 THEN match_tac [reflexive_thm] 1 in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end @@ -92,14 +90,14 @@ (fn {intros,unfolds,refolds,consts} => {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts}) in -val intro_add = Thm.declaration_attribute (map_intros o Drule.add_rule); -val intro_del = Thm.declaration_attribute (map_intros o Drule.del_rule); +val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm); +val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm); -val unfold_add = Thm.declaration_attribute (map_unfolds o Drule.add_rule); -val unfold_del = Thm.declaration_attribute (map_unfolds o Drule.del_rule); +val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm); +val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm); -val refold_add = Thm.declaration_attribute (map_refolds o Drule.add_rule); -val refold_del = Thm.declaration_attribute (map_refolds o Drule.del_rule); +val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm); +val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm); end fun add_const c = Context.theory_map (TransferData.map diff -r 18182c4aec9e -r 273698405054 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Jul 29 14:29:54 2007 +0200 @@ -34,9 +34,9 @@ type T = {eqvts:thm list, freshs:thm list, bijs:thm list}; val empty = ({eqvts=[], freshs=[], bijs=[]}:T); val extend = I; - fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2), - freshs = Drule.merge_rules (#freshs r1, #freshs r2), - bijs = Drule.merge_rules (#bijs r1, #bijs r2)} + fun merge _ (r1:T,r2:T) = {eqvts = Thm.merge_thms (#eqvts r1, #eqvts r2), + freshs = Thm.merge_thms (#freshs r1, #freshs r2), + bijs = Thm.merge_thms (#bijs r1, #bijs r2)} ); (* Exception for when a theorem does not conform with form of an equivariance lemma. *) @@ -102,7 +102,7 @@ val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp) val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) val _ = Display.print_cterm (cterm_of thy goal_term) - in + in Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) end @@ -136,10 +136,10 @@ (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ (Var (n,ty))) => let - (* FIXME: this should be an operation the library *) + (* FIXME: this should be an operation the library *) val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) - in - if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) + in + if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) then [(pi,typi)] else raise EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) @@ -177,7 +177,7 @@ (* case: eqvt-lemma is of the equational form *) | (Const ("Trueprop", _) $ (Const ("op =", _) $ (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) => - (if (apply_pi lhs (pi,typi)) = rhs + (if (apply_pi lhs (pi,typi)) = rhs then [orig_thm] else raise EQVT_FORM "Type Equality") | _ => raise EQVT_FORM "Type unknown") @@ -205,15 +205,15 @@ fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r}; fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))}; -val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); -val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule)); -val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule)); -val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule)); +val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Thm.add_thm)); +val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Thm.del_thm)); +val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Thm.add_thm)); +val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Thm.del_thm)); -val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule)); -val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule)); -val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule)); -val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule)); +val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Thm.add_thm)); +val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Thm.del_thm)); +val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Thm.add_thm)); +val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Thm.del_thm)); @@ -221,7 +221,7 @@ Attrib.add_attributes [("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"), ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del, - "equivariance theorem declaration (without checking the form of the lemma)"), + "equivariance theorem declaration (without checking the form of the lemma)"), ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"), ("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")]; diff -r 18182c4aec9e -r 273698405054 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Sun Jul 29 14:29:54 2007 +0200 @@ -89,7 +89,7 @@ type T = thm list val empty = [] val extend = I - fun merge _ = Drule.merge_rules + fun merge _ = Thm.merge_thms ); @@ -136,7 +136,7 @@ type T = thm list val empty = [] val extend = I - fun merge _ = Drule.merge_rules + fun merge _ = Thm.merge_thms ); val get_termination_rules = TerminationRule.get diff -r 18182c4aec9e -r 273698405054 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Sun Jul 29 14:29:54 2007 +0200 @@ -172,14 +172,14 @@ (* congruence rules *) -val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq); -val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq); +val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq); +val cong_del = Thm.declaration_attribute (map_fundef_congs o Thm.del_thm o safe_mk_meta_eq); (* Datatype hook to declare datatype congs as "fundef_congs" *) fun add_case_cong n thy = - Context.theory_map (map_fundef_congs (Drule.add_rule + Context.theory_map (map_fundef_congs (Thm.add_thm (DatatypePackage.get_datatype thy n |> the |> #case_cong |> safe_mk_meta_eq))) diff -r 18182c4aec9e -r 273698405054 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/HOL/Tools/inductive_package.ML Sun Jul 29 14:29:54 2007 +0200 @@ -134,7 +134,7 @@ val empty = (Symtab.empty, []); val extend = I; fun merge _ ((tab1, monos1), (tab2, monos2)) = - (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2)); + (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2)); ); val get_inductives = InductiveData.get o Context.Proof; @@ -187,8 +187,8 @@ | _ => [thm] end handle THM _ => error ("Bad monotonicity theorem:\n" ^ string_of_thm thm); -val mono_add = Thm.declaration_attribute (map_monos o fold Drule.add_rule o mk_mono); -val mono_del = Thm.declaration_attribute (map_monos o fold Drule.del_rule o mk_mono); +val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono); +val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono); diff -r 18182c4aec9e -r 273698405054 src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/HOL/Tools/inductive_set_package.ML Sun Jul 29 14:29:54 2007 +0200 @@ -172,8 +172,8 @@ set_arities = set_arities1, pred_arities = pred_arities1}, {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2, set_arities = set_arities2, pred_arities = pred_arities2}) = - {to_set_simps = Drule.merge_rules (to_set_simps1, to_set_simps2), - to_pred_simps = Drule.merge_rules (to_pred_simps1, to_pred_simps2), + {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2), + to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2), set_arities = Symtab.merge_list op = (set_arities1, set_arities2), pred_arities = Symtab.merge_list op = (pred_arities1, pred_arities2)}; ); diff -r 18182c4aec9e -r 273698405054 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/HOL/Tools/recdef_package.ML Sun Jul 29 14:29:54 2007 +0200 @@ -105,9 +105,9 @@ ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}), (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T = (Symtab.merge (K true) (tab1, tab2), - mk_hints (Drule.merge_rules (simps1, simps2), + mk_hints (Thm.merge_thms (simps1, simps2), AList.merge (op =) Thm.eq_thm (congs1, congs2), - Drule.merge_rules (wfs1, wfs2))); + Thm.merge_thms (wfs1, wfs2))); ); val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get; @@ -138,12 +138,12 @@ fun attrib f = Thm.declaration_attribute (map_hints o f); -val simp_add = attrib (map_simps o Drule.add_rule); -val simp_del = attrib (map_simps o Drule.del_rule); +val simp_add = attrib (map_simps o Thm.add_thm); +val simp_del = attrib (map_simps o Thm.del_thm); val cong_add = attrib (map_congs o add_cong); val cong_del = attrib (map_congs o del_cong); -val wf_add = attrib (map_wfs o Drule.add_rule); -val wf_del = attrib (map_wfs o Drule.del_rule); +val wf_add = attrib (map_wfs o Thm.add_thm); +val wf_del = attrib (map_wfs o Thm.del_thm); (* modifiers *) diff -r 18182c4aec9e -r 273698405054 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Sun Jul 29 14:29:54 2007 +0200 @@ -122,11 +122,11 @@ lessD = lessD1, neqE=neqE1, simpset = simpset1}, {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, lessD = lessD2, neqE=neqE2, simpset = simpset2}) = - {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2), - mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2), - inj_thms = Drule.merge_rules (inj_thms1, inj_thms2), - lessD = Drule.merge_rules (lessD1, lessD2), - neqE = Drule.merge_rules (neqE1, neqE2), + {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2), + mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2), + inj_thms = Thm.merge_thms (inj_thms1, inj_thms2), + lessD = Thm.merge_thms (lessD1, lessD2), + neqE = Thm.merge_thms (neqE1, neqE2), simpset = Simplifier.merge_ss (simpset1, simpset2)}; ); diff -r 18182c4aec9e -r 273698405054 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/Pure/Isar/calculation.ML Sun Jul 29 14:29:54 2007 +0200 @@ -35,7 +35,7 @@ val extend = I; fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = - ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE); + ((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); ); fun print_rules ctxt = @@ -71,10 +71,10 @@ val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete); val sym_add = - Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.add_rule) + Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) #> ContextRules.elim_query NONE; val sym_del = - Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule) + Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm) #> ContextRules.rule_del; diff -r 18182c4aec9e -r 273698405054 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/Pure/Isar/local_defs.ML Sun Jul 29 14:29:54 2007 +0200 @@ -151,15 +151,15 @@ type T = thm list; val empty = [] val extend = I; - fun merge _ = Drule.merge_rules; + fun merge _ = Thm.merge_thms; ); fun print_rules ctxt = Pretty.writeln (Pretty.big_list "definitional transformations:" (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt)))); -val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule); -val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule); +val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm); +val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm); (* meta rewrite rules *) diff -r 18182c4aec9e -r 273698405054 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/Pure/Isar/object_logic.ML Sun Jul 29 14:29:54 2007 +0200 @@ -51,7 +51,7 @@ fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) = (merge_judgment (judgment1, judgment2), - (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2))); + (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2))); ); @@ -141,8 +141,8 @@ val get_atomize = #1 o #2 o ObjectLogicData.get; val get_rulify = #2 o #2 o ObjectLogicData.get; -val add_atomize = ObjectLogicData.map o apsnd o apfst o Drule.add_rule; -val add_rulify = ObjectLogicData.map o apsnd o apsnd o Drule.add_rule; +val add_atomize = ObjectLogicData.map o apsnd o apfst o Thm.add_thm; +val add_rulify = ObjectLogicData.map o apsnd o apsnd o Thm.add_thm; val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I); val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I); diff -r 18182c4aec9e -r 273698405054 src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/ZF/Tools/typechk.ML Sun Jul 29 14:29:54 2007 +0200 @@ -49,7 +49,7 @@ val extend = I; fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) = - TC {rules = Drule.merge_rules (rules, rules'), + TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')}; );