prefer Proof.context over Context.generic;
authorwenzelm
Thu Nov 23 22:38:29 2006 +0100 (2006-11-23)
changeset 2150513d4dba99337
parent 21504 9c97af4a1567
child 21506 b2a673894ce5
prefer Proof.context over Context.generic;
tuned;
src/HOL/Algebra/ringsimp.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Algebra/ringsimp.ML	Thu Nov 23 22:38:28 2006 +0100
     1.2 +++ b/src/HOL/Algebra/ringsimp.ML	Thu Nov 23 22:38:29 2006 +0100
     1.3 @@ -1,13 +1,13 @@
     1.4  (*
     1.5 -  Title:     Normalisation method for locales ring and cring
     1.6    Id:        $Id$
     1.7    Author:    Clemens Ballarin
     1.8 -  Copyright: TU Muenchen
     1.9 +
    1.10 +Normalisation method for locales ring and cring.
    1.11  *)
    1.12  
    1.13  signature ALGEBRA =
    1.14  sig
    1.15 -  val print_structures: Context.generic -> unit
    1.16 +  val print_structures: Proof.context -> unit
    1.17    val setup: theory -> theory
    1.18  end;
    1.19  
    1.20 @@ -44,7 +44,7 @@
    1.21      end
    1.22  end);
    1.23  
    1.24 -val print_structures = AlgebraData.print;
    1.25 +val print_structures = AlgebraData.print o Context.Proof;
    1.26  
    1.27  
    1.28  (** Method **)
    1.29 @@ -58,8 +58,7 @@
    1.30    in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
    1.31  
    1.32  fun algebra_tac ctxt =
    1.33 -  let val _ = print_structures (Context.Proof ctxt)
    1.34 -  in EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))) end;
    1.35 +  EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
    1.36  
    1.37  val method =
    1.38    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt))
    1.39 @@ -69,7 +68,7 @@
    1.40  
    1.41  fun add_struct_thm s =
    1.42    Thm.declaration_attribute (fn thm => fn ctxt =>
    1.43 -    AlgebraData.map (fn structs => 
    1.44 +    AlgebraData.map (fn structs =>
    1.45        if AList.defined struct_eq structs s
    1.46        then AList.map_entry struct_eq s (fn thms => thm :: thms) structs
    1.47        else (s, [thm])::structs) ctxt);
    1.48 @@ -79,7 +78,7 @@
    1.49  
    1.50  val attribute = Attrib.syntax
    1.51       (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
    1.52 -        Scan.succeed true) -- Scan.lift Args.name -- 
    1.53 +        Scan.succeed true) -- Scan.lift Args.name --
    1.54        Scan.repeat Args.term
    1.55        >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
    1.56  
    1.57 @@ -92,4 +91,4 @@
    1.58    Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
    1.59  
    1.60  
    1.61 -end;  (* struct *)
    1.62 +end;
     2.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Nov 23 22:38:28 2006 +0100
     2.2 +++ b/src/HOL/Tools/recdef_package.ML	Thu Nov 23 22:38:29 2006 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4    val print_recdefs: theory -> unit
     2.5    val get_recdef: theory -> string
     2.6      -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
     2.7 -  val get_hints: Context.generic -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
     2.8 +  val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
     2.9    val simp_add: attribute
    2.10    val simp_del: attribute
    2.11    val cong_add: attribute
    2.12 @@ -130,7 +130,6 @@
    2.13    in GlobalRecdefData.put (tab', hints) thy end;
    2.14  
    2.15  val get_global_hints = #2 o GlobalRecdefData.get;
    2.16 -val map_global_hints = GlobalRecdefData.map o apsnd;
    2.17  
    2.18  
    2.19  (* proof data *)
    2.20 @@ -143,17 +142,8 @@
    2.21    fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
    2.22  end);
    2.23  
    2.24 -val get_local_hints = LocalRecdefData.get;
    2.25 -val map_local_hints = LocalRecdefData.map;
    2.26 -
    2.27 -
    2.28 -(* generic data *)
    2.29 -
    2.30 -fun get_hints (Context.Theory thy) = get_global_hints thy
    2.31 -  | get_hints (Context.Proof ctxt) = get_local_hints ctxt;
    2.32 -
    2.33 -fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
    2.34 -  | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
    2.35 +val get_hints = LocalRecdefData.get;
    2.36 +fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f);
    2.37  
    2.38  
    2.39  (* attributes *)
    2.40 @@ -197,7 +187,7 @@
    2.41        (case opt_src of
    2.42          NONE => ctxt0
    2.43        | SOME src => Method.only_sectioned_args recdef_modifiers I src ctxt0);
    2.44 -    val {simps, congs, wfs} = get_local_hints ctxt;
    2.45 +    val {simps, congs, wfs} = get_hints ctxt;
    2.46      val cs = local_claset_of ctxt;
    2.47      val ss = local_simpset_of ctxt addsimps simps;
    2.48    in (cs, ss, rev (map snd congs), wfs) end;
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Nov 23 22:38:28 2006 +0100
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Nov 23 22:38:29 2006 +0100
     3.3 @@ -5,29 +5,25 @@
     3.4  Transformation of axiom rules (elim/intro/etc) into CNF forms.
     3.5  *)
     3.6  
     3.7 -(*unused during debugging*)
     3.8  signature RES_AXIOMS =
     3.9 -  sig
    3.10 -  val cnf_axiom : (string * thm) -> thm list
    3.11 +sig
    3.12 +  val trace_abs: bool ref
    3.13 +  val cnf_axiom : string * thm -> thm list
    3.14    val cnf_name : string -> thm list
    3.15    val meta_cnf_axiom : thm -> thm list
    3.16 -  val claset_rules_of_thy : theory -> (string * thm) list
    3.17 -  val simpset_rules_of_thy : theory -> (string * thm) list
    3.18 -  val claset_rules_of_ctxt: Proof.context -> (string * thm) list
    3.19 -  val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
    3.20 -  val pairname : thm -> (string * thm)
    3.21 +  val pairname : thm -> string * thm
    3.22    val skolem_thm : thm -> thm list
    3.23    val to_nnf : thm -> thm
    3.24 -  val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
    3.25 +  val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
    3.26    val meson_method_setup : theory -> theory
    3.27    val setup : theory -> theory
    3.28 +  val assume_abstract_list: thm list -> thm list
    3.29 +  val claset_rules_of: Proof.context -> (string * thm) list
    3.30 +  val simpset_rules_of: Proof.context -> (string * thm) list
    3.31 +  val atpset_rules_of: Proof.context -> (string * thm) list
    3.32 +end;
    3.33  
    3.34 -  val atpset_rules_of_thy : theory -> (string * thm) list
    3.35 -  val atpset_rules_of_ctxt : Proof.context -> (string * thm) list
    3.36 -  end;
    3.37 -
    3.38 -structure ResAxioms =
    3.39 -
    3.40 +structure ResAxioms: RES_AXIOMS =
    3.41  struct
    3.42  
    3.43  (*For running the comparison between combinators and abstractions.
    3.44 @@ -552,16 +548,10 @@
    3.45        map (fn r => (#name r, #thm r)) simps
    3.46    end;
    3.47  
    3.48 -fun claset_rules_of_thy thy = rules_of_claset (claset_of thy);
    3.49 -fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy);
    3.50 -
    3.51 -fun atpset_rules_of_thy thy = map pairname (ResAtpset.get_atpset (Context.Theory thy));
    3.52 +fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
    3.53 +fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
    3.54  
    3.55 -
    3.56 -fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt);
    3.57 -fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt);
    3.58 -
    3.59 -fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpset.get_atpset (Context.Proof ctxt));
    3.60 +fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt);
    3.61  
    3.62  
    3.63  (**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)