Search code examples
isabelletheorem-provingformal-verificationisar

In Isabelle, what do the angle brackets and double asterisks mean?

I'm trying to understand some Isabelle code, and there is some syntax I don't understand. I haven't seen them in tutorials, including the two bundled with the Isabelle2017 distribution, "Programming and Proving in Isabelle/HOL" and "The Isabelle/Isar Reference Manual". The fact that they're symbols, combined with Isabelle's very small user base, means that the answer is pretty un-google-able.

The first is tall angle brackets ⟨ ⟩, and the second is a double asterisk ** which renders in the output console as ∧* (which is notably different than ASCII ^).

Here's an example;

lemma pre_fifth_pure [simp]:
  "triple net failures (a ** b ** c ** d ** ⟨ P ⟩) cod post =
   (P ⟶ triple net failures (a ** b ** c ** d) cod post)"

The angle brackets always seem to surround a proposition. The definition of the triple function implies that (a ** b ** c ** d) is of type state_element set ⇒ bool, where a state_element is just a conjunction of a bunch of constructors;

datatype state_element =
    StackHeightElm "nat"
  | StackElm "nat * w256" ... (* 20 lines like this *)

Are these two pieces of syntax related? How could (a ** b ** c ** d) be a function? Why can it have different numbers of the things delimited by the stars? Is this somehow custom defined syntax? The mysteries abound.

Solution

  • Isabelle comes with rich mechanisms to define own notation. Therefore, it is quite common to run into unfamiliar syntax when one inspects theories written by others.

    Using Isabelle/jEdit, you can press Ctrl (Cmd for Mac) and click on syntax and names to jump to their definition sites (cf. 3.5 of the Isabelle/jEdit Manual).

    There are sporadic instances where this might not work. Then, you can try typing print_syntax into your theory text, which will output all rules of the current inner syntax configuration (cf. 8.4.4 of Isabelle/Isar Reference Manual). Hopefully, you can at least figure out which theory some notation is from by this. One should assume that benevolent theory authors would refrain from grammar setups that break the hyperlink feature.

    For the specific problem here, ** is syntactic sugar for sep_conj in https://github.com/pirapira/eth-isabelle/blob/master/sep_algebra/Separation_Algebra.thy#L108 and ⟨ _ ⟩ is sugar for pure from https://github.com/pirapira/eth-isabelle/blob/master/Hoare/Hoare.thy#L257, as Alex found out.