# HG changeset patch # User wenzelm # Date 1164317909 -3600 # Node ID 13d4dba9933732f575ab192c740c6426932bfa14 # Parent 9c97af4a156721529dce01bbb97e84355f71f9b3 prefer Proof.context over Context.generic; tuned; diff -r 9c97af4a1567 -r 13d4dba99337 src/HOL/Algebra/ringsimp.ML --- a/src/HOL/Algebra/ringsimp.ML Thu Nov 23 22:38:28 2006 +0100 +++ b/src/HOL/Algebra/ringsimp.ML Thu Nov 23 22:38:29 2006 +0100 @@ -1,13 +1,13 @@ (* - Title: Normalisation method for locales ring and cring Id: $Id$ Author: Clemens Ballarin - Copyright: TU Muenchen + +Normalisation method for locales ring and cring. *) signature ALGEBRA = sig - val print_structures: Context.generic -> unit + val print_structures: Proof.context -> unit val setup: theory -> theory end; @@ -44,7 +44,7 @@ end end); -val print_structures = AlgebraData.print; +val print_structures = AlgebraData.print o Context.Proof; (** Method **) @@ -58,8 +58,7 @@ in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end; fun algebra_tac ctxt = - let val _ = print_structures (Context.Proof ctxt) - in EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))) end; + EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))); val method = Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt)) @@ -69,7 +68,7 @@ fun add_struct_thm s = Thm.declaration_attribute (fn thm => fn ctxt => - AlgebraData.map (fn structs => + AlgebraData.map (fn structs => if AList.defined struct_eq structs s then AList.map_entry struct_eq s (fn thms => thm :: thms) structs else (s, [thm])::structs) ctxt); @@ -79,7 +78,7 @@ val attribute = Attrib.syntax (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || - Scan.succeed true) -- Scan.lift Args.name -- + Scan.succeed true) -- Scan.lift Args.name -- Scan.repeat Args.term >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts))); @@ -92,4 +91,4 @@ Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")]; -end; (* struct *) +end; diff -r 9c97af4a1567 -r 13d4dba99337 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Thu Nov 23 22:38:28 2006 +0100 +++ b/src/HOL/Tools/recdef_package.ML Thu Nov 23 22:38:29 2006 +0100 @@ -11,7 +11,7 @@ val print_recdefs: theory -> unit val get_recdef: theory -> string -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option - val get_hints: Context.generic -> {simps: thm list, congs: (string * thm) list, wfs: thm list} + val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list} val simp_add: attribute val simp_del: attribute val cong_add: attribute @@ -130,7 +130,6 @@ in GlobalRecdefData.put (tab', hints) thy end; val get_global_hints = #2 o GlobalRecdefData.get; -val map_global_hints = GlobalRecdefData.map o apsnd; (* proof data *) @@ -143,17 +142,8 @@ fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln; end); -val get_local_hints = LocalRecdefData.get; -val map_local_hints = LocalRecdefData.map; - - -(* generic data *) - -fun get_hints (Context.Theory thy) = get_global_hints thy - | get_hints (Context.Proof ctxt) = get_local_hints ctxt; - -fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy) - | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt); +val get_hints = LocalRecdefData.get; +fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f); (* attributes *) @@ -197,7 +187,7 @@ (case opt_src of NONE => ctxt0 | SOME src => Method.only_sectioned_args recdef_modifiers I src ctxt0); - val {simps, congs, wfs} = get_local_hints ctxt; + val {simps, congs, wfs} = get_hints ctxt; val cs = local_claset_of ctxt; val ss = local_simpset_of ctxt addsimps simps; in (cs, ss, rev (map snd congs), wfs) end; diff -r 9c97af4a1567 -r 13d4dba99337 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Nov 23 22:38:28 2006 +0100 +++ b/src/HOL/Tools/res_axioms.ML Thu Nov 23 22:38:29 2006 +0100 @@ -5,29 +5,25 @@ Transformation of axiom rules (elim/intro/etc) into CNF forms. *) -(*unused during debugging*) signature RES_AXIOMS = - sig - val cnf_axiom : (string * thm) -> thm list +sig + val trace_abs: bool ref + val cnf_axiom : string * thm -> thm list val cnf_name : string -> thm list val meta_cnf_axiom : thm -> thm list - val claset_rules_of_thy : theory -> (string * thm) list - val simpset_rules_of_thy : theory -> (string * thm) list - val claset_rules_of_ctxt: Proof.context -> (string * thm) list - val simpset_rules_of_ctxt : Proof.context -> (string * thm) list - val pairname : thm -> (string * thm) + val pairname : thm -> string * thm val skolem_thm : thm -> thm list val to_nnf : thm -> thm - val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list; + val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list val meson_method_setup : theory -> theory val setup : theory -> theory + val assume_abstract_list: thm list -> thm list + val claset_rules_of: Proof.context -> (string * thm) list + val simpset_rules_of: Proof.context -> (string * thm) list + val atpset_rules_of: Proof.context -> (string * thm) list +end; - val atpset_rules_of_thy : theory -> (string * thm) list - val atpset_rules_of_ctxt : Proof.context -> (string * thm) list - end; - -structure ResAxioms = - +structure ResAxioms: RES_AXIOMS = struct (*For running the comparison between combinators and abstractions. @@ -552,16 +548,10 @@ map (fn r => (#name r, #thm r)) simps end; -fun claset_rules_of_thy thy = rules_of_claset (claset_of thy); -fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy); - -fun atpset_rules_of_thy thy = map pairname (ResAtpset.get_atpset (Context.Theory thy)); +fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt); +fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt); - -fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt); -fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); - -fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpset.get_atpset (Context.Proof ctxt)); +fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt); (**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****)