diff -r 8bb064045b4e -r e51c9a67a68d thys/RegLangs.thy
--- a/thys/RegLangs.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/RegLangs.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -1,5 +1,5 @@
 theory RegLangs
-  imports Main "~~/src/HOL/Library/Sublist"
+  imports Main "HOL-Library.Sublist"
 begin
 
 section \<open>Sequential Composition of Languages\<close>
@@ -196,4 +196,41 @@
   shows "ders (s @ [c]) r = der c (ders s r)"
   by (simp add: ders_append)
 
+
+(*
+datatype ctxt = 
+    SeqC rexp bool
+  | AltCL rexp
+  | AltCR rexp 
+  | StarC rexp 
+
+function
+     down :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"
+and  up :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"
+where
+  "down c (SEQ r1 r2) ctxts =
+     (if (nullable r1) then down c r1 (SeqC r2 True # ctxts) 
+      else down c r1 (SeqC r2 False # ctxts))"
+| "down c (CH d) ctxts = 
+     (if c = d then up c ONE ctxts else up c ZERO ctxts)"
+| "down c ONE ctxts = up c ZERO ctxts"
+| "down c ZERO ctxts = up c ZERO ctxts"
+| "down c (ALT r1 r2) ctxts = down c r1 (AltCR r2 # ctxts)"
+| "down c (STAR r1) ctxts = down c r1 (StarC r1 # ctxts)"
+| "up c r [] = (r, [])"
+| "up c r (SeqC r2 False # ctxts) = up c (SEQ r r2) ctxts"
+| "up c r (SeqC r2 True # ctxts) = down c r2 (AltCL (SEQ r r2) # ctxts)"
+| "up c r (AltCL r1 # ctxts) = up c (ALT r1 r) ctxts"
+| "up c r (AltCR r2 # ctxts) = down c r2 (AltCL r # ctxts)"
+| "up c r (StarC r1 # ctxts) = up c (SEQ r (STAR r1)) ctxts"
+  apply(pat_completeness)
+  apply(auto)
+  done
+
+termination
+  sorry
+
+*)
+
+
 end
\ No newline at end of file