*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] (v2007) Strange lemmas generated by inductive_set package*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Mon, 26 Nov 2007 18:32:44 +0100*User-agent*: Thunderbird 1.5.0.9 (X11/20060911)

Hi all, I was porting some code from v2005 to v2007. I encountered just few problems, I'll describe one of them here, perhaps someone knows if this behaviour is intended: I have the following inductive set definitions: text {* Transitive reflexive closure of labelled transition system *} inductive_set trcl :: "('c*'a*'c) set \<Rightarrow> ('c*'a list*'c) set" for t where empty[simp]: "(c,[],c) \<in> trcl t" | cons[simp]: "\<lbrakk> (c,a,c') \<in> t; (c',w,c'') \<in> trcl t \<rbrakk> \<Longrightarrow> (c,a#w,c'') \<in> trcl t" inductive_set foo :: "(('c*'c)*'a*('c*'c)) set" where "((s,c),a,(s,c'))\<in>foo" consts P :: "'a \<Rightarrow> bool" inductive_set bar :: "('c*'a list list*'c) set" where "\<lbrakk>((s,c),a,(s',c'))\<in>trcl foo; (s,w,s')\<in>bar\<rbrakk> \<Longrightarrow> (c,a#w,c')\<in>bar" foo and bar are just some artifical definitions, the point seems to be, that the definition of bar contains trcl applied to an LTS over *pairs*, while trcl is defined over arbitrary states, not just pairs. The last definition of bar creates strange induction, intro and elim theorems: thm bar.intros (* \<lbrakk>((?s, ?c), ?a, ?s', ?c') \<in> trcl {((xa, x), xd, xc, xb). ((xa, x), xd, xc, xb) \<in> foo}; (?s, ?w, ?s') \<in> bar\<rbrakk> \<Longrightarrow> (?c, ?a # ?w, ?c') \<in> bar*) The expression "{((xa, x), xd, xc, xb). ((xa, x), xd, xc, xb) \<in> foo}" is obviously the same as just "foo", the simplifier knows that, too: thm bar.intros[simplified] (* \<lbrakk>((?s, ?c), ?a, ?s', ?c') \<in> trcl foo; (?s, ?w, ?s') \<in> bar\<rbrakk> \<Longrightarrow> (?c, ?a # ?w, ?c') \<in> bar *) I would have expected the latter version of the theorems being generated (as the old inductive package of v2005 did). My current workaround is to use the simplified attribute or some (simp)-steps where the altered definitions cause problems. My question is: Is this the intended behaviour ? If yes: Why? And can I get it to generate the simplified lemmas? regards and thanks in advance for any hints Peter -- Peter Lammich, Institut für Informatik Raum 715, Einsteinstrasse 62, 48149 Münster Mail: peter.lammich at uni-muenster.de Tel: 0251-83-32749 Mobil: 0163-5310380

**Follow-Ups**:**Re: [isabelle] (v2007) Strange lemmas generated by inductive_set package***From:*Stefan Berghofer

- Previous by Date: [isabelle] inductive_set even ...
- Next by Date: [isabelle] AFP 2007
- Previous by Thread: Re: [isabelle] inductive_set even ...
- Next by Thread: Re: [isabelle] (v2007) Strange lemmas generated by inductive_set package
- Cl-isabelle-users November 2007 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