# HG changeset patch
# User nipkow
# Date 1078391082 -3600
# Node ID bb2b0e10d9be78a314f37ec58faceff60fac8111
# Parent  cea7d2f76112de990038685f37aba30b8eca8e8b
Conversion of ML files to Isar.

diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/AutoChopper.ML
--- a/src/HOL/Lex/AutoChopper.ML	Wed Mar 03 22:58:23 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,258 +0,0 @@
-(*  Title:      HOL/Lex/AutoChopper.ML
-    ID:         $Id$
-    Author:     Richard Mayr & Tobias Nipkow
-    Copyright   1995 TUM
-
-Main result: auto_chopper satisfies the is_auto_chopper specification.
-*)
-
-Delsimps (ex_simps @ all_simps);
-Delsimps [split_paired_All];
-
-Addsimps [Let_def];
-
-Goalw [acc_prefix_def] "~acc_prefix A [] s";
-by (Simp_tac 1);
-qed"acc_prefix_Nil";
-Addsimps [acc_prefix_Nil];
-
-Goalw [acc_prefix_def]
- "acc_prefix A (x#xs) s = (fin A (next A x s) | acc_prefix A xs (next A x s))";
-by (simp_tac (simpset() addsimps [thm "prefix_Cons"]) 1);
-by Safe_tac;
-  by (Asm_full_simp_tac 1);
-  by (case_tac "zs=[]" 1);
-   by (hyp_subst_tac 1);
-   by (Asm_full_simp_tac 1);
-  by (Fast_tac 1);
- by (res_inst_tac [("x","[x]")] exI 1);
- by (asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-by (res_inst_tac [("x","x#us")] exI 1);
-by (Asm_simp_tac 1);
-qed"acc_prefix_Cons";
-Addsimps [acc_prefix_Cons];
-
-Goal "!st us p y ys. acc A st p (ys@[y]) xs us ~= ([],zs)";
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed_spec_mp "accept_not_Nil";
-Addsimps [accept_not_Nil];
-
-Goal
-"!st us. acc A st ([],ys) [] xs us = ([], zs) --> \
-\        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (delta A ys st))";
-by (induct_tac "xs" 1);
-by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (rtac conjI 1);
-by (Fast_tac 1);
-by (simp_tac (simpset() addsimps [thm "prefix_Cons"] addcongs [conj_cong]) 1);
-by (strip_tac 1);
-by (REPEAT(eresolve_tac [conjE,exE] 1));
-by (hyp_subst_tac 1);
-by (Simp_tac 1);
-by (case_tac "zsa = []" 1);
-by (Asm_simp_tac 1);
-by (Fast_tac 1);
-qed_spec_mp "no_acc";
-
-
-val [prem] = goal HOL.thy "? x. P(f(x)) ==> ? y. P(y)";
-by (cut_facts_tac [prem] 1);
-by (Fast_tac 1);
-val ex_special = result();
-
-
-Goal
-"! r erk l rst st ys yss zs::'a list. \
-\    acc A st (l,rst) erk xs r = (ys#yss, zs) --> \
-\    ys@concat(yss)@zs = (if acc_prefix A xs st then r@xs else erk@concat(l)@rst)";
-by (induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
-by (rename_tac "vss lrst" 1);  
-by (Asm_simp_tac 1);
-by (case_tac "vss" 1);
- by (hyp_subst_tac 1);
- by (Simp_tac 1);
- by (fast_tac (claset() addSDs [no_acc]) 1);
-by (hyp_subst_tac 1);
-by (Asm_simp_tac 1);
-qed_spec_mp "step2_a";
-
-
-Goal
- "! st erk r l rest ys yss zs.\
-\   acc A st (l,rest) erk xs r = (ys#yss, zs) --> \
-\     (if acc_prefix A xs st \
-\      then ys ~= [] \
-\      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
-by (Simp_tac 1);
-by (induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
-by (rename_tac "vss lrst" 1);  
-by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (case_tac "acc_prefix A list (next A a st)" 1);
- by (Asm_simp_tac 1);
-by (subgoal_tac "r @ [a] ~= []" 1);
- by (Fast_tac 1);
-by (Simp_tac 1);
-qed_spec_mp "step2_b";
-
-
-Goal  
- "! st erk r l rest ys yss zs. \
-\   acc A st (l,rest) erk xs r = (ys#yss, zs) --> \
-\     (if acc_prefix A xs st                   \
-\      then ? g. ys=r@g & fin A (delta A g st)  \
-\      else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
-by (Simp_tac 1);
-by (induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (strip_tac 1);
-by (rtac conjI 1);
- by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
- by (rename_tac "vss lrst" 1);  
- by (Asm_simp_tac 1);
- by (case_tac "acc_prefix A list (next A a st)" 1);
-  by (strip_tac 1);
-  by (res_inst_tac [("f","%k. a#k")] ex_special 1);
-  by (Simp_tac 1);
-  by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
-   by (Simp_tac 1);
-  by (Fast_tac 1);
- by (strip_tac 1);
- by (res_inst_tac [("x","[a]")] exI 1);
- by (Asm_simp_tac 1);
- by (subgoal_tac "r @ [a] ~= []" 1);
-  by (rtac sym 1);
-  by (Fast_tac 1);
- by (Simp_tac 1);
-by (strip_tac 1);
-by (res_inst_tac [("f","%k. a#k")] ex_special 1);
-by (Simp_tac 1);
-by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
- by (Simp_tac 1);
-by (Fast_tac 1);
-qed_spec_mp "step2_c";
-
-
-Goal
- "! st erk r l rest ys yss zs. \
-\   acc A st (l,rest) erk xs r = (ys#yss, zs) --> \
-\     (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)))";
-by (Simp_tac 1);
-by (induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
-by (rename_tac "vss lrst" 1);  
-by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (case_tac "acc_prefix A list (next A a st)" 1);
- by (Asm_simp_tac 1);
-by (subgoal_tac "acc A (start A) ([],list) [] list [] = (yss,zs)" 1);
- by (Asm_simp_tac 2);
- by (subgoal_tac "r@[a] ~= []" 2);
-  by (Fast_tac 2);
- by (Simp_tac 2);
-by (subgoal_tac "concat(yss) @ zs = list" 1);
- by (hyp_subst_tac 1);
- by (atac 1);
-by (case_tac "yss = []" 1);
- by (Asm_simp_tac 1);
- by (hyp_subst_tac 1);
- by (fast_tac (claset() addSDs [no_acc]) 1);
-by (etac ((neq_Nil_conv RS iffD1) RS exE) 1);
-by (etac exE 1);
-by (hyp_subst_tac 1);
-by (Simp_tac 1);
-by (rtac trans 1);
- by (etac step2_a 1);
-by (Simp_tac 1);
-qed_spec_mp "step2_d";
-
-Goal 
-"! st erk r p ys yss zs. \
-\  acc A st p erk xs r = (ys#yss, zs) --> \
-\  (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))";
-by (Simp_tac 1);
-by (induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (strip_tac 1);
-by (case_tac "acc_prefix A list (next A a st)" 1);
- by (rtac conjI 1);
-  by (strip_tac 1);
-  by (res_inst_tac [("f","%k. a#k")] ex_special 1);
-  by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
-   by (Simp_tac 1);
-  by (res_inst_tac [("P","%k. ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (delta A as (next A a st)))")] exE 1);
-   by (asm_simp_tac HOL_ss 1);
-  by (res_inst_tac [("x","x")] exI 1);
-  by (Asm_simp_tac 1);
-  by (rtac allI 1);
-  by (case_tac "as" 1);
-   by (Asm_simp_tac 1);
-  by (asm_simp_tac (simpset() addcongs[conj_cong]) 1);
- by (strip_tac 1);
- by (res_inst_tac [("f","%k. a#k")] ex_special 1);
- by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
-  by (Simp_tac 1);
- by (res_inst_tac [("P","%k. ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (delta A as (next A a st)))")] exE 1);
-  by (asm_simp_tac HOL_ss 1);
- by (res_inst_tac [("x","x")] exI 1);
- by (Asm_simp_tac 1);
- by (rtac allI 1);
- by (case_tac "as" 1);
-  by (Asm_simp_tac 1);
- by (asm_simp_tac (simpset() addcongs[conj_cong]) 1);
-by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (res_inst_tac [("x","[a]")] exI 1);
-by (rtac conjI 1);
- by (subgoal_tac "r @ [a] ~= []" 1);
-  by (Fast_tac 1);
- by (Simp_tac 1);
-by (rtac allI 1);
-by (case_tac "as" 1);
- by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
-by (etac thin_rl 1); (* speed up *)
-by (Fast_tac 1);
-qed_spec_mp "step2_e";
-
-Addsimps[split_paired_All];
-
-Goalw [accepts_def, is_auto_chopper_def, auto_chopper_def,
-           Chopper.is_longest_prefix_chopper_def]
- "is_auto_chopper(auto_chopper)";
-by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
- by (rtac mp 1);
-  by (etac step2_b 2);
- by (Simp_tac 1);
-by (rtac conjI 1);
- by (rtac mp 1);
-  by (etac step2_c 2);
- by (Simp_tac 1);
-by (rtac conjI 1);
- by (asm_simp_tac (simpset() addsimps [step2_a]) 1);
-by (rtac conjI 1);
- by (rtac mp 1);
-  by (etac step2_d 2);
- by (Simp_tac 1);
-by (rtac mp 1);
- by (etac step2_e 2);
- by (Simp_tac 1);
-qed"auto_chopper_is_auto_chopper";
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/AutoChopper.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Lex/AutoChopper.thy
     ID:         $Id$
-    Author:     Tobias Nipkow
+    Author:     Richard Mayr & Tobias Nipkow
     Copyright   1995 TUM
 
 auto_chopper turns an automaton into a chopper. Tricky, because primrec.
@@ -19,16 +19,16 @@
 its antecedents.
 *)
 
-AutoChopper = DA + Chopper +
+theory AutoChopper = DA + Chopper:
 
 constdefs
- is_auto_chopper :: (('a,'s)da => 'a chopper) => bool
+ 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, 's, 'a list list*'a list, 'a list, 'a list, 'a list]
-          => 'a list list * 'a list"
+  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)))" 
@@ -40,12 +40,221 @@
                 else acc A t r ps xs (zs@[x]))"
 
 constdefs
- auto_chopper :: ('a,'s)da => 'a chopper
+ 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 == ? us. us <= xs & us~=[] & fin A (delta A us s)"
+ 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 cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/AutoChopper1.thy
--- a/src/HOL/Lex/AutoChopper1.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/AutoChopper1.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -17,7 +17,7 @@
 No proofs yet.
 *)
 
