Ricardo Correia (Apr 23 2021 at 15:49): 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 ??.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: Apr 19 2024 at 08:19 UTC