*To*: "W. Douglas Maurer" <maurer at gwu.edu>*Subject*: Re: [isabelle] \<^bsub> and \<^esub>*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 23 Feb 2015 08:10:44 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <a0620075ad10d0f36ad42@[192.168.1.20]>*References*: <a06200751d10980831257@[192.168.1.20]> <54E431C4.4090708@inf.ethz.ch> <a06200755d10a772bc6da@[192.168.1.20]> <54E4CFE2.8020207@inf.ethz.ch> <a06200756d10aa5699d51@[192.168.1.20]> <54E58E70.2040501@inf.ethz.ch> <a06200757d10bc1679a18@[192.168.1.20]> <54E6182D.6080505@inf.ethz.ch> <a0620075ad10d0f36ad42@[192.168.1.20]>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

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

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

**References**:**Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)***From:*W. Douglas Maurer

**Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)***From:*Andreas Lochbihler

**Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)***From:*Andreas Lochbihler

**Re: [isabelle] \<^bsub> and \<^esub>***From:*Andreas Lochbihler

- Previous by Date: [isabelle] The Second Workshop on Inductive Theorem Proving 20-21 March 2015
- Next by Date: Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014
- Previous by Thread: Re: [isabelle] \<^bsub> and \<^esub>
- Next by Thread: Re: [isabelle] \<^bsub> and \<^esub>
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list