-AutoChopper1 = DA + Chopper +
+theory AutoChopper1 = DA + Chopper:
 
 consts
   acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/AutoMaxChop.ML
--- a/src/HOL/Lex/AutoMaxChop.ML	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/AutoMaxChop.ML	Thu Mar 04 10:04:42 2004 +0100
@@ -14,12 +14,12 @@
 by (induct_tac "xs" 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
-                           delsimps [delta_append]) 1);
+                           delsimps [thm"delta_append"]) 1);
 qed_spec_mp "auto_split_lemma";
 
-Goalw [accepts_def]
+Goalw [thm"accepts_def"]
  "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs";
-by (stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
+by (stac ((read_instantiate [("s","start A")] (thm"delta_Nil")) RS sym) 1);
 by (stac auto_split_lemma 1);
 by (Simp_tac 1);
 qed_spec_mp "auto_split_is_maxsplit";
@@ -27,11 +27,11 @@
 Goal
  "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)";
 by (simp_tac (simpset() addsimps
-        [auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1);
+        [auto_split_is_maxsplit,thm"is_maxsplitter_maxsplit"]) 1);
 qed "is_maxsplitter_auto_split";
 
-Goalw [auto_chop_def]
+Goalw [thm"auto_chop_def"]
  "is_maxchopper (accepts A) (auto_chop A)";
-by (rtac is_maxchopper_chop 1);
+by (rtac (thm"is_maxchopper_chop") 1);
 by (rtac is_maxsplitter_auto_split 1);
 qed "is_maxchopper_auto_chop";
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/AutoMaxChop.thy
--- a/src/HOL/Lex/AutoMaxChop.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/AutoMaxChop.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -4,7 +4,7 @@
     Copyright   1998 TUM
 *)
 
