[isabelle-dev] NEWS: method facts

Joachim Breitner breitner at kit.edu
Thu Jun 9 16:25:43 CEST 2016

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

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


Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
-------------- 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>

More information about the isabelle-dev mailing list