*To*: <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Type variables, locale import and notation*From*: Ferdinand Vesely <csfvesely at swansea.ac.uk>*Date*: Sun, 24 Apr 2016 00:51:57 +0100*Organization*: Swansea University

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" *) > end But 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 *) > end Anyway, 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) > end Why 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 -- Ferdinand Vesely PhD Candidate Department of Computer Science, Swansea University http://cs.swan.ac.uk/~csfvesely/

**Follow-Ups**:**Re: [isabelle] Type variables, locale import and notation***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Last CfP "Justifying (in) Math" at CADGME 2016
- Next by Date: [isabelle] ADG 2016 : deadline extended until May 2
- Previous by Thread: [isabelle] Last CfP "Justifying (in) Math" at CADGME 2016
- Next by Thread: Re: [isabelle] Type variables, locale import and notation
- 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