-AutoMaxChop = DA + MaxChop +
+theory AutoMaxChop = DA + MaxChop:
 
 consts
  auto_split :: "('a,'s)da => 's  => 'a list * 'a list => 'a list => 'a splitter"
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/AutoProj.ML
--- a/src/HOL/Lex/AutoProj.ML	Wed Mar 03 22:58:23 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      HOL/Lex/AutoProj.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-Goalw [start_def] "start(q,d,f) = q";
-by (Simp_tac 1);
-qed "start_conv";
-
-Goalw [next_def] "next(q,d,f) = d";
-by (Simp_tac 1);
-qed "next_conv";
-
-Goalw [fin_def] "fin(q,d,f) = f";
-by (Simp_tac 1);
-qed "fin_conv";
-
-Addsimps [start_conv,next_conv,fin_conv];
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/AutoProj.thy
--- a/src/HOL/Lex/AutoProj.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/AutoProj.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -9,14 +9,23 @@
 and use foldl instead of foldl2.
 *)
 
-AutoProj = Main +
+theory AutoProj = Main:
 
 constdefs
  start :: "'a * 'b * 'c => 'a"
 "start A == fst A"
- next :: "'a * 'b * 'c => 'b"
+ "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 cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/Automata.ML
--- a/src/HOL/Lex/Automata.ML	Wed Mar 03 22:58:23 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      HOL/Lex/Automata.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-(*** Equivalence of NA and DA ***)
-
-Goalw [na2da_def]
- "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w ` Q)";
-by (induct_tac "w" 1);
- by Auto_tac;
-qed_spec_mp "DA_delta_is_lift_NA_delta";
-
-Goalw [DA.accepts_def,NA.accepts_def]
-  "NA.accepts A w = DA.accepts (na2da A) w";
-by (simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
-by (simp_tac (simpset() addsimps [na2da_def]) 1);
-qed "NA_DA_equiv";
-
-(*** Direct equivalence of NAe and DA ***)
-
-Goalw [nae2da_def]
- "!Q. (eps A)^* `` (DA.delta (nae2da A) w Q) = steps A w `` Q";
-by (induct_tac "w" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
-by (Blast_tac 1);
-qed_spec_mp "espclosure_DA_delta_is_steps";
-
-Goalw [nae2da_def]
- "fin (nae2da A) Q = (? q : (eps A)^* `` Q. fin A q)";
-by (Simp_tac 1);
-val lemma = result();
-
-Goalw [NAe.accepts_def,DA.accepts_def]
-  "DA.accepts (nae2da A) w = NAe.accepts A w";
-by (simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
-by (simp_tac (simpset() addsimps [nae2da_def]) 1);
-by (Blast_tac 1);
-qed "NAe_DA_equiv";
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/Automata.thy
--- a/src/HOL/Lex/Automata.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/Automata.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -6,15 +6,49 @@
 Conversions between different kinds of automata
 *)
 
-Automata = DA + NAe +
+theory Automata = DA + NAe:
 
 constdefs
- na2da :: ('a,'s)na => ('a,'s set)da
+ 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,'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 cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/Chopper.thy
--- a/src/HOL/Lex/Chopper.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/Chopper.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -15,13 +15,13 @@
 i.e. a set of strings.
 *)
 
-Chopper = List_Prefix +
+theory Chopper = List_Prefix:
 
-types   'a chopper = "'a list => 'a list list * 'a list"
+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.
+  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) -->
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/DA.ML
--- a/src/HOL/Lex/DA.ML	Wed Mar 03 22:58:23 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      HOL/Lex/DA.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-Goalw [foldl2_def] "foldl2 f [] a = a";
-by (Simp_tac 1);
-qed "foldl2_Nil";
-
-Goalw [foldl2_def] "foldl2 f (x#xs) a = foldl2 f xs (f x a)";
-by (Simp_tac 1);
-qed "foldl2_Cons";
-
-Addsimps [foldl2_Nil,foldl2_Cons];
-
-Goalw [delta_def] "delta A [] s = s";
-by (Simp_tac 1);
-qed "delta_Nil";
-
-Goalw [delta_def] "delta A (a#w) s = delta A w (next A a s)";
-by (Simp_tac 1);
-qed "delta_Cons";
-
-Addsimps [delta_Nil,delta_Cons];
-
-Goal "!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "delta_append";
-Addsimps [delta_append];
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/DA.thy
--- a/src/HOL/Lex/DA.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/DA.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -6,18 +6,31 @@
 Deterministic automata
 *)
 
