normalized some ML type/val aliases;
authorwenzelm
Thu Jan 01 23:31:49 2009 +0100 (2009-01-01)
changeset 29302eb782d1dc07c
parent 29301 2b845381ba6a
child 29303 57f0d287375e
normalized some ML type/val aliases;
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/Pure/Isar/code.ML
src/Pure/Isar/find_theorems.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Jan 01 22:57:42 2009 +0100
     1.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Jan 01 23:31:49 2009 +0100
     1.3 @@ -5,23 +5,20 @@
     1.4  signature DISTINCT_TREE_PROVER =
     1.5  sig
     1.6    datatype Direction = Left | Right
     1.7 -  val mk_tree : ('a -> Term.term) -> Term.typ -> 'a list -> Term.term
     1.8 -  val dest_tree : Term.term -> Term.term list
     1.9 -  val find_tree :
    1.10 -       Term.term -> Term.term -> Direction list option 
    1.11 +  val mk_tree : ('a -> term) -> typ -> 'a list -> term
    1.12 +  val dest_tree : term -> term list
    1.13 +  val find_tree : term -> term -> Direction list option 
    1.14  
    1.15 -  val neq_to_eq_False : Thm.thm
    1.16 -  val distinctTreeProver : Thm.thm -> Direction list -> Direction list -> Thm.thm
    1.17 -  val neq_x_y :
    1.18 -       Proof.context -> Term.term -> Term.term -> string -> Thm.thm option   
    1.19 -  val distinctFieldSolver : string list -> MetaSimplifier.solver
    1.20 -  val distinctTree_tac :
    1.21 -       string list -> Proof.context -> Term.term * int -> Tactical.tactic
    1.22 -  val distinct_implProver : Thm.thm -> Thm.cterm -> Thm.thm
    1.23 -  val subtractProver : Term.term -> Thm.cterm -> Thm.thm -> Thm.thm
    1.24 -  val distinct_simproc : string list -> MetaSimplifier.simproc
    1.25 +  val neq_to_eq_False : thm
    1.26 +  val distinctTreeProver : thm -> Direction list -> Direction list -> thm
    1.27 +  val neq_x_y : Proof.context -> term -> term -> string -> thm option   
    1.28 +  val distinctFieldSolver : string list -> solver
    1.29 +  val distinctTree_tac : string list -> Proof.context -> term * int -> tactic
    1.30 +  val distinct_implProver : thm -> cterm -> thm
    1.31 +  val subtractProver : term -> cterm -> thm -> thm
    1.32 +  val distinct_simproc : string list -> simproc
    1.33    
    1.34 -  val discharge : Thm.thm list -> Thm.thm -> Thm.thm
    1.35 +  val discharge : thm list -> thm -> thm
    1.36  end;
    1.37  
    1.38  structure DistinctTreeProver : DISTINCT_TREE_PROVER =
     2.1 --- a/src/HOL/Statespace/state_fun.ML	Thu Jan 01 22:57:42 2009 +0100
     2.2 +++ b/src/HOL/Statespace/state_fun.ML	Thu Jan 01 23:31:49 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Statespace/state_fun.ML
     2.5 -    ID:         $Id$
     2.6      Author:     Norbert Schirmer, TU Muenchen
     2.7  *)
     2.8  
     2.9 @@ -8,17 +7,17 @@
    2.10    val lookupN : string
    2.11    val updateN : string
    2.12  
    2.13 -  val mk_constr : Context.theory -> Term.typ -> Term.term
    2.14 -  val mk_destr : Context.theory -> Term.typ -> Term.term
    2.15 +  val mk_constr : theory -> typ -> term
    2.16 +  val mk_destr : theory -> typ -> term
    2.17  
    2.18 -  val lookup_simproc : MetaSimplifier.simproc
    2.19 -  val update_simproc : MetaSimplifier.simproc
    2.20 -  val ex_lookup_eq_simproc : MetaSimplifier.simproc
    2.21 -  val ex_lookup_ss : MetaSimplifier.simpset
    2.22 -  val lazy_conj_simproc : MetaSimplifier.simproc
    2.23 -  val string_eq_simp_tac : int -> Tactical.tactic
    2.24 +  val lookup_simproc : simproc
    2.25 +  val update_simproc : simproc
    2.26 +  val ex_lookup_eq_simproc : simproc
    2.27 +  val ex_lookup_ss : simpset
    2.28 +  val lazy_conj_simproc : simproc
    2.29 +  val string_eq_simp_tac : int -> tactic
    2.30  
    2.31 -  val setup : Context.theory -> Context.theory
    2.32 +  val setup : theory -> theory
    2.33  end;
    2.34  
    2.35  structure StateFun: STATE_FUN = 
     3.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Jan 01 22:57:42 2009 +0100
     3.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu Jan 01 23:31:49 2009 +0100
     3.3 @@ -674,7 +674,7 @@
     3.4       fun prover used ss thm =
     3.5       let fun cong_prover ss thm =
     3.6           let val dummy = say "cong_prover:"
     3.7 -             val cntxt = MetaSimplifier.prems_of_ss ss
     3.8 +             val cntxt = Simplifier.prems_of_ss ss
     3.9               val dummy = print_thms "cntxt:" cntxt
    3.10               val dummy = say "cong rule:"
    3.11               val dummy = say (Display.string_of_thm thm)
    3.12 @@ -687,7 +687,7 @@
    3.13                       val ants = map tych (Logic.strip_imp_prems imp)
    3.14                       val eq = Logic.strip_imp_concl imp
    3.15                       val lhs = tych(get_lhs eq)
    3.16 -                     val ss' = MetaSimplifier.add_prems (map ASSUME ants) ss
    3.17 +                     val ss' = Simplifier.add_prems (map ASSUME ants) ss
    3.18                       val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
    3.19                         handle U.ERR _ => Thm.reflexive lhs
    3.20                       val dummy = print_thms "proven:" [lhs_eq_lhs1]
    3.21 @@ -708,7 +708,7 @@
    3.22                    val Q = get_lhs eq1
    3.23                    val QeqQ1 = pbeta_reduce (tych Q)
    3.24                    val Q1 = #2(D.dest_eq(cconcl QeqQ1))
    3.25 -                  val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
    3.26 +                  val ss' = Simplifier.add_prems (map ASSUME ants1) ss
    3.27                    val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
    3.28                                  handle U.ERR _ => Thm.reflexive Q1
    3.29                    val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
    3.30 @@ -758,7 +758,7 @@
    3.31  
    3.32          fun restrict_prover ss thm =
    3.33            let val dummy = say "restrict_prover:"
    3.34 -              val cntxt = rev(MetaSimplifier.prems_of_ss ss)
    3.35 +              val cntxt = rev(Simplifier.prems_of_ss ss)
    3.36                val dummy = print_thms "cntxt:" cntxt
    3.37                val thy = Thm.theory_of_thm thm
    3.38                val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
     4.1 --- a/src/HOL/Tools/arith_data.ML	Thu Jan 01 22:57:42 2009 +0100
     4.2 +++ b/src/HOL/Tools/arith_data.ML	Thu Jan 01 23:31:49 2009 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/arith_data.ML
     4.5 -    ID:         $Id$
     4.6      Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
     4.7  
     4.8  Basic arithmetic proof tools.
     4.9 @@ -7,9 +6,8 @@
    4.10  
    4.11  signature ARITH_DATA =
    4.12  sig
    4.13 -  val prove_conv: tactic -> (MetaSimplifier.simpset -> tactic)
    4.14 -    -> MetaSimplifier.simpset -> term * term -> thm
    4.15 -  val simp_all_tac: thm list -> MetaSimplifier.simpset -> tactic
    4.16 +  val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
    4.17 +  val simp_all_tac: thm list -> simpset -> tactic
    4.18  
    4.19    val mk_sum: term list -> term
    4.20    val mk_norm_sum: term list -> term
     5.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Jan 01 22:57:42 2009 +0100
     5.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Jan 01 23:31:49 2009 +0100
     5.3 @@ -413,7 +413,7 @@
     5.4      val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
     5.5      val ctxt = ProofContext.init thy;
     5.6      val simpset = Simplifier.context ctxt
     5.7 -      (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
     5.8 +      (Simplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
     5.9      val cos = map (fn (co, tys) =>
    5.10          (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
    5.11      val tac = ALLGOALS (simp_tac simpset)
     6.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Thu Jan 01 22:57:42 2009 +0100
     6.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Thu Jan 01 23:31:49 2009 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOL/Tools/function_package/fundef_lib.ML
     6.5 -    ID:         $Id$
     6.6      Author:     Alexander Krauss, TU Muenchen
     6.7  
     6.8  A package for general recursive function definitions. 
     6.9 @@ -163,7 +162,7 @@
    6.10            else if js = []
    6.11              then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
    6.12              else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
    6.13 -     (K (MetaSimplifier.rewrite_goals_tac ac
    6.14 +     (K (rewrite_goals_tac ac
    6.15           THEN rtac Drule.reflexive_thm 1))
    6.16   end
    6.17  
     7.1 --- a/src/Pure/Isar/code.ML	Thu Jan 01 22:57:42 2009 +0100
     7.2 +++ b/src/Pure/Isar/code.ML	Thu Jan 01 23:31:49 2009 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      Pure/Isar/code.ML
     7.5 -    ID:         $Id$
     7.6      Author:     Florian Haftmann, TU Muenchen
     7.7  
     7.8  Abstract executable content of theory.  Management of data dependent on
     7.9 @@ -16,8 +15,8 @@
    7.10    val del_eqn: thm -> theory -> theory
    7.11    val del_eqns: string -> theory -> theory
    7.12    val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
    7.13 -  val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    7.14 -  val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    7.15 +  val map_pre: (simpset -> simpset) -> theory -> theory
    7.16 +  val map_post: (simpset -> simpset) -> theory -> theory
    7.17    val add_inline: thm -> theory -> theory
    7.18    val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
    7.19    val del_functrans: string -> theory -> theory
    7.20 @@ -186,8 +185,8 @@
    7.21  (* pre- and postprocessor *)
    7.22  
    7.23  datatype thmproc = Thmproc of {
    7.24 -  pre: MetaSimplifier.simpset,
    7.25 -  post: MetaSimplifier.simpset,
    7.26 +  pre: simpset,
    7.27 +  post: simpset,
    7.28    functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
    7.29  };
    7.30  
    7.31 @@ -198,8 +197,8 @@
    7.32  fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
    7.33    Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
    7.34      let
    7.35 -      val pre = MetaSimplifier.merge_ss (pre1, pre2);
    7.36 -      val post = MetaSimplifier.merge_ss (post1, post2);
    7.37 +      val pre = Simplifier.merge_ss (pre1, pre2);
    7.38 +      val post = Simplifier.merge_ss (post1, post2);
    7.39        val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
    7.40      in mk_thmproc ((pre, post), functrans) end;
    7.41  
    7.42 @@ -221,7 +220,7 @@
    7.43      val thmproc = merge_thmproc (thmproc1, thmproc2);
    7.44      val spec = merge_spec (spec1, spec2);
    7.45    in mk_exec (thmproc, spec) end;
    7.46 -val empty_exec = mk_exec (mk_thmproc ((MetaSimplifier.empty_ss, MetaSimplifier.empty_ss), []),
    7.47 +val empty_exec = mk_exec (mk_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []),
    7.48    mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty))));
    7.49  
    7.50  fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x;
    7.51 @@ -417,12 +416,12 @@
    7.52        Pretty.block [
    7.53          Pretty.str "preprocessing simpset:",
    7.54          Pretty.fbrk,
    7.55 -        MetaSimplifier.pretty_ss pre
    7.56 +        Simplifier.pretty_ss pre
    7.57        ],
    7.58        Pretty.block [
    7.59          Pretty.str "postprocessing simpset:",
    7.60          Pretty.fbrk,
    7.61 -        MetaSimplifier.pretty_ss post
    7.62 +        Simplifier.pretty_ss post
    7.63        ],
    7.64        Pretty.block (
    7.65          Pretty.str "function transformers:"
     8.1 --- a/src/Pure/Isar/find_theorems.ML	Thu Jan 01 22:57:42 2009 +0100
     8.2 +++ b/src/Pure/Isar/find_theorems.ML	Thu Jan 01 23:31:49 2009 +0100
     8.3 @@ -165,7 +165,7 @@
     8.4  fun filter_simp ctxt t (_, thm) =
     8.5    let
     8.6      val (_, {mk_rews = {mk, ...}, ...}) =
     8.7 -      MetaSimplifier.rep_ss (Simplifier.local_simpset_of ctxt);
     8.8 +      Simplifier.rep_ss (Simplifier.local_simpset_of ctxt);
     8.9      val extract_simp =
    8.10        (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
    8.11      val ss = is_matching_thm extract_simp ctxt false t thm
     9.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Jan 01 22:57:42 2009 +0100
     9.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Jan 01 23:31:49 2009 +0100
     9.3 @@ -249,7 +249,7 @@
     9.4      |> ListPair.map (fn (t, tacs) =>
     9.5        Goal.prove_global thy1 [] [] t
     9.6          (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
     9.7 -    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
     9.8 +    handle Simplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
     9.9  
    9.10    (********)
    9.11    val dummy = writeln "  Proving the elimination rule...";