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

PVS Bug 748


Synopsis:        auto_rewrite declarations do not work (II)
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Mar 14 02:10:00 2003
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.0
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  even after the fix in 3.1 the auto rewrite declarations do not
  work (as I would expect). Consider the following theories:
  
      B : Theory
      Begin
        val : nat = 4
  
        AUTO_REWRITE- val
  
        lem1 : Lemma val = 4
  
      end B
  
      C : Theory
      Begin
        IMPORTING B
  
        AUTO_REWRITE+ val, lem1
  
        lem2 : Lemma val = 4
  
      end C
  
  After starting a proof for lem2 there is only one auto-rewrite:
  lem1.
  
  Switching the auto-rewrite status for definitions on and off
  would help a lot in proving TCCS in our current project. It would
  be nice to get a patch for this problem soon.
  
  Bye,
  
  Hendrik

How-To-Repeat: 

Fix: 
Made the obvious fix.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools