Improved loop-test for rewrite rules a little.
authornipkow
Wed Feb 18 11:31:25 1998 +0100 (1998-02-18)
changeset 4631c7fa4ae34495
parent 4630 437ddddbfef5
child 4632 0a365c3e4b27
Improved loop-test for rewrite rules a little.
Should be done properly!
src/Pure/logic.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/logic.ML	Wed Feb 18 10:37:48 1998 +0100
     1.2 +++ b/src/Pure/logic.ML	Wed Feb 18 11:31:25 1998 +0100
     1.3 @@ -161,11 +161,7 @@
     1.4  
     1.5  (*Does t occur in u?  Or is alpha-convertible to u?
     1.6    The term t must contain no loose bound variables*)
     1.7 -fun t occs u = (t aconv u) orelse 
     1.8 -      (case u of
     1.9 -          Abs(_,_,body) => t occs body
    1.10 -	| f$t' => t occs f  orelse  t occs t'
    1.11 -	| _ => false);
    1.12 +fun t occs u = exists_subterm (fn s => t aconv s) u;
    1.13  
    1.14  (*Close up a formula over all free variables by quantification*)
    1.15  fun close_form A =
    1.16 @@ -327,11 +323,18 @@
    1.17     (exists (apl (lhs, op occs)) (rhs :: prems))
    1.18    orelse
    1.19     (null prems andalso
    1.20 -    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
    1.21 -(*the condition "null prems" in the last case is necessary because
    1.22 +    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
    1.23 +  orelse
    1.24 +   (case lhs of
    1.25 +      (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse
    1.26 +                                 (null prems andalso f occs rhs)
    1.27 +    | _ => false);
    1.28 +(*the condition "null prems" in the last cases is necessary because
    1.29    conditional rewrites with extra variables in the conditions may terminate
    1.30    although the rhs is an instance of the lhs. Example:
    1.31    ?m < ?n ==> f(?n) == f(?m)*)
    1.32 +(*FIXME: proper test: lhs does not match a subterm of a premise
    1.33 +                      and does not match a subterm of the rhs if null prems *)
    1.34  
    1.35  fun rewrite_rule_extra_vars prems elhs erhs =
    1.36    if not ((term_vars erhs) subset
     2.1 --- a/src/Pure/term.ML	Wed Feb 18 10:37:48 1998 +0100
     2.2 +++ b/src/Pure/term.ML	Wed Feb 18 11:31:25 1998 +0100
     2.3 @@ -154,6 +154,7 @@
     2.4    val add_term_vars: term * term list -> term list
     2.5    val term_vars: term -> term list
     2.6    val exists_Const: (string * typ -> bool) -> term -> bool
     2.7 +  val exists_subterm: (term -> bool) -> term -> bool
     2.8    val compress_type: typ -> typ
     2.9    val compress_term: term -> term
    2.10  end;
    2.11 @@ -729,6 +730,14 @@
    2.12  	|   ex _               = false
    2.13      in ex t end;
    2.14  
    2.15 +fun exists_subterm P =
    2.16 +  let fun ex t = P t orelse
    2.17 +                 (case t of
    2.18 +                    u $ v        => ex u orelse ex v
    2.19 +                  | Abs(_, _, u) => ex u
    2.20 +                  | _            => false)
    2.21 +  in ex end;
    2.22 +
    2.23  (*map classes, tycons*)
    2.24  fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    2.25    | map_typ f _ (TFree (x, S)) = TFree (x, map f S)