The simplifier has been improved a little: equations s=t which used to be
authornipkow
Thu Oct 16 13:45:16 1997 +0200 (1997-10-16)
changeset 38935a1f22e7b359
parent 3892 1d184682ac9f
child 3894 8b9f0bc6dc1a
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.
src/Pure/logic.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/logic.ML	Thu Oct 16 13:43:42 1997 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Oct 16 13:45:16 1997 +0200
     1.3 @@ -26,6 +26,8 @@
     1.4    val list_implies	: term list * term -> term
     1.5    val list_rename_params: string list * term -> term
     1.6    val is_equals         : term -> bool
     1.7 +  val loops		: Sign.sg -> term list -> term -> term
     1.8 +                          -> string option * bool
     1.9    val mk_equals		: term * term -> term
    1.10    val mk_flexpair	: term * term -> term
    1.11    val mk_implies	: term * term -> term
    1.12 @@ -348,4 +350,42 @@
    1.13  
    1.14  fun termless tu = (termord tu = LESS);
    1.15  
    1.16 +(** Check for looping rewrite rules **)
    1.17 +
    1.18 +fun vperm (Var _, Var _) = true
    1.19 +  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
    1.20 +  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
    1.21 +  | vperm (t, u) = (t = u);
    1.22 +
    1.23 +fun var_perm (t, u) =
    1.24 +  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
    1.25 +
    1.26 +(*simple test for looping rewrite*)
    1.27 +fun looptest sign prems lhs rhs =
    1.28 +   is_Var (head_of lhs)
    1.29 +  orelse
    1.30 +   (exists (apl (lhs,occs)) (rhs :: prems))
    1.31 +  orelse
    1.32 +   (null prems andalso
    1.33 +    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
    1.34 +(*the condition "null prems" in the last case is necessary because
    1.35 +  conditional rewrites with extra variables in the conditions may terminate
    1.36 +  although the rhs is an instance of the lhs. Example:
    1.37 +  ?m < ?n ==> f(?n) == f(?m)*)
    1.38 +
    1.39 +fun loops sign prems lhs rhs =
    1.40 +  let
    1.41 +    val elhs = Pattern.eta_contract lhs;
    1.42 +    val erhs = Pattern.eta_contract rhs;
    1.43 +    val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
    1.44 +               andalso not (is_Var elhs)
    1.45 +  in (if not ((term_vars erhs) subset
    1.46 +              (union_term (term_vars elhs, List.concat(map term_vars prems))))
    1.47 +      then Some("extra Var(s) on rhs") else
    1.48 +      if not perm andalso looptest sign prems elhs erhs
    1.49 +      then Some("loops")
    1.50 +      else None
    1.51 +      ,perm)
    1.52 +  end;
    1.53 +
    1.54  end;
     2.1 --- a/src/Pure/thm.ML	Thu Oct 16 13:43:42 1997 +0200
     2.2 +++ b/src/Pure/thm.ML	Thu Oct 16 13:45:16 1997 +0200
     2.3 @@ -1535,44 +1535,16 @@
     2.4  
     2.5  (* mk_rrule *)
     2.6  
     2.7 -fun vperm (Var _, Var _) = true
     2.8 -  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
     2.9 -  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
    2.10 -  | vperm (t, u) = (t = u);
    2.11 -
    2.12 -fun var_perm (t, u) =
    2.13 -  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
    2.14 -
    2.15 -(*simple test for looping rewrite*)
    2.16 -fun loops sign prems (lhs, rhs) =
    2.17 -   is_Var (head_of lhs)
    2.18 -  orelse
    2.19 -   (exists (apl (lhs, Logic.occs)) (rhs :: prems))
    2.20 -  orelse
    2.21 -   (null prems andalso
    2.22 -    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
    2.23 -(*the condition "null prems" in the last case is necessary because
    2.24 -  conditional rewrites with extra variables in the conditions may terminate
    2.25 -  although the rhs is an instance of the lhs. Example:
    2.26 -  ?m < ?n ==> f(?n) == f(?m)*)
    2.27 -
    2.28  fun mk_rrule (thm as Thm {sign, prop, ...}) =
    2.29    let
    2.30      val prems = Logic.strip_imp_prems prop;
    2.31      val concl = Logic.strip_imp_concl prop;
    2.32 -    val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
    2.33 +    val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
    2.34        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
    2.35 -    val econcl = Pattern.eta_contract concl;
    2.36 -    val (elhs, erhs) = Logic.dest_equals econcl;
    2.37 -    val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
    2.38 -      andalso not (is_Var elhs);
    2.39 -  in
    2.40 -    if not ((term_vars erhs) subset
    2.41 -        (union_term (term_vars elhs, List.concat(map term_vars prems)))) then
    2.42 -      (prtm_warning "extra Var(s) on rhs" sign prop; None)
    2.43 -    else if not perm andalso loops sign prems (elhs, erhs) then
    2.44 -      (prtm_warning "ignoring looping rewrite rule" sign prop; None)
    2.45 -    else Some {thm = thm, lhs = lhs, perm = perm}
    2.46 +  in case Logic.loops sign prems lhs rhs of
    2.47 +     (None,perm) => Some {thm = thm, lhs = lhs, perm = perm}
    2.48 +   | (Some msg,_) =>
    2.49 +        (prtm_warning("ignoring rewrite rule ("^msg^")") sign prop; None)
    2.50    end;
    2.51  
    2.52