# HG changeset patch
# User nipkow
# Date 895157660 -7200
# Node ID 2ec84dee79119ae95cef9e2dbe47fdd29dcde519
# Parent  89271bc4e7ed3a59b8d086fc7c2b16cc33ccbead
Reordred arguments in AutoChopper.
Updated README with ref to paper.

diff -r 89271bc4e7ed -r 2ec84dee7911 src/HOL/Lex/AutoChopper.ML
--- a/src/HOL/Lex/AutoChopper.ML	Thu May 14 16:50:09 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Thu May 14 16:54:20 1998 +0200
@@ -34,17 +34,17 @@
 qed"acc_prefix_Cons";
 Addsimps [acc_prefix_Cons];
 
-goal thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
-by (list.induct_tac "xs" 1);
+goal thy "!st us p y ys. acc A st p xs (ys@[y]) us ~= ([],zs)";
+by (induct_tac "xs" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 val accept_not_Nil = result() repeat_RS spec;
 Addsimps [accept_not_Nil];
 
 goal thy
-"!st us. acc xs st [] us ([],ys) A = ([], zs) --> \
+"!st us. acc A st ([],ys) xs [] us = ([], zs) --> \
 \        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (delta A ys st))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (simp_tac (simpset() addcongs [conj_cong]) 1);
 by (Simp_tac 1);
 by (strip_tac 1);
@@ -58,7 +58,7 @@
 by (case_tac "zsa = []" 1);
 by (Asm_simp_tac 1);
 by (Fast_tac 1);
-bind_thm("no_acc", result() RS spec RS spec RS mp);
+qed_spec_mp "no_acc";
 
 
 val [prem] = goal HOL.thy "? x. P(f(x)) ==> ? y. P(y)";
@@ -69,12 +69,12 @@
 
 goal thy
 "! r erk l rst st ys yss zs::'a list. \
-\    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
+\    acc A st (l,rst) xs erk r = (ys#yss, zs) --> \
 \    ys@concat(yss)@zs = (if acc_prefix A xs st then r@xs else erk@concat(l)@rst)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
 by (Asm_simp_tac 1);
-by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 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 (res_inst_tac[("xs","vss")] list_eq_cases 1);
@@ -88,16 +88,16 @@
 
 goal thy
  "! st erk r l rest ys yss zs.\
-\   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
+\   acc A st (l,rest) xs erk 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 (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 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);
@@ -111,18 +111,18 @@
 
 goal thy  
  "! st erk r l rest ys yss zs. \
-\   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
+\   acc A st (l,rest) xs erk 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 (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (strip_tac 1);
 by (rtac conjI 1);
- by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 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);
@@ -150,22 +150,22 @@
 
 goal thy
  "! st erk r l rest ys yss zs. \
-\   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
+\   acc A st (l,rest) xs erk r = (ys#yss, zs) --> \
 \     (if acc_prefix A xs st       \
-\      then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
+\      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 (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 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 list (start A) [] [] ([],list) A = (yss,zs)" 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);
@@ -189,12 +189,12 @@
 Delsimps [split_paired_All];
 goal thy 
 "! st erk r p ys yss zs. \
-\  acc xs st erk r p A = (ys#yss, zs) --> \
+\  acc A st p xs erk 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 (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
diff -r 89271bc4e7ed -r 2ec84dee7911 src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Thu May 14 16:50:09 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.thy	Thu May 14 16:54:20 1998 +0200
@@ -14,6 +14,9 @@
 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.
 *)
 
 AutoChopper = Prefix + DA + Chopper +
@@ -24,21 +27,20 @@
     !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
 
 consts
-  acc :: "['a list, 's, 'a list, 'a list, 'a list list*'a list, ('a,'s)da]
+  acc :: "[('a,'s)da, 's, 'a list list*'a list, 'a list, 'a list, 'a list]
           => 'a list list * 'a list"
 primrec acc List.list
-  "acc [] st ys zs chopsr A =
-              (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
-  "acc(x#xs) s ys zs chopsr A =
+  "acc A s r []     ys zs = (if ys=[] then r else (ys#fst(r),snd(r)))" 
+  "acc A s r (x#xs) ys zs =
             (let t = next A x s
              in if fin A t
-                then acc xs t (zs@[x]) (zs@[x])
-                         (acc xs (start A) [] [] ([],xs) A) A
-                else acc xs t ys (zs@[x]) chopsr A)"
+                then acc A t (acc A (start A) ([],xs) xs [] [])
+                         xs (zs@[x]) (zs@[x])
+                else acc A t r xs ys (zs@[x]))"
 
 constdefs
  auto_chopper :: ('a,'s)da => 'a chopper
-"auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
+"auto_chopper A xs == acc A (start A) ([],xs) xs [] []"
 
 (* acc_prefix is an auxiliary notion for the proof *)
 constdefs
diff -r 89271bc4e7ed -r 2ec84dee7911 src/HOL/Lex/README.html
--- a/src/HOL/Lex/README.html	Thu May 14 16:50:09 1998 +0200
+++ b/src/HOL/Lex/README.html	Thu May 14 16:54:20 1998 +0200
@@ -1,45 +1,31 @@
+<!-- $Id$ -->
 <HTML><HEAD><TITLE>HOL/Lex/README</TITLE></HEAD>
 <BODY>
 
 <H1>A Simplified Scanner Generator</H1>
 
-This is half of a simplified functional scanner generator. The overall design
-is like this:
-<PRE>
-         regular expression
-                  |
-                  v
-             -----------
-             | mk_auto |
-             -----------
-                  |
-        deterministic automaton
-                  |
-                  v
-           ----------------
-string --> | auto_chopper | --> chopped up string
-           ----------------
-</PRE>
-A chopped up string is a pair of
-<UL>
-<LI>a prefix of the input string, chopped up into words of the language,
-<LI>together with the remaining suffix.
-</UL>
-For example, if the language consists just of the word <KBD>ab</KBD>, the
-input <KBD>ababaab</KBD> is partitioned into a chopped up prefix
-<KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
-<P>
+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>.
+<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, 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>
 
-The auto_chopper is implemented in theory AutoChopper. An alternative (more
-efficient) version is defined in AutoChopper1. However, no properties have
-been proved for it yet.
-
-The top part of the diagram, i.e. the translation of regular expressions into
-deterministic finite automata is still missing (although we have some bits
-and pieces).
-<P>
-
-The directory also contains Regset_of_auto, a theory describing the
-translation of deterministic automata into regular sets.
 </BODY>
 </HTML>