Re: [isabelle-dev] NEWS: method facts
On 09/06/16 16:25, Joachim Breitner wrote: > > 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. Such initial 'using' is sometimes indeed awkward, but there is in general nothing wrong with it. BTW, the official indendation is as follows, to emphasize that it belongs to the proof and not the statement, thus it is at least mentally folded away: lemma statement using facts (*indent +2*) by method (*indent =2*) lemma statement using facts (*indent +2*) proof (*indent -2*) ... qed An old-fashioned form to avoid used facts for induction works via Pure rule statements: lemma "x : ind_set ==> P x" proof (induct x set: ind_set) ... qed > 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" 'hence' and 'thus' are definitely obsolete: these left-over aliases from 1999, when separate 'then' did not exist. It would be better to remove 'hence' and 'thus', but it will inevitable provoke fierce complaints. Newer commands like 'obtain' (from 2000) or 'consider' (from 2015) do not have such a compound form. Such aliases tend to cause bad English and confusion: just compare Isar and Mizar in that respect, and try to explain the result to anybody out there. 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
Re: [isabelle-dev] NEWS: method facts
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 signature.asc Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: method facts
Hi, 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? Thanks, Joachim -- Dr. rer. nat. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner signature.asc Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
