# HG changeset patch
# User nipkow
# Date 1080723625 -7200
# Node ID 8d5c551a9260b13442e59549777efea0e7e7f26e
# Parent  2015348ceecba893bc76728d244f83f5a00bc97b
HOL/Lex is now in AFP/Functional-Automata

diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,260 +0,0 @@
-(*  Title:      HOL/Lex/AutoChopper.thy
-    ID:         $Id$
-    Author:     Richard Mayr & Tobias Nipkow
-    Copyright   1995 TUM
-
-auto_chopper turns an automaton into a chopper. Tricky, because primrec.
-
-is_auto_chopper requires its argument to produce longest_prefix_choppers
-wrt the language accepted by the automaton.
-
-Main result: auto_chopper satisfies the is_auto_chopper specification.
-
-WARNING: auto_chopper is exponential(?)
-if the recursive calls in the penultimate argument are evaluated eagerly.
-
-A more efficient version is defined in AutoChopper1.
-
-But both versions are far too specific. Better development in Scanner.thy and
-its antecedents.
-*)
-
-theory AutoChopper = DA + Chopper:
-
-constdefs
- is_auto_chopper :: "(('a,'s)da => 'a chopper) => bool"
-"is_auto_chopper(chopperf) ==
-    !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
-
-consts
-  acc :: "('a,'s)da \<Rightarrow> 's \<Rightarrow> 'a list list * 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list
-          \<Rightarrow> 'a list \<Rightarrow> 'a list list * 'a list"
-
-primrec
-  "acc A s r ps []     zs = (if ps=[] then r else (ps#fst(r),snd(r)))" 
-  "acc A s r ps (x#xs) zs =
-            (let t = next A x s
-             in if fin A t
-                then acc A t (acc A (start A) ([],xs) [] xs [])
-                         (zs@[x]) xs (zs@[x])
-                else acc A t r ps xs (zs@[x]))"
-
-constdefs
- auto_chopper :: "('a,'s)da => 'a chopper"
-"auto_chopper A xs == acc A (start A) ([],xs) [] xs []"
-
-(* acc_prefix is an auxiliary notion for the proof *)
-constdefs
- acc_prefix :: "('a,'s)da => 'a list => 's => bool"
-"acc_prefix A xs s \<equiv> \<exists>us. us \<le> xs \<and> us \<noteq> [] \<and> fin A (delta A us s)"
-
-(*
-Main result: auto_chopper satisfies the is_auto_chopper specification.
-*)
-
-declare
-  ex_simps[simp del] all_simps[simp del] split_paired_All[simp del]
-  Let_def[simp]
-
-lemma acc_prefix_Nil[simp]: "~acc_prefix A [] s"
-by(simp add:acc_prefix_def)
-
-lemma acc_prefix_Cons[simp]:
- "acc_prefix A (x#xs) s = (fin A (next A x s) | acc_prefix A xs (next A x s))"
-apply (simp add: prefix_Cons acc_prefix_def)
-apply safe
-  apply (simp)
-  apply (case_tac "zs = []")
-   apply (simp)
-  apply (fast)
- apply (rule_tac x = "[x]" in exI)
- apply (simp add:eq_sym_conv)
-apply (rule_tac x = "x#us" in exI)
-apply (simp)
-done
-
-lemma accept_not_Nil[simp]:
-  "!!st us p y ys. acc A st p (ys@[y]) xs us \<noteq> ([],zs)"
-by (induct xs) simp_all
-
-lemma no_acc:
-  "!!st us. acc A st ([],ys) [] xs us = ([], zs) \<Longrightarrow>
-            zs = ys \<and> (\<forall>ys. ys \<noteq> [] \<and> ys \<le> xs \<longrightarrow> ~fin A (delta A ys st))"
-apply (induct xs)
- apply (simp cong: conj_cong)
-apply (simp add: prefix_Cons cong: conj_cong split:split_if_asm)
-apply (intro strip)
-apply (elim conjE exE)
-apply (simp)
-apply (case_tac "zsa = []")
- apply (simp)
-apply (fast)
-done
-
-lemma ex_special: "EX x. P(f(x)) ==> EX y. P(y)"
-by (fast)
-
-lemma step2_a:
-"!!r erk l rst st ys yss zs::'a list.
- acc A st (l,rst) erk xs r = (ys#yss, zs) \<Longrightarrow>
- ys@concat(yss)@zs = (if acc_prefix A xs st then r@xs else erk@concat(l)@rst)"
-apply (induct "xs")
- apply (simp cong: conj_cong split:split_if_asm)
-apply (simp split:split_if_asm)
-apply (rule_tac p = "acc A (start A) ([],list) [] list []" in PairE)
-apply (rename_tac vss lrst)
-apply (simp)
-apply (case_tac vss)
- apply (simp)
- apply (fast dest!: no_acc)
-apply (simp)
-done
-
-lemma step2_b:
- "!!st erk r l rest ys yss zs. acc A st (l,rest) erk xs r = (ys#yss, zs) \<Longrightarrow>
-       if acc_prefix A xs st then ys \<noteq> []
-\      else ys \<noteq> [] \<or> (erk=[] \<and> (l,rest) = (ys#yss,zs))"
-apply (simp)
-apply (induct "xs")
- apply (simp cong: conj_cong split:split_if_asm)
-apply (simp cong: conj_cong split:split_if_asm)
-apply (rule_tac p = "acc A (start A) ([],list) [] list []" in PairE)
-apply (rename_tac vss lrst)
-apply (simp)
-apply (case_tac "acc_prefix A list (next A a st)")
- apply (simp)
-apply (subgoal_tac "r @ [a] \<noteq> []")
- apply (fast)
-apply (simp)
-done
-
-lemma step2_c:
- "!!st erk r l rest ys yss zs. acc A st (l,rest) erk xs r = (ys#yss, zs) \<Longrightarrow>
-  if acc_prefix A xs st then EX g. ys = r@g & fin A (delta A g st)
-  else (erk \<noteq> [] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs))"
-apply (simp)
-apply (induct "xs")
- apply (simp cong: conj_cong split:split_if_asm)
-apply (simp cong: conj_cong split:split_if_asm)
- apply (rule_tac p = "acc A (start A) ([],list) [] list []" in PairE)
- apply (rename_tac vss lrst)
- apply (simp)
- apply (case_tac "acc_prefix A list (next A a st)")
-  apply (rule_tac f = "%k. a#k" in ex_special)
-  apply (simp)
-  apply (rule_tac t = "%k. ys=r@a#k" and s = "%k. ys=(r@[a])@k" in subst)
-   apply (simp)
-  apply (fast)
- apply (rule_tac x = "[a]" in exI)
- apply (simp)
- apply (subgoal_tac "r @ [a] ~= []")
-  apply (rule sym)
-  apply (fast)
- apply (simp)
-apply (intro strip)
-apply (rule_tac f = "%k. a#k" in ex_special)
-apply (simp)
-apply (rule_tac t = "%k. ys=r@a#k" and s = "%k. ys=(r@[a])@k" in subst)
- apply (simp)
-apply (fast)
-done
-
-lemma step2_d:
- "!!st erk r l rest ys yss zs. acc A st (l,rest) erk xs r = (ys#yss, zs) \<Longrightarrow>
-  if acc_prefix A xs st
-  then acc A (start A) ([],concat(yss)@zs) [] (concat(yss)@zs) [] = (yss,zs)
-  else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs))"
-apply (simp)
-apply (induct "xs")
- apply (simp cong: conj_cong split:split_if_asm)
-apply (simp cong: conj_cong split:split_if_asm)
-apply (rule_tac p = "acc A (start A) ([],list) [] list []" in PairE)
-apply (rename_tac vss lrst)
-apply (simp)
-apply (case_tac "acc_prefix A list (next A a st)")
- apply (simp)
-apply (subgoal_tac "acc A (start A) ([],list) [] list [] = (yss,zs)")
- prefer 2
- apply (simp)
- apply (subgoal_tac "r@[a] ~= []")
-  apply (fast)
- apply (simp)
-apply (subgoal_tac "concat(yss) @ zs = list")
- apply (simp)
-apply (case_tac "yss = []")
- apply (simp)
- apply (fast dest!: no_acc)
-apply (erule neq_Nil_conv[THEN iffD1, THEN exE])
-apply (auto simp add:step2_a)
-done
-
-lemma step2_e:
-"!!st erk r p ys yss zs. acc A st p erk xs r = (ys#yss, zs) \<Longrightarrow>
-  if acc_prefix A xs st
-  then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (delta A as st))
-  else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p)"
-apply (simp)
-apply (induct "xs")
- apply (simp cong: conj_cong split:split_if_asm)
-apply (simp cong: conj_cong split:split_if_asm)
-apply (case_tac "acc_prefix A list (next A a st)")
-  apply (rule_tac f = "%k. a#k" in ex_special)
-  apply (rule_tac t = "%k. ys=r@a#k" and s = "%k. ys=(r@[a])@k" in subst)
-   apply (simp)
-  apply (rule_tac P = "%k. ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (delta A as (next A a st)))" in exE)
-   apply fastsimp
-  apply (rule_tac x = "x" in exI)
-  apply (simp)
-  apply (rule allI)
-  apply (case_tac "as")
-   apply (simp)
-  apply (simp cong:conj_cong)
- apply (rule_tac f = "%k. a#k" in ex_special)
- apply (rule_tac t = "%k. ys=r@a#k" and s = "%k. ys=(r@[a])@k" in subst)
-  apply (simp)
- apply(subgoal_tac "ys = r @ [a]")
-  prefer 2 apply fastsimp
- apply(rule_tac x = "[]" in exI)
- apply simp
- apply (rule allI)
- apply (case_tac "as")
-  apply (simp)
- apply (simp add: acc_prefix_def cong: conj_cong)
- apply (fastsimp)
-apply (intro strip)
-apply (rule_tac P = "%k. ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (delta A as (next A a st)))" in exE)
- apply rules
-apply simp
-apply(elim conjE exE)
-apply (rule allI)
-apply (case_tac as)
- apply (simp)
-apply (simp cong: conj_cong)
-done
-
-declare split_paired_All[simp]
-
-lemma auto_chopper_is_auto_chopper:
- "is_auto_chopper(auto_chopper)"
-apply(unfold accepts_def is_auto_chopper_def auto_chopper_def
-             Chopper.is_longest_prefix_chopper_def)
-apply(rule no_acc allI impI conjI | assumption)+
- apply (rule mp)
-  prefer 2 apply (erule step2_b)
- apply (simp)
-apply (rule conjI)
- apply (rule mp)
-  prefer 2 apply (erule step2_c)
- apply (simp)
-apply (rule conjI)
- apply (simp add: step2_a)
-apply (rule conjI)
- apply (rule mp)
-  prefer 2 apply (erule step2_d)
- apply (simp)
-apply (rule mp)
- prefer 2 apply (erule step2_e)
-apply (simp)
-done
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/AutoChopper1.thy
--- a/src/HOL/Lex/AutoChopper1.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      HOL/Lex/AutoChopper1.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1997 TUM
-
-This is a version of theory AutoChopper base on a non-primrec definition of
-`acc'. Advantage: does not need lazy evaluation for reasonable (quadratic?)
-performance.
-
-Verification:
-1. Via AutoChopper.acc using
-   Claim: acc A xs s [] [] [] = AutoChopper.acc xs s [] [] ([],xs) A
-   Generalization?
-2. Directly.
-   Hope: acc is easier to verify than AutoChopper.acc because simpler.
-
-No proofs yet.
-*)
-
-theory AutoChopper1 = DA + Chopper:
-
-consts
-  acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
-          => 'a list list * 'a list"
-recdef acc "inv_image (less_than <*lex*> less_than)
-              (%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs,
-                                     length ys))"
-"acc(A,[],s,xss,zs,[]) = (xss, zs)"
-"acc(A,[],s,xss,zs,x#xs) = acc(A,zs,start A, xss @ [x#xs],[],[])"
-"acc(A,y#ys,s,xss,zs,xs) =
-  (let s' = next A y s;
-      zs' = (if fin A s' then [] else zs@[y]);
-      xs' = (if fin A s' then xs@zs@[y] else xs)
-   in acc(A,ys,s',xss,zs',xs'))"
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/AutoMaxChop.thy
--- a/src/HOL/Lex/AutoMaxChop.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-(*  Title:      HOL/Lex/AutoMaxChop.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-theory AutoMaxChop = DA + MaxChop:
-
-consts
- auto_split :: "('a,'s)da => 's  => 'a list * 'a list => 'a list => 'a splitter"
-primrec
-"auto_split A q res ps []     = (if fin A q then (ps,[]) else res)"
-"auto_split A q res ps (x#xs) =
-   auto_split A (next A x q) (if fin A q then (ps,x#xs) else res) (ps@[x]) xs"
-
-constdefs
- auto_chop :: "('a,'s)da => 'a chopper"
-"auto_chop A == chop (%xs. auto_split A (start A) ([],xs) [] xs)"
-
-
-lemma delta_snoc: "delta A (xs@[y]) q = next A y (delta A xs q)";
-by simp
-
-lemma auto_split_lemma:
- "!!q ps res. auto_split A (delta A ps q) res ps xs =
-              maxsplit (%ys. fin A (delta A ys q)) res ps xs"
-apply (induct xs)
- apply simp
-apply (simp add: delta_snoc[symmetric] del: delta_append)
-done
-
-lemma auto_split_is_maxsplit:
- "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs"
-apply (unfold accepts_def)
-apply (subst delta_Nil[where s = "start A", symmetric])
-apply (subst auto_split_lemma)
-apply simp
-done
-
-lemma is_maxsplitter_auto_split:
- "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)"
-by (simp add: auto_split_is_maxsplit is_maxsplitter_maxsplit)
-
-
-lemma is_maxchopper_auto_chop:
- "is_maxchopper (accepts A) (auto_chop A)"
-apply (unfold auto_chop_def)
-apply (rule is_maxchopper_chop)
-apply (rule is_maxsplitter_auto_split)
-done
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/AutoProj.thy
--- a/src/HOL/Lex/AutoProj.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      HOL/Lex/AutoProj.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Is there an optimal order of arguments for `next'?
-Currently we can have laws like `delta A (a#w) = delta A w o delta A a'
-Otherwise we could have `acceps A == fin A o delta A (start A)'
-and use foldl instead of foldl2.
-*)
-
-theory AutoProj = Main:
-
-constdefs
- start :: "'a * 'b * 'c => 'a"
-"start A == fst A"
- "next" :: "'a * 'b * 'c => 'b"
-"next A == fst(snd(A))"
- fin :: "'a * 'b * 'c => 'c"
-"fin A == snd(snd(A))"
-
-lemma [simp]: "start(q,d,f) = q"
-by(simp add:start_def)
-
-lemma [simp]: "next(q,d,f) = d"
-by(simp add:next_def)
-
-lemma [simp]: "fin(q,d,f) = f"
-by(simp add:fin_def)
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/Automata.thy
--- a/src/HOL/Lex/Automata.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-(*  Title:      HOL/Lex/Automata.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Conversions between different kinds of automata
-*)
-
-theory Automata = DA + NAe:
-
-constdefs
- na2da :: "('a,'s)na => ('a,'s set)da"
-"na2da A == ({start A}, %a Q. Union(next A a ` Q), %Q. ? q:Q. fin A q)"
-
- nae2da :: "('a,'s)nae => ('a,'s set)da"
-"nae2da A == ({start A},
-              %a Q. Union(next A (Some a) ` ((eps A)^* `` Q)),
-              %Q. ? p: (eps A)^* `` Q. fin A p)"
-
-(*** Equivalence of NA and DA ***)
-
-lemma DA_delta_is_lift_NA_delta:
- "!!Q. DA.delta (na2da A) w Q = Union(NA.delta A w ` Q)"
-by (induct w)(auto simp:na2da_def)
-
-lemma NA_DA_equiv:
-  "NA.accepts A w = DA.accepts (na2da A) w"
-apply (simp add: DA.accepts_def NA.accepts_def DA_delta_is_lift_NA_delta)
-apply (simp add: na2da_def)
-done
-
-(*** Direct equivalence of NAe and DA ***)
-
-lemma espclosure_DA_delta_is_steps:
- "!!Q. (eps A)^* `` (DA.delta (nae2da A) w Q) = steps A w `` Q";
-apply (induct w)
- apply(simp)
-apply (simp add: step_def nae2da_def)
-apply (blast)
-done
-
-lemma NAe_DA_equiv:
-  "DA.accepts (nae2da A) w = NAe.accepts A w"
-proof -
-  have "!!Q. fin (nae2da A) Q = (EX q : (eps A)^* `` Q. fin A q)"
-    by(simp add:nae2da_def)
-  thus ?thesis
-    apply(simp add:espclosure_DA_delta_is_steps NAe.accepts_def DA.accepts_def)
-    apply(simp add:nae2da_def)
-    apply blast
-    done
-qed
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/Chopper.thy
--- a/src/HOL/Lex/Chopper.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(*  Title:      HOL/Lex/Chopper.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1995 TUM
-
-A 'chopper' is a function which returns
-  1. a chopped up prefix of the input string
-  2. together with the remaining suffix.
-
-It is a longest_prefix_chopper if it
-  1. chops up as much of the input as possible and
-  2. chops it up into the longest substrings possible.
-
-A chopper is parametrized by a language ('a list => bool),
-i.e. a set of strings.
-*)
-
-theory Chopper = List_Prefix:
-
-types 'a chopper = "'a list => 'a list list * 'a list"
-
-constdefs
-  is_longest_prefix_chopper :: "('a list => bool) => 'a chopper => bool"
- "is_longest_prefix_chopper L chopper == !xs.
-       (!zs. chopper(xs) = ([],zs) -->
-             zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &
-       (!ys yss zs. chopper(xs) = (ys#yss,zs) -->
-          ys ~= [] & L(ys) & xs=ys@concat(yss)@zs &
-          chopper(concat(yss)@zs) = (yss,zs) &
-          (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/DA.thy
--- a/src/HOL/Lex/DA.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      HOL/Lex/DA.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Deterministic automata
-*)
-
-theory DA = AutoProj:
-
-types ('a,'s)da = "'s * ('a => 's => 's) * ('s => bool)"
-
-constdefs
- foldl2 :: "('a => 'b => 'b) => 'a list => 'b => 'b"
-"foldl2 f xs a == foldl (%a b. f b a) a xs"
-
- delta :: "('a,'s)da => 'a list => 's => 's"
-"delta A == foldl2 (next A)"
-
- accepts :: "('a,'s)da => 'a list => bool"
-"accepts A == %w. fin A (delta A w (start A))"
-
-lemma [simp]: "foldl2 f [] a = a & foldl2 f (x#xs) a = foldl2 f xs (f x a)"
-by(simp add:foldl2_def)
-
-lemma delta_Nil[simp]: "delta A [] s = s"
-by(simp add:delta_def)
-
-lemma delta_Cons[simp]: "delta A (a#w) s = delta A w (next A a s)"
-by(simp add:delta_def)
-
-lemma delta_append[simp]:
- "!!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)"
-by(induct xs, simp_all)
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/MaxChop.thy
--- a/src/HOL/Lex/MaxChop.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,126 +0,0 @@
-(*  Title:      HOL/Lex/MaxChop.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-theory MaxChop = MaxPrefix:
-
-types   'a chopper = "'a list => 'a list list * 'a list"
-
-constdefs
- is_maxchopper :: "('a list => bool) => 'a chopper => bool"
-"is_maxchopper P chopper ==
- !xs zs yss.
-    (chopper(xs) = (yss,zs)) =
-    (xs = concat yss @ zs & (!ys : set yss. ys ~= []) &
-     (case yss of
-        [] => is_maxpref P [] xs
-      | us#uss => is_maxpref P us xs & chopper(concat(uss)@zs) = (uss,zs)))"
-
-constdefs
- reducing :: "'a splitter => bool"
-"reducing splitf ==
- !xs ys zs. splitf xs = (ys,zs) & ys ~= [] --> length zs < length xs"
-
-consts
- chopr :: "'a splitter * 'a list => 'a list list * 'a list"
-recdef (permissive) chopr "measure (length o snd)"
-"chopr (splitf,xs) = (if reducing splitf
-                      then let pp = splitf xs
-                           in if fst(pp)=[] then ([],xs)
-                           else let qq = chopr (splitf,snd pp)
-                                in (fst pp # fst qq,snd qq)
-                      else arbitrary)"
-
-constdefs
- chop :: "'a splitter  => 'a chopper"
-"chop splitf xs == chopr(splitf,xs)"
-
-(* Termination of chop *)
-
-lemma reducing_maxsplit: "reducing(%qs. maxsplit P ([],qs) [] qs)"
-by (simp add: reducing_def maxsplit_eq)
-
-recdef_tc chopr_tc: chopr
-apply(unfold reducing_def)
-apply(blast dest: sym)
-done
-
-lemmas chopr_rule = chopr.simps[OF chopr_tc]
-
-lemma chop_rule: "reducing splitf ==>
-  chop splitf xs = (let (pre,post) = splitf xs
-                    in if pre=[] then ([],xs)
-                       else let (xss,zs) = chop splitf post
-                            in (pre#xss,zs))"
-apply(simp add: chop_def chopr_rule)
-apply(simp add: chop_def Let_def split: split_split)
-done
-
-lemma is_maxsplitter_reducing:
- "is_maxsplitter P splitf ==> reducing splitf";
-by(simp add:is_maxsplitter_def reducing_def)
-
-lemma chop_concat[rule_format]: "is_maxsplitter P splitf ==>
-  (!yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs)"
-apply (induct xs rule:length_induct)
-apply (simp (no_asm_simp) split del: split_if
-            add: chop_rule[OF is_maxsplitter_reducing])
-apply (simp add: Let_def is_maxsplitter_def split: split_split)
-done
-
-lemma chop_nonempty: "is_maxsplitter P splitf ==>
-  !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])"
-apply (induct xs rule:length_induct)
-apply (simp (no_asm_simp) add: chop_rule is_maxsplitter_reducing)
-apply (simp add: Let_def is_maxsplitter_def split: split_split)
-apply (intro allI impI)
-apply (rule ballI)
-apply (erule exE)
-apply (erule allE)
-apply auto
-done
-
-lemma is_maxchopper_chop:
- assumes prem: "is_maxsplitter P splitf" shows "is_maxchopper P (chop splitf)"
-apply(unfold is_maxchopper_def)
-apply clarify
-apply (rule iffI)
- apply (rule conjI)
-  apply (erule chop_concat[OF prem])
- apply (rule conjI)
-  apply (erule prem[THEN chop_nonempty[THEN spec, THEN spec, THEN mp]])
- apply (erule rev_mp)
- apply (subst prem[THEN is_maxsplitter_reducing[THEN chop_rule]])
- apply (simp add: Let_def prem[simplified is_maxsplitter_def]
-             split: split_split)
- apply clarify
- apply (rule conjI)
-  apply (clarify)
- apply (clarify)
- apply simp
- apply (frule chop_concat[OF prem])
- apply (clarify)
-apply (subst prem[THEN is_maxsplitter_reducing, THEN chop_rule])
-apply (simp add: Let_def prem[simplified is_maxsplitter_def]
-             split: split_split)
-apply (clarify)
-apply (rename_tac xs1 ys1 xss1 ys)
-apply (simp split: list.split_asm)
- apply (simp add: is_maxpref_def)
- apply (blast intro: prefix_append[THEN iffD2])
-apply (rule conjI)
- apply (clarify)
- apply (simp (no_asm_use) add: is_maxpref_def)
- apply (blast intro: prefix_append[THEN iffD2])
-apply (clarify)
-apply (rename_tac us uss)
-apply (subgoal_tac "xs1=us")
- apply simp
-apply simp
-apply (simp (no_asm_use) add: is_maxpref_def)
-apply (blast intro: prefix_append[THEN iffD2] order_antisym)
-done
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/MaxPrefix.thy
--- a/src/HOL/Lex/MaxPrefix.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-(*  Title:      HOL/Lex/MaxPrefix.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-theory MaxPrefix = List_Prefix:
-
-constdefs
- is_maxpref :: "('a list => bool) => 'a list => 'a list => bool"
-"is_maxpref P xs ys ==
- xs <= ys & (xs=[] | P xs) & (!zs. zs <= ys & P zs --> zs <= xs)"
-
-types 'a splitter = "'a list => 'a list * 'a list"
-
-constdefs
- is_maxsplitter :: "('a list => bool) => 'a splitter => bool"
-"is_maxsplitter P f ==
- (!xs ps qs. f xs = (ps,qs) = (xs=ps@qs & is_maxpref P ps xs))"
-
-consts
- maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => 'a splitter"
-primrec
-"maxsplit P res ps []     = (if P ps then (ps,[]) else res)"
-"maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res)
-                                     (ps@[q]) qs"
-
-declare split_if[split del]
-
-lemma maxsplit_lemma: "!!(ps::'a list) res.
-  (maxsplit P res ps qs = (xs,ys)) =
-  (if EX us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs)
-   else (xs,ys)=res)"
-apply(unfold is_maxpref_def)
-apply (induct "qs")
- apply (simp split: split_if)
- apply blast
-apply simp
-apply (erule thin_rl)
-apply clarify
-apply (case_tac "EX us. us <= list & P (ps @ a # us)")
- apply (subgoal_tac "EX us. us <= a # list & P (ps @ us)")
-  apply simp
- apply (blast intro: prefix_Cons[THEN iffD2])
-apply (subgoal_tac "~P(ps@[a])")
- prefer 2 apply blast
-apply (simp (no_asm_simp))
-apply (case_tac "EX us. us <= a#list & P (ps @ us)")
- apply simp
- apply clarify
- apply (case_tac "us")
-  apply (rule iffI)
-   apply (simp add: prefix_Cons prefix_append)
-   apply blast
-  apply (simp add: prefix_Cons prefix_append)
-  apply clarify
-  apply (erule disjE)
-   apply (fast dest: order_antisym)
-  apply clarify
-  apply (erule disjE)
-   apply clarify
-   apply simp
-  apply (erule disjE)
-   apply clarify
-   apply simp
-  apply blast
- apply simp
-apply (subgoal_tac "~P(ps)")
-apply (simp (no_asm_simp))
-apply fastsimp
-done
-
-declare split_if[split add]
-
-lemma is_maxpref_Nil[simp]:
- "~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])"
-apply(unfold is_maxpref_def)
-apply blast
-done
-
-lemma is_maxsplitter_maxsplit:
- "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)"
-apply(unfold is_maxsplitter_def)
-apply (simp add: maxsplit_lemma)
-apply (fastsimp)
-done
-
-lemmas maxsplit_eq = is_maxsplitter_maxsplit[simplified is_maxsplitter_def]
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/NA.thy
--- a/src/HOL/Lex/NA.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(*  Title:      HOL/Lex/NA.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Nondeterministic automata
-*)
-
-theory NA = AutoProj:
-
-types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)"
-
-consts delta :: "('a,'s)na => 'a list => 's => 's set"
-primrec
-"delta A []    p = {p}"
-"delta A (a#w) p = Union(delta A w ` next A a p)"
-
-constdefs
- accepts :: "('a,'s)na => 'a list => bool"
-"accepts A w == EX q : delta A w (start A). fin A q"
-
- step :: "('a,'s)na => 'a => ('s * 's)set"
-"step A a == {(p,q) . q : next A a p}"
-
-consts steps :: "('a,'s)na => 'a list => ('s * 's)set"
-primrec
-"steps A [] = Id"
-"steps A (a#w) = steps A w  O  step A a"
-
-lemma steps_append[simp]:
- "steps A (v@w) = steps A w  O  steps A v";
-by(induct v, simp_all add:O_assoc)
-
-lemma in_steps_append[iff]:
-  "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))"
-apply(rule steps_append[THEN equalityE])
-apply blast
-done
-
-lemma delta_conv_steps: "!!p. delta A w p = {q. (p,q) : steps A w}"
-by(induct w)(auto simp:step_def)
-
-lemma accepts_conv_steps:
- "accepts A w = (? q. (start A,q) : steps A w & fin A q)";
-by(simp add: delta_conv_steps accepts_def)
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/NAe.thy
--- a/src/HOL/Lex/NAe.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(*  Title:      HOL/Lex/NAe.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Nondeterministic automata with epsilon transitions
-*)
-
-theory NAe = NA:
-
-types ('a,'s)nae = "('a option,'s)na"
-
-syntax eps :: "('a,'s)nae => ('s * 's)set"
-translations "eps A" == "step A None"
-
-consts steps :: "('a,'s)nae => 'a list =>   ('s * 's)set"
-primrec
-"steps A [] = (eps A)^*"
-"steps A (a#w) = steps A w  O  step A (Some a)  O  (eps A)^*"
-
-constdefs
- accepts :: "('a,'s)nae => 'a list => bool"
-"accepts A w == ? q. (start A,q) : steps A w & fin A q"
-
-(* not really used:
-consts delta :: "('a,'s)nae => 'a list => 's => 's set"
-primrec
-"delta A [] s = (eps A)^* `` {s}"
-"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* `` {s}))"
-*)
-
-lemma steps_epsclosure[simp]: "steps A w O (eps A)^* = steps A w"
-by(cases w)(simp_all add:O_assoc)
-
-lemma in_steps_epsclosure:
-  "[| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w"
-apply(rule steps_epsclosure[THEN equalityE])
-apply blast
-done
-
-lemma epsclosure_steps: "(eps A)^* O steps A w = steps A w";
-apply(induct w)
- apply simp
-apply(simp add:O_assoc[symmetric])
-done
-
-lemma in_epsclosure_steps:
-  "[| (p,q) : steps A w; (q,r) : (eps A)^* |] ==> (p,r) : steps A w"
-apply(rule epsclosure_steps[THEN equalityE])
-apply blast
-done
-
-lemma steps_append[simp]:  "steps A (v@w) = steps A w  O  steps A v"
-by(induct v)(simp_all add:O_assoc)
-
-lemma in_steps_append[iff]:
-  "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))"
-apply(rule steps_append[THEN equalityE])
-apply blast
-done
-
-(* Equivalence of steps and delta
-* Use "(? x : f ` A. P x) = (? a:A. P(f x))" ?? *
-Goal "!p. (p,q) : steps A w = (q : delta A w p)";
-by (induct_tac "w" 1);
- by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
-by (Blast_tac 1);
-qed_spec_mp "steps_equiv_delta";
-*)
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/README.html
--- a/src/HOL/Lex/README.html	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/Lex/README</TITLE></HEAD>
-<BODY>
-
-<H1>A Simplified Scanner Generator</H1>
-
-This directory contains the theories for the functional scanner generator
-described
-<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols98.html">
-here</A>. In contrast to the paper, the latest version of the theories
-provides a fully executable scanner generator. The non-executable bits
-(transitive closure) have been eliminated by going from regular expressions
-directly to nondeterministic automata, thus bypassing epsilon-moves.
-<br>
-<br>
-Overview:
-<dl>
-<dt>Automata</dt>
-<dd>AutoProj, NA, NAe, DA, Automata</dd>
-<dt>Regular expressions and their conversion to automata</dt>
-<dd>RegSet, RegExp, RegExp2NA, RegExp2NAe</dd>
-<dt>Scanning</dt>
-<dd>Prefix, MaxPrefix, MaxChop, AutoMaxChop, Scanner</dd>
-</dl>
-In addition there are some bits and pieces:
-<ul>
-<li> Regset_of_nat_DA describes the translation of deterministic automata
-     into regular sets. Should be completed to translate finite automata
-     into regular expressions.
-<li> Chopper, AutoChopper and AutoChopper1 are old versions of the scanner
-     (excluding regular expressions). Mainly of historic interest.
-</ul>
-
-</BODY>
-</HTML>
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/ROOT.ML
--- a/src/HOL/Lex/ROOT.ML	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  Title:      HOL/Lex/ROOT.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-time_use_thy "AutoChopper";
-time_use_thy "AutoChopper1";
-time_use_thy "AutoMaxChop";
-time_use_thy "RegSet_of_nat_DA";
-time_use_thy "Scanner";
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/RegExp.thy
--- a/src/HOL/Lex/RegExp.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      HOL/Lex/RegExp.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Regular expressions
-*)
-
-RegExp = RegSet +
-
-datatype 'a rexp = Empty
-                 | Atom 'a
-                 | Or   ('a rexp) ('a rexp)
-                 | Conc ('a rexp) ('a rexp)
-                 | Star ('a rexp)
-
-consts lang :: 'a rexp => 'a list set
-primrec
-"lang Empty = {}"
-"lang (Atom a) = {[a]}"
-"lang (Or el er) = (lang el) Un (lang er)"
-"lang (Conc el er) = RegSet.conc (lang el) (lang er)"
-"lang (Star e) = RegSet.star(lang e)"
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/RegExp2NA.thy
--- a/src/HOL/Lex/RegExp2NA.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,440 +0,0 @@
-(*  Title:      HOL/Lex/RegExp2NA.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Conversion of regular expressions *directly*
-into nondeterministic automata *without* epsilon transitions
-*)
-
-theory RegExp2NA = RegExp + NA:
-
-types 'a bitsNA = "('a,bool list)na"
-
-syntax "##" :: "'a => 'a list set => 'a list set" (infixr 65)
-translations "x ## S" == "Cons x ` S"
-
-constdefs
- atom  :: "'a => 'a bitsNA"
-"atom a == ([True],
-            %b s. if s=[True] & b=a then {[False]} else {},
-            %s. s=[False])"
-
- or :: "'a bitsNA => 'a bitsNA => 'a bitsNA"
-"or == %(ql,dl,fl)(qr,dr,fr).
-   ([],
-    %a s. case s of
-            [] => (True ## dl a ql) Un (False ## dr a qr)
-          | left#s => if left then True ## dl a s
-                              else False ## dr a s,
-    %s. case s of [] => (fl ql | fr qr)
-                | left#s => if left then fl s else fr s)"
-
- conc :: "'a bitsNA => 'a bitsNA => 'a bitsNA"
-"conc == %(ql,dl,fl)(qr,dr,fr).
-   (True#ql,
-    %a s. case s of
-            [] => {}
-          | left#s => if left then (True ## dl a s) Un
-                                   (if fl s then False ## dr a qr else {})
-                              else False ## dr a s,
-    %s. case s of [] => False | left#s => left & fl s & fr qr | ~left & fr s)"
-
- epsilon :: "'a bitsNA"
-"epsilon == ([],%a s. {}, %s. s=[])"
-
- plus :: "'a bitsNA => 'a bitsNA"
-"plus == %(q,d,f). (q, %a s. d a s Un (if f s then d a q else {}), f)"
-
- star :: "'a bitsNA => 'a bitsNA"
-"star A == or epsilon (plus A)"
-
-consts rexp2na :: "'a rexp => 'a bitsNA"
-primrec
-"rexp2na Empty      = ([], %a s. {}, %s. False)"
-"rexp2na(Atom a)    = atom a"
-"rexp2na(Or r s)    = or   (rexp2na r) (rexp2na s)"
-"rexp2na(Conc r s)  = conc (rexp2na r) (rexp2na s)"
-"rexp2na(Star r)    = star (rexp2na r)"
-
-declare split_paired_all[simp]
-
-(******************************************************)
-(*                       atom                         *)
-(******************************************************)
-
-lemma fin_atom: "(fin (atom a) q) = (q = [False])"
-by(simp add:atom_def)
-
-lemma start_atom: "start (atom a) = [True]"
-by(simp add:atom_def)
-
-lemma in_step_atom_Some[simp]:
- "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)"
-by (simp add: atom_def step_def)
-
-lemma False_False_in_steps_atom:
- "([False],[False]) : steps (atom a) w = (w = [])"
-apply (induct "w")
- apply simp
-apply (simp add: rel_comp_def)
-done
-
-lemma start_fin_in_steps_atom:
- "(start (atom a), [False]) : steps (atom a) w = (w = [a])"
-apply (induct "w")
- apply (simp add: start_atom)
-apply (simp add: False_False_in_steps_atom rel_comp_def start_atom)
-done
-
-lemma accepts_atom:
- "accepts (atom a) w = (w = [a])"
-by (simp add: accepts_conv_steps start_fin_in_steps_atom fin_atom)
-
-(******************************************************)
-(*                      or                            *)
-(******************************************************)
-
-(***** lift True/False over fin *****)
-
-lemma fin_or_True[iff]:
- "!!L R. fin (or L R) (True#p) = fin L p"
-by(simp add:or_def)
-
-lemma fin_or_False[iff]:
- "!!L R. fin (or L R) (False#p) = fin R p"
-by(simp add:or_def)
-
-(***** lift True/False over step *****)
-
-lemma True_in_step_or[iff]:
-"!!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)"
-apply (simp add:or_def step_def)
-apply blast
-done
-
-lemma False_in_step_or[iff]:
-"!!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)"
-apply (simp add:or_def step_def)
-apply blast
-done
-
-
-(***** lift True/False over steps *****)
-
-lemma lift_True_over_steps_or[iff]:
- "!!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)"
-apply (induct "w")
- apply force
-apply force
-done
-
-lemma lift_False_over_steps_or[iff]:
- "!!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)"
-apply (induct "w")
- apply force
-apply force
-done
-
-(** From the start  **)
-
-lemma start_step_or[iff]:
- "!!L R. (start(or L R),q) : step(or L R) a = 
-         (? p. (q = True#p & (start L,p) : step L a) | 
-               (q = False#p & (start R,p) : step R a))"
-apply (simp add:or_def step_def)
-apply blast
-done
-
-lemma steps_or:
- "(start(or L R), q) : steps (or L R) w = 
-  ( (w = [] & q = start(or L R)) | 
-    (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | 
-                      q = False # p & (start R,p) : steps R w)))"
-apply (case_tac "w")
- apply (simp)
- apply blast
-apply (simp)
-apply blast
-done
-
-lemma fin_start_or[iff]:
- "!!L R. fin (or L R) (start(or L R)) = (fin L (start L) | fin R (start R))"
-by (simp add:or_def)
-
-lemma accepts_or[iff]:
- "accepts (or L R) w = (accepts L w | accepts R w)"
-apply (simp add: accepts_conv_steps steps_or)
-(* get rid of case_tac: *)
-apply (case_tac "w = []")
- apply auto
-done
-
-(******************************************************)
-(*                      conc                        *)
-(******************************************************)
-
-(** True/False in fin **)
-
-lemma fin_conc_True[iff]:
- "!!L R. fin (conc L R) (True#p) = (fin L p & fin R (start R))"
-by(simp add:conc_def)
-
-lemma fin_conc_False[iff]:
- "!!L R. fin (conc L R) (False#p) = fin R p"
-by(simp add:conc_def)
-
-
-(** True/False in step **)
-
-lemma True_step_conc[iff]:
- "!!L R. (True#p,q) : step (conc L R) a = 
-        ((? r. q=True#r & (p,r): step L a) | 
-         (fin L p & (? r. q=False#r & (start R,r) : step R a)))"
-apply (simp add:conc_def step_def)
-apply blast
-done
-
-lemma False_step_conc[iff]:
- "!!L R. (False#p,q) : step (conc L R) a = 
-       (? r. q = False#r & (p,r) : step R a)"
-apply (simp add:conc_def step_def)
-apply blast
-done
-
-(** False in steps **)
-
-lemma False_steps_conc[iff]:
- "!!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)"
-apply (induct "w")
- apply fastsimp
-apply force
-done
-
-(** True in steps **)
-
-lemma True_True_steps_concI:
- "!!L R p. (p,q) : steps L w ==> (True#p,True#q) : steps (conc L R) w"
-apply (induct "w")
- apply simp
-apply simp
-apply fast
-done
-
-lemma True_False_step_conc[iff]:
- "!!L R. (True#p,False#q) : step (conc L R) a = 
-         (fin L p & (start R,q) : step R a)"
-by simp
-
-lemma True_steps_concD[rule_format]:
- "!p. (True#p,q) : steps (conc L R) w --> 
-     ((? r. (p,r) : steps L w & q = True#r)  | 
-  (? u a v. w = u@a#v & 
-            (? r. (p,r) : steps L u & fin L r & 
-            (? s. (start R,s) : step R a & 
-            (? t. (s,t) : steps R v & q = False#t)))))"
-apply (induct "w")
- apply simp
-apply simp
-apply (clarify del:disjCI)
-apply (erule disjE)
- apply (clarify del:disjCI)
- apply (erule allE, erule impE, assumption)
- apply (erule disjE)
-  apply blast
- apply (rule disjI2)
- apply (clarify)
- apply simp
- apply (rule_tac x = "a#u" in exI)
- apply simp
- apply blast
-apply (rule disjI2)
-apply (clarify)
-apply simp
-apply (rule_tac x = "[]" in exI)
-apply simp
-apply blast
-done
-
-lemma True_steps_conc:
- "(True#p,q) : steps (conc L R) w = 
- ((? r. (p,r) : steps L w & q = True#r)  | 
-  (? u a v. w = u@a#v & 
-            (? r. (p,r) : steps L u & fin L r & 
-            (? s. (start R,s) : step R a & 
-            (? t. (s,t) : steps R v & q = False#t)))))"
-by(force dest!: True_steps_concD intro!: True_True_steps_concI)
-
-(** starting from the start **)
-
-lemma start_conc:
-  "!!L R. start(conc L R) = True#start L"
-by (simp add:conc_def)
-
-lemma final_conc:
- "!!L R. fin(conc L R) p = ((fin R (start R) & (? s. p = True#s & fin L s)) | 
-                           (? s. p = False#s & fin R s))"
-apply (simp add:conc_def split: list.split)
-apply blast
-done
-
-lemma accepts_conc:
- "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)"
-apply (simp add: accepts_conv_steps True_steps_conc final_conc start_conc)
-apply (rule iffI)
- apply (clarify)
- apply (erule disjE)
-  apply (clarify)
-  apply (erule disjE)
-   apply (rule_tac x = "w" in exI)
-   apply simp
-   apply blast
-  apply blast
- apply (erule disjE)
-  apply blast
- apply (clarify)
- apply (rule_tac x = "u" in exI)
- apply simp
- apply blast
-apply (clarify)
-apply (case_tac "v")
- apply simp
- apply blast
-apply simp
-apply blast
-done
-
-(******************************************************)
-(*                     epsilon                        *)
-(******************************************************)
-
-lemma step_epsilon[simp]: "step epsilon a = {}"
-by(simp add:epsilon_def step_def)
-
-lemma steps_epsilon: "((p,q) : steps epsilon w) = (w=[] & p=q)"
-by (induct "w") auto
-
-lemma accepts_epsilon[iff]: "accepts epsilon w = (w = [])"
-apply (simp add: steps_epsilon accepts_conv_steps)
-apply (simp add: epsilon_def)
-done
-
-(******************************************************)
-(*                       plus                         *)
-(******************************************************)
-
-lemma start_plus[simp]: "!!A. start (plus A) = start A"
-by(simp add:plus_def)
-
-lemma fin_plus[iff]: "!!A. fin (plus A) = fin A"
-by(simp add:plus_def)
-
-lemma step_plusI:
-  "!!A. (p,q) : step A a ==> (p,q) : step (plus A) a"
-by(simp add:plus_def step_def)
-
-lemma steps_plusI: "!!p. (p,q) : steps A w ==> (p,q) : steps (plus A) w"
-apply (induct "w")
- apply simp
-apply simp
-apply (blast intro: step_plusI)
-done
-
-lemma step_plus_conv[iff]:
- "!!A. (p,r): step (plus A) a = 
-       ( (p,r): step A a | fin A p & (start A,r) : step A a )"
-by(simp add:plus_def step_def)
-
-lemma fin_steps_plusI:
- "[| (start A,q) : steps A u; u ~= []; fin A p |] 
- ==> (p,q) : steps (plus A) u"
-apply (case_tac "u")
- apply blast
-apply simp
-apply (blast intro: steps_plusI)
-done
-
-(* reverse list induction! Complicates matters for conc? *)
-lemma start_steps_plusD[rule_format]:
- "!r. (start A,r) : steps (plus A) w --> 
-     (? us v. w = concat us @ v & 
-              (!u:set us. accepts A u) & 
-              (start A,r) : steps A v)"
-apply (induct w rule: rev_induct)
- apply simp
- apply (rule_tac x = "[]" in exI)
- apply simp
-apply simp
-apply (clarify)
-apply (erule allE, erule impE, assumption)
-apply (clarify)
-apply (erule disjE)
- apply (rule_tac x = "us" in exI)
- apply (simp)
- apply blast
-apply (rule_tac x = "us@[v]" in exI)
-apply (simp add: accepts_conv_steps)
-apply blast
-done
-
-lemma steps_star_cycle[rule_format]:
- "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)"
-apply (simp add: accepts_conv_steps)
-apply (induct us rule: rev_induct)
- apply simp
-apply (rename_tac u us)
-apply simp
-apply (clarify)
-apply (case_tac "us = []")
- apply (simp)
- apply (blast intro: steps_plusI fin_steps_plusI)
-apply (clarify)
-apply (case_tac "u = []")
- apply (simp)
- apply (blast intro: steps_plusI fin_steps_plusI)
-apply (blast intro: steps_plusI fin_steps_plusI)
-done
-
-lemma accepts_plus[iff]:
- "accepts (plus A) w = 
- (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))"
-apply (rule iffI)
- apply (simp add: accepts_conv_steps)
- apply (clarify)
- apply (drule start_steps_plusD)
- apply (clarify)
- apply (rule_tac x = "us@[v]" in exI)
- apply (simp add: accepts_conv_steps)
- apply blast
-apply (blast intro: steps_star_cycle)
-done
-
-(******************************************************)
-(*                       star                         *)
-(******************************************************)
-
-lemma accepts_star:
- "accepts (star A) w = (? us. (!u : set us. accepts A u) & w = concat us)"
-apply(unfold star_def)
-apply (rule iffI)
- apply (clarify)
- apply (erule disjE)
-  apply (rule_tac x = "[]" in exI)
-  apply simp
- apply blast
-apply force
-done
-
-(***** Correctness of r2n *****)
-
-lemma accepts_rexp2na:
- "!!w. accepts (rexp2na r) w = (w : lang r)"
-apply (induct "r")
-    apply (simp add: accepts_conv_steps)
-   apply (simp add: accepts_atom)
-  apply (simp)
- apply (simp add: accepts_conc RegSet.conc_def)
-apply (simp add: accepts_star in_star)
-done
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/RegExp2NAe.thy
--- a/src/HOL/Lex/RegExp2NAe.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,622 +0,0 @@
-(*  Title:      HOL/Lex/RegExp2NAe.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Conversion of regular expressions
-into nondeterministic automata with epsilon transitions
-*)
-
-theory RegExp2NAe = RegExp + NAe:
-
-types 'a bitsNAe = "('a,bool list)nae"
-
-syntax "##" :: "'a => 'a list set => 'a list set" (infixr 65)
-translations "x ## S" == "Cons x ` S"
-
-constdefs
- atom  :: "'a => 'a bitsNAe"
-"atom a == ([True],
-            %b s. if s=[True] & b=Some a then {[False]} else {},
-            %s. s=[False])"
-
- or :: "'a bitsNAe => 'a bitsNAe => 'a bitsNAe"
-"or == %(ql,dl,fl)(qr,dr,fr).
-   ([],
-    %a s. case s of
-            [] => if a=None then {True#ql,False#qr} else {}
-          | left#s => if left then True ## dl a s
-                              else False ## dr a s,
-    %s. case s of [] => False | left#s => if left then fl s else fr s)"
-
- conc :: "'a bitsNAe => 'a bitsNAe => 'a bitsNAe"
-"conc == %(ql,dl,fl)(qr,dr,fr).
-   (True#ql,
-    %a s. case s of
-            [] => {}
-          | left#s => if left then (True ## dl a s) Un
-                                   (if fl s & a=None then {False#qr} else {})
-                              else False ## dr a s,
-    %s. case s of [] => False | left#s => ~left & fr s)"
-
- star :: "'a bitsNAe => 'a bitsNAe"
-"star == %(q,d,f).
-   ([],
-    %a s. case s of
-            [] => if a=None then {True#q} else {}
-          | left#s => if left then (True ## d a s) Un
-                                   (if f s & a=None then {True#q} else {})
-                              else {},
-    %s. case s of [] => True | left#s => left & f s)"
-
-consts rexp2nae :: "'a rexp => 'a bitsNAe"
-primrec
-"rexp2nae Empty      = ([], %a s. {}, %s. False)"
-"rexp2nae(Atom a)    = atom a"
-"rexp2nae(Or r s)    = or   (rexp2nae r) (rexp2nae s)"
-"rexp2nae(Conc r s)  = conc (rexp2nae r) (rexp2nae s)"
-"rexp2nae(Star r)    = star (rexp2nae r)"
-
-declare split_paired_all[simp]
-
-(******************************************************)
-(*                       atom                         *)
-(******************************************************)
-
-lemma fin_atom: "(fin (atom a) q) = (q = [False])"
-by(simp add:atom_def)
-
-lemma start_atom: "start (atom a) = [True]"
-by(simp add:atom_def)
-
-(* Use {x. False} = {}? *)
-
-lemma eps_atom[simp]:
- "eps(atom a) = {}"
-by (simp add:atom_def step_def)
-
-lemma in_step_atom_Some[simp]:
- "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)"
-by (simp add:atom_def step_def)
-
-lemma False_False_in_steps_atom:
-  "([False],[False]) : steps (atom a) w = (w = [])"
-apply (induct "w")
- apply (simp)
-apply (simp add: rel_comp_def)
-done
-
-lemma start_fin_in_steps_atom:
-  "(start (atom a), [False]) : steps (atom a) w = (w = [a])"
-apply (induct "w")
- apply (simp add: start_atom rtrancl_empty)
-apply (simp add: False_False_in_steps_atom rel_comp_def start_atom)
-done
-
-lemma accepts_atom: "accepts (atom a) w = (w = [a])"
-by (simp add: accepts_def start_fin_in_steps_atom fin_atom)
-
-
-(******************************************************)
-(*                      or                            *)
-(******************************************************)
-
-(***** lift True/False over fin *****)
-
-lemma fin_or_True[iff]:
- "!!L R. fin (or L R) (True#p) = fin L p"
-by(simp add:or_def)
-
-lemma fin_or_False[iff]:
- "!!L R. fin (or L R) (False#p) = fin R p"
-by(simp add:or_def)
-
-(***** lift True/False over step *****)
-
-lemma True_in_step_or[iff]:
-"!!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)"
-apply (simp add:or_def step_def)
-apply blast
-done
-
-lemma False_in_step_or[iff]:
-"!!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)"
-apply (simp add:or_def step_def)
-apply blast
-done
-
-
-(***** lift True/False over epsclosure *****)
-
-lemma lemma1a:
- "(tp,tq) : (eps(or L R))^* ==> 
- (!!p. tp = True#p ==> ? q. (p,q) : (eps L)^* & tq = True#q)"
-apply (induct rule:rtrancl_induct)
- apply (blast)
-apply (clarify)
-apply (simp)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma lemma1b:
- "(tp,tq) : (eps(or L R))^* ==> 
- (!!p. tp = False#p ==> ? q. (p,q) : (eps R)^* & tq = False#q)"
-apply (induct rule:rtrancl_induct)
- apply (blast)
-apply (clarify)
-apply (simp)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma lemma2a:
- "(p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(or L R))^*"
-apply (induct rule: rtrancl_induct)
- apply (blast)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma lemma2b:
- "(p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(or L R))^*"
-apply (induct rule: rtrancl_induct)
- apply (blast)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma True_epsclosure_or[iff]:
- "(True#p,q) : (eps(or L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)"
-by (blast dest: lemma1a lemma2a)
-
-lemma False_epsclosure_or[iff]:
- "(False#p,q) : (eps(or L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)"
-by (blast dest: lemma1b lemma2b)
-
-(***** lift True/False over steps *****)
-
-lemma lift_True_over_steps_or[iff]:
- "!!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)"
-apply (induct "w")
- apply auto
-apply force
-done
-
-lemma lift_False_over_steps_or[iff]:
- "!!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)"
-apply (induct "w")
- apply auto
-apply (force)
-done
-
-(***** Epsilon closure of start state *****)
-
-lemma unfold_rtrancl2:
- "R^* = Id Un (R^* O R)"
-apply (rule set_ext)
-apply (simp)
-apply (rule iffI)
- apply (erule rtrancl_induct)
-  apply (blast)
- apply (blast intro: rtrancl_into_rtrancl)
-apply (blast intro: converse_rtrancl_into_rtrancl)
-done
-
-lemma in_unfold_rtrancl2:
- "(p,q) : R^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))"
-apply (rule unfold_rtrancl2[THEN equalityE])
-apply (blast)
-done
-
-lemmas [iff] = in_unfold_rtrancl2[where p = "start(or L R)", standard]
-
-lemma start_eps_or[iff]:
- "!!L R. (start(or L R),q) : eps(or L R) = 
-       (q = True#start L | q = False#start R)"
-by (simp add:or_def step_def)
-
-lemma not_start_step_or_Some[iff]:
- "!!L R. (start(or L R),q) ~: step (or L R) (Some a)"
-by (simp add:or_def step_def)
-
-lemma steps_or:
- "(start(or L R), q) : steps (or L R) w = 
- ( (w = [] & q = start(or L R)) | 
-   (? p.  q = True  # p & (start L,p) : steps L w | 
-          q = False # p & (start R,p) : steps R w) )"
-apply (case_tac "w")
- apply (simp)
- apply (blast)
-apply (simp)
-apply (blast)
-done
-
-lemma start_or_not_final[iff]:
- "!!L R. ~ fin (or L R) (start(or L R))"
-by (simp add:or_def)
-
-lemma accepts_or:
- "accepts (or L R) w = (accepts L w | accepts R w)"
-apply (simp add:accepts_def steps_or)
- apply auto
-done
-
-
-(******************************************************)
-(*                      conc                          *)
-(******************************************************)
-
-(** True/False in fin **)
-
-lemma in_conc_True[iff]:
- "!!L R. fin (conc L R) (True#p) = False"
-by (simp add:conc_def)
-
-lemma fin_conc_False[iff]:
- "!!L R. fin (conc L R) (False#p) = fin R p"
-by (simp add:conc_def)
-
-(** True/False in step **)
-
-lemma True_step_conc[iff]:
- "!!L R. (True#p,q) : step (conc L R) a = 
-       ((? r. q=True#r & (p,r): step L a) | 
-        (fin L p & a=None & q=False#start R))"
-by (simp add:conc_def step_def) (blast)
-
-lemma False_step_conc[iff]:
- "!!L R. (False#p,q) : step (conc L R) a = 
-       (? r. q = False#r & (p,r) : step R a)"
-by (simp add:conc_def step_def) (blast)
-
-(** False in epsclosure **)
-
-lemma lemma1b:
- "(tp,tq) : (eps(conc L R))^* ==> 
-  (!!p. tp = False#p ==> ? q. (p,q) : (eps R)^* & tq = False#q)"
-apply (induct rule: rtrancl_induct)
- apply (blast)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma lemma2b:
- "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*"
-apply (induct rule: rtrancl_induct)
- apply (blast)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma False_epsclosure_conc[iff]:
- "((False # p, q) : (eps (conc L R))^*) = 
- (? r. q = False # r & (p, r) : (eps R)^*)"
-apply (rule iffI)
- apply (blast dest: lemma1b)
-apply (blast dest: lemma2b)
-done
-
-(** False in steps **)
-
-lemma False_steps_conc[iff]:
- "!!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)"
-apply (induct "w")
- apply (simp)
-apply (simp)
-apply (fast)  (*MUCH faster than blast*)
-done
-
-(** True in epsclosure **)
-
-lemma True_True_eps_concI:
- "(p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*"
-apply (induct rule: rtrancl_induct)
- apply (blast)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma True_True_steps_concI:
- "!!p. (p,q) : steps L w ==> (True#p,True#q) : steps (conc L R) w"
-apply (induct "w")
- apply (simp add: True_True_eps_concI)
-apply (simp)
-apply (blast intro: True_True_eps_concI)
-done
-
-lemma lemma1a:
- "(tp,tq) : (eps(conc L R))^* ==> 
- (!!p. tp = True#p ==> 
-  (? q. tq = True#q & (p,q) : (eps L)^*) | 
-  (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*))"
-apply (induct rule: rtrancl_induct)
- apply (blast)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma lemma2a:
- "(p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*"
-apply (induct rule: rtrancl_induct)
- apply (blast)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma lem:
- "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None"
-by(simp add: conc_def step_def)
-
-lemma lemma2b:
- "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*"
-apply (induct rule: rtrancl_induct)
- apply (blast)
-apply (drule lem)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma True_False_eps_concI:
- "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)"
-by(simp add: conc_def step_def)
-
-lemma True_epsclosure_conc[iff]:
- "((True#p,q) : (eps(conc L R))^*) = 
- ((? r. (p,r) : (eps L)^* & q = True#r) | 
-  (? r. (p,r) : (eps L)^* & fin L r & 
-        (? s. (start R, s) : (eps R)^* & q = False#s)))"
-apply (rule iffI)
- apply (blast dest: lemma1a)
-apply (erule disjE)
- apply (blast intro: lemma2a)
-apply (clarify)
-apply (rule rtrancl_trans)
-apply (erule lemma2a)
-apply (rule converse_rtrancl_into_rtrancl)
-apply (erule True_False_eps_concI)
-apply (erule lemma2b)
-done
-
-(** True in steps **)
-
-lemma True_steps_concD[rule_format]:
- "!p. (True#p,q) : steps (conc L R) w --> 
-     ((? r. (p,r) : steps L w & q = True#r)  | 
-      (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & 
-              (? s. (start R,s) : steps R v & q = False#s))))"
-apply (induct "w")
- apply (simp)
-apply (simp)
-apply (clarify del: disjCI)
- apply (erule disjE)
- apply (clarify del: disjCI)
- apply (erule disjE)
-  apply (clarify del: disjCI)
-  apply (erule allE, erule impE, assumption)
-  apply (erule disjE)
-   apply (blast)
-  apply (rule disjI2)
-  apply (clarify)
-  apply (simp)
-  apply (rule_tac x = "a#u" in exI)
-  apply (simp)
-  apply (blast)
- apply (blast)
-apply (rule disjI2)
-apply (clarify)
-apply (simp)
-apply (rule_tac x = "[]" in exI)
-apply (simp)
-apply (blast)
-done
-
-lemma True_steps_conc:
- "(True#p,q) : steps (conc L R) w = 
- ((? r. (p,r) : steps L w & q = True#r)  | 
-  (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & 
-          (? s. (start R,s) : steps R v & q = False#s))))"
-by (blast dest: True_steps_concD
-    intro: True_True_steps_concI in_steps_epsclosure)
-
-(** starting from the start **)
-
-lemma start_conc:
-  "!!L R. start(conc L R) = True#start L"
-by (simp add: conc_def)
-
-lemma final_conc:
- "!!L R. fin(conc L R) p = (? s. p = False#s & fin R s)"
-by (simp add:conc_def split: list.split)
-
-lemma accepts_conc:
- "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)"
-apply (simp add: accepts_def True_steps_conc final_conc start_conc)
-apply (blast)
-done
-
-(******************************************************)
-(*                       star                         *)
-(******************************************************)
-
-lemma True_in_eps_star[iff]:
- "!!A. (True#p,q) : eps(star A) = 
-     ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )"
-by (simp add:star_def step_def) (blast)
-
-lemma True_True_step_starI:
-  "!!A. (p,q) : step A a ==> (True#p, True#q) : step (star A) a"
-by (simp add:star_def step_def)
-
-lemma True_True_eps_starI:
-  "(p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*"
-apply (induct rule: rtrancl_induct)
- apply (blast)
-apply (blast intro: True_True_step_starI rtrancl_into_rtrancl)
-done
-
-lemma True_start_eps_starI:
- "!!A. fin A p ==> (True#p,True#start A) : eps(star A)"
-by (simp add:star_def step_def)
-
-lemma lem:
- "(tp,s) : (eps(star A))^* ==> (! p. tp = True#p --> 
- (? r. ((p,r) : (eps A)^* | 
-        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & 
-       s = True#r))"
-apply (induct rule: rtrancl_induct)
- apply (simp)
-apply (clarify)
-apply (simp)
-apply (blast intro: rtrancl_into_rtrancl)
-done
-
-lemma True_eps_star[iff]:
- "((True#p,s) : (eps(star A))^*) = 
- (? r. ((p,r) : (eps A)^* | 
-        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & 
-       s = True#r)"
-apply (rule iffI)
- apply (drule lem)
- apply (blast)
-(* Why can't blast do the rest? *)
-apply (clarify)
-apply (erule disjE)
-apply (erule True_True_eps_starI)
-apply (clarify)
-apply (rule rtrancl_trans)
-apply (erule True_True_eps_starI)
-apply (rule rtrancl_trans)
-apply (rule r_into_rtrancl)
-apply (erule True_start_eps_starI)
-apply (erule True_True_eps_starI)
-done
-
-(** True in step Some **)
-
-lemma True_step_star[iff]:
- "!!A. (True#p,r): step (star A) (Some a) = 
-     (? q. (p,q): step A (Some a) & r=True#q)"
-by (simp add:star_def step_def) (blast)
-
-
-(** True in steps **)
-
-(* reverse list induction! Complicates matters for conc? *)
-lemma True_start_steps_starD[rule_format]:
- "!rr. (True#start A,rr) : steps (star A) w --> 
- (? us v. w = concat us @ v & 
-             (!u:set us. accepts A u) & 
-             (? r. (start A,r) : steps A v & rr = True#r))"
-apply (induct w rule: rev_induct)
- apply (simp)
- apply (clarify)
- apply (rule_tac x = "[]" in exI)
- apply (erule disjE)
-  apply (simp)
- apply (clarify)
- apply (simp)
-apply (simp add: O_assoc epsclosure_steps)
-apply (clarify)
-apply (erule allE, erule impE, assumption)
-apply (clarify)
-apply (erule disjE)
- apply (rule_tac x = "us" in exI)
- apply (rule_tac x = "v@[x]" in exI)
- apply (simp add: O_assoc epsclosure_steps)
- apply (blast)
-apply (clarify)
-apply (rule_tac x = "us@[v@[x]]" in exI)
-apply (rule_tac x = "[]" in exI)
-apply (simp add: accepts_def)
-apply (blast)
-done
-
-lemma True_True_steps_starI:
-  "!!p. (p,q) : steps A w ==> (True#p,True#q) : steps (star A) w"
-apply (induct "w")
- apply (simp)
-apply (simp)
-apply (blast intro: True_True_eps_starI True_True_step_starI)
-done
-
-lemma steps_star_cycle:
- "(!u : set us. accepts A u) ==> 
- (True#start A,True#start A) : steps (star A) (concat us)"
-apply (induct "us")
- apply (simp add:accepts_def)
-apply (simp add:accepts_def)
-by(blast intro: True_True_steps_starI True_start_eps_starI in_epsclosure_steps)
-
-(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
-lemma True_start_steps_star:
- "(True#start A,rr) : steps (star A) w = 
- (? us v. w = concat us @ v & 
-             (!u:set us. accepts A u) & 
-             (? r. (start A,r) : steps A v & rr = True#r))"
-apply (rule iffI)
- apply (erule True_start_steps_starD)
-apply (clarify)
-apply (blast intro: steps_star_cycle True_True_steps_starI)
-done
-
-(** the start state **)
-
-lemma start_step_star[iff]:
-  "!!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)"
-by (simp add:star_def step_def)
-
-lemmas epsclosure_start_step_star =
-  in_unfold_rtrancl2[where p = "start(star A)", standard]
-
-lemma start_steps_star:
- "(start(star A),r) : steps (star A) w = 
- ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)"
-apply (rule iffI)
- apply (case_tac "w")
-  apply (simp add: epsclosure_start_step_star)
- apply (simp)
- apply (clarify)
- apply (simp add: epsclosure_start_step_star)
- apply (blast)
-apply (erule disjE)
- apply (simp)
-apply (blast intro: in_steps_epsclosure)
-done
-
-lemma fin_star_True[iff]: "!!A. fin (star A) (True#p) = fin A p"
-by (simp add:star_def)
-
-lemma fin_star_start[iff]: "!!A. fin (star A) (start(star A))"
-by (simp add:star_def)
-
-(* too complex! Simpler if loop back to start(star A)? *)
-lemma accepts_star:
- "accepts (star A) w = 
- (? us. (!u : set(us). accepts A u) & (w = concat us) )"
-apply(unfold accepts_def)
-apply (simp add: start_steps_star True_start_steps_star)
-apply (rule iffI)
- apply (clarify)
- apply (erule disjE)
-  apply (clarify)
-  apply (simp)
-  apply (rule_tac x = "[]" in exI)
-  apply (simp)
- apply (clarify)
- apply (rule_tac x = "us@[v]" in exI)
- apply (simp add: accepts_def)
- apply (blast)
-apply (clarify)
-apply (rule_tac xs = "us" in rev_exhaust)
- apply (simp)
- apply (blast)
-apply (clarify)
-apply (simp add: accepts_def)
-apply (blast)
-done
-
-
-(***** Correctness of r2n *****)
-
-lemma accepts_rexp2nae:
- "!!w. accepts (rexp2nae r) w = (w : lang r)"
-apply (induct "r")
-    apply (simp add: accepts_def)
-   apply (simp add: accepts_atom)
-  apply (simp add: accepts_or)
- apply (simp add: accepts_conc RegSet.conc_def)
-apply (simp add: accepts_star in_star)
-done
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/RegSet.thy
--- a/src/HOL/Lex/RegSet.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(*  Title:      HOL/Lex/RegSet.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Regular sets
-*)
-
-theory RegSet = Main:
-
-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"
-intros
-  NilI[iff]:   "[] : star A"
-  ConsI[intro,simp]:  "[| a:A; as : star A |] ==> a@as : star A"
-
-lemma concat_in_star: "!xs: set xss. xs:S ==> concat xss : star S"
-by (induct "xss") simp_all
-
-lemma in_star:
- "w : star U = (? us. (!u : set(us). u : U) & (w = concat us))"
-apply (rule iffI)
- apply (erule star.induct)
-  apply (rule_tac x = "[]" in exI)
-  apply simp
- apply clarify
- apply (rule_tac x = "a#us" in exI)
- apply simp
-apply clarify
-apply (simp add: concat_in_star)
-done
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/RegSet_of_nat_DA.thy
--- a/src/HOL/Lex/RegSet_of_nat_DA.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,236 +0,0 @@
-(*  Title:      HOL/Lex/RegSet_of_nat_DA.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-
-Conversion of deterministic automata into regular sets.
-
-To generate a regual expression, the alphabet must be finite.
-regexp needs to be supplied with an 'a list for a unique order
-
-add_Atom d i j r a = (if d a i = j then Union r (Atom a) else r)
-atoms d i j as = foldl (add_Atom d i j) Empty as
-
-regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as)
-                        else atoms d i j as
-*)
-
-theory RegSet_of_nat_DA = RegSet + DA:
-
-types 'a nat_next = "'a => nat => nat"
-
-syntax deltas :: "'a nat_next => 'a list => nat => nat"
-translations "deltas" == "foldl2"
-
-consts trace :: "'a nat_next => nat => 'a list => nat list"
-primrec
-"trace d i [] = []"
-"trace d i (x#xs) = d x i # trace d (d x i) xs"
-
-(* conversion a la Warshall *)
-
-consts regset :: "'a nat_next => nat => nat => nat => 'a list set"
-primrec
-"regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
-                          else {[a] | a. d a i = j})"
-"regset d i j (Suc k) = regset d i j k Un
-                        conc (regset d i k k)
-                             (conc (star(regset d k k k))
-                                   (regset d k j k))"
-
-constdefs
- regset_of_DA :: "('a,nat)da => nat => 'a list set"
-"regset_of_DA A k == UN j:{j. j<k & fin A j}. regset (next A) (start A) j k"
-
- bounded :: "'a => nat => bool"
-"bounded d k == !n. n < k --> (!x. d x n < k)"
-
-declare
-  in_set_butlast_appendI[simp,intro] less_SucI[simp] image_eqI[simp]
-
-(* Lists *)
-
-lemma butlast_empty[iff]:
-  "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])"
-by (case_tac "xs") simp_all
-
-lemma in_set_butlast_concatI:
- "x:set(butlast xs) ==> xs:set xss ==> x:set(butlast(concat xss))"
-apply (induct "xss")
- apply simp
-apply (simp add: butlast_append del: ball_simps)
-apply (rule conjI)
- apply (clarify)
- apply (erule disjE)
-  apply (blast)
- apply (subgoal_tac "xs=[]")
-  apply simp
- apply (blast)
-apply (blast dest: in_set_butlastD)
-done
-
-(* Regular sets *)
-
-(* The main lemma:
-   how to decompose a trace into a prefix, a list of loops and a suffix.
-*)
-lemma decompose[rule_format]:
- "!i. k : set(trace d i xs) --> (EX pref mids suf.
-  xs = pref @ concat mids @ suf &
-  deltas d pref i = k & (!n:set(butlast(trace d i pref)). n ~= k) &
-  (!mid:set mids. (deltas d mid k = k) &
-                  (!n:set(butlast(trace d k mid)). n ~= k)) &
-  (!n:set(butlast(trace d k suf)). n ~= k))"
-apply (induct "xs")
- apply (simp)
-apply (rename_tac a as)
-apply (intro strip)
-apply (case_tac "d a i = k")
- apply (rule_tac x = "[a]" in exI)
- apply simp
- apply (case_tac "k : set(trace d (d a i) as)")
-  apply (erule allE)
-  apply (erule impE)
-   apply (assumption)
-  apply (erule exE)+
-  apply (rule_tac x = "pref#mids" in exI)
-  apply (rule_tac x = "suf" in exI)
-  apply simp
- apply (rule_tac x = "[]" in exI)
- apply (rule_tac x = "as" in exI)
- apply simp
- apply (blast dest: in_set_butlastD)
-apply simp
-apply (erule allE)
-apply (erule impE)
- apply (assumption)
-apply (erule exE)+
-apply (rule_tac x = "a#pref" in exI)
-apply (rule_tac x = "mids" in exI)
-apply (rule_tac x = "suf" in exI)
-apply simp
-done
-
-lemma length_trace[simp]: "!!i. length(trace d i xs) = length xs"
-by (induct "xs") simp_all
-
-lemma deltas_append[simp]:
-  "!!i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)"
-by (induct "xs") simp_all
-
-lemma trace_append[simp]:
-  "!!i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys"
-by (induct "xs") simp_all
-
-lemma trace_concat[simp]:
- "(!xs: set xss. deltas d xs i = i) ==>
-  trace d i (concat xss) = concat (map (trace d i) xss)"
-by (induct "xss") simp_all
-
-lemma trace_is_Nil[simp]: "!!i. (trace d i xs = []) = (xs = [])"
-by (case_tac "xs") simp_all
-
-lemma trace_is_Cons_conv[simp]:
- "(trace d i xs = n#ns) =
-  (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)"
-apply (case_tac "xs")
-apply simp_all
-apply (blast)
-done
-
-lemma set_trace_conv:
- "!!i. set(trace d i xs) =
-  (if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))"
-apply (induct "xs")
- apply (simp)
-apply (simp add: insert_commute)
-done
-
-lemma deltas_concat[simp]:
- "(!mid:set mids. deltas d mid k = k) ==> deltas d (concat mids) k = k"
-by (induct mids) simp_all
-
-lemma lem: "[| n < Suc k; n ~= k |] ==> n < k"
-by arith
-
-lemma regset_spec:
- "!!i j xs. xs : regset d i j k =
-        ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)"
-apply (induct k)
- apply(simp split: list.split)
- apply(fastsimp)
-apply (simp add: conc_def)
-apply (rule iffI)
- apply (erule disjE)
-  apply simp
- apply (erule exE conjE)+
- apply simp
- apply (subgoal_tac
-      "(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n")
-  apply (simp add: set_trace_conv butlast_append ball_Un)
- apply (erule star.induct)
-  apply (simp)
- apply (simp add: set_trace_conv butlast_append ball_Un)
-apply (case_tac "n : set(butlast(trace d i xs))")
- prefer 2 apply (rule disjI1)
- apply (blast intro:lem)
-apply (rule disjI2)
-apply (drule in_set_butlastD[THEN decompose])
-apply (clarify)
-apply (rule_tac x = "pref" in exI)
-apply simp
-apply (rule conjI)
- apply (rule ballI)
- apply (rule lem)
-  prefer 2 apply simp
- apply (drule bspec) prefer 2 apply assumption
- apply simp
-apply (rule_tac x = "concat mids" in exI)
-apply (simp)
-apply (rule conjI)
- apply (rule concat_in_star)
- apply simp
- apply (rule ballI)
- apply (rule ballI)
- apply (rule lem)
-  prefer 2 apply simp
- apply (drule bspec) prefer 2 apply assumption
- apply (simp add: image_eqI in_set_butlast_concatI)
-apply (rule ballI)
-apply (rule lem)
- apply auto
-done
-
-lemma trace_below:
- "bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)"
-apply (unfold bounded_def)
-apply (induct "xs")
- apply simp
-apply (simp (no_asm))
-apply (blast)
-done
-
-lemma regset_below:
- "[| bounded d k; i < k; j < k |] ==>
-  regset d i j k = {xs. deltas d xs i = j}"
-apply (rule set_ext)
-apply (simp add: regset_spec)
-apply (blast dest: trace_below in_set_butlastD)
-done
-
-lemma deltas_below:
- "!!i. bounded d k ==> i < k ==> deltas d w i < k"
-apply (unfold bounded_def)
-apply (induct "w")
- apply simp_all
-done
-
-lemma regset_DA_equiv:
- "[| bounded (next A) k; start A < k; j < k |] ==> \
-\ w : regset_of_DA A k = accepts A w"
-apply(unfold regset_of_DA_def)
-apply (simp cong: conj_cong
-            add: regset_below deltas_below accepts_def delta_def)
-done
-
-end
diff -r 2015348ceecb -r 8d5c551a9260 src/HOL/Lex/Scanner.thy
--- a/src/HOL/Lex/Scanner.thy	Wed Mar 31 10:51:50 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*  Title:      HOL/Lex/Scanner.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-theory Scanner = Automata + RegExp2NA + RegExp2NAe:
-
-theorem "DA.accepts (na2da(rexp2na r)) w = (w : lang r)"
-by (simp add: NA_DA_equiv[THEN sym] accepts_rexp2na)
-
-theorem  "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"
-by (simp add: NAe_DA_equiv accepts_rexp2nae)
-
-(* Testing code generation: *)
-
-types_code
-  set ("_ list")
-
-consts_code
-  "{}"     ("[]")
-  "insert" ("(_ ins _)")
-  "op :"   ("(_ mem _)")
-  "op Un"  ("(_ union _)")
-  "image"  ("map")
-  "UNION"  ("(fn A => fn f => flat(map f A))")
-  "Bex"    ("(fn A => fn f => exists f A)")
-
-generate_code
-  test = "let r0 = Atom(0::nat);
-              r1 = Atom(1::nat);
-              re = Conc (Star(Or(Conc r1 r1)r0))
-                        (Star(Or(Conc r0 r0)r1));
-              N = rexp2na re;
-              D = na2da N
-          in (NA.accepts N [0,1,1,0,0,1], DA.accepts D [0,1,1,0,0,1])"
-ML test
-
-end