-DA = AutoProj +
+theory DA = AutoProj:
 
 types ('a,'s)da = "'s * ('a => 's => 's) * ('s => bool)"
 
 constdefs
- foldl2 :: ('a => 'b => 'b) => 'a list => 'b => 'b
+ 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,'s)da => 'a list => 's => 's"
 "delta A == foldl2 (next A)"
 
- accepts ::  ('a,'s)da => 'a list => bool
+ 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 cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Wed Mar 03 22:58:23 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-(*  Title:      HOL/Lex/MaxChop.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-(* Termination of chop *)
-
-Goalw [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)";
-by (asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1);
-qed "reducing_maxsplit";
-
-val [tc] = chopr.tcs;
-goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
-by (blast_tac (claset() addDs [sym]) 1);
-val lemma = result();
-
-val chopr_rule = let val [chopr_rule] = chopr.simps in lemma RS chopr_rule end;
-
-Goalw [chop_def] "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))";
-by (asm_simp_tac (simpset() addsimps [chopr_rule]) 1);
-by (simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
-qed "chop_rule";
-
-Goalw [is_maxsplitter_def,reducing_def]
- "is_maxsplitter P splitf ==> reducing splitf";
-by (Asm_full_simp_tac 1);
-qed "is_maxsplitter_reducing";
-
-Goal "is_maxsplitter P splitf ==> \
-\ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
-by (induct_thm_tac length_induct "xs" 1);
-by (asm_simp_tac (simpset() delsplits [split_if]
-                           addsimps [chop_rule,is_maxsplitter_reducing]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
-                                addsplits [split_split]) 1);
-qed_spec_mp "chop_concat";
-
-Goal "is_maxsplitter P splitf ==> \
-\ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
-by (induct_thm_tac length_induct "xs" 1);
-by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
-                                 addsplits [split_split]) 1);
-by (simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
-                        addsplits [split_split]) 1);
-by (etac thin_rl 1);
-by (strip_tac 1);
-by (rtac ballI 1);
-by (etac exE 1);
-by (etac allE 1);
-by Auto_tac;
-qed "chop_nonempty";
-
-val [prem] = goalw thy [is_maxchopper_def]
- "is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)";
-by (Clarify_tac 1);
-by (rtac iffI 1);
- by (rtac conjI 1);
-  by (etac (prem RS chop_concat) 1);
- by (rtac conjI 1);
-  by (etac (prem RS (chop_nonempty RS spec RS spec RS mp)) 1);
- by (etac rev_mp 1);
- by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
- by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
-                        addsplits [split_split]) 1);
- by (Clarify_tac 1);
- by (rtac conjI 1);
-  by (Clarify_tac 1);
- by (Clarify_tac 1);
- by (Asm_full_simp_tac 1);
- by (forward_tac [prem RS chop_concat] 1);
- by (Clarify_tac 1);
-by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
-by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
-                        addsplits [split_split]) 1);
-by (Clarify_tac 1);
-by (rename_tac "xs1 ys1 xss1 ys" 1);
-by (split_asm_tac [thm "list.split_asm"] 1);
- by (Asm_full_simp_tac 1);
- by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
- by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1);
-by (rtac conjI 1);
- by (Clarify_tac 1);
- by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
- by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1);
-by (Clarify_tac 1);
-by (rename_tac "us uss" 1);
-by (subgoal_tac "xs1=us" 1);
- by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
-by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2, order_antisym]) 1);
-qed "is_maxchopper_chop";
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/MaxChop.thy
--- a/src/HOL/Lex/MaxChop.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/MaxChop.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -4,12 +4,12 @@
     Copyright   1998 TUM
 *)
 
-MaxChop = MaxPrefix +
+theory MaxChop = MaxPrefix:
 
 types   'a chopper = "'a list => 'a list list * 'a list"
 
 constdefs
