src/HOL/Lex/Regset_of_auto.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Regset_of_auto.thy	Wed Nov 05 09:08:35 1997 +0100
@@ -0,0 +1,44 @@
+(*
+Conversion of automata into regular sets.
+use_thy"Auto";
+*)
+
+Regset_of_auto = List +
+
+(* autos *)
+
+types 'a auto = "'a => nat => nat"
+
+consts deltas :: 'a auto => 'a list => nat => nat
+primrec deltas list
+"deltas A [] i = i"
+"deltas A (x#xs) i = deltas A xs (A x i)"
+
+consts trace :: 'a auto => nat => 'a list => nat list
+primrec trace list
+"trace A i [] = []"
+"trace A i (x#xs) = A x i # trace A (A x i) xs"
+
+(* regular sets *)
+
+constdefs conc :: 'a list set => 'a list set => 'a list set
+         "conc A B == {xs@ys | xs ys. xs:A & ys:B}"
+
+consts star :: 'a list set => 'a list set
+inductive "star A"
+intrs
+  NilI   "[] : star A"
+  ConsI  "[| a:A; as : star A |] ==> a@as : star A"
+
+(* conversion a la Warshall *)
+
+consts regset_of :: 'a auto => nat => nat => nat => 'a list set
+primrec regset_of nat
+"regset_of A i j 0 = (if i=j then insert [] {[a] | a. A a i = j}
+                             else {[a] | a. A a i = j})"
+"regset_of A i j (Suc k) = regset_of A i j k Un
+                           conc (regset_of A i k k)
+                          (conc (star(regset_of A k k k))
+                                (regset_of A k j k))"
+
+end