Search code examples
isabelle

What do double brackets mean in Isabelle?

What do the double brackets (and semicolon) stand for and how can I type them in jEdit?

lemma "[[ xs @ zs = ys @ xs; [] @ xs = [] @ [] ]] ==> ys = zs"
apply simp
done

Pasting this to jedit directly yields

Inner syntax error⌂
Failed to parse prop

but I see this being used Tutorial on Isabelle/HOL in https://isabelle.in.tum.de/dist/Isabelle2022/doc/tutorial.pdf section 3.1.5 Assumptions.

Solution

  • This is a shorthand notation for

    lemma "xs @ zs = ys @ xs ==> [] @ xs = [] @ [] ==> ys = zs"
apply simp
done

    in general

    [| P1; P2; ... ; Pn |] ==> C

    denotes

    P1 ==> P2 ==> ... ==> Pn ==> C

    This is explained in Programming and Proving in Isabelle/HOL https://isabelle.in.tum.de/dist/Isabelle2022/doc/prog-prove.pdf at the end of section 2.1.1 Types, Terms and Formulas

    To display implications in this style in Isabelle/jEdit you need to set Plugins > Plugin Options > Isabelle/General > Print Mode to “brackets” and restart.