Merge branch 'master' into enhancement/forwarding-broadcasting-equiva…

…lence

Isabelle/Chi_Calculus/Basic_Transition_System.thy

@@ -29,14 +29,17 @@ text \<open>
   variable.
 \<close>
 
-datatype 't basic_residual =
-  Acting \<open>basic_action\<close> \<open>'t\<close> ("\<lbrace>_\<rbrace> _" [0, 51] 51) |
-  Opening \<open>chan \<Rightarrow> 't\<close>
+datatype 'p basic_residual =
+  Acting \<open>basic_action\<close> \<open>'p\<close> ("\<lbrace>_\<rbrace> _" [0, 51] 51) |
+  Opening \<open>chan \<Rightarrow> 'p\<close>
 syntax
-  "_Opening" :: "pttrn \<Rightarrow> process \<Rightarrow> 't basic_residual"
+  "_Opening" :: "pttrn \<Rightarrow> process \<Rightarrow> 'p basic_residual"
   ("\<lbrace>\<nu> _\<rbrace> _" [0, 51] 51)
 translations
   "\<lbrace>\<nu> a\<rbrace> p" \<rightleftharpoons> "CONST Opening (\<lambda>a. p)"
+print_translation \<open>
+  [Syntax_Trans.preserve_binder_abs_tr' @{const_syntax Opening} @{syntax_const "_Opening"}]
+\<close>
 
 text \<open>
   We introduce the alias \<open>basic_lift\<close> for the automatically generated relator
@@ -46,7 +49,7 @@ text \<open>
 \<close>
 
 abbreviation
-  basic_lift :: "(['t, 't] \<Rightarrow> bool) \<Rightarrow> (['t basic_residual, 't basic_residual] \<Rightarrow> bool)"
+  basic_lift :: "(['p, 'q] \<Rightarrow> bool) \<Rightarrow> (['p basic_residual, 'q basic_residual] \<Rightarrow> bool)"
 where
   "basic_lift \<equiv> rel_basic_residual"
 

Isabelle/Chi_Calculus/Basic_Weak_Transition_System.thy

@@ -7,7 +7,7 @@ theory Basic_Weak_Transition_System
     Basic_Transition_System
 begin
 
-inductive basic_silent :: "[process, process basic_residual] \<Rightarrow> bool" where
+inductive basic_silent :: "['p, 'p basic_residual] \<Rightarrow> bool" where
   basic_internal_is_silent: "basic_silent p (\<lbrace>\<tau>\<rbrace> p)"
 
 interpretation basic: std_weak_residual basic_lift basic_silent
@@ -36,6 +36,7 @@ qed
 interpretation basic: weak_transition_system basic_silent basic.absorb basic_transition
   by intro_locales
 
+notation basic.weak_transition (infix "\<Rightarrow>\<^sub>\<flat>" 50)
 notation basic.weak.pre_bisimilarity (infix "\<lessapprox>\<^sub>\<flat>" 50)
 notation basic.weak.bisimilarity (infix "\<approx>\<^sub>\<flat>" 50)
 

Isabelle/Chi_Calculus/Communication.thy

@@ -13,6 +13,9 @@ syntax
   ("(3_ \<triangleright>\<^sup>\<infinity> _./ _)" [101, 0, 100] 100)
 translations
   "a \<triangleright>\<^sup>\<infinity> x. p" \<rightleftharpoons> "CONST multi_receive a (\<lambda>x. p)"
+print_translation \<open>
+  [preserve_binder_abs_receive_tr' @{const_syntax multi_receive} @{syntax_const "_multi_receive"}]
+\<close>
 
 (* FIXME:
   We should base the proofs of the compatibility laws on \<open>natural_transition_system\<close>, which would

Isabelle/Chi_Calculus/Core_Bisimilarities.thy

@@ -1085,9 +1085,16 @@ definition tagged_new_channel :: "[nat, chan \<Rightarrow> process] \<Rightarrow
 
 syntax
   "_tagged_new_channel" :: "[bool list, pttrn, process] \<Rightarrow> process"
-  ("(3\<langle>_\<rangle> \<nu>_./ _)" [0, 0, 100] 100)
+  ("(3\<langle>_\<rangle> \<nu> _./ _)" [0, 0, 100] 100)
 translations
   "\<langle>t\<rangle> \<nu> a. p" \<rightleftharpoons> "CONST tagged_new_channel t (\<lambda>a. p)"
+print_translation \<open>
+  [
+    preserve_binder_abs_receive_tr'
+      @{const_syntax tagged_new_channel}
+      @{syntax_const "_tagged_new_channel"}
+  ]
+\<close>
 
 context begin
 

Isabelle/Chi_Calculus/Processes.thy

@@ -4,6 +4,8 @@ theory Processes
   imports Channels
 begin
 
+ML_file \<open>binder_preservation.ML\<close>
+
 text \<open>
   The definition of the type of processes is fairly straightforward.
 \<close>
@@ -14,7 +16,7 @@ codatatype process =
   Send \<open>chan\<close> \<open>val\<close> (infix "\<triangleleft>" 100) |
   Receive \<open>chan\<close> \<open>val \<Rightarrow> process\<close> |
   Parallel \<open>process\<close> \<open>process\<close> (infixr "\<parallel>" 65) |
-  NewChannel \<open>chan \<Rightarrow> process\<close> (binder "\<nu>" 100)
+  NewChannel \<open>chan \<Rightarrow> process\<close> (binder "\<nu> " 100)
 
 text \<open>
   The notation for \<^const>\<open>Receive\<close> cannot be declared with @{theory_text \<open>binder\<close>}, for the
@@ -24,15 +26,18 @@ text \<open>
 
     \<^item> It has an extra parameter (for the channel) before the binder.
 
-  Therefore we introduce this notation using the low-level @{theory_text \<open>syntax\<close>} and
-  @{theory_text \<open>translations\<close>} constructs.
+  Therefore we introduce this notation using the low-level @{theory_text \<open>syntax\<close>},
+  @{theory_text \<open>translations\<close>}, and @{theory_text \<open>print_translation\<close>} constructs.
 \<close>
 
 syntax
   "_Receive" :: "chan \<Rightarrow> pttrn \<Rightarrow> process \<Rightarrow> process"
   ("(3_ \<triangleright> _./ _)" [101, 0, 100] 100)
 translations
   "a \<triangleright> x. p" \<rightleftharpoons> "CONST Receive a (\<lambda>x. p)"
+print_translation \<open>
+  [preserve_binder_abs_receive_tr' @{const_syntax Receive} @{syntax_const "_Receive"}]
+\<close>
 
 text \<open>
   We define guarding of processes at the host-language level.
@@ -60,6 +65,13 @@ syntax
   "_general_parallel" :: "pttrn => 'a list => process => process" ("(3\<Prod>_\<leftarrow>_. _)" [0, 0, 100] 100)
 translations
   "\<Prod>x\<leftarrow>xs. p" \<rightleftharpoons> "CONST general_parallel (\<lambda>x. p) xs"
+print_translation \<open>
+  [
+    preserve_binder_abs_general_parallel_tr'
+      @{const_syntax general_parallel}
+      @{syntax_const "_general_parallel"}
+  ]
+\<close>
 
 lemma general_parallel_conversion_deferral:
   shows "\<Prod>y\<leftarrow>map f xs. P y = \<Prod>x\<leftarrow>xs. P (f x)"

Isabelle/Chi_Calculus/Proper_Transition_System.thy

@@ -30,9 +30,9 @@ text \<open>
   transition. Its syntax is part of the syntax of output transitions.
 \<close>
 
-datatype 't output_rest =
-  WithoutOpening \<open>val\<close> \<open>'t\<close> ("_\<rparr> _" [52, 51] 51) |
-  WithOpening \<open>chan \<Rightarrow> 't output_rest\<close> (binder "\<nu>" 51)
+datatype 'p output_rest =
+  WithoutOpening \<open>val\<close> \<open>'p\<close> ("_\<rparr> _" [52, 51] 51) |
+  WithOpening \<open>chan \<Rightarrow> 'p output_rest\<close> (binder "\<nu> " 51)
 
 text \<open>
   Note that the definition of \<open>output_rest\<close> is actually more permissive than the verbal definition
@@ -50,7 +50,7 @@ text \<open>
 \<close>
 
 abbreviation
-  output_rest_lift :: "(['t, 't] \<Rightarrow> bool) \<Rightarrow> (['t output_rest, 't output_rest] \<Rightarrow> bool)"
+  output_rest_lift :: "(['p, 'q] \<Rightarrow> bool) \<Rightarrow> (['p output_rest, 'q output_rest] \<Rightarrow> bool)"
 where
   "output_rest_lift \<equiv> rel_output_rest"
 
@@ -83,9 +83,9 @@ text \<open>
   \<open>\<lparr>a \<triangleleft> \<nu> b\<^sub>1 \<dots> b\<^sub>n. X b\<^sub>1 \<dots> b\<^sub>n\<rparr> Q b\<^sub>1 \<dots> b\<^sub>n\<close> where \<open>a\<close> is a channel and the \<open>b\<^sub>i\<close> are channel variables.
 \<close>
 
-datatype 't proper_residual =
-  Simple \<open>proper_action\<close> \<open>'t\<close> ("\<lparr>_\<rparr> _" [0, 51] 51) |
-  Output \<open>chan\<close> \<open>'t output_rest\<close> ("\<lparr>_ \<triangleleft> _" [0, 51] 51)
+datatype 'p proper_residual =
+  Simple \<open>proper_action\<close> \<open>'p\<close> ("\<lparr>_\<rparr> _" [0, 51] 51) |
+  Output \<open>chan\<close> \<open>'p output_rest\<close> ("\<lparr>_ \<triangleleft> _" [0, 51] 51)
 
 text \<open>
   We introduce the alias \<open>proper_lift\<close> for the automatically generated relator
@@ -95,7 +95,7 @@ text \<open>
 \<close>
 
 abbreviation
-  proper_lift :: "(['t, 't] \<Rightarrow> bool) \<Rightarrow> (['t proper_residual, 't proper_residual] \<Rightarrow> bool)"
+  proper_lift :: "(['p, 'q] \<Rightarrow> bool) \<Rightarrow> (['p proper_residual, 'q proper_residual] \<Rightarrow> bool)"
 where
   "proper_lift \<equiv> rel_proper_residual"
 

Isabelle/Chi_Calculus/Proper_Weak_Transition_System.thy

@@ -4,7 +4,7 @@ theory Proper_Weak_Transition_System
   imports Basic_Weak_Transition_System Proper_Transition_System
 begin
 
-inductive proper_silent :: "[process, process proper_residual] \<Rightarrow> bool" where
+inductive proper_silent :: "['p, 'p proper_residual] \<Rightarrow> bool" where
   proper_internal_is_silent: "proper_silent p (\<lparr>\<tau>\<rparr> p)"
 
 interpretation proper: std_weak_residual proper_lift proper_silent
@@ -33,6 +33,7 @@ qed
 interpretation proper: weak_transition_system proper_silent proper.absorb proper_transition
   by intro_locales
 
+notation proper.weak_transition (infix "\<Rightarrow>\<^sub>\<sharp>" 50)
 notation proper.weak.pre_bisimilarity (infix "\<lessapprox>\<^sub>\<sharp>" 50)
 notation proper.weak.bisimilarity (infix "\<approx>\<^sub>\<sharp>" 50)
 

Isabelle/Chi_Calculus/Typed_Basic_Transition_System.thy

@@ -19,13 +19,24 @@ abbreviation
 where
   "\<aa> \<triangleright>\<degree> \<xx> \<equiv> untyped_channel \<aa> \<triangleright> untyped_value \<xx>"
 
-abbreviation typed_opening :: "('a channel \<Rightarrow> 't) \<Rightarrow> 't basic_residual" where
+abbreviation typed_opening :: "('a channel \<Rightarrow> 'p) \<Rightarrow> 'p basic_residual" where
   "typed_opening \<PP> \<equiv> \<lbrace>\<nu> a\<rbrace> \<PP> (typed_channel a)"
 syntax
-  "_typed_opening" :: "pttrn \<Rightarrow> process \<Rightarrow> 't basic_residual"
+  "_typed_opening" :: "pttrn \<Rightarrow> process \<Rightarrow> 'p basic_residual"
   ("\<lbrace>\<nu>\<degree>_\<rbrace> _" [0, 51] 51)
 translations
   "\<lbrace>\<nu>\<degree>\<aa>\<rbrace> \<pp>" \<rightleftharpoons> "CONST typed_opening (\<lambda>\<aa>. \<pp>)"
+print_translation \<open>
+  [
+    Syntax_Trans.preserve_binder_abs_tr'
+      @{const_syntax typed_opening}
+      @{syntax_const "_typed_opening"}
+  ]
+\<close>
+(* FIXME:
+  The @{command print_translation} part will only work once we have changed @{command abbreviation}
+  to @{command definition}.
+*)
 
 lemma typed_ltr: "typed_basic_out \<aa> \<xx> \<bowtie> typed_basic_in \<aa> \<xx>"
   by (fact ltr)

Isabelle/Chi_Calculus/Typed_Processes.thy

@@ -11,6 +11,13 @@ syntax
   ("(3_ \<triangleright>\<degree> _./ _)" [101, 0, 100] 100)
 translations
   "\<aa> \<triangleright>\<degree> \<xx>. \<pp>" \<rightleftharpoons> "CONST typed_receive \<aa> (\<lambda>\<xx>. \<pp>)"
+print_translation \<open>
+  [preserve_binder_abs_receive_tr' @{const_syntax typed_receive} @{syntax_const "_typed_receive"}]
+\<close>
+(* FIXME:
+  The @{command print_translation} part will only work once we have changed @{command abbreviation}
+  to @{command definition}.
+*)
 abbreviation typed_new_channel :: "('a channel \<Rightarrow> process) \<Rightarrow> process" (binder "\<nu>\<degree>" 100) where
   "\<nu>\<degree>\<aa>. \<PP> \<aa> \<equiv> \<nu> a. \<PP> (typed_channel a)"
 

Isabelle/Chi_Calculus/Typed_Proper_Transition_System.thy

@@ -7,27 +7,27 @@ abbreviation
 where
   "\<aa> \<triangleright>\<degree> \<xx> \<equiv> ProperIn (untyped_channel \<aa>) (untyped_value \<xx>)"
 
-datatype ('a, 't) typed_output_rest =
-  TypedWithoutOpening \<open>'a\<close> \<open>'t\<close> ("_\<rparr> _" [52, 51] 51) |
-  TypedWithOpening \<open>chan \<Rightarrow> ('a, 't) typed_output_rest\<close>
+datatype ('a, 'p) typed_output_rest =
+  TypedWithoutOpening \<open>'a\<close> \<open>'p\<close> ("_\<rparr> _" [52, 51] 51) |
+  TypedWithOpening \<open>chan \<Rightarrow> ('a, 'p) typed_output_rest\<close>
 
 (*
   We use the ordinary-font K to denote a function whose argument is untyped but whose resulting
   output rest is typed.
 *)
 
-primrec untyped_output_rest :: "('a::countable, 't) typed_output_rest \<Rightarrow> 't output_rest" where
+primrec untyped_output_rest :: "('a::countable, 'p) typed_output_rest \<Rightarrow> 'p output_rest" where
   "untyped_output_rest (\<xx>\<rparr> p) = untyped_value \<xx>\<rparr> p" |
   "untyped_output_rest (TypedWithOpening K) = WithOpening (untyped_output_rest \<circ> K)"
 
 abbreviation
-  typed_with_opening :: "('a channel \<Rightarrow> ('b, 't) typed_output_rest) \<Rightarrow> ('b, 't) typed_output_rest"
+  typed_with_opening :: "('a channel \<Rightarrow> ('b, 'p) typed_output_rest) \<Rightarrow> ('b, 'p) typed_output_rest"
   (binder "\<nu>\<degree>" 51)
 where
   "\<nu>\<degree>\<aa>. \<KK> \<aa> \<equiv> TypedWithOpening (\<KK> \<circ> typed_channel)"
 
 abbreviation
-  typed_output :: "['a channel, ('a::countable, 't) typed_output_rest] \<Rightarrow> 't proper_residual"
+  typed_output :: "['a channel, ('a::countable, 'p) typed_output_rest] \<Rightarrow> 'p proper_residual"
   ("\<lparr>_ \<triangleleft>\<degree> _" [0, 51] 51)
 where
   "\<lparr>\<aa> \<triangleleft>\<degree> \<kk> \<equiv> \<lparr>untyped_channel \<aa> \<triangleleft> untyped_output_rest \<kk>"

Isabelle/Chi_Calculus/binder_preservation.ML

@@ -0,0 +1,17 @@
+(*  Title:      Chi_Calculus/binder_preservation.ML
+    Author:     Wolfgang Jeltsch, Well-Typed LLP
+
+Further variants of Syntax_Trans.preserve_binder_abs_tr' from Pure/Syntax/syntax_trans.ML.
+*)
+
+(* Constructs like Receive *)
+
+fun preserve_binder_abs_receive_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts =>
+  let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+  in list_comb (Syntax.const syn $ A $ x $ t, ts) end);
+
+(* Constructs like general_parallel *)
+
+fun preserve_binder_abs_general_parallel_tr' name syn = (name, fn _ => fn Abs abs :: A :: ts =>
+  let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+  in list_comb (Syntax.const syn $ x $ A $ t, ts) end);