From 1b18f88e41ba47d4af49ef4ab6d286992aa61baf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 5 Jan 2023 18:44:22 -0300 Subject: [PATCH 1/6] Add `family_uncurry_after_distributor` --- src/Network_Equivalences-Communication.thy | 24 ++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/Network_Equivalences-Communication.thy b/src/Network_Equivalences-Communication.thy index 83e0bf5..e0a9e58 100644 --- a/src/Network_Equivalences-Communication.thy +++ b/src/Network_Equivalences-Communication.thy @@ -13,6 +13,30 @@ lemma adapted_after_distributor: shows "(A \ Bs) \ \ = A \ \ \ map (\B. B \ \) Bs" sorry +lemma family_uncurry_after_distributor [induct_simp]: + shows "\ (\b. \ b \ map (\\. \ b) \s) = \ \ \ map \ \s" +proof - + have "\ (\b. \ b \ map (\\. \ b) \s) = \ (\b. \ b \\<^sup>\ x. \B \ map (\\. \ b) \s. B \ \ x)" + unfolding distributor_def .. + also have "\ = \ (\b. \ b \\<^sup>\ x. \\ \ \s. \ b \ \ x)" + unfolding general_parallel_conversion_deferral .. + also have "\ = \ \ \\<^sup>\ x. \ (\b. \\ \ \s. \ b \ \ x)" + unfolding family_uncurry_after_repeated_receive .. + also have "\ = \ \ \\<^sup>\ x. \\ \ \s. \ (\b. \ b \ \ x)" + unfolding family_uncurry_after_general_parallel .. + also have "\ = \ \ \\<^sup>\ x. \\ \ \s. \ \ \ \ (\b.\ x)" + unfolding family_uncurry_after_send .. + also have "\ = \ \ \\<^sup>\ x. \\ \ \s. \ \ \ \ x \ tail" + unfolding constant_function_family_uncurry .. + also have "\ = \ \ \\<^sup>\ x. \\ \ \s. \ \ \ \ x" + unfolding tail_def by transfer simp + also have "\ = \ \ \\<^sup>\ x. \B \ map \ \s. B \ \ x" + unfolding general_parallel_conversion_deferral .. + also have "\ = \ \ \ map \ \s" + unfolding distributor_def .. + finally show ?thesis . +qed + lemma distributor_idempotency [thorn_simps]: shows "A \ Bs \ A \ Bs \\<^sub>s A \ Bs" unfolding distributor_def From af95d914f3da11807b4254fb87c14b1d1a39def6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 5 Jan 2023 18:46:52 -0300 Subject: [PATCH 2/6] Add `family_uncurry_after_loss` --- src/Network_Equivalences-Communication.thy | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Network_Equivalences-Communication.thy b/src/Network_Equivalences-Communication.thy index e0a9e58..1eceb6a 100644 --- a/src/Network_Equivalences-Communication.thy +++ b/src/Network_Equivalences-Communication.thy @@ -62,6 +62,11 @@ lemma adapted_after_loss: shows "\\<^sup>? A \ \ = \\<^sup>? (A \ \)" by (simp del: distributor_def add: adapted_after_distributor) +lemma family_uncurry_after_loss [induct_simp]: + shows "\ (\b. \\<^sup>? (\ b)) = \\<^sup>? (\ \)" + using family_uncurry_after_distributor [where \s = "[]"] + by simp + lemma loss_idempotency [thorn_simps]: shows "\\<^sup>? A \ \\<^sup>? A \\<^sub>s \\<^sup>? A" unfolding loss_def From 9cc6f36b2f4d5af2333ed1523b818ae86b9bb897 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 5 Jan 2023 18:55:40 -0300 Subject: [PATCH 3/6] Add `family_uncurry_after_duplication` --- src/Network_Equivalences-Communication.thy | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Network_Equivalences-Communication.thy b/src/Network_Equivalences-Communication.thy index 1eceb6a..24daf44 100644 --- a/src/Network_Equivalences-Communication.thy +++ b/src/Network_Equivalences-Communication.thy @@ -91,6 +91,11 @@ lemma adapted_after_duplication: shows "\\<^sup>+ A \ \ = \\<^sup>+ (A \ \)" by (simp del: distributor_def add: adapted_after_distributor) +lemma family_uncurry_after_duplication [induct_simp]: + shows "\ (\b. \\<^sup>+ (\ b)) = \\<^sup>+ (\ \)" + using family_uncurry_after_distributor [where \s = "[\, \]"] + by simp + lemma duplication_idempotency [thorn_simps]: shows "\\<^sup>+ A \ \\<^sup>+ A \\<^sub>s \\<^sup>+ A" unfolding duplication_def From b2da42e11368a69bd610ea7e695fa940eb6a50f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 5 Jan 2023 18:56:59 -0300 Subject: [PATCH 4/6] Add `family_uncurry_after_duploss` --- src/Network_Equivalences-Communication.thy | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Network_Equivalences-Communication.thy b/src/Network_Equivalences-Communication.thy index 24daf44..0b1c389 100644 --- a/src/Network_Equivalences-Communication.thy +++ b/src/Network_Equivalences-Communication.thy @@ -125,6 +125,14 @@ lemma adapted_after_duploss: shows "\\<^sup>* A \ \ = \\<^sup>* (A \ \)" by (simp only: duploss_def adapted_after_parallel adapted_after_loss adapted_after_duplication) +lemma family_uncurry_after_duploss [induct_simp]: + shows "\ (\b. \\<^sup>* (\ b)) = \\<^sup>* (\ \)" + unfolding + duploss_def + and + family_uncurry_after_parallel and family_uncurry_after_loss and family_uncurry_after_duplication + .. + lemma duploss_idempotency [thorn_simps]: shows "\\<^sup>* A \ \\<^sup>* A \\<^sub>s \\<^sup>* A" unfolding duploss_def From 147ee8fac1845233af4aeca79fdb03809c71acce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 5 Jan 2023 18:58:19 -0300 Subject: [PATCH 5/6] Add `family_uncurry_after_unidirectional_bridge` --- src/Network_Equivalences-Communication.thy | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Network_Equivalences-Communication.thy b/src/Network_Equivalences-Communication.thy index 0b1c389..d50d9b9 100644 --- a/src/Network_Equivalences-Communication.thy +++ b/src/Network_Equivalences-Communication.thy @@ -231,6 +231,11 @@ lemma adapted_after_unidirectional_bridge: shows "(A \ B) \ \ = A \ \ \ B \ \" by (simp del: distributor_def add: adapted_after_distributor) +lemma family_uncurry_after_unidirectional_bridge [induct_simp]: + shows "\ (\b. \ b \ \ b) = \ \ \ \ \" + using family_uncurry_after_distributor [where \s = "[\]"] + by simp + lemma unidirectional_bridge_idempotency [thorn_simps]: shows "A \ B \ A \ B \\<^sub>s A \ B" unfolding unidirectional_bridge_def From fc1650c7dba5c88d8fbb8742ab0a8bf2ee0bc164 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 5 Jan 2023 18:59:48 -0300 Subject: [PATCH 6/6] Add `family_uncurry_after_bidirectional_bridge` --- src/Network_Equivalences-Communication.thy | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Network_Equivalences-Communication.thy b/src/Network_Equivalences-Communication.thy index d50d9b9..ef79f03 100644 --- a/src/Network_Equivalences-Communication.thy +++ b/src/Network_Equivalences-Communication.thy @@ -289,6 +289,14 @@ lemma adapted_after_bidirectional_bridge: shows "(A \ B) \ \ = A \ \ \ B \ \" by (simp only: bidirectional_bridge_def adapted_after_parallel adapted_after_unidirectional_bridge) +lemma family_uncurry_after_bidirectional_bridge [induct_simp]: + shows "\ (\b. \ b \ \ b) = \ \ \ \ \" + unfolding + bidirectional_bridge_def + and + family_uncurry_after_parallel and family_uncurry_after_unidirectional_bridge + .. + lemma bidirectional_bridge_idempotency [thorn_simps]: shows "A \ B \ A \ B \\<^sub>s A \ B" unfolding bidirectional_bridge_def