Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] simpsets

Email Gateway (Aug 18 2022 at 09:32):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
In Isabelle 2005,

simpset () addsimps [refl] ;

Ignoring duplicate rewrite rule:

?x1 = ?x1 == True

val it = ? : FullMetaSimplifier.simpset

Addsimps [refl] ;

Ignoring duplicate rewrite rule:

?x1 = ?x1 == True

val it = () : unit

but in a recent development snapshot

simpset () addsimps [refl] addsimps [refl] ;
val it = ? : MetaSimplifier.simpset
simpset () addsimps [refl] ;
val it = ? : MetaSimplifier.simpset
Addsimps [refl] ;

Ignoring duplicate rewrite rule:

?x1 = ?x1 == True

val it = () : unit

What's happening here? Does simpset () now return a different simpset
from the current default?
Should Simp_tac work the same as simp_tac (simpset ()) ?
(as I always understood it did, but I'd like to know whether it still
does, since I'm trying to debug a proof which doesn't seem to use the
simplification rules I'm expecting it to)

Thanks,

Jeremy

Email Gateway (Aug 18 2022 at 09:33):

From: Makarius <makarius@sketis.net>
On Wed, 16 Aug 2006, Jeremy Dawson wrote:

but in a recent development snapshot

simpset () addsimps [refl] addsimps [refl] ;
val it = ? : MetaSimplifier.simpset
simpset () addsimps [refl] ;
val it = ? : MetaSimplifier.simpset
Addsimps [refl] ;

Ignoring duplicate rewrite rule:

?x1 = ?x1 == True

val it = () : unit

What's happening here?

This is due to a recent change in producing the warning messages. A
simpset that is explicitly drawn from the context (simpset()) to be used
in actual simplification acts silently in this respect.

Does simpset () now return a different simpset from the current default?
Should Simp_tac work the same as simp_tac (simpset ()) ?

It should be still the same, but note that both simpset() and the capital
Simp_tacs are essentially legacy. Better pass through an explicit
Proof.context and use local_simpset_of.

Makarius

Last updated: May 03 2024 at 04:19 UTC