# 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 \ 'b) \ 'a ref \ 'b \ ('a \ 'b)" - (\_/'((_ \ _)')\ [1000,0] 900) + (\(\open_block notation=\mixfix Hoare ref update\\_/'((_ \ _)'))\ [1000,0] 900) "_fassign" :: "'a ref => id => 'v => 's com" - (\(2_^._ :=/ _)\ [70,1000,65] 61) + (\(\indent=2 notation=\mixfix Hoare ref assignment\\_^._ :=/ _)\ [70,1000,65] 61) "_faccess" :: "'a ref => ('a ref \ 'v) => 'v" - (\_^._\ [65,1000] 65) + (\(\open_block notation=\infix Hoare ref access\\_^._)\ [65,1000] 65) translations "f(r \ v)" == "f(CONST addr r := v)" "p^.f := e" => "f := f(p \ 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 \ 'b) \ 'a ref \ 'b \ ('a \ 'b)" - (\_/'((_ \ _)')\ [1000,0] 900) + (\(\open_block notation=\mixfix Hoare ref update\\_/'((_ \ _)'))\ [1000,0] 900) "_fassign" :: "'a ref => id => 'v => 's com" - (\(2_^._ :=/ _)\ [70,1000,65] 61) + (\(\indent=2 notation=\mixfix Hoare ref assignment\\_^._ :=/ _)\ [70,1000,65] 61) "_faccess" :: "'a ref => ('a ref \ 'v) => 'v" - (\_^._\ [65,1000] 65) + (\(\open_block notation=\infix Hoare ref access\\_^._)\ [65,1000] 65) translations "_refupdate f r v" == "f(CONST addr r := v)" "p^.f := e" => "(p \ CONST Null) \ (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 @@ \ \Special syntax for guarded statements and guarded array updates:\ syntax - "_guarded_com" :: "bool \ 'a com \ 'a com" (\(2_ \/ _)\ 71) - "_array_update" :: "'a list \ nat \ 'a \ 'a com" (\(2_[_] :=/ _)\ [70, 65] 61) + "_guarded_com" :: "bool \ 'a com \ 'a com" + (\(\indent=2 notation=\mixfix Hoare guarded statement\\_ \/ _)\ 71) + "_array_update" :: "'a list \ nat \ 'a \ 'a com" + (\(\indent=2 notation=\mixfix Hoare array update\\_[_] :=/ _)\ [70, 65] 61) translations "P \ c" \ "IF P THEN c ELSE CONST Abort FI" "a[i] := v" \ "(i < CONST length a) \ (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 \ 'b \ 'com" (\(2_ :=/ _)\ [70, 65] 61) - "_Seq" :: "'com \ 'com \ 'com" (\(_;/ _)\ [61,60] 60) - "_Cond" :: "'bexp \ 'com \ 'com \ 'com" (\(IF _/ THEN _ / ELSE _/ FI)\ [0,0,0] 61) - "_While" :: "'bexp \ 'assn \ 'var \ 'com \ 'com" (\(WHILE _/ INV {(_)} / VAR {(_)} //DO _ /OD)\ [0,0,0,0] 61) + "_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: \<^item> \VAR {x = t}\ where \t::nat\ is the decreasing expression, @@ -23,21 +27,25 @@ \ syntax - "_While0" :: "'bexp \ 'assn \ 'com \ 'com" (\(1WHILE _/ INV {_} //DO _ /OD)\ [0,0,0] 61) - + "_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" (\VARS _// {_} // _ // {_}\ [0,0,55,0] 50) - "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \ bool" (\VARS _// [_] // _ // [_]\ [0,0,55,0] 50) + "_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" (\({_}//_//{_})\ [0,55,0] 50) - "_hoare_tc" :: "['assn, 'com, 'assn] \ bool" (\([_]//_//[_])\ [0,55,0] 50) + "_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\ +But the \x\ should only occur in invariants. To enforce this, syntax translations in \<^file>\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.)\ 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" - (\(2_^._ :=/ _)\ [70,1000,65] 61) + (\(\indent=2 notation=\mixfix Hoare field assignment\\_^._ :=/ _)\ [70,1000,65] 61) "_faccess" :: "'a::ref => ('a::ref \ 'v) => 'v" - (\_^._\ [65,1000] 65) + (\(\open_block notation=\mixfix Hoare field access\\_^._)\ [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 \ \Restriction of a relation\ - restr ::"('a \ 'a) set \ ('a \ bool) \ ('a \ 'a) set" (\(_/ | _)\ [50, 51] 50) + restr ::"('a \ 'a) set \ ('a \ bool) \ ('a \ 'a) set" + (\(\notation=\mixfix relation restriction\\_/ | _)\ [50, 51] 50) where "restr r m = {(x,y). (x,y) \ r \ \ m x}" text \Rewrite rules for the restriction of a relation\ 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" (\emp\) - "_singl" :: "nat \ nat \ bool" (\[_ \ _]\) - "_star" :: "bool \ bool \ bool" (infixl \**\ 60) - "_wand" :: "bool \ bool \ bool" (infixl \-*\ 60) + "_singl" :: "nat \ nat \ bool" (\(\open_block notation=\mixfix singl\\[_ \ _])\) + "_star" :: "bool \ bool \ bool" (infixl \**\ 60) + "_wand" :: "bool \ bool \ bool" (infixl \-*\ 60) + +syntax_consts + "_emp" \ is_empty and + "_singl" \ singl and + "_star" \ star and + "_wand" \ wand (* FIXME does not handle "_idtdummy" *) ML \