Theory HOL-Hoare.Hoare_Syntax

(*  Title:      HOL/Hoare/Hoare_Syntax.thy
    Author:     Leonor Prensa Nieto & Tobias Nipkow
    Author:     Walter Guttmann (extension to total-correctness proofs)
*)

section ‹Concrete syntax for Hoare logic, with translations for variables›

theory Hoare_Syntax
  imports Main
begin

syntax
  "_assign" :: "idt ⇒ 'b ⇒ 'com"
    (‹(‹indent notation=‹infix Hoare assignment››_ :=/ _)› [70, 65] 61)
  "_Seq" :: "'com ⇒ 'com ⇒ 'com"
    (‹(‹notation=‹infix Hoare sequential composition››_;/ _)› [61, 60] 60)
  "_Cond" :: "'bexp ⇒ 'com ⇒ 'com ⇒ 'com"
    (‹(‹notation=‹mixfix Hoare if expression››IF _/ THEN _ / ELSE _/ FI)› [0, 0, 0] 61)
  "_While" :: "'bexp ⇒ 'assn ⇒ 'var ⇒ 'com ⇒ 'com"
    (‹(‹notation=‹mixfix Hoare while expression››WHILE _/ INV {(_)} / VAR {(_)} //DO _ /OD)› [0, 0, 0, 0] 61)

text ‹The ‹VAR {_}› syntax supports two variants:
▪ ‹VAR {x = t}› where ‹t::nat› is the decreasing expression,
  the variant, and ‹x› a variable that can be referred to from inner annotations.
  The ‹x› can be necessary for nested loops, e.g. to prove that the inner loops do not mess with ‹t›.
▪ ‹VAR {t}› where the variable is omitted because it is not needed.
›

syntax
  "_While0" :: "'bexp ⇒ 'assn ⇒ 'com ⇒ 'com"
    (‹(‹indent=1 notation=‹mixfix Hoare while expression››WHILE _/ INV (‹open_block notation=‹mixfix Hoare invariant››{_}) //DO _ /OD)› [0, 0, 0] 61)
text ‹The ‹_While0› syntax is translated into the ‹_While› syntax with the trivial variant 0.
This is ok because partial correctness proofs do not make use of the variant.›

syntax
  "_hoare_vars" :: "[idts, 'assn,'com, 'assn] ⇒ bool"
    (‹(‹open_block notation=‹mixfix Hoare triple››VARS _// (‹open_block notation=‹mixfix Hoare precondition››{_}) // _ // (‹open_block notation=‹mixfix Hoare postcondition››{_}))› [0, 0, 55, 0] 50)
  "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] ⇒ bool"
    (‹(‹open_block notation=‹mixfix Hoare triple››VARS _// (‹open_block notation=‹mixfix Hoare precondition››[_]) // _ // (‹open_block notation=‹mixfix Hoare postcondition››[_]))› [0, 0, 55, 0] 50)
syntax (output)
  "_hoare" :: "['assn, 'com, 'assn] ⇒ bool"
    (‹(‹notation=‹mixfix Hoare triple››(‹open_block notation=‹mixfix Hoare precondition››{_})//_//(‹open_block notation=‹mixfix Hoare postcondition››{_}))› [0, 55, 0] 50)
  "_hoare_tc" :: "['assn, 'com, 'assn] ⇒ bool"
    (‹(‹notation=‹mixfix Hoare triple››(‹open_block notation=‹mixfix Hoare precondition››[_])//_//(‹open_block notation=‹mixfix Hoare postcondition››[_]))› [0, 55, 0] 50)

text ‹Completeness requires(?) the ability to refer to an outer variant in an inner invariant.
Thus we need to abstract over a variable equated with the variant, the ‹x› in ‹VAR {x = t}›.
But the ‹x› should only occur in invariants. To enforce this, syntax translations in 🗏‹hoare_syntax.ML›
separate the program from its annotations and only the latter are abstracted over over ‹x›.
(Thus ‹x› can also occur in inner variants, but that neither helps nor hurts.)›

datatype 'a anno =
  Abasic |
  Aseq "'a anno"  "'a anno" |
  Acond "'a anno" "'a anno" |
  Awhile "'a set" "'a ⇒ nat" "nat ⇒ 'a anno"

ML_file ‹hoare_syntax.ML›

end