--- a/src/HOL/Lex/Regset_of_auto.thy Mon Apr 27 16:45:27 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(*
-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