interface to Pattern.rewrite_term;
authorwenzelm
Wed Jan 16 23:17:44 2002 +0100 (2002-01-16)
changeset 1278336ca5ea8092c
parent 12782 a4183c50ae5f
child 12784 bab3b002cbbb
interface to Pattern.rewrite_term;
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Wed Jan 16 22:24:37 2002 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Wed Jan 16 23:17:44 2002 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/meta_simplifier.ML
     1.5      ID:         $Id$
     1.6      Author:     Tobias Nipkow and Stefan Berghofer
     1.7 -    Copyright   1994  University of Cambridge
     1.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  
    1.10  Meta-level Simplification.
    1.11  *)
    1.12 @@ -54,6 +54,7 @@
    1.13    val rewrite_goal_rule : bool* bool * bool
    1.14                            -> (meta_simpset -> thm -> thm option)
    1.15                            -> meta_simpset -> int -> thm -> thm
    1.16 +  val rewrite_term: Sign.sg -> thm list -> term -> term
    1.17  end;
    1.18  
    1.19  structure MetaSimplifier : META_SIMPLIFIER =
    1.20 @@ -284,6 +285,12 @@
    1.21                   andalso not (is_Var (term_of elhs))
    1.22    in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
    1.23  
    1.24 +fun decomp_simp' thm =
    1.25 +  let val (_, _, _, elhs, rhs, _) = decomp_simp thm in
    1.26 +    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
    1.27 +    else (term_of elhs, rhs)
    1.28 +  end;
    1.29 +
    1.30  fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
    1.31    case mk_eq_True thm of
    1.32      None => []
    1.33 @@ -978,6 +985,10 @@
    1.34    then fconv_rule (goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
    1.35    else raise THM("rewrite_goal_rule",i,[thm]);
    1.36  
    1.37 +
    1.38 +(*simple term rewriting -- without proofs*)
    1.39 +fun rewrite_term sg rules = Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules);
    1.40 +
    1.41  end;
    1.42  
    1.43  structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;