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

On Tue, 29 May 2012, Andreas Lochbihler wrote:

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
 show "test ys = []" by simp (* fails *)

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

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

Is this behaviour intended?

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]]
  show "y = y" ..

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:

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

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.