Theory RG_Syntax_Extensions
section ‹Rely-Guarantee Syntax Extensions›
text ‹This theory contains the improved syntax of rely-guarantee sentences,
with support for quintuple-style, keyword-style, and data-invariants.
It also includes subgoal-generating methods that work with the structured
proof-language, Isar.›
theory RG_Syntax_Extensions
imports "HOL-Hoare_Parallel.RG_Syntax" "HOL-Eisbach.Eisbach"
begin
text ‹First, we enable the notation for forward function-composition, which is
used in the built-in @{text ‹Fun.thy›} but disabled at the end of that file.
We also augment the simp-set with some related definitions from the built-in library.›
notation fcomp (infixl "∘>" 60)
lemmas definitions [simp] =
stable_def Pre_def Rely_def Guar_def Post_def Com_def
text ‹Guarantee-relations often simply stipulates that a thread @{text i} should
``preserve the rely-relations of all other threads''. This pattern is supported
by the following syntactic sugar, where @{text j} ranges through all the threads
that are not @{text i}.›
abbreviation for_others :: "('index ⇒ 'state rel) ⇒ 'index ⇒ 'state rel" where
"for_others R i ≡ ⋂ j ∈ -{i}. R j"
text ‹Relies and guarantees often state that certain variables remain unchanged.
We support this pattern with the following syntactic sugars.›
abbreviation record_id :: "('record ⇒ 'field) ⇒ 'record rel"
("id'(_')" [75] 74) where
"id(c) ≡ ⦃ ªc = ºc ⦄"
abbreviation record_ids :: "('record ⇒ 'field) set ⇒ 'record rel"
("ids'(_')" [75] 74) where
"ids(cs) ≡ ⋂ c ∈ cs. id(c)"
abbreviation record_id_indexed ::
"('record ⇒ 'index ⇒ 'field) ⇒ 'index ⇒ 'record rel"
("id'( _ @ _ ')") where
"id(c @ self) ≡ ⦃ ºc self = ªc self ⦄"
abbreviation record_ids_indexed ::
"('record ⇒ 'index ⇒ 'field) set ⇒ 'index ⇒ 'record rel"
("ids'( _ @ _ ')") where
"ids(cs @ self) ≡ ⋂ c ∈ cs. id(c @ self)"
text ‹The following simple method performs an optional simplification-step, and
then tries to apply one of the RG rules, before attempting to discharge each
subgoal using @{text force}. This method works well on simple RG sentences.›
method method_rg_try_each =
(clarsimp | simp)?,
( rule Basic | rule Seq | rule Cond | rule While
| rule Await | rule Conseq | rule Parallel);
force+
subsection ‹Lifting of Invariants›
text ‹To incorporate the invariant in a rely-guarantee sentence,
we need a way to combine the invariant, as a set,
with the rely and guarantee, which are relations.›
definition lift_guar :: "'a set ⇒ 'a rel ⇒ 'a rel" where
"lift_guar P R ≡ Id ∪ Restr R P"
definition lift_rely :: "'a set ⇒ 'a rel ⇒ 'a rel" where
"lift_rely P R ≡ R ∩ {(s,s'). s ∈ P ⟶ s' ∈ P }"
lemmas simp_defs [simp] = lift_guar_def lift_rely_def
text ‹Some properties of these two lifting functions:
Firstly, @{term lift_guar} is stronger than @{term lift_rely},
provided that the relation @{term R} contains the identity-relation.
Indeed, this assumption typically holds in RG reasoning when @{term R}
is a rely- or guarantee-relation.›
lemma lift_guar_stronger_than_lift_rely:
"Id ⊆ R ⟹ lift_guar I R ⊆ lift_rely I R"
by auto
text ‹Secondly, both @{term lift_guar} and @{term lift_rely} are `correct'
in the context of RG reasoning, as the invariant is stable under both.›
lemma stable_both_lift:
shows "stable I (lift_guar I R)"
and "stable I (lift_rely I R)"
by auto
subsection ‹RG Sentences›
text ‹The quintuple-style of RG sentences.›
abbreviation rg_quint ::
"'a set ⇒ 'a rel ⇒ 'a com ⇒ 'a rel ⇒ 'a set ⇒ bool"
("{_,_} _ {_,_}") where
"{P, R} C {G, Q} ≡ ⊢ C sat [P, R, G, Q]"
text ‹Quintuples with invariants.›
abbreviation rg_quintn_invar ::
"'a set ⇒ 'a rel ⇒ 'a com ⇒ 'a set ⇒ 'a rel ⇒ 'a set ⇒ bool"
("{_,_} _ ⫽ _ {_,_}") where
"{P, R} C ⫽ I {G, Q} ≡ ⊢ C sat [
P ∩ I,
lift_rely I R,
lift_guar I G,
Q ∩ I]"
text ‹The keyword-style of RG sentences.›
abbreviation rg_keyword ::
"'a rel ⇒ 'a rel ⇒ 'a set ⇒ 'a com ⇒ 'a set ⇒ bool"
("rely:_ guar:_ code: {_} _ {_}") where
"rg_keyword R G P C Q ≡ ⊢ C sat [P, R, G, Q]"
text ‹Keyword-style RG sentences with invariants.›
abbreviation rg_keyword_invar ::
"'a rel ⇒ 'a rel ⇒ 'a set ⇒ 'a set ⇒ 'a com ⇒ 'a set ⇒ bool"
("rely:_ guar:_ inv:_ code: {_} _ {_}") where
"rg_keyword_invar R G I P C Q ≡ ⊢ C sat [
P ∩ I,
lift_rely I R,
lift_guar I G,
Q ∩ I]"
subsection ‹RG Subgoal-Generating Methods›
text ‹As in Floyd-Hoare logic, in RG we can strengthen (make smaller) the
precondition and weaken (make larger) the postcondition without affecting the
validity of an RG sentence.›
theorem strengthen_pre:
assumes "P' ⊆ P"
and "⊢ c sat [P, R, G, Q]"
shows "⊢ c sat [P', R, G, Q]"
using assms Conseq by blast
theorem weaken_post:
assumes "Q ⊆ Q'"
and "⊢ c sat [P, R, G, Q ]"
shows "⊢ c sat [P, R, G, Q']"
using assms Conseq by blast
text ‹We then develop subgoal-generating methods for various instruction
types and patterns, to be used in conjunction with the Isar proof-language.›
subsubsection ‹Basic›
text ‹A @{text Basic} instruction wraps a state-transformation function.›
theorem rg_basic_named[intro]:
assumes stable_pre: "stable P R"
and stable_post: "stable Q R"
and guar_id: "∀s. s ∈ P ⟶ (s, s) ∈ G"
and establish_guar: "∀s. s ∈ P ⟶ (s, f s) ∈ G"
and establish_post: "P ⊆ ⦃ ´f ∈ Q ⦄"
shows "{P, R} Basic f {G, Q}"
apply (rule Basic)
using assms by auto
method method_basic =
rule rg_basic_named,
goal_cases stable_pre stable_post guar_id establish_guar establish_post
text ‹The \emph{skip} command is a @{text Basic} instruction whose function is
the identity.›
theorem rg_skip_named:
assumes stab_pre: "stable P R"
and stab_post: "stable Q R"
and guar_id: "Id ⊆ G"
and est_post: "P ⊆ Q"
shows "{P, R} SKIP {G, Q}"
using assms by force
method method_skip =
rule rg_skip_named,
goal_cases stab_pre stab_post guar_id est_post
text ‹An alternative version with an invariant subgoal.›
theorem rg_basic_inv[intro]:
assumes stab_pre: "stable (P ∩ I) (lift_rely I R)"
and stab_post: "stable (Q ∩ I) (lift_rely I R)"
and id_guar: "∀s. s ∈ P ∩ I ⟶ (s, s) ∈ G"
and est_inv: "∀s. s ∈ P ∩ I ⟶ f s ∈ I"
and est_post: "∀s. s ∈ P ∩ I ⟶ f s ∈ Q"
and est_guar: "∀s. s ∈ P ∩ I ⟶ (s, f s) ∈ G"
shows "⊢ (Basic f) sat [
P ∩ I,
lift_rely I R,
lift_guar I G,
Q ∩ I]"
proof method_basic
case stable_pre
then show ?case using stab_pre by blast
next
case stable_post
then show ?case using stab_post by blast
next
case guar_id
then show ?case using id_guar by simp
next
case establish_guar
then show ?case using est_inv est_guar by simp
next
case establish_post
then show ?case using est_post est_inv by blast
qed
method method_basic_inv = rule rg_basic_inv,
goal_cases stab_pre stab_post id_guar est_inv est_post est_guar
subsubsection ‹Looping constructs›
theorem rg_general_loop_named[intro]:
assumes stab_pre: "stable P R"
and stab_post: "stable Q R"
and guar_id: "Id ⊆ G"
and loop_exit: "P ∩ -b ⊆ Q"
and loop_body: "{P ∩ b, R} c {G, P}"
shows "{P, R} While b c {G, Q}"
apply (rule While)
using assms by force+
method method_loop =
rule rg_general_loop_named,
goal_cases stable_pre stable_post id_guar loop_exit loop_body
text ‹A similar version but with the @{text loop_body} subgoal having a
weakend precondition.›
theorem rg_general_loop_no_guard[intro]:
assumes stab_pre: "stable P R"
and stab_post: "stable Q R"
and guar_id: "Id ⊆ G"
and loop_exit: "P ∩ -b ⊆ Q"
and loop_body: "{P, R} c {G, P}"
shows "{P, R} While b c {G, Q}"
by (meson assms strengthen_pre Int_lower1 rg_general_loop_named)
method method_loop_no_guard =
rule rg_general_loop_no_guard,
goal_cases stab_pre stab_post guar_id loop_exit loop_body
text ‹A \emph{spinloop} is a loop with an empty body. Such a loop repeatedly
checks a property, and is a key construct in mutual exclusion algorithms.›
theorem rg_spinloop_named[intro]:
assumes stab_pre: "stable P R"
and stab_post: "stable Q R"
and guar_id: "Id ⊆ G"
and est_post: "P ∩ -b ⊆ Q"
shows "{P, R} While b SKIP {G, Q}"
apply (rule While)
using stab_pre apply blast
using est_post apply blast
using stab_post apply blast
apply (metis dual_order.refl guar_id inf_le1 rg_skip_named stab_pre strengthen_pre)
using guar_id by blast
method method_spinloop =
rule rg_spinloop_named,
goal_cases stable_pre stable_post guar_id est_post
theorem rg_infinite_loop:
assumes stab_pre: "stable P R"
and guar_id: "Id ⊆ G"
and loop_body: "{P, R} C {G, P}"
shows "{P, R} While UNIV C {G, Q}"
proof -
have "{P, R} While UNIV C {G, {}}"
apply (rule While)
using assms by force+
thus ?thesis
using weaken_post by fastforce
qed
method method_infinite_loop =
rule rg_infinite_loop,
goal_cases stable_pre guar_id loop_body,
clarsimp+
theorem rg_infinite_loop_syntax:
assumes stab_pre: "stable P R"
and guar_id: "Id ⊆ G"
and loop_body: "{P, R} C {G, P}"
shows "{P, R} WHILE True DO C OD {G, Q}"
using assms by (simp, rule rg_infinite_loop)
method method_infinite_loop_syntax =
rule rg_infinite_loop_syntax,
goal_cases stable_pre guar_id loop_body
text ‹A \emph{repeat-loop} encodes the pattern where the loop body is executed
before the first evaluation of the guard.›
theorem rg_repeat_loop[intro]:
assumes stab_pre: "stable P R"
and stab_post: "stable Q R"
and guar_id: "Id ⊆ G"
and loop_exit: "P ∩ b ⊆ Q"
and loop_body: "{P, R} C {G, P}"
shows "{P, R} C ;; While (-b) C {G, Q}"
apply (rule Seq[where ?mid = "P"])
using loop_body apply blast
apply (method_loop_no_guard)
using assms by auto
method method_repeat_loop =
rule rg_repeat_loop,
goal_cases stab_pre stab_post guar_id loop_exit loop_body
text ‹When reasoning about repeat-loops, we may need information from @{text P}
to determine whether we reach the postcondition. In this case we can use the
following form, which introduces a mid-state.›
theorem rg_repeat_loop_mid[intro]:
assumes stab_pre: "stable (P ∩ M) R"
and stab_post: "stable Q R"
and guar_id: "Id ⊆ G"
and loop_exit: "P ∩ M ∩ b ⊆ Q"
and loop_body: "{P, R} C {G, P ∩ M}"
shows "{P, R} C ;; While (-b) C {G, Q}"
apply (rule Seq[where ?mid = "P ∩ M"])
using loop_body apply blast
apply (method_loop_no_guard)
using stab_pre apply blast
using stab_post apply blast
using guar_id apply blast
using loop_exit apply blast
using loop_body strengthen_pre[of "P ∩ M" P] by blast
method method_repeat_loop_mid =
rule rg_repeat_loop_mid,
goal_cases stab_pre stab_post guar_id loop_exit loop_body
text ‹We define dedicated syntax for the repeat-loop pattern.›
definition Repeat :: "'a com ⇒ 'a bexp ⇒ 'a com" where
"Repeat c b ≡ c ;; While (-b) c"
syntax "_Repeat" :: "'a com ⇒ 'a bexp ⇒ 'a com" ("(0REPEAT _ /UNTIL _ /END)" [0, 0] 61)
translations "REPEAT c UNTIL b END" ⇀ "CONST Repeat c ⦃b⦄"
theorem rg_repeat_loop_def[intro]:
assumes stab_pre: "stable P R"
and stab_post: "stable Q R"
and guar_id: "Id ⊆ G"
and loop_exit: "P ∩ b ⊆ Q"
and loop_body: "{P, R} C {G, P}"
shows "{P, R} Repeat C b {G, Q}"
by (metis assms Repeat_def rg_repeat_loop)
method method_repeat_loop_def =
rule rg_repeat_loop_def,
goal_cases stab_pre stab_post guar_id loop_exit loop_body
subsubsection ‹Conditionals›
text ‹We first cover conditional-statements with or without the else-branch.›
theorem rg_cond_named[intro]:
assumes stab_pre: "stable P R"
and stab_post: "stable Q R"
and guar_id: "Id ⊆ G"
and then_br: "{P ∩ b, R} c1 {G, Q}"
and else_br: "{P ∩ -b, R} c2 {G, Q}"
shows "{P, R} Cond b c1 c2 {G, Q}"
apply (rule Cond)
using assms by auto
theorem rg_cond2_named[intro]:
assumes stab_pre: "stable P R"
and stab_post: "stable Q R"
and guar_id: "Id ⊆ G"
and then_br: "{P ∩ b, R} c1 {G, Q}"
and else_br: "P ∩ -b ⊆ Q"
shows "{P, R} Cond b c1 SKIP {G, Q}"
apply (rule rg_cond_named)
using stab_pre apply blast
using stab_post apply blast
using guar_id apply blast
using then_br apply blast
by (meson dual_order.eq_iff else_br guar_id rg_skip_named stab_post strengthen_pre)
method method_cond =
(rule rg_cond2_named | rule rg_cond_named),
goal_cases stab_pre stab_post guar_id then_br else_br
text ‹Variants without the stable-post subgoal.›
theorem rg_cond_no_post[intro]:
assumes stable_pre: "stable P R"
and guar_id: "Id ⊆ G"
and then_br: "{P ∩ b, R} c1 {G, Q}"
and else_br: "{P ∩ -b, R} c2 {G, Q}"
shows "{P, R} Cond b c1 c2 {G, Q}"
by (metis Cond IdI assms subsetD)
theorem rg_cond_no_guard_no_post[intro]:
assumes stable_pre: "stable P R"
and guar_id: "Id ⊆ G"
and then_br: "{P, R} c1 {G, Q}"
and else_br: "{P, R} c2 {G, Q}"
shows "{P, R} Cond b c1 c2 {G, Q}"
by (meson assms inf_sup_ord(1) rg_cond_no_post strengthen_pre)
method method_cond_no_post =
(rule rg_cond_no_post | rule rg_cond_no_guard_no_post),
goal_cases stab_pre guar_id then_br else_br
subsection ‹Parallel Compositions›
text ‹We now turn to the parallel composition, and cover several variants,
from the \emph{binary} parallel composition of two commands, to the
\emph{multi-parallel} composition of an indexed list of commands.
For each variant, we define the syntax and devise the subgoal-generating methods.›
subsubsection ‹Binary Parallel›
text ‹The syntax of binary parallel composition, without and with invariant.›
abbreviation binary_parallel ::
"'a set ⇒ 'a rel ⇒ 'a com ⇒ 'a com ⇒ 'a rel ⇒ 'a set ⇒ bool"
("{_, _} _ ∥ _ {_, _}") where
"{P, R} C1 ∥ C2 {G, Q} ≡
∃ P1 P2 R1 R2 G1 G2 Q1 Q2.
⊢ COBEGIN
(C1, P1, R1, G1, Q1)
∥
(C2, P2, R2, G2, Q2)
COEND SAT [P, R, G, Q]"
text ‹Some helper lemmas for later.›
lemma simp_all_2:
"(∀ i < Suc (Suc 0). P i) ⟷ P 0 ∧ P 1"
using less_Suc_eq by fastforce
lemma simp_gen_Un_2:
"(⋃ x ∈ ⦃´(<) (Suc (Suc 0)) ⦄. S x) = S 0 ∪ S 1"
using less_Suc_eq by auto
lemma simp_gen_Un_2_not0:
"(⋃ x ∈ ⦃´(<) (Suc (Suc 0)) ∧ ´(≠) (Suc 0) ⦄. S x) = S 0"
using less_Suc_eq by auto
lemma simp_gen_Int_2:
"(⋂ x ∈ ⦃´(<) (Suc (Suc 0)) ⦄. S x) = S 0 ∩ S 1"
using less_Suc_eq by auto
theorem rg_binary_parallel:
assumes "{P1, R1} (C1::'a com) {G1, Q1}"
and "{P2, R2} (C2::'a com) {G2, Q2}"
and "G1 ⊆ R2"
and "G2 ⊆ R1"
and "P ⊆ P1 ∩ P2"
and "R ⊆ R1 ∩ R2"
and "G1 ∪ G2 ⊆ G"
and "Q1 ∩ Q2 ⊆ Q"
shows "⊢ COBEGIN
(C1, P1, R1, G1, Q1)
∥
(C2, P2, R2, G2, Q2)
COEND SAT [P, R, G, Q]"
apply (rule Parallel)
apply (simp_all add: simp_all_2 simp_gen_Un_2 simp_gen_Int_2 simp_gen_Un_2_not0)
using assms by force+
theorem rg_binary_parallel_exists:
assumes "{P1, R1} (C1::'a com) {G1, Q1}"
and "{P2, R2} (C2::'a com) {G2, Q2}"
and "G1 ⊆ R2"
and "G2 ⊆ R1"
and "P ⊆ P1 ∩ P2"
and "R ⊆ R1 ∩ R2"
and "G1 ∪ G2 ⊆ G"
and "Q1 ∩ Q2 ⊆ Q"
shows "{P, R} C1 ∥ C2 {G, Q}"
by (meson rg_binary_parallel assms)
subsubsection ‹Multi-Parallel›
text ‹The syntax of multi-parallel, without and with invariants.›
syntax multi_parallel ::
"'a set ⇒ 'a rel ⇒ idt ⇒ nat ⇒
(nat ⇒ 'a set) ⇒ (nat ⇒ 'a rel) ⇒
(nat ⇒ 'a com) ⇒
(nat ⇒ 'a rel) ⇒ (nat ⇒ 'a set) ⇒
'a rel ⇒ 'a set ⇒ bool"
("global'_init: _ global'_rely: _ ∥ _ < _ @ {_,_} _ {_,_} global'_guar: _ global'_post: _")
translations
"global_init: Init global_rely: RR ∥ i < N @
{P,R} c {G,Q} global_guar: GG global_post: QQ"
⇀ "⊢ COBEGIN SCHEME [0 ≤ i < N] (c, P, R, G, Q) COEND
SAT [Init, RR , GG, QQ]"
syntax multi_parallel_inv ::
"'a set ⇒ 'a rel ⇒ idt ⇒ nat ⇒
(nat ⇒ 'a set) ⇒ (nat ⇒ 'a rel) ⇒
(nat ⇒ 'a com) ⇒ (nat ⇒ 'a set) ⇒
(nat ⇒ 'a rel) ⇒ (nat ⇒ 'a set) ⇒
'a rel ⇒ 'a set ⇒ bool"
("global'_init: _ global'_rely: _ ∥ _ < _ @ {_,_} _ ⫽ _ {_,_} global'_guar: _ global'_post: _")
translations
"global_init: Init global_rely: RR ∥ i < N @
{P, R} c ⫽ I {G, Q} global_guar: GG global_post: QQ"
⇀ "⊢ COBEGIN SCHEME [0 ≤ i < N] (c,
P ∩ I,
CONST lift_rely I R,
CONST lift_guar I G,
Q ∩ I
) COEND
SAT [Init, RR , GG, QQ]"
text ‹The subgoal-generating method for multi-parallel.›
theorem rg_multi_parallel_subgoals:
assumes assm_guar_rely: "∀ i j. i ≠ j ⟶ i<N ⟶ j<N ⟶ G j ⊆ R i"
and assm_pre: "∀ i<N. P' ⊆ P i"
and assm_rely: "∀ i<N. R' ⊆ R i"
and assm_guar: "∀ i<N. G i ⊆ G'"
and assm_post: "(⋂ i ∈ { i. i < N }. Q i) ⊆ Q'"
and assm_local: "∀ i<N. ⊢ C i sat [P i, R i, G i, Q i]"
shows "⊢ COBEGIN SCHEME [0 ≤ i < (N::nat)]
(C i, P i, R i, G i, Q i)
COEND SAT [P', R', G', Q']"
proof (rule Parallel, goal_cases)
case 1 show ?case using assm_rely assm_guar_rely by (simp add: SUP_le_iff)
case 2 show ?case using assm_guar by force
case 3 show ?case using assm_pre by force
case 4 show ?case using assm_post by force
case 5 show ?case using assm_local by force
qed
method method_multi_parallel = rule rg_multi_parallel_subgoals,
goal_cases guar_rely pre rely guar post body
theorem rg_multi_parallel_nobound_subgoals:
assumes assm_guar_rely: "∀ i j. i ≠ j ⟶ G j ⊆ R i"
and assm_pre: "∀ i. P' ⊆ P i"
and assm_rely: "∀ i. R' ⊆ R i"
and assm_guar: "∀ i. G i ⊆ G'"
and assm_post: "(⋂ i ∈ { i. i < N }. Q i) ⊆ Q'"
and assm_local: "∀ i. ⊢ C i sat [P i, R i, G i, Q i]"
shows "⊢ COBEGIN SCHEME [0 ≤ i < (N::nat)]
(C i, P i, R i, G i, Q i)
COEND SAT [P', R', G', Q']"
proof (rule Parallel, goal_cases)
case 1 show ?case using assm_rely assm_guar_rely by (simp add: SUP_le_iff)
case 2 show ?case using assm_guar by force
case 3 show ?case using assm_pre by force
case 4 show ?case using assm_post by force
case 5 show ?case using assm_local by force
qed
method method_multi_parallel_nobound =
rule rg_multi_parallel_nobound_subgoals,
goal_cases guar_rely pre rely guar post body
subsection ‹Syntax of Record-Updates›
text ‹This section contains syntactic sugars for updating a field of a record.
As we use records to model the states of a program, these record-update
operations correspond to the variable-assignments.
The type @{typ idt} denotes a field of a record. The first syntactic sugar
expresses a Basic command (of type @{typ[cartouche=true] ‹'a com›}) that
updates a record-field @{term x} that is a function; often @{term x} models
an array. After the update, the new value of @{term[cartouche=true] ‹x i›}
becomes @{term a}.›
syntax "_record_array_assign" ::
"idt ⇒ 'index ⇒ 'expr ⇒ 'state com" ("(´_[_] :=/ _)" [70, 65, 64] 61)
translations "´x[i] := a"
⇀ "CONST Basic «´(_update_name x (λ_. ´x(i:= a)))»"
text ‹The next two syntactic sugars express a state-transformation
function (rather than a command) that updates record-fields.
The first one simply updates an entire variable @{term x},
while the second updates an array @{term[cartouche=true] ‹x i›}.›
syntax "_record_update_field" ::
"idt ⇒ 'expr ⇒ ('a ⇒ 'a)" ("´_ ←/ _" [70] 61)
translations "´x ← a"
⇌ "«´(_update_name x (λ_. a))»"
syntax "_record_update_array" ::
"idt ⇒ 'expr ⇒ 'expr ⇒ ('a ⇒ 'a)" ("´_[_] ←/ _" [70, 71] 61)
translations "´x[i] ← a"
⇀ "«´(_update_name x (λ_. ´x(i:= a)))»"
text ‹Syntactic sugars for incrementing variables.›
syntax "_inc_fn" :: "idt ⇒ 'c ⇒ 'c" ("(´_.++)" 61)
translations "´x.++ " ⇀
" «´(_update_name x (λ_. ´x + 1))»"
syntax "_inc" :: "idt ⇒ 'c com" ("(´_++)" 61)
translations "´x++ " ⇀
"CONST Basic (´x.++)"
end