# HG changeset patch
# User nipkow
# Date 894890440 -7200
# Node ID 697d17fe16654b77e7e2476ad232c5155f3d031b
# Parent  2213a9ac0e4c63f23b6b6378df063f4952dc2d92
Reordered a few parameters.

diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/AutoMaxChop.ML
--- a/src/HOL/Lex/AutoMaxChop.ML	Mon May 11 13:18:25 1998 +0200
+++ b/src/HOL/Lex/AutoMaxChop.ML	Mon May 11 14:40:40 1998 +0200
@@ -9,8 +9,8 @@
 qed "delta_snoc";
 
 goal thy
- "!q ps res. auto_split A (delta A ps q) ps xs res = \
-\            maxsplit (%ys. fin A (delta A ys q)) ps xs res";
+ "!q ps res. auto_split A (delta A ps q) res ps xs = \
+\            maxsplit (%ys. fin A (delta A ys q)) res ps xs";
 by(induct_tac "xs" 1);
 by(Simp_tac 1);
 by(asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
@@ -18,14 +18,14 @@
 qed_spec_mp "auto_split_lemma";
 
 goalw thy [accepts_def]
- "auto_split A (start A) [] xs res = maxsplit (accepts A) [] xs res";
+ "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 auto_split_lemma 1);
 by(Simp_tac 1);
 qed_spec_mp "auto_split_is_maxsplit";
 
 goal thy
- "is_maxsplitter (accepts A) (%xs. auto_split A (start A) [] xs ([],xs))";
+ "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);
 qed "is_maxsplitter_auto_split";
diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/AutoMaxChop.thy
--- a/src/HOL/Lex/AutoMaxChop.thy	Mon May 11 13:18:25 1998 +0200
+++ b/src/HOL/Lex/AutoMaxChop.thy	Mon May 11 14:40:40 1998 +0200
@@ -7,14 +7,13 @@
 AutoMaxChop = DA + MaxChop +
 
 consts
- auto_split :: "('a,'s)da => 's => 'a list => 'a list => 'a list * 'a list
-                => 'a list * 'a list"
+ auto_split :: "('a,'s)da => 's  => 'a list * 'a list => 'a list => 'a splitter"
 primrec auto_split list
-"auto_split A q ps []     res = (if fin A q then (ps,[]) else res)"
-"auto_split A q ps (x#xs) res = auto_split A (next A x q) (ps@[x]) xs
-                                     (if fin A q then (ps,x#xs) else res)"
+"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))"
+"auto_chop A == chop (%xs. auto_split A (start A) ([],xs) [] xs)"
 end
diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Mon May 11 13:18:25 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Mon May 11 14:40:40 1998 +0200
@@ -6,7 +6,7 @@
 
 (* Termination of chop *)
 
-goalw thy [reducing_def] "reducing(%qs. maxsplit P [] qs ([],qs))";
+goalw thy [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)";
 by(asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1);
 qed "reducing_maxsplit";
 
diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/MaxPrefix.ML
--- a/src/HOL/Lex/MaxPrefix.ML	Mon May 11 13:18:25 1998 +0200
+++ b/src/HOL/Lex/MaxPrefix.ML	Mon May 11 14:40:40 1998 +0200
@@ -6,8 +6,8 @@
 
 Delsplits [split_if];
 goalw thy [is_maxpref_def] "!(ps::'a list) res. \
-\ (maxsplit P ps qs res = (xs,ys)) = \
-\ (if (? us. us <= qs & P(ps@us)) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \
+\ (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);
@@ -56,7 +56,7 @@
 Addsimps [is_maxpref_Nil];
 
 goalw thy [is_maxsplitter_def]
- "is_maxsplitter P (%xs. maxsplit P [] xs ([],xs))";
+ "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";
diff -r 2213a9ac0e4c -r 697d17fe1665 src/HOL/Lex/MaxPrefix.thy
--- a/src/HOL/Lex/MaxPrefix.thy	Mon May 11 13:18:25 1998 +0200
+++ b/src/HOL/Lex/MaxPrefix.thy	Mon May 11 14:40:40 1998 +0200
@@ -18,10 +18,9 @@
  (!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 list
-              => 'a list * 'a list"
+ maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => 'a splitter"
 primrec maxsplit list
-"maxsplit P ps []     res = (if P ps then (ps,[]) else res)"
-"maxsplit P ps (q#qs) res = maxsplit P (ps@[q]) qs
-                               (if P ps then (ps,q#qs) else res)"
+"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"
 end