Make synchronous channels work for process families

src/Thorn_Calculus-Derived-Channels-Synchronous.thy

@@ -10,20 +10,16 @@ theory "Thorn_Calculus-Derived-Channels-Synchronous"
     "Thorn_Calculus-Processes"
 begin
 
+consts
+  sync_send :: "'c \<Rightarrow> 'v \<Rightarrow> 'p \<Rightarrow> 'p" (\<open>(_ \<triangleleft>\<^bsub>s\<^esub> _;/ _)\<close> [53, 0, 52] 52)
+  sync_receive :: "'c \<Rightarrow> ('v \<Rightarrow> 'p) \<Rightarrow> 'p"
+
 typedef 'a sync_channel = "UNIV :: 'a channel channel set"
   morphisms sync_channel_to_nested_channel sync_channel_from_nested_channel ..
 
 instance sync_channel :: (type) embeddable
   by standard (meson sync_channel_to_nested_channel_inject ex_inj inj_def)
 
-lift_definition
-  sync_send :: "'a sync_channel \<Rightarrow> 'a::embeddable \<Rightarrow> process \<Rightarrow> process"
-  (\<open>(_ \<triangleleft>\<^bsub>s\<^esub> _;/ _)\<close> [53, 0, 52] 52)
-  is "\<lambda>A x p. A \<triangleright> (a :: 'a channel). (a \<triangleleft> x \<parallel> p)" .
-
-lift_definition sync_receive :: "'a sync_channel \<Rightarrow> ('a::embeddable \<Rightarrow> process) \<Rightarrow> process"
-  is "\<lambda>A P. \<nu> (a :: 'a channel). (A \<triangleleft> a \<parallel> a \<triangleright> x. P x)" .
-
 syntax
   "_sync_receive" :: "'a::embeddable sync_channel \<Rightarrow> pttrn \<Rightarrow> process \<Rightarrow> process"
   (\<open>(3_ \<triangleright>\<^bsub>s\<^esub> _./ _)\<close> [53, 0, 52] 52)
@@ -33,6 +29,32 @@ print_translation \<open>
   [preserve_binder_abs_receive_tr' @{const_syntax sync_receive} @{syntax_const "_sync_receive"}]
 \<close>
 
+overloading
+  plain_sync_send \<equiv> "sync_send :: chan \<Rightarrow> val \<Rightarrow> process \<Rightarrow> process"
+  plain_sync_receive \<equiv> "receive :: chan \<Rightarrow> (val \<Rightarrow> process) \<Rightarrow> process"
+begin
+
+lift_definition plain_sync_send :: "'a sync_channel \<Rightarrow> 'a \<Rightarrow> process \<Rightarrow> process"
+  is "\<lambda>A x p. A \<triangleright> (a :: 'a channel). (a \<triangleleft> x \<parallel> p)" .
+
+lift_definition plain_sync_receive :: "'a sync_channel \<Rightarrow> ('a \<Rightarrow> process) \<Rightarrow> process"
+  is "\<lambda>A P. \<nu> (a :: 'a channel). (A \<triangleleft> a \<parallel> a \<triangleright> x. P x)" .
+
+end
+
+overloading
+  sync_send_family \<equiv> "sync_send :: chan family \<Rightarrow> val family \<Rightarrow> process family \<Rightarrow> process family"
+  sync_receive_family \<equiv> "sync_receive :: chan family \<Rightarrow> (val \<Rightarrow> process family) \<Rightarrow> process family"
+begin
+
+definition sync_send_family :: "chan family \<Rightarrow> val family \<Rightarrow> process family \<Rightarrow> process family" where
+  [simp]: "sync_send_family A X P = (\<lambda>e. A e \<triangleleft>\<^bsub>s\<^esub> X e; P e)"
+
+definition sync_receive_family :: "chan family \<Rightarrow> (val \<Rightarrow> process family) \<Rightarrow> process family" where
+  [simp]: "sync_receive_family A \<P> = (\<lambda>e. A e \<triangleright>\<^bsub>s\<^esub> x. \<P> x e)"
+
+end
+
 typedef sync_chan = "UNIV :: chan set" morphisms sync_chan_to_chan sync_chan_from_chan ..
 
 instance sync_chan :: embeddable