Email Gateway (Aug 22 2022 at 19:10): Email Gateway (Aug 22 2022 at 19:10):From: noam neer <noamneer@gmail.com>
hi everybody.
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]
[image: query_19_02_16b.png]
I'm attaching the text files just in case.
thanx in advance.
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=icon>
Virus-free.
www.avast.com
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=link>
<#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2>
query_19_02_16a.png
query_19_02_16b.png
query_19_02_16a.thy
query_19_02_16b.thy
Email Gateway (Aug 22 2022 at 19:10):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
I think you shouldn’t send screenshots and add the text files with the
source code “just in case”. Instead you should only send the source code
(perhaps as part of the e-mail text). It’s the source code that counts,
not its appearance on your screen. Having the source code allows others
to easily put it into the Isabelle IDE and experiment with them to
diagnose the source of your problems.
All the best,
Wolfgang
query_19_02_16a.png
query_19_02_16b.png
Email Gateway (Aug 22 2022 at 19:10):From: Dominique Unruh <unruh@ut.ee>
The error in the second example (involving ...) is due to the behaviour of
...
If you show a fact have "x=y" then ... will afterwards be short for y
as you expect.
You can check this using the command term "..."
However, in some cases, it is not possible to bind ... to the rhs of the
fact.
For example, if you show have "!!z. x = y" where y is a term containing
z, then it is not possible to have ... denote y because then ...
would contain an unbound variable.
Instead, ... is defined as %z. y, i.e., as a function such that ... z
is y. (Again, you can try term "..." and term "... z" to see.)
So if you continue your calculation, you have to write have "... z = w"
not have "... = w".
In your example, you seem to have a similar case.
Except that the "unbound variable" is a type variable.
(Although I am not sure why.)
This is why the type ??'a itself occurs in your typing error.
Namely, ... is now a function that takes an extra argument that indicates
what type it should be instantiated with.
Try using ... TYPE(t) instead of just ... where t is whatever type
you want plugged in.
(Or ... TYPE(_) probably also works to leave it to type inference.)
Again, try term "..." to understand how ... is defined.
Best wishes,
Dominique.
query_19_02_16a.png
query_19_02_16b.png
Email Gateway (Aug 22 2022 at 19:10):From: Makarius <makarius@sketis.net>
This is due to a numeral 2::'a -- numerals are polymorphic by default,
and sometimes the inferred types can be confusing.
Included is my version of both of your examples: the first problem was
an improperly oriented rewrite rule -- the "simp" method usually wants
an actual simplification from left to right.
A few more notes:
* A theory name should be always Capitalized.
* Meaning less fact names can be , , or 1, 2, 3, 4, ... --
there is no need to attach meaningless letters as in "L7".
* Too many redundant parentheses obscure the term structure; the
output uses minimal parentheses, this helps to figure out what is
required an what not.
* The auto-indentation of the Isabelle Prover IDE helps to get the
source structure right.
Makarius
Query_19_02_16.thy
Email Gateway (Aug 22 2022 at 19:11):From: noam neer <noamneer@gmail.com>
thank u very much.
is there a way to tell Isabelle that in a certain region of the code all
numerals will be real (or some other specific type)?
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=icon>
Virus-free.
www.avast.com
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=link>
<#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2>
Email Gateway (Aug 22 2022 at 19:11):From: Makarius <makarius@sketis.net>
No.
Numerals are like polymorphic constants in type-inference. You need to
provide sufficient syntactic context in the term to force it to be some
type, but sometimes this means to add a type-constraint.
Note that the Prover IDE allows to query the inferred type of
polymorphic constants via normal C-mouse-hover.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC