# HG changeset patch
# User nipkow
# Date 877002316 -7200
# Node ID 5a1f22e7b359afaa0ddb616e9611f59c6b534943
# Parent  1d184682ac9fdeda60d8f042edcadecf4f4c2018
The simplifier has been improved a little: equations s=t which used to be
rejected because of looping are now treated as (s=t) == True. The latter
translation must be done outside of Thm because it involves the object-logic
specific True. Therefore the simple loop test has been moved from Thm to
Logic.

diff -r 1d184682ac9f -r 5a1f22e7b359 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Oct 16 13:43:42 1997 +0200
+++ b/src/Pure/logic.ML	Thu Oct 16 13:45:16 1997 +0200
@@ -26,6 +26,8 @@
   val list_implies	: term list * term -> term
   val list_rename_params: string list * term -> term
   val is_equals         : term -> bool
+  val loops		: Sign.sg -> term list -> term -> term
+                          -> string option * bool
   val mk_equals		: term * term -> term
   val mk_flexpair	: term * term -> term
   val mk_implies	: term * term -> term
@@ -348,4 +350,42 @@
 
 fun termless tu = (termord tu = LESS);
 
+(** Check for looping rewrite rules **)
+
+fun vperm (Var _, Var _) = true
+  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
+  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
+  | vperm (t, u) = (t = u);
+
+fun var_perm (t, u) =
+  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
+
+(*simple test for looping rewrite*)
+fun looptest sign prems lhs rhs =
+   is_Var (head_of lhs)
+  orelse
+   (exists (apl (lhs,occs)) (rhs :: prems))
+  orelse
+   (null prems andalso
+    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
+(*the condition "null prems" in the last case is necessary because
+  conditional rewrites with extra variables in the conditions may terminate
+  although the rhs is an instance of the lhs. Example:
+  ?m < ?n ==> f(?n) == f(?m)*)
+
+fun loops sign prems lhs rhs =
+  let
+    val elhs = Pattern.eta_contract lhs;
+    val erhs = Pattern.eta_contract rhs;
+    val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
+               andalso not (is_Var elhs)
+  in (if not ((term_vars erhs) subset
+              (union_term (term_vars elhs, List.concat(map term_vars prems))))
+      then Some("extra Var(s) on rhs") else
+      if not perm andalso looptest sign prems elhs erhs
+      then Some("loops")
+      else None
+      ,perm)
+  end;
+
 end;
diff -r 1d184682ac9f -r 5a1f22e7b359 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 16 13:43:42 1997 +0200
+++ b/src/Pure/thm.ML	Thu Oct 16 13:45:16 1997 +0200
@@ -1535,44 +1535,16 @@
 
 (* mk_rrule *)
 
-fun vperm (Var _, Var _) = true
-  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
-  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
-  | vperm (t, u) = (t = u);
-
-fun var_perm (t, u) =
-  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
-
-(*simple test for looping rewrite*)
-fun loops sign prems (lhs, rhs) =
-   is_Var (head_of lhs)
-  orelse
-   (exists (apl (lhs, Logic.occs)) (rhs :: prems))
-  orelse
-   (null prems andalso
-    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
-(*the condition "null prems" in the last case is necessary because
-  conditional rewrites with extra variables in the conditions may terminate
-  although the rhs is an instance of the lhs. Example:
-  ?m < ?n ==> f(?n) == f(?m)*)
-
 fun mk_rrule (thm as Thm {sign, prop, ...}) =
   let
     val prems = Logic.strip_imp_prems prop;
     val concl = Logic.strip_imp_concl prop;
-    val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
+    val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
       raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
-    val econcl = Pattern.eta_contract concl;
-    val (elhs, erhs) = Logic.dest_equals econcl;
-    val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
-      andalso not (is_Var elhs);
-  in
-    if not ((term_vars erhs) subset
-        (union_term (term_vars elhs, List.concat(map term_vars prems)))) then
-      (prtm_warning "extra Var(s) on rhs" sign prop; None)
-    else if not perm andalso loops sign prems (elhs, erhs) then
-      (prtm_warning "ignoring looping rewrite rule" sign prop; None)
-    else Some {thm = thm, lhs = lhs, perm = perm}
+  in case Logic.loops sign prems lhs rhs of
+     (None,perm) => Some {thm = thm, lhs = lhs, perm = perm}
+   | (Some msg,_) =>
+        (prtm_warning("ignoring rewrite rule ("^msg^")") sign prop; None)
   end;