Re: [isabelle] \<^bsub> and \<^esub>





On 21/02/15 02:21, W. Douglas Maurer wrote:
The Isabelle/Isar reference manual (available from the documentation panel) explains the
general syntax of mixfix syntax annotations. They are normally enclosed in parenthesis
and go between the type declaration and the "where" clause of fun/definition/inductive,
etc. Alternatively, you can also use the command "notation" for functions that have
already been defined. Examples of \<^bsub> \<^esub> can be found in library in theory
Map.thy for the function restrict_map.

Thanks. I'm not sure that I will ever do this myself, but I am going to show my students
how to do it in case they would like to try it.
Meanwhile I'm putting together some proofs involving dvd and the even function, using
theory Parity. One of the lemmas in Parity is lemma even_iff_2_dvd [algebra]: even a <-->
2 dvd a by (simp add: even_def dvd_eq_mod_eq_0). So I substituted 38 for a, obtaining
"even((38::int)) <--> (2::int) dvd (38::int)". Then I used try0, and try0 said: Try this:
by auto (auto, presburger, force: 0 ms; simp: 1 ms; fastforce: 8 ms). But one of the
methods that try0 tried was algebra, and algebra is not on that list. So what does lemma
even_iff_2_dvd [algebra] mean, then? If it read [simp] instead of [algebra], that would
mean that this is a simprule, something that simp tries. So why doesn't [algebra] mean
that this is something that algebra tries? And does that apply to other rule names in
square brackets, like [presburger]? Thanks! -WDMaurer
The annotations in square brackets are called attributes and they have a variety of purposes. In the case of [algebra] and [presburger], they indeed indicate that these rules should be used by these proof methods. From what I know, these two methods reason abstractly, not for concrete numbers like 38. Moreover, I am not familiar with the internals of try or try0. If you want to see whether algebra can solve this, just write "by algebra" and see whether this works, too.

Andreas

--
Prof. W. Douglas Maurer       Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University Fax  (1-202)994-4875




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.