[isabelle-dev] NEWS: method facts

[Joachim Breitner]

Dear Markarius,

Am Donnerstag, den 09.06.2016, 15:58 +0200 schrieb Makarius:
> 
> [..] 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.

thanks for that view on things, and the stratificationof the lange
makes sense.

But while I like "using" inside an proof, it does not please my sense
of aesthetic to have such a command before the initial "proof" command.

Maybe a way out would be to take inspiration of how we can avoid some
explicit fact chaining inside proof..qed blocks, namely using "thus"
instead of "then show", and apply the usual logic of “appending s moves
a command from the local variant to the corresponding context
specification command”.

This would allow me to write (applying the usual rules of the English
grammer):

    lemma foo:
      assumes "inductive_predicate x"
      thuses "something_about x"
    proof(use assms in ‹induction x›)
     ...
    qed

SCNR,
Joachim

-- 
Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160609/afa1ee73/attachment.sig>