*To*: Ferdinand Vesely <csfvesely at swansea.ac.uk>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Type variables, locale import and notation*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 25 Apr 2016 08:35:05 +0200*In-reply-to*: <20160424005157.702ea201@arcana.Home>*References*: <20160424005157.702ea201@arcana.Home>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

Dear Ferdinand,

context s3 begin notation bar (infix "â" 50)

Best, Andreas On 24/04/16 01:51, Ferdinand Vesely wrote:

Dear List, I have a problem with using (infix) notation inside a locale in combination with type variables. In summary, I'm trying to introduce a binary abbreviation of a ternary predicate, where the type of the omitted parameter is a type variable (restricted by a sort). On the top-level, such a binary abbreviation is generalised to three parameters again by introducing a "type parameter" (e.g., "'a itself"). I've figured out that by using locales I can fix the (abstract) type locally and use the binary predicate inside the locale as I've intended. However, this does not play well when I also want to use infix notation for the abbreviation in a specialised locale (= import with instantiated parameter). Here is a contrived example of my problem. First the basic definitions:class a = fixes pred :: "'a â bool" locale s = fixes foo :: "'a â ('b :: a) â 'a â bool" begin definition bar :: "'a â 'a â bool" (infix "â" 50) where "x â y = (â(l :: 'b). foo x l y â pred l)" end class b = a + assumes b_pred: "âl. pred l" definition ex :: "nat â ('b :: b) â nat â bool" where "ex x l y = (y = x + 1 â pred l)"Now if I create a new locale where I only import locale s above, the types are as expected:locale s1 = s begin term bar (* "op â" :: "'a â 'a â bool" *) term "op â" (* "op â" :: "'a â 'a â bool" *) endBut if I want to specialise the locale with the above definition of 'ex, the type parameter is re-introduced even inside the locale and the infix notation does not work anymore (Isabelle does not warn about this). I'm not sure why the parameter is introduced inside the locale. Why is this the case? Shouldn't the types of the corresponding parameters of 'foo' and 'ex' be unified?locale s2 = s where foo = ex begin term bar (* "Îtype. spec.bar ex" :: "'a itself â nat â nat â bool", where "'a :: b" *) term "op â" (* Inner lexical error. Failed to parse term *) endAnyway, I've found out that if I add a new locale parameter with the same sort constraint on the type as in the type of 'ex', the additional "itself parameter" is not introduced. However, the infix notation still does not work.locale s3 = s where foo = "ex :: nat â ('b :: b) â nat â bool" + fixes t :: "('b :: b) itself" begin term bar (* "s.bar ex" :: "nat â nat â bool" *) term "op â" (* Inner lexical error. Failed to parse term *) lemma "1 â 2" (* Inner lexical error. Failed to parse term *) lemma "bar 1 2" (* OK *) by (simp add: bar_def ex_def b_pred) lemma "Âbar 2 1" (* OK *) by (simp add: bar_def ex_def) endWhy is the infix notation for bar silently dropped in locale s3? Is there any way around this, i.e., using the infix notation introduced in locale s? My other question is if there is a better way to introduce such an abbreviation without implicitly adding the extra "type parameter" and to keep the infix notation. Kind regards, Ferdinand

**References**:**[isabelle] Type variables, locale import and notation***From:*Ferdinand Vesely

- Previous by Date: [isabelle] ADG 2016 : deadline extended until May 2
- Next by Date: [isabelle] Going from Isabelle 2013 to Isabelle 2016
- Previous by Thread: [isabelle] Type variables, locale import and notation
- Next by Thread: [isabelle] ADG 2016 : deadline extended until May 2
- Cl-isabelle-users April 2016 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