- is_maxchopper :: ('a list => bool) => 'a chopper => bool
+ is_maxchopper :: "('a list => bool) => 'a chopper => bool"
 "is_maxchopper P chopper ==
  !xs zs yss.
     (chopper(xs) = (yss,zs)) =
@@ -25,15 +25,102 @@
 
 consts
  chopr :: "'a splitter * 'a list => 'a list list * 'a list"
-recdef chopr "measure (length o snd)"
+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 :: "'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 cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/MaxPrefix.ML
--- a/src/HOL/Lex/MaxPrefix.ML	Wed Mar 03 22:58:23 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title:      HOL/Lex/MaxPrefix.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-Delsplits [split_if];
-Goalw [is_maxpref_def] "!(ps::'a list) res. \
-\ (maxsplit P res ps qs = (xs,ys)) = \
-\ (if ? us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \
-\  else (xs,ys)=res)";
-by (induct_tac "qs" 1);
- by (simp_tac (simpset() addsplits [split_if]) 1);
- by (Blast_tac 1);
-by (Asm_simp_tac 1);
-by (etac thin_rl 1);
-by (Clarify_tac 1);
-by (case_tac "? us. us <= list & P (ps @ a # us)" 1);
- by (Asm_simp_tac 1);
- by (subgoal_tac "? us. us <= a # list & P (ps @ us)" 1);
-  by (Asm_simp_tac 1);
- by (blast_tac (claset() addIs [thm "prefix_Cons" RS iffD2]) 1);
-by (subgoal_tac "~P(ps@[a])" 1);
- by (Blast_tac 2);
-by (Asm_simp_tac 1);
-by (case_tac "? us. us <= a#list & P (ps @ us)" 1);
- by (Asm_simp_tac 1);
- by (Clarify_tac 1);
- by (case_tac "us" 1);
-  by (rtac iffI 1);
-   by (asm_full_simp_tac (simpset() addsimps [thm "prefix_Cons", thm "prefix_append"]) 1);
-   by (Blast_tac 1);
-  by (asm_full_simp_tac (simpset() addsimps [thm "prefix_Cons", thm "prefix_append"]) 1);
-  by (Clarify_tac 1);
-  by (etac disjE 1);
-   by (fast_tac (claset() addDs [order_antisym]) 1);
-  by (Clarify_tac 1);
-  by (etac disjE 1);
-   by (Clarify_tac 1);
-   by (Asm_full_simp_tac 1);
-  by (etac disjE 1);
-   by (Clarify_tac 1);
-   by (Asm_full_simp_tac 1);
-  by (Blast_tac 1);
- by (Asm_full_simp_tac 1);
-by (subgoal_tac "~P(ps)" 1);
-by (Asm_simp_tac 1);
-by (fast_tac (claset() addss simpset()) 1);
-qed_spec_mp "maxsplit_lemma";
-Addsplits [split_if];
-
-Goalw [is_maxpref_def]
- "~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])";
-by (Blast_tac 1);
-qed "is_maxpref_Nil";
-Addsimps [is_maxpref_Nil];
-
-Goalw [is_maxsplitter_def]
- "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)";
-by (simp_tac (simpset() addsimps [maxsplit_lemma]) 1);
-by (fast_tac (claset() addss simpset()) 1);
-qed "is_maxsplitter_maxsplit";
-
-val maxsplit_eq = rewrite_rule [is_maxsplitter_def] is_maxsplitter_maxsplit;
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/MaxPrefix.thy
--- a/src/HOL/Lex/MaxPrefix.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/MaxPrefix.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -4,14 +4,15 @@
     Copyright   1998 TUM
 *)
 
-MaxPrefix = List_Prefix +
+theory MaxPrefix = List_Prefix:
 
 constdefs
- is_maxpref :: ('a list => bool) => 'a list => 'a list => bool
+ 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 ==
@@ -23,4 +24,67 @@
 "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 cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/NA.ML
--- a/src/HOL/Lex/NA.ML	Wed Mar 03 22:58:23 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(*  Title:      HOL/Lex/NA.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-Goal
- "steps A (v@w) = steps A w  O  steps A v";
-by (induct_tac "v" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
-qed "steps_append";
-Addsimps [steps_append];
-
-Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
-by (rtac (steps_append RS equalityE) 1);
-by (Blast_tac 1);
-qed "in_steps_append";
-AddIffs [in_steps_append];
-
-Goal
- "!p. delta A w p = {q. (p,q) : steps A w}";
-by (induct_tac "w" 1);
-by (auto_tac (claset(), simpset() addsimps [step_def]));
-qed_spec_mp "delta_conv_steps";
-
-Goalw [accepts_def]
- "accepts A w = (? q. (start A,q) : steps A w & fin A q)";
-by (simp_tac (simpset() addsimps [delta_conv_steps]) 1);
-qed "accepts_conv_steps";
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/NA.thy
--- a/src/HOL/Lex/NA.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/NA.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -6,7 +6,7 @@
 Nondeterministic automata
 *)
 
-NA = AutoProj +
+theory NA = AutoProj:
 
 types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)"
 
@@ -16,10 +16,9 @@
 "delta A (a#w) p = Union(delta A w ` next A a p)"
 
 constdefs
- accepts ::   ('a,'s)na => 'a list => bool
-"accepts A w == ? q : delta A w (start A). fin A q"
+ accepts :: "('a,'s)na => 'a list => bool"
+"accepts A w == EX q : delta A w (start A). fin A q"
 
-constdefs
  step :: "('a,'s)na => 'a => ('s * 's)set"
 "step A a == {(p,q) . q : next A a p}"
 
@@ -28,4 +27,21 @@
 "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 cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/NAe.ML
--- a/src/HOL/Lex/NAe.ML	Wed Mar 03 22:58:23 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(*  Title:      HOL/Lex/NAe.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-Goal "steps A w O (eps A)^* = steps A w";
-by (case_tac "w" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
-qed_spec_mp "steps_epsclosure";
-Addsimps [steps_epsclosure];
-
-Goal "[| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w";
-by (rtac (steps_epsclosure RS equalityE) 1);
-by (Blast_tac 1);
-qed "in_steps_epsclosure";
-
-Goal "(eps A)^* O steps A w = steps A w";
-by (induct_tac "w" 1);
- by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [O_assoc RS sym]) 1);
-qed "epsclosure_steps";
-
-Goal "[| (p,q) : steps A w; (q,r) : (eps A)^* |] ==> (p,r) : steps A w";
-by (rtac (epsclosure_steps RS equalityE) 1);
-by (Blast_tac 1);
-qed "in_epsclosure_steps";
-
-Goal "steps A (v@w) = steps A w  O  steps A v";
-by (induct_tac "v" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
-qed "steps_append";
-Addsimps [steps_append];
-
-Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
-by (rtac (steps_append RS equalityE) 1);
-by (Blast_tac 1);
-qed "in_steps_append";
-AddIffs [in_steps_append];
-
-(* 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";
-*)
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/NAe.thy
--- a/src/HOL/Lex/NAe.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/NAe.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -6,9 +6,9 @@
 Nondeterministic automata with epsilon transitions
 *)
 
-NAe = NA +
+theory NAe = NA:
 
-types ('a,'s)nae = ('a option,'s)na
+types ('a,'s)nae = "('a option,'s)na"
 
 syntax eps :: "('a,'s)nae => ('s * 's)set"
 translations "eps A" == "step A None"
@@ -19,7 +19,7 @@
 "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,'s)nae => 'a list => bool"
 "accepts A w == ? q. (start A,q) : steps A w & fin A q"
 
 (* not really used:
@@ -28,4 +28,45 @@
 "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 cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/RegExp2NA.ML
--- a/src/HOL/Lex/RegExp2NA.ML	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/RegExp2NA.ML	Thu Mar 04 10:04:42 2004 +0100
@@ -16,7 +16,7 @@
 by (Simp_tac 1);
 qed "start_atom";
 
-Goalw [atom_def,step_def]
+Goalw [atom_def,thm"step_def"]
  "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)";
 by (Simp_tac 1);
 qed "in_step_atom_Some";
@@ -40,7 +40,7 @@
 Goal
  "accepts (atom a) w = (w = [a])";
 by (simp_tac(simpset() addsimps
-       [accepts_conv_steps,start_fin_in_steps_atom,fin_atom]) 1);
+       [thm"accepts_conv_steps",start_fin_in_steps_atom,fin_atom]) 1);
 qed "accepts_atom";
 
 
