Email Gateway (Aug 18 2022 at 11:03): Email Gateway (Aug 18 2022 at 11:03):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Email Gateway (Aug 18 2022 at 11:04):From: Stefan Berghofer <berghofe@in.tum.de>
Peter Lammich wrote:
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: [...]
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*)
Hi Peter,
in Isabelle 2007, inductive_set is just a wrapper for the inductive
command, which now defines predicates rather than sets of n-tuples.
This means that the introduction rules specified in an inductive_set
definition are translated to predicate notation internally. Then,
an inductive predicate is defined, and the resulting rules (introduction,
elimination, and induction) are translated back to set notation. In
order to translate a set of n-tuples to a predicate, its "arity" (i.e. the n)
has to be inferred, which is done by inspecting the introduction rules.
Unfortunately, due to the encoding of tuples in Isabelle/HOL, it is
sometimes difficult to find out whether the user wanted to define a
5-ary relation, or a 3-ary relation, whose first and third component is
a pair. In your example, Isabelle infers that the argument t of trcl has
arity 3, whereas the inferred arity for foo is 5. More precisely, the
introduction rules for the predicate trclp corresponding to the set trcl are
trclp t c [] c
[| t c a c'; trclp t c' w c'' |] ==> trclp t c (a # w) c''
and the introduction rule for the predicate foop corresponding to the
set foo is
foop s c a s c'
Due to this arity mismatch, the conversion back to set notation is only
done in an incomplete way, which leads to the abovementioned "strange"
rules.
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:
I'll try to add the required simplification rules to the conversion function
in the development snapshot.
Note that this problem would not have occurred if you had defined foo as follows:
inductive_set
foo :: "(('c'c)'a('c'c)) set"
where
"(sc,a,sc') : foo"
In this case, the arity inferred for foo is the same as the one inferred for
the argument of trcl.
Greetings,
Stefan
Last updated: May 03 2024 at 12:27 UTC