From ce22b5f906af5852187bd7065ee24ca3284e2f53 Mon Sep 17 00:00:00 2001
From: Simon Foster <simon.foster@york.ac.uk>
Date: Fri, 21 Jun 2024 10:41:36 +0100
Subject: [PATCH] Added dot notation for channel sets

---
 Channels_Events.thy | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/Channels_Events.thy b/Channels_Events.thy
index bf6941e..b97e90b 100644
--- a/Channels_Events.thy
+++ b/Channels_Events.thy
@@ -52,17 +52,23 @@ definition csempty ("\<lbrace>\<rbrace>") where [code_unfold]: "\<lbrace>\<rbrac
 nonterminal chan and chans
 
 syntax 
-  "_chan"          :: "id \<Rightarrow> chans" ("_")
-  "_chans"         :: "id \<Rightarrow> chans \<Rightarrow> chans" ("_,/ _")
+  "_chan_id"       :: "id \<Rightarrow> chan" ("_")
+  "_chan_inst"     :: "chan \<Rightarrow> id \<Rightarrow> chan" ("_\<cdot>_" [100,101] 101)
+  "_chan"          :: "chan \<Rightarrow> chans" ("_")
+  "_chans"         :: "chan \<Rightarrow> chans \<Rightarrow> chans" ("_,/ _")
   "_ch_enum"       :: "chans \<Rightarrow> logic" ("\<lbrace>_\<rbrace>")
   "_ch_collect"    :: "id \<Rightarrow> pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("\<lbrace>_/ _ \<in> _./ _\<rbrace>")
   "_ch_collect_ns" :: "id \<Rightarrow> pttrn \<Rightarrow> logic \<Rightarrow> logic" ("\<lbrace>_/ _./ _\<rbrace>")
 
-translations 
+translations
+  "_chan_id c" => "c"
+  "_chan_inst c x" => "CONST chinst c x" 
   "_chan c" => "CONST csbasic c"
   "_chans e es" => "CONST csinsert e es"
   "_ch_enum A" => "A"
   "_ch_enum (_chan c)" <= "CONST csbasic c"
+  "_chan (_chan_inst c x)" <= "_chan (CONST chinst c x)"
+  "_chan_inst (_chan_inst c x) y" <= "_chan_inst (CONST chinst c x) y"
   "_ch_enum (_chans c cs)" <= "CONST csinsert c (_ch_enum cs)"
   "_ch_collect e x A P" == "CONST cscollect e A (\<lambda> x. P)"
   "_ch_collect_ns e x P" == "_ch_collect e x (CONST UNIV) P"
@@ -108,5 +114,4 @@ translations
   "_rncollect (_evt_id c\<^sub>1) (_evt_id c\<^sub>2) x A P" == "CONST rncollect c\<^sub>1 c\<^sub>2 A (\<lambda> x. (((), ()), P))"
   "_rncollect_ns e\<^sub>1 e\<^sub>2 x P" == "_rncollect e\<^sub>1 e\<^sub>2 x (CONST UNIV) P"
 
-
 end
\ No newline at end of file