From c92cc194f5ee3228a2ac7616edc3fd6e7613bc76 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Javier=20D=C3=ADaz?= <javier.diaz@iohk.io>
Date: Sat, 16 Feb 2019 00:19:33 -0300
Subject: [PATCH] Simplify proof of `big_parallel_cong`

---
 Isabelle/Chi_Calculus_Examples/Utilities.thy | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/Isabelle/Chi_Calculus_Examples/Utilities.thy b/Isabelle/Chi_Calculus_Examples/Utilities.thy
index c7f2b56..3316853 100644
--- a/Isabelle/Chi_Calculus_Examples/Utilities.thy
+++ b/Isabelle/Chi_Calculus_Examples/Utilities.thy
@@ -272,20 +272,12 @@ next
   case (Cons y ys)
   have "big_parallel f xs = big_parallel f (y # ys)"
     by (simp add: \<open>xs = y # ys\<close>)
-  also have "... = foldr (\<lambda>x p. f x \<parallel> p) (y # ys) \<zero>"
-    by (unfold big_parallel_def) simp
-  also have "... = f y \<parallel> foldr (\<lambda>x p. f x \<parallel> p) ys \<zero>"
-    by (simp add: foldr_Cons)
   also have "... = f y \<parallel> big_parallel f ys"
-    by (fold big_parallel_def) simp
+    by (simp add: big_parallel_def)
   also have "... = g y \<parallel> big_parallel g ys"
     by (simp add: Cons.IH Cons.prems(1-2))
-  also have "... = g y \<parallel> foldr (\<lambda>x p. g x \<parallel> p) ys \<zero>"
-    by (unfold big_parallel_def) simp
-  also have "... = foldr (\<lambda>x p. g x \<parallel> p) (y # ys) \<zero>"
-    by (simp add: foldr_Cons)
   also have "... = big_parallel g (y # ys)"
-    by (fold big_parallel_def) simp
+    by (simp add: big_parallel_def)
   finally show ?case
     by simp
 qed