[isabelle-dev] NEWS: method facts

[Makarius]

On 09/06/16 10:48, Joachim Breitner wrote:
> 
> Am Mittwoch, den 08.06.2016, 19:46 +0200 schrieb Makarius:
>> There are further possibilities for "use", e.g. to eliminate
>> auxiliary
>> "-" or "insert" steps, notably:
>>
>>   qed (insert a, auto)  ~>  qed (use a in auto)
> 
> does this mean that the old idiom of
> 
>     lemma foo:
>       assumes "inductive_predicate x"
>       shows "something_about x"
>     using assms
>     proof(induction x)
>      ...
>     qed
> 
> can (and should) now become the slightly nicer
> 
>     lemma foo:
>       assumes "inductive_predicate x"
>       shows "something_about x"
>     p
>     roof(use assms in ‹induction x›)
>      ...
>     qed
> 
> or is the need for method nesting no better than the extra using assms?

"Old" has a special meaning in Isabelle jargon, and explicit 'from' or
'using' is definitely not old: it belongs to the first-class proof
language of Isar.

To understand the Isar language properly one always needs to keep in
mind that it is a 3-class society:

* first class: proof commands, e.g. 'from', 'using'
* second class: proof methods, e.g. "rule", "use"
* third class: attributes, e.g. "THEN", "OF"

It is often possible to move through the class hierarchy upwards or
downwards, without changing the reasoning. Good Isar style means a
certain balance of nice structure and good readability / maintainability.


The awkward goal transformation via "insert" above is turned into
structured method facts, so this is an upgrade within the proof method
language.

Turning 'using' into "use" is a downgrade of proof command into proof
method. This is occasionally useful, like e.g. using attribute
expressions instead of proof methods, but not something I would do all
the time.

First-class tickets on the Isar train are preferable.


	Makarius


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160609/96c3b436/attachment.sig>