# HG changeset patch
# User nipkow
# Date 878717315 -3600
# Node ID 2ce2e659c2b1e770b56a4a796ffa9d2fffd9a55a
# Parent  ba267836dd7a1a500eb75ddcdba6145b7f472332
Added an alternativ version of AutoChopper and a theory for the conversion of
automata into regular sets.

diff -r ba267836dd7a -r 2ce2e659c2b1 src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Tue Nov 04 20:52:20 1997 +0100
+++ b/src/HOL/Lex/AutoChopper.thy	Wed Nov 05 09:08:35 1997 +0100
@@ -12,6 +12,8 @@
 
 WARNING: auto_chopper is exponential(?)
 if the recursive calls in the penultimate argument are evaluated eagerly.
+
+A more efficient version is defined in AutoChopper1.
 *)
 
 AutoChopper = Auto + Chopper +
@@ -39,32 +41,3 @@
                 else acc xs (nxt st x) ys (zs@[x]) chopsr A)"
 
 end
-
-(* The following definition of acc should also work:
-consts
-  acc1 :: [('a,'b)auto, 'a list, 'b, 'a list list, 'a list, 'a list]
-          => 'a list list * 'a list
-
-acc1 A [] s xss zs xs =
-  (if xs=[] then (xss, zs)
-   else acc1 A zs (start A) (xss @ [xs]) [] [])
-acc1 A (y#ys) s xss zs rec =
-  let s' = next A s;
-      zs' = (if fin A s' then [] else zs@[y])
-      xs' = (if fin A s' then xs@zs@[y] else xs)
-  in acc1 A ys s' xss zs' xs'
-
-Advantage: does not need lazy evaluation for reasonable (quadratic)
-performance.
-
-Disadavantage: not primrec.
-  
-Termination measure:
-  size(A,ys,s,xss,zs,rec) = (|xs| + |ys| + |zs|, |ys|)
-
-Termination proof: the first clause reduces the first component by |xs|,
-the second clause leaves the first component alone but reduces the second by 1.
-
-Claim: acc1 A xs s [] [] [] = acc xs s [] [] ([],xs) A
-Generalization?
-*)
diff -r ba267836dd7a -r 2ce2e659c2b1 src/HOL/Lex/AutoChopper1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/AutoChopper1.thy	Wed Nov 05 09:08:35 1997 +0100
@@ -0,0 +1,37 @@
+(*  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.
+*)
+
+AutoChopper1 = Auto + Chopper + WF_Rel +
+
+consts
+  acc :: "(('a,'b)auto * 'a list * 'b * 'a list list * 'a list * 'a list)
+          => 'a list list * 'a list"
+recdef acc "inv_image (less_than ** less_than)
+              (%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs,
+                                     length ys))"
+simpset "simpset() addsimps (less_add_Suc2::add_ac) addsplits [expand_if]"
+"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 s y;
+      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 ba267836dd7a -r 2ce2e659c2b1 src/HOL/Lex/README.html
--- a/src/HOL/Lex/README.html	Tue Nov 04 20:52:20 1997 +0100
+++ b/src/HOL/Lex/README.html	Wed Nov 05 09:08:35 1997 +0100
@@ -30,9 +30,16 @@
 <KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
 <P>
 
-The auto_chopper is implemented in theory AutoChopper. The top part of the
-diagram, i.e. the translation of regular expressions into deterministic
-finite automata is still missing.  <P>
+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>
diff -r ba267836dd7a -r 2ce2e659c2b1 src/HOL/Lex/ROOT.ML
--- a/src/HOL/Lex/ROOT.ML	Tue Nov 04 20:52:20 1997 +0100
+++ b/src/HOL/Lex/ROOT.ML	Wed Nov 05 09:08:35 1997 +0100
@@ -7,3 +7,5 @@
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
 use_thy"AutoChopper";
