# HG changeset patch
# User nipkow
# Date 889532833 -3600
# Node ID bcdf68c78e18a241a24a16892893128972c19715
# Parent  bea2ab2e360b0b730c9a00d7ff122942dca7c463
New scanner in abstract form.

diff -r bea2ab2e360b -r bcdf68c78e18 src/HOL/Lex/AutoMaxChop.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/AutoMaxChop.ML	Tue Mar 10 13:27:13 1998 +0100
@@ -0,0 +1,44 @@
+(*  Title:      HOL/Lex/AutoMaxChop.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+goal thy "!q ys. nexts A q (xs@ys) = nexts A (nexts A q xs) ys";
+by(induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "nexts_append";
+Addsimps [nexts_append];
+
+goal thy "nexts A q (xs@[y]) = next A (nexts A q xs) y";
+by(Simp_tac 1);
+qed "nexts_snoc";
+Addsimps [nexts_append];
+
+goal thy
+ "!q ps res. auto_split A (nexts A q ps) ps xs res = \
+\            maxsplit (%ys. fin A (nexts A q ys)) ps xs res";
+by(induct_tac "xs" 1);
+by(Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps [nexts_snoc RS sym]
+                           delsimps [nexts_append]) 1);
+qed_spec_mp "auto_split_lemma";
+
+goalw thy [accepts_def]
+ "auto_split A (start A) [] xs res = maxsplit (accepts A) [] xs res";
+by(stac ((read_instantiate [("st","start A")] nexts_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))";
+by(simp_tac (simpset() addsimps
+        [auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1);
+qed "is_maxsplitter_auto_split";
+
+goalw thy [auto_chop_def]
+ "is_maxchopper (accepts A) (auto_chop A)";
+br is_maxchopper_chop 1;
+br is_maxsplitter_auto_split 1;
+qed "is_maxchopper_auto_chop";
diff -r bea2ab2e360b -r bcdf68c78e18 src/HOL/Lex/AutoMaxChop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/AutoMaxChop.thy	Tue Mar 10 13:27:13 1998 +0100
@@ -0,0 +1,20 @@
+(*  Title:      HOL/Lex/AutoMaxChop.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+AutoMaxChop = Auto + MaxChop +
+
+consts
+ auto_split :: "('a,'s)auto => 's => 'a list => 'a list => 'a list * 'a list
+                => 'a list * 'a list"
+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 q x) (ps@[x]) xs
+                                     (if fin A q then (ps,x#xs) else res)"
+
+constdefs
+ auto_chop :: "('a,'s)auto => 'a chopper"
+"auto_chop A == chop (%xs. auto_split A (start A) [] xs ([],xs))"
+end
diff -r bea2ab2e360b -r bcdf68c78e18 src/HOL/Lex/MaxChop.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/MaxChop.ML	Tue Mar 10 13:27:13 1998 +0100
@@ -0,0 +1,106 @@
+(*  Title:      HOL/Lex/MaxChop.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+(* Termination of chop *)
+
+goalw thy [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.rules in lemma RS chopr_rule end;
+
+goalw thy [chop_def] "!!splitf. 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] addcongs [if_weak_cong]) 1);
+by(simp_tac (simpset() addsimps [Let_def] addsplits [expand_split]) 1);
+qed "chop_rule";
+
+goalw thy [is_maxsplitter_def,reducing_def]
+ "!!splitf. is_maxsplitter P splitf ==> reducing splitf";
+by(Asm_full_simp_tac 1);
+qed "is_maxsplitter_reducing";
+
+goal thy "!!P. is_maxsplitter P splitf ==> \
+\ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
+by(res_inst_tac [("xs","xs")] length_induct 1);
+by(asm_simp_tac (simpset() delsplits [expand_if]
+                           addsimps [chop_rule,is_maxsplitter_reducing]
+                           addcongs [if_weak_cong]) 1);
+by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
+                                addsplits [expand_split]) 1);
+qed_spec_mp "chop_concat";
+
+goal thy "!!P. is_maxsplitter P splitf ==> \
+\ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
+by(res_inst_tac [("xs","xs")] length_induct 1);
+by(asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
+                           addcongs [if_weak_cong]) 1);
+by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
+                                addsplits [expand_split]) 1);
+by(simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
+                       addsplits [expand_split]) 1);
+be thin_rl 1;
+by(strip_tac 1);
+br ballI 1;
+be exE 1;
+be allE 1;
+auto();
+qed_spec_mp "chop_nonempty";
+
+val [prem] = goalw thy [is_maxchopper_def]
+ "is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)";
+by(Clarify_tac 1);
+br iffI 1;
+ br conjI 1;
+  be (prem RS chop_concat) 1;
+ br conjI 1;
+  be (prem RS chop_nonempty) 1;
+ be 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 [expand_split]) 1);
+ by(Clarify_tac 1);
+ br conjI 1;
+  by(Clarify_tac 1);
+  by(Asm_full_simp_tac 1);
+ by(Clarify_tac 1);
+ by(Asm_full_simp_tac 1);
+ by(forward_tac [prem RS chop_concat] 1);
+ by(Clarify_tac 1);
+ ba 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 [expand_split]) 1);
+by(Clarify_tac 1);
+br conjI 1;
+ by(Clarify_tac 1);
+ by(exhaust_tac "yss" 1);
+  by(Asm_simp_tac 1);
+ by(Asm_full_simp_tac 1);
+ by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
+ by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
+by(exhaust_tac "yss" 1);
+ by(Asm_full_simp_tac 1);
+ by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
+ by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
+by(Clarify_tac 1);
+by(Asm_full_simp_tac 1);
+by(subgoal_tac "x=a" 1);
+ by(Clarify_tac 1);
+ by(Asm_full_simp_tac 1);
+by(rotate_tac ~2 1);
+by(Asm_full_simp_tac 1);
+by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
+by(blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);
+qed "is_maxchopper_chop";
diff -r bea2ab2e360b -r bcdf68c78e18 src/HOL/Lex/MaxChop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/MaxChop.thy	Tue Mar 10 13:27:13 1998 +0100
@@ -0,0 +1,39 @@
+(*  Title:      HOL/Lex/MaxChop.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+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 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)"
+
+end
diff -r bea2ab2e360b -r bcdf68c78e18 src/HOL/Lex/MaxPrefix.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/MaxPrefix.ML	Tue Mar 10 13:27:13 1998 +0100
@@ -0,0 +1,65 @@
+(*  Title:      HOL/Lex/MaxPrefix.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+Delsplits [expand_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) \
+\  else (xs,ys)=res)";
+by(induct_tac "qs" 1);
+ by(simp_tac (simpset() addsplits [expand_if]) 1);
+ by(Blast_tac 1);
+by(Asm_simp_tac 1);
+be 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 [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(exhaust_tac "us" 1);
+  br iffI 1;
+   by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
+   by(Blast_tac 1);
+  by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
+  by(Clarify_tac 1);
+  be disjE 1;
+   by(fast_tac (claset() addDs [prefix_antisym]) 1);
+  by(Clarify_tac 1);
+  be disjE 1;
+   by(Clarify_tac 1);
+   by(Asm_full_simp_tac 1);
+  be disjE 1;
+   by(Clarify_tac 1);
+   by(Asm_full_simp_tac 1);
+ by(Blast_tac 1);
+ by(Asm_full_simp_tac 1);
+ by(Blast_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 [expand_if];
+
+goalw thy [is_maxpref_def]
+ "!!P. ~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])";
+by(Blast_tac 1);
+qed "is_maxpref_Nil";
+Addsimps [is_maxpref_Nil];
+
+goalw thy [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 bea2ab2e360b -r bcdf68c78e18 src/HOL/Lex/MaxPrefix.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/MaxPrefix.thy	Tue Mar 10 13:27:13 1998 +0100
@@ -0,0 +1,27 @@
+(*  Title:      HOL/Lex/MaxPrefix.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+MaxPrefix = 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 list
+              => 'a list * 'a list"
+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)"
+end