1.1 --- a/src/Pure/meta_simplifier.ML	Thu Oct 04 15:21:17 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Oct 04 15:21:47 2001 +0200
     1.3 @@ -1,13 +1,20 @@
     1.4  (*  Title:      Pure/meta_simplifier.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 +    Author:     Tobias Nipkow and Stefan Berghofer
     1.8      Copyright   1994  University of Cambridge
     1.9  
    1.10 -Meta Simplification
    1.11 +Meta-level Simplification.
    1.12  *)
    1.13  
    1.14 +signature BASIC_META_SIMPLIFIER =
    1.15 +sig
    1.16 +  val trace_simp: bool ref
    1.17 +  val debug_simp: bool ref
    1.18 +end;
    1.19 +
    1.20  signature META_SIMPLIFIER =
    1.21  sig
    1.22 +  include BASIC_META_SIMPLIFIER
    1.23    exception SIMPLIFIER of string * thm
    1.24    type meta_simpset
    1.25    val dest_mss		: meta_simpset ->
    1.26 @@ -32,11 +39,9 @@
    1.27    val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
    1.28    val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
    1.29    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
    1.30 -  val trace_simp        : bool ref
    1.31 -  val debug_simp        : bool ref
    1.32 -  val rewrite_cterm     : bool * bool * bool
    1.33 -                          -> (meta_simpset -> thm -> thm option)
    1.34 -                          -> meta_simpset -> cterm -> thm
    1.35 +  val rewrite_cterm: bool * bool * bool ->
    1.36 +    (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
    1.37 +  val full_rewrite_cterm_aux: (meta_simpset -> thm -> thm option) -> thm list -> cterm -> cterm
    1.38    val rewrite_rule_aux  : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.39    val rewrite_thm       : bool * bool * bool
    1.40                            -> (meta_simpset -> thm -> thm option)
    1.41 @@ -931,6 +936,12 @@
    1.42  (*Use a conversion to transform a theorem*)
    1.43  fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.44  
    1.45 +(*Rewrite a cterm (yielding again a cterm instead of a theorem)*)
    1.46 +fun full_rewrite_cterm_aux _ [] = (fn ct => ct)
    1.47 +  | full_rewrite_cterm_aux prover thms =
    1.48 +      #2 o Thm.dest_comb o #prop o Thm.crep_thm o
    1.49 +        rewrite_cterm (true, false, false) prover (mss_of thms);
    1.50 +
    1.51  (*Rewrite a theorem*)
    1.52  fun rewrite_rule_aux _ [] = (fn th => th)
    1.53    | rewrite_rule_aux prover thms =
    1.54 @@ -952,4 +963,5 @@
    1.55  
    1.56  end;
    1.57  
    1.58 -open MetaSimplifier;
    1.59 +structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
    1.60 +open BasicMetaSimplifier;