--- a/thys2/BitCoded.thy	Wed Apr 13 22:20:08 2022 +0100
+++ b/thys2/BitCoded.thy	Fri Apr 15 19:35:29 2022 +0100
@@ -1,5 +1,5 @@
 
-theory BitCodedCT
+theory BitCoded
   imports "Lexer" 
 begin
 
@@ -29,7 +29,7 @@
 where
   "decode' ds ZERO = (Void, [])"
 | "decode' ds ONE = (Void, ds)"
-| "decode' ds (CHAR d) = (Char d, ds)"
+| "decode' ds (CH d) = (Char d, ds)"
 | "decode' [] (ALT r1 r2) = (Void, [])"
 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
@@ -111,7 +111,7 @@
 where
   "erase AZERO = ZERO"
 | "erase (AONE _) = ONE"
-| "erase (ACHAR _ c) = CHAR c"
+| "erase (ACHAR _ c) = CH c"
 | "erase (AALTs _ []) = ZERO"
 | "erase (AALTs _ [r]) = (erase r)"
 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
@@ -131,21 +131,6 @@
 | "nonalt r = True"
 
 
-fun good :: "arexp \<Rightarrow> bool" where
-  "good AZERO = False"
-| "good (AONE cs) = True" 
-| "good (ACHAR cs c) = True"
-| "good (AALTs cs []) = False"
-| "good (AALTs cs [r]) = False"
-| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
-| "good (ASEQ _ AZERO _) = False"
-| "good (ASEQ _ (AONE _) _) = False"
-| "good (ASEQ _ _ AZERO) = False"
-| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
-| "good (ASTAR cs r) = True"
-
-
-
 
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
   "fuse bs AZERO = AZERO"
@@ -165,7 +150,7 @@
 fun intern :: "rexp \<Rightarrow> arexp" where
   "intern ZERO = AZERO"
 | "intern ONE = AONE []"
-| "intern (CHAR c) = ACHAR [] c"
+| "intern (CH c) = ACHAR [] c"
 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
                                 (fuse [S]  (intern r2))"
 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
@@ -1118,6 +1103,25 @@
    apply(simp_all)
   done
 
+fun nonalt :: "arexp \<Rightarrow> bool"
+  where
+  "nonalt (AALTs bs2 rs) = False"
+| "nonalt r = True"
+
+
+fun good :: "arexp \<Rightarrow> bool" where
+  "good AZERO = False"
+| "good (AONE cs) = True" 
+| "good (ACHAR cs c) = True"
+| "good (AALTs cs []) = False"
+| "good (AALTs cs [r]) = False"
+| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
+| "good (ASEQ _ AZERO _) = False"
+| "good (ASEQ _ (AONE _) _) = False"
+| "good (ASEQ _ _ AZERO) = False"
+| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
+| "good (ASTAR cs r) = True"
+
 lemma bbbbs:
   assumes "good r" "r = AALTs bs1 rs"
   shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"