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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev