[isabelle-dev] Referring to unfolded chained facts

[Makarius]

On Thu, 1 Sep 2011, Alexander Krauss wrote:

>> Here's an example. After "unfolding null_def", the user invoked 
>> Sledgehammer and asked for an Isar proof. The "proof - ... qed" block after 
>> that is generated by Sledgehammer:
>>
>>      lemma "null xs ==>  tl xs = xs"
>>      proof -
>>        assume nx: "null xs"
>>        show "tl xs = xs"
>>        using `null xs`
>>        unfolding null_def
>>        proof -
>>          have "tl xs = []" by (metis `xs = []` tl.simps(1))
>>          thus "tl xs = xs" by (metis `xs = []`)
>>        qed
>
> What about just generating
>
>  assume "xs = []"
>
> after "proof -" to properly introduce the unfolded proposition in the 
> text. If you give it a name, it'll also be less verbose than the current 
> version, since you don't have to repeat the proposition...

This is at least a partial solution: it works as long as the facts are 
non-schematic.  (The "-" method inserts them as goal prems, so the assume 
in the body is justified.)


There is in fact an old omission in Isar concerning compositionality of 
proofs involving chained facts.  Consider this prototype:

   <facts> then have A by method

Here the atomic proof cannot be refined into a full text without 
reconsidering the syntactic construction of <facts> again.  Some derived 
elements like 'obtain' avoid this problem by using the actual facts value 
in ML, bypassing the Isar syntax structure.  This cannot be done with 
generated sources, though.

I have some potential solutions in the drawer for a long time already, but 
so far there was never the critical mass to make it into the 
implementation.  Here is one speculative way using cases produced by the 
regular goal structure (or the "-" method).  E.g. consider this refinement 
of the above text:

   <facts> then have A
   proof -
     case facts
     ...
     show ?thesis using facts by method
   qed

Here "facts" is the litaral name of that case. (Some technical limitation 
of cases need to be overcome here first, because there cannot be 'note' 
elements right now.)


I have also thought again about 'unfolding' as such: it might actually 
qualify as preserving textual structure and thus as something that can be 
included in the textual scope for `...` -- assuming it will someday really 
cease to perform arbitrary simplification by accident.


There may well be other ways -- it needs some digging on my universal TODO 
list.

We should develop some feeling in which direction to move for the source 
generation business.  Anyway, is this mission critical for the upcoming 
release?


 	Makarius