[isabelle] Problem with "additional type variables" in a definition



Hi,

I'm having a problem with Isabelle 2016 which I've minimised to the following file. There seems to be something particular in how Isabelle handles types appearing in a definition but not in any arguments to the thing being defined.

  theory Test
  imports
    HOL
  begin

  definition foo :: "bool" ("f" 50) where
    "foo â âx :: 'a. True"

  abbreviation bar :: "bool" where
    "bar â foo"

  lemma "foo"
    sorry
  end
  
The definition gives the output

  consts
    foo :: "bool" 
   Additional type variable(s) in specification of "foo": 'a
   Dropping mixfix syntax ("foo" [] 50)

The abbreviation and lemma both give the output

   Type unification failed: Clash of types "_ â _" and "bool"

   Type error in application: incompatible operand type

   Operator:  op â bar :: bool â prop
   Operand:   foo :: ??'a itself â bool


Why is the mixfix syntax dropped?
Why has foo -- which was defined to be a constant and this was confirmed by the output -- become a function?

Is there a way to get the mixfix syntax and abbreviation to work?

Thanks,

Lars-Henrik Eriksson, PhD, Senior Lecturer
Computing Science, Dept. of Information Technology, Uppsala University, Sweden





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