*To*: munddr at gmail.com*Subject*: Re: [isabelle] Auto and set ordering -- unpredictable?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 1 Feb 2011 16:42:01 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20cf3054a4d52d1179049b400114@google.com>*References*: <20cf3054a4d52d1179049b400114@google.com>*Sender*: huffman.brian.c at gmail.com

Hi John, I tried this example with "trace simplifier" enabled, and it reveals what the problem is. Here is the first part of the tracing output: [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM: ⟦f i1 = 1; f i2 = 2; Set = {i1, i2}⟧ ⟹ {i2} = {x ∈ {i1, i2}. f x = 2} [1]Adding rewrite rule "??.unknown": f i2 ≡ 2 [1]Adding rewrite rule "??.unknown": {i1, i2} ≡ Set Note the orientation of the rule in the last line. Usually, when you have an assumption of the form "lhs = rhs", the simplifier will add the rewrite rule "lhs == rhs" to the local simpset. But depending on some heuristic, the simplifier may decide to add the rewrite "rhs == lhs", or even "(lhs = rhs) == True" instead. I have seen this behavior before in situations where the rule "lhs == rhs" would obviously loop, so it only makes sense to use the opposite orientation. "(lhs = rhs) == True" is used when either orientation would obviously loop. Apparently the heuristic also reorients rules like "Set = {i1, i2}", where the lhs is a top-level constant. Usually this reorientation makes sense (for example, with the assumption "[] = xs", it is better to replace each occurrence of "xs" with "[]" than vice-versa) since for most top-level constants, there will be further applicable simp rules in the simpset. Note that the heuristic does not apply to locally-fixed variables. So the following proof works: lemma fixes f :: "nat => nat" and Set :: "nat set" and i1 :: nat and i2 :: nat assumes f1 : "f i1 = 1" and f2 : "f i2 = 2" and s1 : "Set = {i1, i2}" shows "{i2} = {x : {i1, i2}. f x = 2}" using f1 f2 s1 by auto I expect that if you changed your axiomatization to a locale, the reorientation would similarly go away. Also, if you use "simp add" instead of "using", the reorientation does not happen: lemma "{i2} = {x : {i1, i2}. f x = 2}" by (auto simp add: f1 f2 s1) - Brian On Tue, Feb 1, 2011 at 2:25 PM, <munddr at gmail.com> wrote: > Hi, > > I'm trying to prove a very simple lemma in the following simple example: > > axiomatization > f :: "nat => nat" and > Set :: "nat set" and > i1 :: nat and > i2 :: nat > where > f1 : "f i1 = 1" and > f2 : "f i2 = 2" and > s1 : "Set = {i1,i2}" > > lemma "{i2} = {x : {i2,i1}. fx = 2}" > using f1 f2 s1 > by auto > > It works and I know s1 is redundant here. Now, let's try: > > lemma "{i2} = {x : {i1,i2}. fx = 2}" > using f1 f2 s1 > by auto > > Auto doesn't work. However, if s1 was removed, it works. So how come using > the redundant fact "s1" requires the set to be ordered in a particular way? > It doesn't seem intuitive. > > Help will be appreciated! > > Thanks > John >

**References**:**[isabelle] Auto and set ordering -- unpredictable?***From:*munddr

- Previous by Date: [isabelle] Auto and set ordering -- unpredictable?
- Next by Date: Re: [isabelle] unicode tokens in isabelle2011+pg4.0
- Previous by Thread: [isabelle] Auto and set ordering -- unpredictable?
- Next by Thread: [isabelle] difference between "using" versus auto simp:
- Cl-isabelle-users February 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list