Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Having trouble on Producing an inductive lemma...

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

From: TIMOTHY KREMANN <twksoa262@verizon.net>
inductive finite_stp :: "('a => bool) => 'a set => bool"
where
stp_emptyI [simp, intro!]: "finite_stp Pa {}" |
stp_insertI[simp, intro!]: "finite_stp Pa A /\ Pa a ==>
finite_stp Pa (insert a A)"

I want to prove:

lemma stp_finite_induct [case_names empty insert, induct set: finite_stp]:
"finite_stp Pa F /\ Pa x ==>
P {} ==> (!!x Pa F . finite_stp Pa F ==> x \<notin> F ==>
P F ==> P (insert x F))
==> P F"

Is this a true?

Thanks,
Tim

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

From: Tobias Nipkow <nipkow@in.tum.de>
I doubt that your lemma is true. The "Pa x" should be underneath the !!x.

Unless finite_stp is just a boiled down version of some larger def, I
would not define finite_stp at all but would write "finite F & (ALL x:F.
Pa x)" explicitly.

Tobias

TIMOTHY KREMANN schrieb:

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

From: Tjark Weber <webertj@in.tum.de>
"Pa x" is actually not needed at all. Here's an (unpolished) Isabelle
proof of the lemma (assuming "/\" meant "&"):

lemma stp_finite_induct:
"finite_stp Pa F & Pa x ==>
P {} ==> (!!x Pa F . finite_stp Pa F ==> x \<notin> F ==>
P F ==> P (insert x F))
==> P F"
apply (erule conjE)
apply (thin_tac "Pa x")
apply (erule finite_stp.induct)
apply assumption
apply (case_tac "a : A")
apply (subgoal_tac "insert a A = A")
apply auto
done

Regards,
Tjark

Last updated: May 03 2024 at 08:18 UTC