# HG changeset patch
# User wenzelm
# Date 1729262259 -7200
# Node ID 47a0dfee26eaadd565b98349aa1f83a8a53f22cd
# Parent  d9f087befd5c9ce7209d706661b2fe2b4fd61b61
more inner-syntax markup;

diff -r d9f087befd5c -r 47a0dfee26ea src/HOL/Hoare/HeapSyntax.thy
--- 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)"
diff -r d9f087befd5c -r 47a0dfee26ea src/HOL/Hoare/HeapSyntaxAbort.thy
--- 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)"
diff -r d9f087befd5c -r 47a0dfee26ea src/HOL/Hoare/Hoare_Logic_Abort.thy
--- 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)"
diff -r d9f087befd5c -r 47a0dfee26ea src/HOL/Hoare/Hoare_Syntax.thy
--- 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>
 
diff -r d9f087befd5c -r 47a0dfee26ea src/HOL/Hoare/Pointers0.thy
--- 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"
diff -r d9f087befd5c -r 47a0dfee26ea src/HOL/Hoare/SchorrWaite.thy
--- 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>
diff -r d9f087befd5c -r 47a0dfee26ea src/HOL/Hoare/Separation.thy
--- 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>