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
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?

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





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