@@ -64,13 +64,13 @@
 
 (***** True/False ueber step anheben *****)
 
-Goalw [or_def,step_def]
+Goalw [or_def,thm"step_def"]
 "!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "True_in_step_or";
 
-Goalw [or_def,step_def]
+Goalw [or_def,thm"step_def"]
 "!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)";
 by (Simp_tac 1);
 by (Blast_tac 1);
@@ -98,7 +98,7 @@
 
 (** From the start  **)
 
-Goalw [or_def,step_def]
+Goalw [or_def,thm"step_def"]
  "!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))";
@@ -128,7 +128,7 @@
 
 Goal
  "accepts (or L R) w = (accepts L w | accepts R w)";
-by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_or]) 1);
+by (simp_tac (simpset() addsimps [thm"accepts_conv_steps",steps_or]) 1);
 (* get rid of case_tac: *)
 by (case_tac "w = []" 1);
 by (Auto_tac);
@@ -155,7 +155,7 @@
 
 (** True/False in step **)
 
-Goalw [conc_def,step_def]
+Goalw [conc_def,thm"step_def"]
  "!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)))";
@@ -163,7 +163,7 @@
 by (Blast_tac 1);
 qed_spec_mp "True_step_conc";
 
-Goalw [conc_def,step_def]
+Goalw [conc_def,thm"step_def"]
  "!L R. (False#p,q) : step (conc L R) a = \
 \       (? r. q = False#r & (p,r) : step R a)";
 by (Simp_tac 1);
@@ -256,7 +256,7 @@
 Goal
  "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
 by (simp_tac (simpset() addsimps
-     [accepts_conv_steps,True_steps_conc,final_conc,start_conc]) 1);
+     [thm"accepts_conv_steps",True_steps_conc,final_conc,start_conc]) 1);
 by (rtac iffI 1);
  by (Clarify_tac 1);
  by (etac disjE 1);
@@ -284,7 +284,7 @@
 (*                     epsilon                        *)
 (******************************************************)
 
-Goalw [epsilon_def,step_def] "step epsilon a = {}";
+Goalw [epsilon_def,thm"step_def"] "step epsilon a = {}";
 by (Simp_tac 1);
 qed "step_epsilon";
 Addsimps [step_epsilon];
@@ -295,7 +295,7 @@
 qed "steps_epsilon";
 
 Goal "accepts epsilon w = (w = [])";
