[isabelle-dev] Referring to unfolded chained facts

Makarius makarius at sketis.net
Fri Sep 2 16:42:08 CEST 2011

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

```