Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Isabelle] some proof problems

Email Gateway (Aug 22 2022 at 19:10):

From: noam neer <noamneer@gmail.com>
hi everybody.
(I'm sending this mail again with '[Isabelle]' in the subject. sorry for
the mess.)

I have two problems I encountered while proving something.
I'm bringing them here in a very simplified form.
I'm working with Isabelle/jEdit 2018 on win10.

1) here there is external lemma which is not really important,
so I simplified it to "Y=Y".
inside the proof there is a lemma L7 whose proof is again not important,
so I used "sorry".
the problem comes in the "apply" statement where the cursor stands.
for some reason the simplifier can't apply L7, and I don't know why.
maybe you know?

[image: query_19_02_16a.png]

2. it seems I can solve the first problem by applying 'subst' and 'auto'
   instead of 'simp'.
   but when I'm trying to continue the equality, before even applying anything,
   I get some typing problem I don't understand. maybe you do.

[image: query_19_02_16b.png]

I'm attaching the text files just in case.
thanx in advance.
query_19_02_16b.png
query_19_02_16a.png
query_19_02_16b.thy
query_19_02_16a.thy

Email Gateway (Aug 22 2022 at 19:10):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
The string “[isabelle]” is automatically added by the mailing list
software, so it’s better not to add it yourself.
All the best,
Wolfgang
query_19_02_16a.png
query_19_02_16b.png

Last updated: Apr 26 2024 at 04:17 UTC