-by (simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
+by (simp_tac (simpset() addsimps [steps_epsilon,thm"accepts_conv_steps"]) 1);
 by (simp_tac (simpset() addsimps [epsilon_def]) 1);
 qed "accepts_epsilon";
 AddIffs [accepts_epsilon];
@@ -314,7 +314,7 @@
 qed_spec_mp "fin_plus";
 AddIffs [fin_plus];
 
-Goalw [plus_def,step_def]
+Goalw [plus_def,thm"step_def"]
   "!A. (p,q) : step A a --> (p,q) : step (plus A) a";
 by (Simp_tac 1);
 qed_spec_mp "step_plusI";
@@ -326,7 +326,7 @@
 by (blast_tac (claset() addIs [step_plusI]) 1);
 qed_spec_mp "steps_plusI";
 
-Goalw [plus_def,step_def]
+Goalw [plus_def,thm"step_def"]
  "!A. (p,r): step (plus A) a = \
 \     ( (p,r): step A a | fin A p & (start A,r) : step A a )";
 by (Simp_tac 1);
@@ -361,13 +361,13 @@
  by (Asm_simp_tac 1);
  by (Blast_tac 1);
 by (res_inst_tac [("x","us@[v]")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (asm_full_simp_tac (simpset() addsimps [thm"accepts_conv_steps"]) 1);
 by (Blast_tac 1);
 qed_spec_mp "start_steps_plusD";
 
 Goal
  "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
-by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (simp_tac (simpset() addsimps [thm"accepts_conv_steps"]) 1);
 by (res_inst_tac [("xs","us")] rev_induct 1);
  by (Simp_tac 1);
 by (rename_tac "u us" 1);
@@ -388,12 +388,12 @@
  "accepts (plus A) w = \
 \ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))";
 by (rtac iffI 1);
- by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [thm"accepts_conv_steps"]) 1);
  by (Clarify_tac 1);
  by (dtac start_steps_plusD 1);
  by (Clarify_tac 1);
  by (res_inst_tac [("x","us@[v]")] exI 1);
- by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [thm"accepts_conv_steps"]) 1);
  by (Blast_tac 1);
 by (blast_tac (claset() addIs [steps_star_cycle]) 1);
 qed "accepts_plus";
@@ -421,7 +421,7 @@
 Goal
  "!w. accepts (rexp2na r) w = (w : lang r)";
 by (induct_tac "r" 1);
-    by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+    by (simp_tac (simpset() addsimps [thm"accepts_conv_steps"]) 1);
    by (simp_tac(simpset() addsimps [accepts_atom]) 1);
   by (Asm_simp_tac 1);
  by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Mar 04 10:04:42 2004 +0100
@@ -18,13 +18,13 @@
 
 (* Use {x. False} = {}? *)
 
-Goalw [atom_def,step_def]
+Goalw [atom_def,thm"step_def"]
  "eps(atom a) = {}";
 by (Simp_tac 1);
 qed "eps_atom";
 Addsimps [eps_atom];
 
-Goalw [atom_def,step_def]
+Goalw [atom_def,thm"step_def"]
  "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)";
 by (Simp_tac 1);
 qed "in_step_atom_Some";
@@ -45,7 +45,7 @@
 
 Goal "accepts (atom a) w = (w = [a])";
 by (simp_tac(simpset() addsimps
-       [accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
+       [thm"accepts_def",start_fin_in_steps_atom,fin_atom]) 1);
 qed "accepts_atom";
 
 
@@ -69,13 +69,13 @@
 
 (***** True/False ueber step anheben *****)
 
-Goalw [or_def,step_def]
+Goalw [or_def,thm"step_def"]
 "!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "True_in_step_or";
 
-Goalw [or_def,step_def]
+Goalw [or_def,thm"step_def"]
 "!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)";
 by (Simp_tac 1);
 by (Blast_tac 1);
@@ -173,14 +173,14 @@
   read_instantiate [("p","start(or L R)")] in_unfold_rtrancl2;
 AddIffs [epsclosure_start_step_or];
 
-Goalw [or_def,step_def]
+Goalw [or_def,thm"step_def"]
  "!L R. (start(or L R),q) : eps(or L R) = \
 \       (q = True#start L | q = False#start R)";
 by (Simp_tac 1);
 qed_spec_mp "start_eps_or";
 AddIffs [start_eps_or];
 
-Goalw [or_def,step_def]
+Goalw [or_def,thm"step_def"]
  "!L R. (start(or L R),q) ~: step (or L R) (Some a)";
 by (Simp_tac 1);
 qed_spec_mp "not_start_step_or_Some";
@@ -204,7 +204,7 @@
 qed_spec_mp "start_or_not_final";
 AddIffs [start_or_not_final];
 
-Goalw [accepts_def]
+Goalw [thm"accepts_def"]
  "accepts (or L R) w = (accepts L w | accepts R w)";
 by (simp_tac (simpset() addsimps [steps_or]) 1);
 by Auto_tac;
@@ -231,7 +231,7 @@
 
 (** True/False in step **)
 
-Goalw [conc_def,step_def]
+Goalw [conc_def,thm"step_def"]
  "!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))";
@@ -239,7 +239,7 @@
 by (Blast_tac 1);
 qed_spec_mp "True_step_conc";
 
-Goalw [conc_def,step_def]
+Goalw [conc_def,thm"step_def"]
  "!L R. (False#p,q) : step (conc L R) a = \
 \       (? r. q = False#r & (p,r) : step R a)";
 by (Simp_tac 1);
@@ -319,7 +319,7 @@
 by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma2a = result();
 
-Goalw [conc_def,step_def]
+Goalw [conc_def,thm"step_def"]
  "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None";
 by (split_all_tac 1);
 by (Asm_full_simp_tac 1);
@@ -333,7 +333,7 @@
 by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma2b = result();
 
-Goalw [conc_def,step_def]
+Goalw [conc_def,thm"step_def"]
  "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)";
 by (split_all_tac 1);
 by (Asm_full_simp_tac 1);
@@ -396,7 +396,7 @@
 \  (? 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_tac (claset() addDs [True_steps_concD]
-     addIs [True_True_steps_concI,in_steps_epsclosure]) 1);
+     addIs [True_True_steps_concI,thm"in_steps_epsclosure"]) 1);
 qed "True_steps_conc";
 
 (** starting from the start **)