+use_thy"AutoChopper1";
+use_thy"Regset_of_auto";
diff -r ba267836dd7a -r 2ce2e659c2b1 src/HOL/Lex/Regset_of_auto.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Regset_of_auto.ML	Wed Nov 05 09:08:35 1997 +0100
@@ -0,0 +1,221 @@
+Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2];
+AddIs    [in_set_butlast_appendI1,in_set_butlast_appendI2];
+Addsimps [image_eqI];
+
+AddIffs [star.NilI];
+Addsimps [star.ConsI];
+AddIs [star.ConsI];
+
+(* Lists *)
+
+(*
+(* could go into List. Needs WF_Rel as ancestor. *)
+(* Induction over the length of a list: *)
+val prems = goal thy
+ "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
+by(res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
+     wf_induct 1);
+by(Simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
+bes prems 1;
+qed "list_length_induct";
+*)
+
+goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
+by(exhaust_tac "xs" 1);
+by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+qed "butlast_empty";
+AddIffs [butlast_empty];
+
+goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))";
+by(induct_tac "xss" 1);
+ by(Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
+                           addsplits [expand_if]) 1);
+br conjI 1;
+ by(Clarify_tac 1);
+ br conjI 1;
+  by(Blast_tac 1);
+ by(Clarify_tac 1);
+ by(subgoal_tac "xs=[]" 1);
+  by(rotate_tac ~1 1);
+  by(Asm_full_simp_tac 1);
+ by(Blast_tac 1);
+by(blast_tac (claset() addDs [in_set_butlastD]) 1);
+qed_spec_mp "in_set_butlast_concatI";
+
+(* Regular sets *)
+
+goal thy "(!xs: set xss. xs:A) --> concat xss : star A";
+by(induct_tac "xss" 1);
+by(ALLGOALS Asm_full_simp_tac);
+qed_spec_mp "concat_in_star";
+
+(* The main lemma:
+   how to decompose a trace into a prefix, a list of loops and a suffix.
+*)
+goal thy "!i. k : set(trace A i xs) --> (? pref mids suf. \
+\ xs = pref @ concat mids @ suf & \
+\ deltas A pref i = k & (!n:set(butlast(trace A i pref)). n ~= k) & \
+\ (!mid:set mids. (deltas A mid k = k) & \
+\                 (!n:set(butlast(trace A k mid)). n ~= k)) & \
+\ (!n:set(butlast(trace A k suf)). n ~= k))";
+by(induct_tac "xs" 1);
+ by(Simp_tac 1);
+by(rename_tac "a as" 1);
+br allI 1;
+by(case_tac "A a i = k" 1);
+ by(strip_tac 1);
+ by(res_inst_tac[("x","[a]")]exI 1);
+ by(Asm_full_simp_tac 1);
+ by(case_tac "k : set(trace A (A a i) as)" 1);
+  be allE 1;
+  be impE 1;
+   ba 1;
+  by(REPEAT(etac exE 1));
+  by(res_inst_tac[("x","pref#mids")]exI 1);
+  by(res_inst_tac[("x","suf")]exI 1);
+  by(Asm_full_simp_tac 1);
+ by(res_inst_tac[("x","[]")]exI 1);
+ by(res_inst_tac[("x","as")]exI 1);
+ by(Asm_full_simp_tac 1);
+ by(blast_tac (claset() addDs [in_set_butlastD]) 1);
+by(Asm_simp_tac 1);
+br conjI 1;
+ by(Blast_tac 1);
+by(strip_tac 1);
+be allE 1;
+be impE 1;
+ ba 1;
+by(REPEAT(etac exE 1));
+by(res_inst_tac[("x","a#pref")]exI 1);
+by(res_inst_tac[("x","mids")]exI 1);
+by(res_inst_tac[("x","suf")]exI 1);
+by(asm_simp_tac (simpset() addsplits [expand_if]) 1);
+qed_spec_mp "decompose";
+
+goal thy "!i. length(trace A i xs) = length xs";
+by(induct_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "length_trace";
+Addsimps [length_trace];
+
+goal thy "!i. deltas A (xs@ys) i = deltas A ys (deltas A xs i)";
+by(induct_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "deltas_append";
+Addsimps [deltas_append];
+
+goal thy "!i. trace A i (xs@ys) = trace A i xs @ trace A (deltas A xs i) ys";
+by(induct_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "trace_append";
+Addsimps [trace_append];
+
+goal thy "(!xs: set xss. deltas A xs i = i) --> \
+\         trace A i (concat xss) = concat (map (trace A i) xss)";
+by(induct_tac "xss" 1);
+by(ALLGOALS Asm_simp_tac);
+qed_spec_mp "trace_concat";
+Addsimps [trace_concat];
+
+goal thy "!i. (trace A i xs = []) = (xs = [])";
+by(exhaust_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "trace_is_Nil";
+Addsimps [trace_is_Nil];
+
+goal thy "(trace A i xs = n#ns) = \
+\         (case xs of [] => False | y#ys => n = A y i & ns = trace A n ys)";
+by(exhaust_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+by(Blast_tac 1);
+qed_spec_mp "trace_is_Cons_conv";
+Addsimps [trace_is_Cons_conv];
+
+goal thy "!i. set(trace A i xs) = \
+\ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))";
+by(induct_tac "xs" 1);
+ by(Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
+qed "set_trace_conv";
+
+goal thy
+ "(!mid:set mids. deltas A mid k = k) --> deltas A (concat mids) k = k";
+by(induct_tac "mids" 1);
+by(ALLGOALS Asm_simp_tac);
+qed_spec_mp "deltas_concat";
+Addsimps [deltas_concat];
+
+goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
+be nat_neqE 1;
+by(ALLGOALS trans_tac);
+val lemma = result();
+
+
+goal thy
+ "!i j xs. xs : regset_of A i j k = \
+\          ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)";
+by(induct_tac "k" 1);
+ by(simp_tac (simpset() addcongs [conj_cong]
+                        addsplits [expand_if,split_list_case]) 1);
+by(strip_tac 1);
+by(asm_simp_tac (simpset() addsimps [conc_def]) 1);
+br iffI 1;
+ be disjE 1;
+  by(Asm_simp_tac 1);
+ by(REPEAT(eresolve_tac[exE,conjE] 1));
+ by(Asm_full_simp_tac 1);
+ by(subgoal_tac
+      "(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1);
+  by(asm_simp_tac (simpset() addsplits [expand_if]
+       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
+ be star.induct 1;
+  by(Simp_tac 1);
+ by(asm_full_simp_tac (simpset() addsplits [expand_if]
+       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
+by(case_tac "k : set(butlast(trace A i xs))" 1);
+ br disjI1 2;
+ by(blast_tac (claset() addIs [lemma]) 2);
+br disjI2 1;
+bd (in_set_butlastD RS decompose) 1;
+by(Clarify_tac 1);
+by(res_inst_tac [("x","pref")] exI 1);
+by(Asm_full_simp_tac 1);
+br conjI 1;
+ br ballI 1;
+ br lemma 1;
+  by(Asm_simp_tac 2);
+ by(EVERY[dtac bspec 1, atac 2]);
+ by(Asm_simp_tac 1);
+by(res_inst_tac [("x","concat mids")] exI 1);
+by(Simp_tac 1);
+br conjI 1;
+ br concat_in_star 1;
+ by(Asm_simp_tac 1);
+ br ballI 1;
+ br ballI 1;
+ br lemma 1;
+  by(Asm_simp_tac 2);
+ by(EVERY[dtac bspec 1, atac 2]);
+ by(asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
+br ballI 1;
+br lemma 1;
+ by(Asm_simp_tac 2);
+by(EVERY[dtac bspec 1, atac 2]);
+by(Asm_simp_tac 1);
+qed_spec_mp "regset_of_spec";
+
+goal thy "!!A. !n. n < k --> (!x. A x n < k) ==> \
+\         !i. i < k --> (!n:set(trace A i xs). n < k)";
+by(induct_tac "xs" 1);
+ by(ALLGOALS Simp_tac);
+by(Blast_tac 1);
+qed_spec_mp "trace_below";
+
+goal thy "!!A. [| !n. n < k --> (!x. A x n < k); i < k; j < k |] ==> \
+\         regset_of A i j k = {xs. deltas A xs i = j}";
+br set_ext 1;
+by(simp_tac (simpset() addsimps [regset_of_spec]) 1);
+by(blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
+qed "regset_of_below";
diff -r ba267836dd7a -r 2ce2e659c2b1 src/HOL/Lex/Regset_of_auto.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Regset_of_auto.thy	Wed Nov 05 09:08:35 1997 +0100
@@ -0,0 +1,44 @@
+(*
+Conversion of automata into regular sets.
+use_thy"Auto";
+*)
+
+Regset_of_auto = List +
+
+(* autos *)
+
+types 'a auto = "'a => nat => nat"
+
+consts deltas :: 'a auto => 'a list => nat => nat
+primrec deltas list
+"deltas A [] i = i"
+"deltas A (x#xs) i = deltas A xs (A x i)"
+
+consts trace :: 'a auto => nat => 'a list => nat list
+primrec trace list
+"trace A i [] = []"
+"trace A i (x#xs) = A x i # trace A (A x i) xs"
+
+(* regular sets *)
+
+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"
+intrs
+  NilI   "[] : star A"
+  ConsI  "[| a:A; as : star A |] ==> a@as : star A"
+
+(* conversion a la Warshall *)
+
+consts regset_of :: 'a auto => nat => nat => nat => 'a list set
+primrec regset_of nat
+"regset_of A i j 0 = (if i=j then insert [] {[a] | a. A a i = j}
+                             else {[a] | a. A a i = j})"
+"regset_of A i j (Suc k) = regset_of A i j k Un
+                           conc (regset_of A i k k)
+                          (conc (star(regset_of A k k k))
+                                (regset_of A k j k))"
+
+end