--- a/thys/RegLangs.thy	Mon Feb 22 03:22:26 2021 +0000
+++ b/thys/RegLangs.thy	Thu Feb 25 22:46:58 2021 +0000
@@ -1,16 +1,15 @@
-   
 theory RegLangs
   imports Main "~~/src/HOL/Library/Sublist"
 begin
 
-section {* Sequential Composition of Languages *}
+section \<open>Sequential Composition of Languages\<close>
 
 definition
   Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 where 
   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
 
-text {* Two Simple Properties about Sequential Composition *}
+text \<open>Two Simple Properties about Sequential Composition\<close>
 
 lemma Sequ_empty_string [simp]:
   shows "A ;; {[]} = A"
@@ -22,22 +21,8 @@
   and   "{} ;; A = {}"
   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 *}
+section \<open>Semantic Derivative (Left Quotient) of Languages\<close>
 
 definition
   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
@@ -75,7 +60,7 @@
 by (auto simp add: Cons_eq_append_conv)
 
 
-section {* Kleene Star for Languages *}
+section \<open>Kleene Star for Languages\<close>
 
 inductive_set
   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
@@ -104,7 +89,7 @@
 by(auto simp add: Star_decomp)
 
 
-lemma Der_star [simp]:
+lemma Der_star[simp]:
   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 proof -    
   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"  
@@ -134,37 +119,37 @@
 
 
 
-section {* Regular Expressions *}
+section \<open>Regular Expressions\<close>
 
 datatype rexp =
   ZERO
 | ONE
-| CHAR char
+| CH char
 | SEQ rexp rexp
 | ALT rexp rexp
 | STAR rexp
 
-section {* Semantics of Regular Expressions *}
+section \<open>Semantics of Regular Expressions\<close>
  
 fun
   L :: "rexp \<Rightarrow> string set"
 where
   "L (ZERO) = {}"
 | "L (ONE) = {[]}"
-| "L (CHAR c) = {[c]}"
+| "L (CH c) = {[c]}"
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 | "L (STAR r) = (L r)\<star>"
 
 
-section {* Nullable, Derivatives *}
+section \<open>Nullable, Derivatives\<close>
 
 fun
  nullable :: "rexp \<Rightarrow> bool"
 where
   "nullable (ZERO) = False"
 | "nullable (ONE) = True"
-| "nullable (CHAR c) = False"
+| "nullable (CH c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 | "nullable (STAR r) = True"
@@ -175,7 +160,7 @@
 where
   "der c (ZERO) = ZERO"
 | "der c (ONE) = ZERO"
-| "der c (CHAR d) = (if c = d then ONE else ZERO)"
+| "der c (CH d) = (if c = d then ONE else ZERO)"
 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 | "der c (SEQ r1 r2) = 
      (if nullable r1