@@ -414,7 +414,7 @@
 Goal
  "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
 by (simp_tac (simpset() addsimps
-     [accepts_def,True_steps_conc,final_conc,start_conc]) 1);
+     [thm"accepts_def",True_steps_conc,final_conc,start_conc]) 1);
 by (Blast_tac 1);
 qed "accepts_conc";
 
@@ -422,7 +422,7 @@
 (*                       star                         *)
 (******************************************************)
 
-Goalw [star_def,step_def]
+Goalw [star_def,thm"step_def"]
  "!A. (True#p,q) : eps(star A) = \
 \     ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )";
 by (Simp_tac 1);
@@ -430,7 +430,7 @@
 qed_spec_mp "True_in_eps_star";
 AddIffs [True_in_eps_star];
 
-Goalw [star_def,step_def]
+Goalw [star_def,thm"step_def"]
   "!A. (p,q) : step A a --> (True#p, True#q) : step (star A) a";
 by (Simp_tac 1);
 qed_spec_mp "True_True_step_starI";
@@ -442,7 +442,7 @@
 by (blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
 qed_spec_mp "True_True_eps_starI";
 
-Goalw [star_def,step_def]
+Goalw [star_def,thm"step_def"]
  "!A. fin A p --> (True#p,True#start A) : eps(star A)";
 by (Simp_tac 1);
 qed_spec_mp "True_start_eps_starI";
@@ -483,7 +483,7 @@
 
 (** True in step Some **)
 
-Goalw [star_def,step_def]
+Goalw [star_def,thm"step_def"]
  "!A. (True#p,r): step (star A) (Some a) = \
 \     (? q. (p,q): step A (Some a) & r=True#q)";
 by (Simp_tac 1);
@@ -508,19 +508,19 @@
   by (Asm_simp_tac 1);
  by (Clarify_tac 1);
  by (Asm_simp_tac 1);
-by (simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
+by (simp_tac (simpset() addsimps [O_assoc,thm"epsclosure_steps"]) 1);
 by (Clarify_tac 1);
 by (etac allE 1 THEN mp_tac 1);
 by (Clarify_tac 1);
 by (etac disjE 1);
  by (res_inst_tac [("x","us")] exI 1);
  by (res_inst_tac [("x","v@[x]")] exI 1);
- by (asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
+ by (asm_simp_tac (simpset() addsimps [O_assoc,thm"epsclosure_steps"]) 1);
  by (Blast_tac 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("x","us@[v@[x]]")] exI 1);
 by (res_inst_tac [("x","[]")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [thm"accepts_def"]) 1);
 by (Blast_tac 1);
 qed_spec_mp "True_start_steps_starD";
 
@@ -531,13 +531,13 @@
 by (blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
 qed_spec_mp "True_True_steps_starI";
 
-Goalw [accepts_def]
+Goalw [thm"accepts_def"]
  "(!u : set us. accepts A u) --> \
 \ (True#start A,True#start A) : steps (star A) (concat us)";
 by (induct_tac "us" 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
-by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,in_epsclosure_steps]) 1);
+by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,thm"in_epsclosure_steps"]) 1);
 qed_spec_mp "steps_star_cycle";
 
 (* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
@@ -555,7 +555,7 @@
 
 (** the start state **)
 
-Goalw [star_def,step_def]
+Goalw [star_def,thm"step_def"]
   "!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)";
 by (Simp_tac 1);
 qed_spec_mp "start_step_star";
@@ -578,7 +578,7 @@
  by (Blast_tac 1);
 by (etac disjE 1);
  by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [in_steps_epsclosure]) 1);
+by (blast_tac (claset() addIs [thm"in_steps_epsclosure"]) 1);
 qed "start_steps_star";
 
 Goalw [star_def] "!A. fin (star A) (True#p) = fin A p";
@@ -592,7 +592,7 @@
 AddIffs [fin_star_start];
 
 (* too complex! Simpler if loop back to start(star A)? *)
-Goalw [accepts_def]
+Goalw [thm"accepts_def"]
  "accepts (star A) w = \
 \ (? us. (!u : set(us). accepts A u) & (w = concat us) )";
 by (simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
@@ -605,14 +605,14 @@
   by (Simp_tac 1);
  by (Clarify_tac 1);
  by (res_inst_tac [("x","us@[v]")] exI 1);
- by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [thm"accepts_def"]) 1);
  by (Blast_tac 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("xs","us")] rev_exhaust 1);
  by (Asm_simp_tac 1);
  by (Blast_tac 1);
 by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [thm"accepts_def"]) 1);
 by (Blast_tac 1);
 qed "accepts_star";
 
@@ -622,7 +622,7 @@
 Goal
  "!w. accepts (rexp2nae r) w = (w : lang r)";
 by (induct_tac "r" 1);
-    by (simp_tac (simpset() addsimps [accepts_def]) 1);
+    by (simp_tac (simpset() addsimps [thm"accepts_def"]) 1);
    by (simp_tac(simpset() addsimps [accepts_atom]) 1);
   by (asm_simp_tac (simpset() addsimps [accepts_or]) 1);
  by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
diff -r cea7d2f76112 -r bb2b0e10d9be src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Mar 04 10:04:42 2004 +0100
@@ -204,5 +204,5 @@
  "[| bounded (next A) k; start A < k; j < k |] ==> \
 \ w : regset_of_DA A k = accepts A w";
 by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps
- [regset_below,deltas_below,accepts_def,delta_def]) 1);
+ [regset_below,deltas_below,thm"accepts_def",thm"delta_def"]) 1);
 qed "regset_DA_equiv";