Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] includes bundle works only in first case

Email Gateway (Aug 18 2022 at 19:58):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi all,

I stumbled across the following (unexpected) behaviour: If I do an Isar proof of
multiple goals I have refined the proof state by including a bundle prior to the
opening "proof", the "next" separator deletes the bundle.

Here's an example:

definition test :: "'a list => 'a list" where "test xs = []"
bundle test = test_def[simp]
lemma shows "test xs = []" and "test ys = []"
including test
proof -
show "test xs = []" by simp
next
show "test ys = []" by simp (* fails *)
qed

Surprisingly, it works if I nest the multiple goals inside a block:

proof -
{
show "test xs = []" by simp
next
show "test ys = []" by simp (* works *)
}
qed

Is this behaviour intended?

Andreas

Email Gateway (Aug 18 2022 at 19:58):

From: Makarius <makarius@sketis.net>
It follows naturally from the true meaning of Isar commands, also from the
principle of liberality in Isar design (cf. the concluding note on "abusus
non tollit usus" in my PhD thesis).

So yes, it is all within the normal parameters of Isar, despite the
potential surprise. The above example indicates that the new 'including'
command is better not used before a proof block. BTW, the longer existing
'using', with its later addition to affect the context, already produces
the same effect:

lemma "x = x" "y = y"
using [[show_types]]
proof
next
show "y = y" ..
qed

In some sense the above indentation provides a vague hint on the scoping
rules, although it is better not to stretch things that far.

Generally, the 'next' command switches blocks, here the implicit one of
the enclosing goal statement. So you don't delete declarations from the
context, you go back to an earlier context that does not have them.

In the example above you are using 'next' as if would "separate subgoals",
but this is not really its meaning. Plain 'show' statements do not have
to be separated. Separate blocks are only required for goals with their
own local context. In that case { ... show ... next ... show ... } works,
but is a bit awkward just to get a common context for what you are
proving.

Here is an alternative form that includes a bundle in the context of a
toplevel statement:

lemma
includes test
shows "test xs = []" and "test ys = []"
proof -
show "test xs = []" by simp
next -- "redundant"
show "test ys = []" by simp
qed

For local statements within a proof you can use 'include' with regular
block structure, if it is really required.

Makarius

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

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Makarius,

thanks for the explanation.

So yes, it is all within the normal parameters of Isar, despite the potential
surprise. The above example indicates that the new 'including' command is better
not used before a proof block. BTW, the longer existing 'using', with its later
addition to affect the context, already produces the same effect:

lemma "x = x" "y = y"
using [[show_types]]
proof
next
show "y = y" ..
qed
I have never tried this. So far, I only used "using <facts>" and "unfolding
<some_def>". The latter always worked on all goals and the former affected all
goals if used with the right initial method (-, simp_all, auto, etc.), so I
would have expected that something similar applies to including.

In the example above you are using 'next' as if would "separate subgoals", but
this is not really its meaning. Plain 'show' statements do not have to be
separated.
In my real use case, each goal had the full fix-assume-show chain, so the next
was necessary there.

Here is an alternative form that includes a bundle in the context of a toplevel
statement:

lemma
includes test
shows "test xs = []" and "test ys = []"
proof -
show "test xs = []" by simp
next -- "redundant"
show "test ys = []" by simp
qed
I read about that alternative, but I actually prefer "including" over
"includes", because including does not clutter the statement of the lemma with
hints to the prover.

Andreas

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

From: Makarius <makarius@sketis.net>
Yet another alternative keeps the context and the statement separate:

context includes test
begin

lemma shows ...

end

Makarius

Last updated: Nov 21 2024 at 12:39 UTC