--- a/src/HOL/Hoare/HeapSyntax.thy Fri Oct 18 16:31:35 2024 +0200
+++ b/src/HOL/Hoare/HeapSyntax.thy Fri Oct 18 16:37:39 2024 +0200
@@ -13,11 +13,11 @@
syntax
"_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
- (\<open>_/'((_ \<rightarrow> _)')\<close> [1000,0] 900)
+ (\<open>(\<open>open_block notation=\<open>mixfix Hoare ref update\<close>\<close>_/'((_ \<rightarrow> _)'))\<close> [1000,0] 900)
"_fassign" :: "'a ref => id => 'v => 's com"
- (\<open>(2_^._ :=/ _)\<close> [70,1000,65] 61)
+ (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare ref assignment\<close>\<close>_^._ :=/ _)\<close> [70,1000,65] 61)
"_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
- (\<open>_^._\<close> [65,1000] 65)
+ (\<open>(\<open>open_block notation=\<open>infix Hoare ref access\<close>\<close>_^._)\<close> [65,1000] 65)
translations
"f(r \<rightarrow> v)" == "f(CONST addr r := v)"
"p^.f := e" => "f := f(p \<rightarrow> e)"
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Fri Oct 18 16:31:35 2024 +0200
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Fri Oct 18 16:37:39 2024 +0200
@@ -21,11 +21,11 @@
syntax
"_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
- (\<open>_/'((_ \<rightarrow> _)')\<close> [1000,0] 900)
+ (\<open>(\<open>open_block notation=\<open>mixfix Hoare ref update\<close>\<close>_/'((_ \<rightarrow> _)'))\<close> [1000,0] 900)
"_fassign" :: "'a ref => id => 'v => 's com"
- (\<open>(2_^._ :=/ _)\<close> [70,1000,65] 61)
+ (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare ref assignment\<close>\<close>_^._ :=/ _)\<close> [70,1000,65] 61)
"_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
- (\<open>_^._\<close> [65,1000] 65)
+ (\<open>(\<open>open_block notation=\<open>infix Hoare ref access\<close>\<close>_^._)\<close> [65,1000] 65)
translations
"_refupdate f r v" == "f(CONST addr r := v)"
"p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Oct 18 16:31:35 2024 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Oct 18 16:37:39 2024 +0200
@@ -187,8 +187,10 @@
\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
syntax
- "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" (\<open>(2_ \<rightarrow>/ _)\<close> 71)
- "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" (\<open>(2_[_] :=/ _)\<close> [70, 65] 61)
+ "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"
+ (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare guarded statement\<close>\<close>_ \<rightarrow>/ _)\<close> 71)
+ "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"
+ (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare array update\<close>\<close>_[_] :=/ _)\<close> [70, 65] 61)
translations
"P \<rightarrow> c" \<rightleftharpoons> "IF P THEN c ELSE CONST Abort FI"
"a[i] := v" \<rightharpoonup> "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
--- a/src/HOL/Hoare/Hoare_Syntax.thy Fri Oct 18 16:31:35 2024 +0200
+++ b/src/HOL/Hoare/Hoare_Syntax.thy Fri Oct 18 16:37:39 2024 +0200
@@ -10,10 +10,14 @@
begin
syntax
- "_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com" (\<open>(2_ :=/ _)\<close> [70, 65] 61)
- "_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com" (\<open>(_;/ _)\<close> [61,60] 60)
- "_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com" (\<open>(IF _/ THEN _ / ELSE _/ FI)\<close> [0,0,0] 61)
- "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com" (\<open>(WHILE _/ INV {(_)} / VAR {(_)} //DO _ /OD)\<close> [0,0,0,0] 61)
+ "_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com"
+ (\<open>(\<open>indent notation=\<open>infix Hoare assignment\<close>\<close>_ :=/ _)\<close> [70, 65] 61)
+ "_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com"
+ (\<open>(\<open>notation=\<open>infix Hoare sequential composition\<close>\<close>_;/ _)\<close> [61, 60] 60)
+ "_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com"
+ (\<open>(\<open>notation=\<open>mixfix Hoare if expression\<close>\<close>IF _/ THEN _ / ELSE _/ FI)\<close> [0, 0, 0] 61)
+ "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com"
+ (\<open>(\<open>notation=\<open>mixfix Hoare while expression\<close>\<close>WHILE _/ INV {(_)} / VAR {(_)} //DO _ /OD)\<close> [0, 0, 0, 0] 61)
text \<open>The \<open>VAR {_}\<close> syntax supports two variants:
\<^item> \<open>VAR {x = t}\<close> where \<open>t::nat\<close> is the decreasing expression,
@@ -23,21 +27,25 @@
\<close>
syntax
- "_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com" (\<open>(1WHILE _/ INV {_} //DO _ /OD)\<close> [0,0,0] 61)
-
+ "_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix Hoare while expression\<close>\<close>WHILE _/ INV (\<open>open_block notation=\<open>mixfix Hoare invariant\<close>\<close>{_}) //DO _ /OD)\<close> [0, 0, 0] 61)
text \<open>The \<open>_While0\<close> syntax is translated into the \<open>_While\<close> syntax with the trivial variant 0.
This is ok because partial correctness proofs do not make use of the variant.\<close>
syntax
- "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool" (\<open>VARS _// {_} // _ // {_}\<close> [0,0,55,0] 50)
- "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool" (\<open>VARS _// [_] // _ // [_]\<close> [0,0,55,0] 50)
+ "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool"
+ (\<open>(\<open>open_block notation=\<open>mixfix Hoare triple\<close>\<close>VARS _// (\<open>open_block notation=\<open>mixfix Hoare precondition\<close>\<close>{_}) // _ // (\<open>open_block notation=\<open>mixfix Hoare postcondition\<close>\<close>{_}))\<close> [0, 0, 55, 0] 50)
+ "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool"
+ (\<open>(\<open>open_block notation=\<open>mixfix Hoare triple\<close>\<close>VARS _// (\<open>open_block notation=\<open>mixfix Hoare precondition\<close>\<close>[_]) // _ // (\<open>open_block notation=\<open>mixfix Hoare postcondition\<close>\<close>[_]))\<close> [0, 0, 55, 0] 50)
syntax (output)
- "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool" (\<open>({_}//_//{_})\<close> [0,55,0] 50)
- "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool" (\<open>([_]//_//[_])\<close> [0,55,0] 50)
+ "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool"
+ (\<open>(\<open>notation=\<open>mixfix Hoare triple\<close>\<close>(\<open>open_block notation=\<open>mixfix Hoare precondition\<close>\<close>{_})//_//(\<open>open_block notation=\<open>mixfix Hoare postcondition\<close>\<close>{_}))\<close> [0, 55, 0] 50)
+ "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool"
+ (\<open>(\<open>notation=\<open>mixfix Hoare triple\<close>\<close>(\<open>open_block notation=\<open>mixfix Hoare precondition\<close>\<close>[_])//_//(\<open>open_block notation=\<open>mixfix Hoare postcondition\<close>\<close>[_]))\<close> [0, 55, 0] 50)
text \<open>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 \<open>x\<close> in \<open>VAR {x = t}\<close>.
-But the \<open>x\<close> should only occur in invariants. To enforce this, syntax translations in \<open>hoare_syntax.ML\<close>
+But the \<open>x\<close> should only occur in invariants. To enforce this, syntax translations in \<^file>\<open>hoare_syntax.ML\<close>
separate the program from its annotations and only the latter are abstracted over over \<open>x\<close>.
(Thus \<open>x\<close> can also occur in inner variants, but that neither helps nor hurts.)\<close>
--- a/src/HOL/Hoare/Pointers0.thy Fri Oct 18 16:31:35 2024 +0200
+++ b/src/HOL/Hoare/Pointers0.thy Fri Oct 18 16:37:39 2024 +0200
@@ -24,9 +24,9 @@
syntax
"_fassign" :: "'a::ref => id => 'v => 's com"
- (\<open>(2_^._ :=/ _)\<close> [70,1000,65] 61)
+ (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare field assignment\<close>\<close>_^._ :=/ _)\<close> [70,1000,65] 61)
"_faccess" :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
- (\<open>_^._\<close> [65,1000] 65)
+ (\<open>(\<open>open_block notation=\<open>mixfix Hoare field access\<close>\<close>_^._)\<close> [65,1000] 65)
translations
"p^.f := e" => "f := CONST fun_upd f p e"
"p^.f" => "f p"
--- a/src/HOL/Hoare/SchorrWaite.thy Fri Oct 18 16:31:35 2024 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy Fri Oct 18 16:37:39 2024 +0200
@@ -85,7 +85,8 @@
definition
\<comment> \<open>Restriction of a relation\<close>
- restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set" (\<open>(_/ | _)\<close> [50, 51] 50)
+ restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set"
+ (\<open>(\<open>notation=\<open>mixfix relation restriction\<close>\<close>_/ | _)\<close> [50, 51] 50)
where "restr r m = {(x,y). (x,y) \<in> r \<and> \<not> m x}"
text \<open>Rewrite rules for the restriction of a relation\<close>
--- a/src/HOL/Hoare/Separation.thy Fri Oct 18 16:31:35 2024 +0200
+++ b/src/HOL/Hoare/Separation.thy Fri Oct 18 16:37:39 2024 +0200
@@ -52,9 +52,15 @@
syntax
"_emp" :: "bool" (\<open>emp\<close>)
- "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" (\<open>[_ \<mapsto> _]\<close>)
- "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>**\<close> 60)
- "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>-*\<close> 60)
+ "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" (\<open>(\<open>open_block notation=\<open>mixfix singl\<close>\<close>[_ \<mapsto> _])\<close>)
+ "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>**\<close> 60)
+ "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>-*\<close> 60)
+
+syntax_consts
+ "_emp" \<rightleftharpoons> is_empty and
+ "_singl" \<rightleftharpoons> singl and
+ "_star" \<rightleftharpoons> star and
+ "_wand" \<rightleftharpoons> wand
(* FIXME does not handle "_idtdummy" *)
ML \<open>