Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 885


Synopsis:        some AUTO_REWRITE+ rules are not applied
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Sat Dec 18 05:25:00 2004
Originator:      Alfons Geser
Organization:    nianet.org
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  Hi Sam/Dave,
  
  Lemma t1 is proven by (skosimp*) (assert): the auto-rewrite rule
  inv_appl_L is applied during assert. Lemma t2 is similar, but PVS 3.2
  does not apply the rule inv_appl_R during assert. In contrast,
  (skosimp*) (rewrite "rule inv_appl_R") works. M-x show-auto-rewrites
  lists both rules.
  
  Kind Regards,
  Alfons
  
  no_auto[T: TYPE]: THEORY
  
  BEGIN
  
    x, y: VAR T
    iota: VAR (bijective?[T, T])
  
    inv(iota): (bijective?[T, T])
  
    inv_appl_L: AXIOM inv(iota)(iota(x)) = x
    inv_appl_R: AXIOM iota(inv(iota)(x)) = x
  
    AUTO_REWRITE+ inv_appl_L
    AUTO_REWRITE+ inv_appl_R
  
    % inv_appl_L is used for auto-rewriting as specified
    t1: LEMMA
      inv(iota)(iota(x)) = x
  
    % inv_appl_R is not used for auto-rewriting
    t2: LEMMA
      iota(inv(iota)(x)) = x
  
  END no_auto

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools