[isabelle-dev] NEWS: method facts
breitner at kit.edu
Thu Jun 9 16:25:43 CEST 2016
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
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
This would allow me to write (applying the usual rules of the English
assumes "inductive_predicate x"
thuses "something_about x"
proof(use assms in ‹induction x›)
Dr. rer. nat. Joachim Breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: This is a digitally signed message part
More information about the isabelle-dev