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



24 maj 2016 kl. 12:09 skrev Thiemann, Rene <Rene.Thiemann at uibk.ac.at>:
> 
> Dear Lars-Henrik,
> 
> The problem is the implicit type âa in the definition of foo. To this end, Isabelle inserts a 
> dummy argument in the definition of foo of type (âa itself). So your definition becomes
> 
> definition foo' :: "'a itself â bool" where
>  "foo' _ â â x :: 'a. Trueâ
> 
> you also see this definition, if you perform a âprint_theoremsâ after your definition of âfooâ.
> 
> Hope this helps,
> RenÃ

Dear RenÃ,

Thank you. I suspected as much, but it doesn't really help me until I understand why and how this happens. It seems the extra argument to foo is not an ordinary argument but some kind of type argument. The definition does not become what you suggest but rather (using the command thm foo_def with show_types)

  foo TYPE(?'a) â âx::?'a. True

Even more confusing, when the definition is in a locale where the additional type is also used in the locale definition, as in:

  locale test =
    assumes "âx :: 'a. True"
  begin

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

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

    lemma "foo" unfolding foo_def by simp

    lemma "bar"
      sorry
  end

then both the abbreviation and the lemma "foo" work (although the mixfix syntax is still dropped), however the lemma "bar" gives the same type error that lemma "foo" did in my original example.

Is there some document that describes the behaviour of definitions in the presence of "additional" type variables? I find no explanation of it neither in the Isabelle/Isar Reference Manual, nor in the Tutorial on Locales. (I have specifically searched for "itself" and "TYPE".)

Lars-Henrik

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.