Email Gateway (Aug 22 2022 at 10:36): Email Gateway (Aug 22 2022 at 10:36):From: Lars Noschinski <noschinl@in.tum.de>
A small hint: You may call the fixed variables as you like, so
fix P x assume "⋀ y . x = y ⟹ P" then show P by simp
is also allowed (and may look nicer).
Email Gateway (Aug 22 2022 at 10:37):From: Gergely Buday <gbuday@gmail.com>
nominal_function simple5 :: "lam ⇒ lam"
where
"simple5 x = x"
proof -
show "eqvt simple5_graph_aux" by (simp add: eqvt_def simple5_graph_aux_def)
next
fix x y assume "simple5_graph x y" show True by auto
next
fix P x assume "⋀ xa . x = xa ⟹ P" then show P by simp
next
fix x xa assume "x = xa"
from this show "x = xa" by assumption
qed
proves the lemma.
One thing is not clear: I get exclamation marks aside on the last two
assumption:
after
assume "⋀ xa . x = xa ⟹ P"
Introduced fixed type variable(s): 'a in "x__"
and after
assume "x = xa"
Introduced fixed type variable(s): 'a in "x__" or "xa__"
I guess I can ignore these for now but when could this be significant?
Email Gateway (Aug 22 2022 at 10:51):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
I have a Nominal Isabelle definition that ends up in four proof obligations. My question is more about Isar so write it to this general list.
nominal_function simple4 :: "lam ⇒ lam"
where
"simple4 x = x"
goal (4 subgoals):
apply (simp_all add: eqvt_def simple4_graph_aux_def)
would solve all the subgoals but how can I write an Isar proof that takes care of the subgoals individually?
I started an Isar proof but it is not clear how can I proceed:
theory Simple
imports "../../thy/Nominal2-Isabelle2015/Nominal/Ex/Lambda"
begin
nominal_function simple4 :: "lam ⇒ lam"
where
"simple4 x = x"
proof -
have "eqvt simple4_graph_aux" by (simp add: eqvt_def simple4_graph_aux_def)
Email Gateway (Aug 22 2022 at 10:52):From: Lars Noschinski <noschinl@in.tum.de>
On 13.07.2015 14:02, Buday Gergely wrote:
nominal_function simple4 :: "lam ⇒ lam"
where
"simple4 x = x"goal (4 subgoals):
1. eqvt simple4_graph_aux
2. ⋀x y. simple4_graph x y ⟹ True
3. ⋀P x. (⋀xa. x = xa ⟹ P) ⟹ P
4. ⋀x xa. x = xa ⟹ x = xaapply (simp_all add: eqvt_def simple4_graph_aux_def)
would solve all the subgoals but how can I write an Isar proof that takes care of the subgoals individually?
[...]
nominal_function simple4 :: "lam ⇒ lam"
where
"simple4 x = x"
proof -
have "eqvt simple4_graph_aux" by (simp add: eqvt_def simple4_graph_aux_def)
show "eqvt simple4_graph_aux" ...
next
fix x y assume "simple4_graph x y" show True ...
next
fix P y assume "!!x. y = x ==> P" show P ...
...
Email Gateway (Aug 22 2022 at 10:52):From: Buday Gergely <gbuday@karolyrobert.hu>
Lars Noschinski wrote:
I know this is trivial with automatic methods but I need to learn Isar.
I have a problem proving the third subgoal:
lemma "⋀ (P::bool) (x::lam). (⋀ xa. x = xa ⟹ P) ⟹ P"
proof -
fix P x assume "⋀ xa. x = xa ⟹ P" show P by auto
Isabelle tells me
show P∷bool
Successful attempt to solve goal by exported rule:
(⋀xa∷?'a∷type. (?x2∷?'a∷type) = xa ⟹ ?P2∷bool) ⟹ ?P2
proof (state): depth 0
this:
P∷bool
goal:
No subgoals!
Failed to apply initial proof method:
goal (1 subgoal):
Email Gateway (Aug 22 2022 at 10:52):From: Jason Dagit <dagitj@gmail.com>
How did you get isabelle to show you the types? I've been searching for a
way to get this information while using jEdit (without having to C-hover).
The problems I have with C-hover are:
* it's slow to popup
* if you need to see the types of multiple terms it's flaky (once it
disappears it can be hard to make it appear again)
* it's hard for me to hold down a control key while also positioning the
mouse just right. You can't position the mouse ahead of time because the
control has to be down when the mouse moves for the hover to begin.
* if you are trying to compare two complicated types for a small
difference it's frustrating that you can't see them on the screen at the
same time. I end up copying and pasting both types from the popup windows
into my buffer to look a them.
Email Gateway (Aug 22 2022 at 10:53):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Jason,
On 07/14/2015 07:30 PM, Jason Dagit wrote:
How did you get isabelle to show you the types? I've been searching for a
way to get this information while using jEdit (without having to C-hover).
you can use
declare [[show_types=true]]
in order to get a list of variables and their types as part of the output.
(Two equivalent forms would be
using [[show_types=true]]
and
from [[show_types=true]]
depending on the context.)
* if you are trying to compare two complicated types for a small
difference it's frustrating that you can't see them on the screen at the
same time. I end up copying and pasting both types from the popup windows
into my buffer to look a them.
Did you know that you can "detach" any popup you obtained via C-hover?
There is a tiny icon in the left-upper corner (right next to the X) for
doing so. This might be useful for comparing different terms.
cheers
chris
Email Gateway (Aug 22 2022 at 10:53):From: Jason Dagit <dagitj@gmail.com>
On Tue, Jul 14, 2015 at 10:48 AM, Christian Sternagel <c.sternagel@gmail.com
wrote:
Dear Jason,
On 07/14/2015 07:30 PM, Jason Dagit wrote:
How did you get isabelle to show you the types? I've been searching for a
way to get this information while using jEdit (without having to C-hover).
you can use
declare [[show_types=true]]
in order to get a list of variables and their types as part of the output.
(Two equivalent forms would be
using [[show_types=true]]
and
from [[show_types=true]]
depending on the context.)
Thanks! I didn't know I could do that. It looks like in the future I can
use print_options to get a listing of all the current options.
* if you are trying to compare two complicated types for a small
difference it's frustrating that you can't see them on the screen at the
same time. I end up copying and pasting both types from the popup windows
into my buffer to look a them.
Did you know that you can "detach" any popup you obtained via C-hover?
There is a tiny icon in the left-upper corner (right next to the X) for
doing so. This might be useful for comparing different terms.
Yeah that might help a little. It would help more if the detached window
had something connecting it to place it was detached from.
Thanks,
Jason
Email Gateway (Aug 22 2022 at 10:53):From: Lars Noschinski <noschinl@in.tum.de>
On 14.07.2015 11:19, Buday Gergely wrote:
I have a problem proving the third subgoal:
lemma "⋀ (P::bool) (x::lam). (⋀ xa. x = xa ⟹ P) ⟹ P"
proof -
fix P x assume "⋀ xa. x = xa ⟹ P" show P by autoIsabelle tells me
show P∷bool
Successful attempt to solve goal by exported rule:
(⋀xa∷?'a∷type. (?x2∷?'a∷type) = xa ⟹ ?P2∷bool) ⟹ ?P2
proof (state): depth 0this:
P∷bool
This tells you that the show statement can discharge one of the subgoals ...
goal:
No subgoals!
Failed to apply initial proof method:
goal (1 subgoal):
1. P
variables:
P :: bool
... but auto failed to solve it. Notice the suspicious lack of "!!xa. x
= xa" in the second part? That is because you did not feed the
assumption into the show statement (which you could do e.g. using "then").
-- Lars
Last updated: Apr 26 2024 at 01:06 UTC