--- a/thys/RegLangs.thy	Wed Sep 18 16:35:57 2019 +0100
+++ b/thys/RegLangs.thy	Sat Oct 24 12:13:39 2020 +0100
@@ -20,8 +20,22 @@
 lemma Sequ_empty [simp]:
   shows "A ;; {} = {}"
   and   "{} ;; A = {}"
-by (simp_all add: Sequ_def)
+  by (simp_all add: Sequ_def)
+
+lemma
+  shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
+  apply(auto simp add: Sequ_def)  
+  done
 
+lemma
+  shows "(A \<inter> B) ;; C \<subseteq> (A ;; C) \<inter> (B ;; C)"
+  apply(auto simp add: Sequ_def) 
+  done
+
+lemma
+  shows "(A ;; C) \<inter> (B ;; C) \<subseteq> (A \<inter> B) ;; C"
+  apply(auto simp add: Sequ_def) 
+  oops
 
 section {* Semantic Derivative (Left Quotient) of Languages *}