Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A Problem with Inductive Sets

Email Gateway (Aug 18 2022 at 12:13):

From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi

I have an inductive set, and I want to assert properties of members of
this set. However, I am having trouble proving a seemingly trivial
thing. In essence, my problem is as follows

inductive_set A :: "('a list * bool) set"
where I[intro]: "([], P i ) : A"

where i is some natural number, and P a (predefined) function from 'a
to bool.

Now, if I try to prove the following

lemma test
assumes "S : A"
shows "\<exists> i. S = ([], P i)"

I reach an impasse:

proof-
from assms and A.I[where i=i] show ?thesis
apply (rule_tac x=i in exI)

gives me the state

[| S : A ; ([], P i) : A |] ==> S = ( [] , P i )

but this does not fall to any of the usual methods. Since I is the
only formation rule, I would have thought the lemma would be easy to
prove. Usually I would just use "by (cases) (auto)" but in this case
it did not work.

Can any one see what I am doing wrong? Am I trying to prove something
that is false, or is it a simple thing which I am doing incorrectly?

Many thanks

Peter

Email Gateway (Aug 18 2022 at 12:13):

From: Makarius <makarius@sketis.net>
On Fri, 18 Jul 2008, Peter Chapman wrote:

I have an inductive set, and I want to assert properties of members of this
set. However, I am having trouble proving a seemingly trivial thing. In
essence, my problem is as follows

inductive_set A :: "('a list * bool) set"
where I[intro]: "([], P i ) : A"

where i is some natural number, and P a (predefined) function from 'a to bool.

Now, if I try to prove the following

lemma test
assumes "S : A"
shows "\<exists> i. S = ([], P i)"

I reach an impasse:

proof-
from assms and A.I[where i=i] show ?thesis
apply (rule_tac x=i in exI)

gives me the state

[| S : A ; ([], P i) : A |] ==> S = ( [] , P i )

but this does not fall to any of the usual methods.

You first need to eliminate the "S : A" fact, before trying to introduce
the existential quantifier.

Since I is the only formation rule, I would have thought the lemma would
be easy to prove.

This argument is exactly elimination S by splitting over the cases
stemming from the inductive definition, cf. the rule S.cases.

Usually I would just use "by (cases) (auto)" but in this case it did not
work.

You need to present the membership judgment with an explicitly paired
argument.

Here is my version of your example, which explains every single step
without any automagic:

locale test =
fixes P :: "'a => bool"
begin

inductive_set A :: "('a list * bool) set"
where "([], P i) : A"

lemma
assumes "S : A"
shows "\<exists>i. S = ([], P i)"
proof -
obtain x y where "S = (x, y)" by (cases S)
with S : A have "(x, y) : A" by simp
then obtain i where "x = []" and "y = P i" by cases
with S = (x, y) have "S = ([], P i)" by simp
then show ?thesis ..
qed

end

Makarius

Last updated: May 03 2024 at 12:27 UTC