Overhaul the `Filtering_On_Receipt_Forwarding_Broadcasting_Equivalenc…

…e` theory
input-output-hk · Oct 23, 2019 · 0a3e9d2 · 0a3e9d2
1 parent d67b33e
commit 0a3e9d2
Show file tree

Hide file tree

Showing 6 changed files with 693 additions and 2,359 deletions.
diff --git a/Isabelle/Chi_Calculus/Basic_Transition_System.thy b/Isabelle/Chi_Calculus/Basic_Transition_System.thy
@@ -616,6 +616,10 @@ private lift_definition new_channel' :: "(chan \<Rightarrow> basic_behavior) \<R
   is NewChannel
   using basic_new_channel_preservation .
 
+private lift_definition guard' :: "[bool, basic_behavior] \<Rightarrow> basic_behavior"
+  is guard
+  using basic.guard_preservation .
+
 private lift_definition general_parallel' :: "['a \<Rightarrow> basic_behavior, 'a list] \<Rightarrow> basic_behavior"
   is general_parallel
   using basic.general_parallel_preservation .
@@ -626,6 +630,7 @@ lemmas [equivalence_transfer] =
   receive'.abs_eq
   parallel'.abs_eq
   new_channel'.abs_eq
+  guard'.abs_eq
   general_parallel'.abs_eq
 
 end

diff --git a/Isabelle/Chi_Calculus/Basic_Weak_Transition_System.thy b/Isabelle/Chi_Calculus/Basic_Weak_Transition_System.thy
@@ -96,6 +96,11 @@ private
   is NewChannel
   using basic_weak_new_channel_preservation .
 
+private
+  lift_definition guard' :: "[bool, basic_weak_behavior] \<Rightarrow> basic_weak_behavior"
+  is guard
+  sorry
+
 private
   lift_definition general_parallel' :: "['a \<Rightarrow> basic_weak_behavior, 'a list] \<Rightarrow> basic_weak_behavior"
   is general_parallel
@@ -107,6 +112,7 @@ lemmas [equivalence_transfer] =
   receive'.abs_eq
   parallel'.abs_eq
   new_channel'.abs_eq
+  guard'.abs_eq
   general_parallel'.abs_eq
 
 end

diff --git a/Isabelle/Chi_Calculus/Natural_Transition_Systems.thy b/Isabelle/Chi_Calculus/Natural_Transition_Systems.thy
@@ -20,6 +20,11 @@ locale natural_transition_system =
     "\<And>P Q. (\<And>a. P a \<sim> Q a) \<Longrightarrow> \<nu> a. P a \<sim> \<nu> a. Q a"
 begin
 
+lemma guard_preservation:
+  assumes "p \<sim> q"
+  shows "\<phi> ? p \<sim> \<phi> ? q"
+  using assms by simp
+
 lemma general_parallel_preservation:
   assumes "\<And>x. f x \<sim> g x"
   shows "general_parallel f xs \<sim> general_parallel g xs"

diff --git a/Isabelle/Chi_Calculus/Proper_Transition_System.thy b/Isabelle/Chi_Calculus/Proper_Transition_System.thy
@@ -303,6 +303,10 @@ private lift_definition new_channel' :: "(chan \<Rightarrow> proper_behavior) \<
   is NewChannel
   using proper_new_channel_preservation .
 
+private lift_definition guard' :: "[bool, proper_behavior] \<Rightarrow> proper_behavior"
+  is guard
+  using proper.guard_preservation .
+
 private lift_definition general_parallel' :: "['a \<Rightarrow> proper_behavior, 'a list] \<Rightarrow> proper_behavior"
   is general_parallel
   using proper.general_parallel_preservation .
@@ -313,6 +317,7 @@ lemmas [equivalence_transfer] =
   receive'.abs_eq
   parallel'.abs_eq
   new_channel'.abs_eq
+  guard'.abs_eq
   general_parallel'.abs_eq
 
 end

diff --git a/Isabelle/Chi_Calculus/Proper_Weak_Transition_System.thy b/Isabelle/Chi_Calculus/Proper_Weak_Transition_System.thy
@@ -103,6 +103,11 @@ private
   is NewChannel
   using proper_weak_new_channel_preservation .
 
+private
+  lift_definition guard' :: "[bool, proper_weak_behavior] \<Rightarrow> proper_weak_behavior"
+  is guard
+  sorry
+
 private
   lift_definition general_parallel' :: "['a \<Rightarrow> proper_weak_behavior, 'a list] \<Rightarrow> proper_weak_behavior"
   is general_parallel
@@ -114,6 +119,7 @@ lemmas [equivalence_transfer] =
   receive'.abs_eq
   parallel'.abs_eq
   new_channel'.abs_eq
+  guard'.abs_eq
   general_parallel'.abs_eq
 
 end