Theory 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"  ("(2_ :=/ _)" [70, 65] 61)
  "_Seq" :: "'com ⇒ 'com ⇒ 'com"  ("(_;/ _)" [61,60] 60)
  "_Cond" :: "'bexp ⇒ 'com ⇒ 'com ⇒ 'com"  ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
  "_While" :: "'bexp ⇒ 'assn ⇒ 'var ⇒ 'com ⇒ 'com"  ("(1WHILE _/ 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"  ("(1WHILE _/ INV {_} //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"  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
 "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] ⇒ bool"  ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
syntax (output)
 "_hoare" :: "['assn, 'com, 'assn] ⇒ bool"  ("{_} // _ // {_}" [0,55,0] 50)
 "_hoare_tc" :: "['assn, 'com, 'assn] ⇒ bool"  ("[_] // _ // [_]" [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