Added an alternativ version of AutoChopper and a theory for the conversion of
authornipkow
Wed Nov 05 09:08:35 1997 +0100 (1997-11-05)
changeset 41372ce2e659c2b1
parent 4136 ba267836dd7a
child 4138 af6743b065fb
Added an alternativ version of AutoChopper and a theory for the conversion of
automata into regular sets.
src/HOL/Lex/AutoChopper.thy
src/HOL/Lex/AutoChopper1.thy
src/HOL/Lex/README.html
src/HOL/Lex/ROOT.ML
src/HOL/Lex/Regset_of_auto.ML
src/HOL/Lex/Regset_of_auto.thy
     1.1 --- a/src/HOL/Lex/AutoChopper.thy	Tue Nov 04 20:52:20 1997 +0100
     1.2 +++ b/src/HOL/Lex/AutoChopper.thy	Wed Nov 05 09:08:35 1997 +0100
     1.3 @@ -12,6 +12,8 @@
     1.4  
     1.5  WARNING: auto_chopper is exponential(?)
     1.6  if the recursive calls in the penultimate argument are evaluated eagerly.
     1.7 +
     1.8 +A more efficient version is defined in AutoChopper1.
     1.9  *)
    1.10  
    1.11  AutoChopper = Auto + Chopper +
    1.12 @@ -39,32 +41,3 @@
    1.13                  else acc xs (nxt st x) ys (zs@[x]) chopsr A)"
    1.14  
    1.15  end
    1.16 -
    1.17 -(* The following definition of acc should also work:
    1.18 -consts
    1.19 -  acc1 :: [('a,'b)auto, 'a list, 'b, 'a list list, 'a list, 'a list]
    1.20 -          => 'a list list * 'a list
    1.21 -
    1.22 -acc1 A [] s xss zs xs =
    1.23 -  (if xs=[] then (xss, zs)
    1.24 -   else acc1 A zs (start A) (xss @ [xs]) [] [])
    1.25 -acc1 A (y#ys) s xss zs rec =
    1.26 -  let s' = next A s;
    1.27 -      zs' = (if fin A s' then [] else zs@[y])
    1.28 -      xs' = (if fin A s' then xs@zs@[y] else xs)
    1.29 -  in acc1 A ys s' xss zs' xs'
    1.30 -
    1.31 -Advantage: does not need lazy evaluation for reasonable (quadratic)
    1.32 -performance.
    1.33 -
    1.34 -Disadavantage: not primrec.
    1.35 -  
    1.36 -Termination measure:
    1.37 -  size(A,ys,s,xss,zs,rec) = (|xs| + |ys| + |zs|, |ys|)
    1.38 -
    1.39 -Termination proof: the first clause reduces the first component by |xs|,
    1.40 -the second clause leaves the first component alone but reduces the second by 1.
    1.41 -
    1.42 -Claim: acc1 A xs s [] [] [] = acc xs s [] [] ([],xs) A
    1.43 -Generalization?
    1.44 -*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Lex/AutoChopper1.thy	Wed Nov 05 09:08:35 1997 +0100
     2.3 @@ -0,0 +1,37 @@
     2.4 +(*  Title:      HOL/Lex/AutoChopper1.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +    Copyright   1997 TUM
     2.8 +
     2.9 +This is a version of theory AutoChopper base on a non-primrec definition of
    2.10 +`acc'. Advantage: does not need lazy evaluation for reasonable (quadratic?)
    2.11 +performance.
    2.12 +
    2.13 +Verification:
    2.14 +1. Via AutoChopper.acc using
    2.15 +   Claim: acc A xs s [] [] [] = AutoChopper.acc xs s [] [] ([],xs) A
    2.16 +   Generalization?
    2.17 +2. Directly.
    2.18 +   Hope: acc is easier to verify than AutoChopper.acc because simpler.
    2.19 +
    2.20 +No proofs yet.
    2.21 +*)
    2.22 +
    2.23 +AutoChopper1 = Auto + Chopper + WF_Rel +
    2.24 +
    2.25 +consts
    2.26 +  acc :: "(('a,'b)auto * 'a list * 'b * 'a list list * 'a list * 'a list)
    2.27 +          => 'a list list * 'a list"
    2.28 +recdef acc "inv_image (less_than ** less_than)
    2.29 +              (%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs,
    2.30 +                                     length ys))"
    2.31 +simpset "simpset() addsimps (less_add_Suc2::add_ac) addsplits [expand_if]"
    2.32 +"acc(A,[],s,xss,zs,[]) = (xss, zs)"
    2.33 +"acc(A,[],s,xss,zs,x#xs) = acc(A,zs,start A, xss @ [x#xs],[],[])"
    2.34 +"acc(A,y#ys,s,xss,zs,xs) =
    2.35 +  (let s' = next A s y;
    2.36 +      zs' = (if fin A s' then [] else zs@[y]);
    2.37 +      xs' = (if fin A s' then xs@zs@[y] else xs)
    2.38 +   in acc(A,ys,s',xss,zs',xs'))"
    2.39 +
    2.40 +end
     3.1 --- a/src/HOL/Lex/README.html	Tue Nov 04 20:52:20 1997 +0100
     3.2 +++ b/src/HOL/Lex/README.html	Wed Nov 05 09:08:35 1997 +0100
     3.3 @@ -30,9 +30,16 @@
     3.4  <KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
     3.5  <P>
     3.6  
     3.7 -The auto_chopper is implemented in theory AutoChopper. The top part of the
     3.8 -diagram, i.e. the translation of regular expressions into deterministic
     3.9 -finite automata is still missing.  <P>
    3.10 +The auto_chopper is implemented in theory AutoChopper. An alternative (more
    3.11 +efficient) version is defined in AutoChopper1. However, no properties have
    3.12 +been proved for it yet.
    3.13  
    3.14 +The top part of the diagram, i.e. the translation of regular expressions into
    3.15 +deterministic finite automata is still missing (although we have some bits
    3.16 +and pieces).
    3.17 +<P>
    3.18 +
    3.19 +The directory also contains Regset_of_auto, a theory describing the
    3.20 +translation of deterministic automata into regular sets.
    3.21  </BODY>
    3.22  </HTML>
     4.1 --- a/src/HOL/Lex/ROOT.ML	Tue Nov 04 20:52:20 1997 +0100
     4.2 +++ b/src/HOL/Lex/ROOT.ML	Wed Nov 05 09:08:35 1997 +0100
     4.3 @@ -7,3 +7,5 @@
     4.4  HOL_build_completed;    (*Make examples fail if HOL did*)
     4.5  
     4.6  use_thy"AutoChopper";
     4.7 +use_thy"AutoChopper1";
     4.8 +use_thy"Regset_of_auto";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Lex/Regset_of_auto.ML	Wed Nov 05 09:08:35 1997 +0100
     5.3 @@ -0,0 +1,221 @@
     5.4 +Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2];
     5.5 +AddIs    [in_set_butlast_appendI1,in_set_butlast_appendI2];
     5.6 +Addsimps [image_eqI];
     5.7 +
     5.8 +AddIffs [star.NilI];
     5.9 +Addsimps [star.ConsI];
    5.10 +AddIs [star.ConsI];
    5.11 +
    5.12 +(* Lists *)
    5.13 +
    5.14 +(*
    5.15 +(* could go into List. Needs WF_Rel as ancestor. *)
    5.16 +(* Induction over the length of a list: *)
    5.17 +val prems = goal thy
    5.18 + "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
    5.19 +by(res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
    5.20 +     wf_induct 1);
    5.21 +by(Simp_tac 1);
    5.22 +by(asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
    5.23 +bes prems 1;
    5.24 +qed "list_length_induct";
    5.25 +*)
    5.26 +
    5.27 +goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
    5.28 +by(exhaust_tac "xs" 1);
    5.29 +by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    5.30 +qed "butlast_empty";
    5.31 +AddIffs [butlast_empty];
    5.32 +
    5.33 +goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))";
    5.34 +by(induct_tac "xss" 1);
    5.35 + by(Simp_tac 1);
    5.36 +by(asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
    5.37 +                           addsplits [expand_if]) 1);
    5.38 +br conjI 1;
    5.39 + by(Clarify_tac 1);
    5.40 + br conjI 1;
    5.41 +  by(Blast_tac 1);
    5.42 + by(Clarify_tac 1);
    5.43 + by(subgoal_tac "xs=[]" 1);
    5.44 +  by(rotate_tac ~1 1);
    5.45 +  by(Asm_full_simp_tac 1);
    5.46 + by(Blast_tac 1);
    5.47 +by(blast_tac (claset() addDs [in_set_butlastD]) 1);
    5.48 +qed_spec_mp "in_set_butlast_concatI";
    5.49 +
    5.50 +(* Regular sets *)
    5.51 +
    5.52 +goal thy "(!xs: set xss. xs:A) --> concat xss : star A";
    5.53 +by(induct_tac "xss" 1);
    5.54 +by(ALLGOALS Asm_full_simp_tac);
    5.55 +qed_spec_mp "concat_in_star";
    5.56 +
    5.57 +(* The main lemma:
    5.58 +   how to decompose a trace into a prefix, a list of loops and a suffix.
    5.59 +*)
    5.60 +goal thy "!i. k : set(trace A i xs) --> (? pref mids suf. \
    5.61 +\ xs = pref @ concat mids @ suf & \
    5.62 +\ deltas A pref i = k & (!n:set(butlast(trace A i pref)). n ~= k) & \
    5.63 +\ (!mid:set mids. (deltas A mid k = k) & \
    5.64 +\                 (!n:set(butlast(trace A k mid)). n ~= k)) & \
    5.65 +\ (!n:set(butlast(trace A k suf)). n ~= k))";
    5.66 +by(induct_tac "xs" 1);
    5.67 + by(Simp_tac 1);
    5.68 +by(rename_tac "a as" 1);
    5.69 +br allI 1;
    5.70 +by(case_tac "A a i = k" 1);
    5.71 + by(strip_tac 1);
    5.72 + by(res_inst_tac[("x","[a]")]exI 1);
    5.73 + by(Asm_full_simp_tac 1);
    5.74 + by(case_tac "k : set(trace A (A a i) as)" 1);
    5.75 +  be allE 1;
    5.76 +  be impE 1;
    5.77 +   ba 1;
    5.78 +  by(REPEAT(etac exE 1));
    5.79 +  by(res_inst_tac[("x","pref#mids")]exI 1);
    5.80 +  by(res_inst_tac[("x","suf")]exI 1);
    5.81 +  by(Asm_full_simp_tac 1);
    5.82 + by(res_inst_tac[("x","[]")]exI 1);
    5.83 + by(res_inst_tac[("x","as")]exI 1);
    5.84 + by(Asm_full_simp_tac 1);
    5.85 + by(blast_tac (claset() addDs [in_set_butlastD]) 1);
    5.86 +by(Asm_simp_tac 1);
    5.87 +br conjI 1;
    5.88 + by(Blast_tac 1);
    5.89 +by(strip_tac 1);
    5.90 +be allE 1;
    5.91 +be impE 1;
    5.92 + ba 1;
    5.93 +by(REPEAT(etac exE 1));
    5.94 +by(res_inst_tac[("x","a#pref")]exI 1);
    5.95 +by(res_inst_tac[("x","mids")]exI 1);
    5.96 +by(res_inst_tac[("x","suf")]exI 1);
    5.97 +by(asm_simp_tac (simpset() addsplits [expand_if]) 1);
    5.98 +qed_spec_mp "decompose";
    5.99 +
   5.100 +goal thy "!i. length(trace A i xs) = length xs";
   5.101 +by(induct_tac "xs" 1);
   5.102 +by(ALLGOALS Asm_simp_tac);
   5.103 +qed "length_trace";
   5.104 +Addsimps [length_trace];
   5.105 +
   5.106 +goal thy "!i. deltas A (xs@ys) i = deltas A ys (deltas A xs i)";
   5.107 +by(induct_tac "xs" 1);
   5.108 +by(ALLGOALS Asm_simp_tac);
   5.109 +qed "deltas_append";
   5.110 +Addsimps [deltas_append];
   5.111 +
   5.112 +goal thy "!i. trace A i (xs@ys) = trace A i xs @ trace A (deltas A xs i) ys";
   5.113 +by(induct_tac "xs" 1);
   5.114 +by(ALLGOALS Asm_simp_tac);
   5.115 +qed "trace_append";
   5.116 +Addsimps [trace_append];
   5.117 +
   5.118 +goal thy "(!xs: set xss. deltas A xs i = i) --> \
   5.119 +\         trace A i (concat xss) = concat (map (trace A i) xss)";
   5.120 +by(induct_tac "xss" 1);
   5.121 +by(ALLGOALS Asm_simp_tac);
   5.122 +qed_spec_mp "trace_concat";
   5.123 +Addsimps [trace_concat];
   5.124 +
   5.125 +goal thy "!i. (trace A i xs = []) = (xs = [])";
   5.126 +by(exhaust_tac "xs" 1);
   5.127 +by(ALLGOALS Asm_simp_tac);
   5.128 +qed "trace_is_Nil";
   5.129 +Addsimps [trace_is_Nil];
   5.130 +
   5.131 +goal thy "(trace A i xs = n#ns) = \
   5.132 +\         (case xs of [] => False | y#ys => n = A y i & ns = trace A n ys)";
   5.133 +by(exhaust_tac "xs" 1);
   5.134 +by(ALLGOALS Asm_simp_tac);
   5.135 +by(Blast_tac 1);
   5.136 +qed_spec_mp "trace_is_Cons_conv";
   5.137 +Addsimps [trace_is_Cons_conv];
   5.138 +
   5.139 +goal thy "!i. set(trace A i xs) = \
   5.140 +\ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))";
   5.141 +by(induct_tac "xs" 1);
   5.142 + by(Simp_tac 1);
   5.143 +by(asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
   5.144 +qed "set_trace_conv";
   5.145 +
   5.146 +goal thy
   5.147 + "(!mid:set mids. deltas A mid k = k) --> deltas A (concat mids) k = k";
   5.148 +by(induct_tac "mids" 1);
   5.149 +by(ALLGOALS Asm_simp_tac);
   5.150 +qed_spec_mp "deltas_concat";
   5.151 +Addsimps [deltas_concat];
   5.152 +
   5.153 +goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
   5.154 +be nat_neqE 1;
   5.155 +by(ALLGOALS trans_tac);
   5.156 +val lemma = result();
   5.157 +
   5.158 +
   5.159 +goal thy
   5.160 + "!i j xs. xs : regset_of A i j k = \
   5.161 +\          ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)";
   5.162 +by(induct_tac "k" 1);
   5.163 + by(simp_tac (simpset() addcongs [conj_cong]
   5.164 +                        addsplits [expand_if,split_list_case]) 1);
   5.165 +by(strip_tac 1);
   5.166 +by(asm_simp_tac (simpset() addsimps [conc_def]) 1);
   5.167 +br iffI 1;
   5.168 + be disjE 1;
   5.169 +  by(Asm_simp_tac 1);
   5.170 + by(REPEAT(eresolve_tac[exE,conjE] 1));
   5.171 + by(Asm_full_simp_tac 1);
   5.172 + by(subgoal_tac
   5.173 +      "(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1);
   5.174 +  by(asm_simp_tac (simpset() addsplits [expand_if]
   5.175 +       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
   5.176 + be star.induct 1;
   5.177 +  by(Simp_tac 1);
   5.178 + by(asm_full_simp_tac (simpset() addsplits [expand_if]
   5.179 +       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
   5.180 +by(case_tac "k : set(butlast(trace A i xs))" 1);
   5.181 + br disjI1 2;
   5.182 + by(blast_tac (claset() addIs [lemma]) 2);
   5.183 +br disjI2 1;
   5.184 +bd (in_set_butlastD RS decompose) 1;
   5.185 +by(Clarify_tac 1);
   5.186 +by(res_inst_tac [("x","pref")] exI 1);
   5.187 +by(Asm_full_simp_tac 1);
   5.188 +br conjI 1;
   5.189 + br ballI 1;
   5.190 + br lemma 1;
   5.191 +  by(Asm_simp_tac 2);
   5.192 + by(EVERY[dtac bspec 1, atac 2]);
   5.193 + by(Asm_simp_tac 1);
   5.194 +by(res_inst_tac [("x","concat mids")] exI 1);
   5.195 +by(Simp_tac 1);
   5.196 +br conjI 1;
   5.197 + br concat_in_star 1;
   5.198 + by(Asm_simp_tac 1);
   5.199 + br ballI 1;
   5.200 + br ballI 1;
   5.201 + br lemma 1;
   5.202 +  by(Asm_simp_tac 2);
   5.203 + by(EVERY[dtac bspec 1, atac 2]);
   5.204 + by(asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
   5.205 +br ballI 1;
   5.206 +br lemma 1;
   5.207 + by(Asm_simp_tac 2);
   5.208 +by(EVERY[dtac bspec 1, atac 2]);
   5.209 +by(Asm_simp_tac 1);
   5.210 +qed_spec_mp "regset_of_spec";
   5.211 +
   5.212 +goal thy "!!A. !n. n < k --> (!x. A x n < k) ==> \
   5.213 +\         !i. i < k --> (!n:set(trace A i xs). n < k)";
   5.214 +by(induct_tac "xs" 1);
   5.215 + by(ALLGOALS Simp_tac);
   5.216 +by(Blast_tac 1);
   5.217 +qed_spec_mp "trace_below";
   5.218 +
   5.219 +goal thy "!!A. [| !n. n < k --> (!x. A x n < k); i < k; j < k |] ==> \
   5.220 +\         regset_of A i j k = {xs. deltas A xs i = j}";
   5.221 +br set_ext 1;
   5.222 +by(simp_tac (simpset() addsimps [regset_of_spec]) 1);
   5.223 +by(blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
   5.224 +qed "regset_of_below";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Lex/Regset_of_auto.thy	Wed Nov 05 09:08:35 1997 +0100
     6.3 @@ -0,0 +1,44 @@
     6.4 +(*
     6.5 +Conversion of automata into regular sets.
     6.6 +use_thy"Auto";
     6.7 +*)
     6.8 +
     6.9 +Regset_of_auto = List +
    6.10 +
    6.11 +(* autos *)
    6.12 +
    6.13 +types 'a auto = "'a => nat => nat"
    6.14 +
    6.15 +consts deltas :: 'a auto => 'a list => nat => nat
    6.16 +primrec deltas list
    6.17 +"deltas A [] i = i"
    6.18 +"deltas A (x#xs) i = deltas A xs (A x i)"
    6.19 +
    6.20 +consts trace :: 'a auto => nat => 'a list => nat list
    6.21 +primrec trace list
    6.22 +"trace A i [] = []"
    6.23 +"trace A i (x#xs) = A x i # trace A (A x i) xs"
    6.24 +
    6.25 +(* regular sets *)
    6.26 +
    6.27 +constdefs conc :: 'a list set => 'a list set => 'a list set
    6.28 +         "conc A B == {xs@ys | xs ys. xs:A & ys:B}"
    6.29 +
    6.30 +consts star :: 'a list set => 'a list set
    6.31 +inductive "star A"
    6.32 +intrs
    6.33 +  NilI   "[] : star A"
    6.34 +  ConsI  "[| a:A; as : star A |] ==> a@as : star A"
    6.35 +
    6.36 +(* conversion a la Warshall *)
    6.37 +
    6.38 +consts regset_of :: 'a auto => nat => nat => nat => 'a list set
    6.39 +primrec regset_of nat
    6.40 +"regset_of A i j 0 = (if i=j then insert [] {[a] | a. A a i = j}
    6.41 +                             else {[a] | a. A a i = j})"
    6.42 +"regset_of A i j (Suc k) = regset_of A i j k Un
    6.43 +                           conc (regset_of A i k k)
    6.44 +                          (conc (star(regset_of A k k k))
    6.45 +                                (regset_of A k j k))"
    6.46 +
    6.47 +end