Re: [isabelle] Implicitly referring to previous facts in the moreover-ultimately paradigm
On 23/03/18 14:19, Peter Lammich wrote:
>> I don't see anything unnatural or unnecessary about it. On the
>> too much implicit fact management can make Isar proofs hard to read
>> hard to maintain, also hard to explain to casual readers who are not
>> familiar with the language.
> In my opinion, it is indeed a bit strange that the moreover-ultimately
> construction chains the implicit facts (so they are available for your
> last proof) but you cannot name them.
> ultimately have "D" by (blast intro: foo)
> which the more experienced Isabelle user might be tempted to write is
> not exactly clearer than
> using foo[OF ...] .
> So we have a construct that provides some nice implicit fact management
> for the complicated cases, but not for the simpler cases, where a
> simple forward proof does work.
We are talking about the final step of a calculational proof here, i.e.
'finally' or 'ultimately'. The proof following that can be more than
just 'by', but there is no systematic way to refer to the chained facts
in a complex proof here.
This is not a problem of the calculation, but of what can be done with
"proof method ... qed method". I've once had something like this in the
then show ?thesis sorry
I.e. the proof method "-" provides a case that "notes" the chained facts
for later use in the subproof. It did not emerge so far, because "notes"
cannot be part of proof method cases -- just by accident: it was not
required so far, and these things have some complexities internally.
Moreover, prospective applications for that have been too rare so far.
As a rule of thumb there need to be 2-3 good reasons to add more
features (read: complexity), not just half a reason. Alternatively, it
is possible to "trade" features: removing historic things that are not
really needed, and using the freed conceptual space to add new things.
This archive was generated by a fusion of
Pipermail (Mailman edition) and