Simplify proof of big_parallel_cong

input-output-hk · Feb 16, 2019 · c92cc19 · c92cc19
1 parent 9f01230
commit c92cc19
Showing 1 changed file with 2 additions and 10 deletions.
diff --git 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