Stream: Isabelle/ML

Topic: Illegal fixed variable error

view this post on Zulip Ricardo Correia (Apr 23 2021 at 15:49):

I'm using Isabelle 2019 and I'm trying to debug an error in Why3's Isabelle/ML code but I'm having some difficulties understanding what's happening.

As far as I understand, the code is trying to add an axiom with multiple facts to the theory, something equivalent to this:

typedef foo

axiomatization baz_1: "(x::foo) = (y::foo)" and baz_2: "(y::foo) = (x::foo)"
lemmas baz = baz_1 baz_2

This is the code that is adding the facts to the theory:

fun add_axioms s [t] =
      Specification.axiom ((fact_binding s, []), t) #> snd
  | add_axioms s ts =
      fold_map Specification.axiom
        (map_index (fn (i, t) =>
           ((fact_binding (s ^ "_" ^ string_of_int (i + 1)), []), t)) ts) #>
      apfst (pair (fact_binding s) #> rpair [] #> single) #>
      uncurry Global_Theory.add_thmss #> snd;

This seems to work fine in this situation, but if I replace foo with 'a foo, then Global_Theory.add_thmss fails with Illegal fixed variable: "'a". Unfortunately, I'm just a beginner Isabelle user so I don't know what this means.

I've traced the code to print the first argument to add_thmss and this is the result (with declare [[show_types]]):

[(("facts.baz", ["(?y::'a ?? = (?x::'a ??", "(?x::'a ?? = (?y::'a ??"]), [])]

Which is almost exactly what is passed as the first argument to add_thmss when foo doesn't have a type variable, except for the added 'a. So I'm really lost as to why add_thmss is failing when the axiom has a type variable.

Just to see what would happen, I've tried to call Global_Theory.note_thms instead of add_thmss but I run into the same error.

I think the error in add_thmss is coming from Logic.unvarify_global (which calls Logic.bad_fixed) but unfortunately I don't understand what the code is doing or even exactly what a fixed variable is in this context, or why it would be illegal.

Does anyone know how this can be fixed?

Last updated: Feb 27 2024 at 08:17 UTC