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
'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
[(("facts.baz", ["(?y::'a ??.Why3_Setup.g.foo) = (?x::'a ??.Why3_Setup.g.foo)", "(?x::'a ??.Why3_Setup.g.foo) = (?y::'a ??.Why3_Setup.g.foo)"]), )]
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: Dec 07 2023 at 16:21 UTC