Mentions légales du service

Skip to content

Fix conjunctions in Isabelle (fix #491).

Guillaume Melquiond requested to merge fix-491 into master

(This patch was proposed by Ricardo M. Correia. It does not seem to be a complete fix for #491 (closed), but I am opening a pull request so that it does not get lost. Below is Ricardo's detailed explanation which came with the patch.)

I've looked at this a bit more and it seems that my initial analysis was wrong. The problem wasn't the incorrect syntax, because this incorrect syntax was only being shown to the user as part of the why3_status command, it wasn't actually being parsed by Isabelle as part of the theory.

It turns out that Why3 is actually defining the axioms using Isabelle/ML code and it was already doing something equivalent to the following for axioms that have a conjunction in their conclusion:

axiomatization baz_1: "x = y" and baz_2: "y = x"
lemmas baz = baz_1 baz_2

So, Why3 was already splitting the facts and adding an underscore and an index to the fact names.

In fact, the code that creates the axioms seems to be working absolutely fine. The error is in the part of the code that joins the indexed facts together under the same name (i.e. the code equivalent to the "lemmas" command).

This is the actual code which leads to the error:

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;

The axiom facts are defined by calling Isabelle's Specification.axiom function.

But the error comes from Isabelle's Global_Theory.add_thmss function, which is being called at the end and which seems to do the equivalent of the "lemmas" command.

I've tried looking into the add_thmss code but it's hard for me to understand all that's going on in there and I can't justify dedicating more time to this issue, unfortunately.

Last week I've posted to Isabelle's Zulip asking for help with this problem but I haven't gotten an answer so far.

Instead, to workaround the issue, I've simply removed the call to add_thmss, which means that the axioms are still defined but they aren't available together under a single name binding. Instead, we'd have to name the facts separately in proofs.

I'm attaching the patch which does this. It's not a complete fix but at least, it lets me continue doing my work.

Merge request reports