Half a lexical analyzer generator.
authornipkow
Sat Nov 18 14:55:44 1995 +0100 (1995-11-18)
changeset 1344f172a7f14e49
parent 1343 8770c062b092
child 1345 d4e26f632bca
Half a lexical analyzer generator.
src/HOL/Lex/Auto.ML
src/HOL/Lex/Auto.thy
src/HOL/Lex/AutoChopper.ML
src/HOL/Lex/AutoChopper.thy
src/HOL/Lex/Chopper.thy
src/HOL/Lex/Prefix.ML
src/HOL/Lex/Prefix.thy
src/HOL/Lex/README.html
src/HOL/Lex/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Lex/Auto.ML	Sat Nov 18 14:55:44 1995 +0100
     1.3 @@ -0,0 +1,39 @@
     1.4 +(*  Title: 	HOL/Lex/Auto.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Richard Mayr & Tobias Nipkow
     1.7 +    Copyright   1995 TUM
     1.8 +*)
     1.9 +
    1.10 +open Auto;
    1.11 +
    1.12 +goalw Auto.thy [nexts_def] "nexts A st [] = st";
    1.13 +by(Simp_tac 1);
    1.14 +qed"nexts_Nil";
    1.15 +
    1.16 +goalw Auto.thy [nexts_def] "nexts A st (x#xs) = nexts A (next A st x) xs";
    1.17 +by(Simp_tac 1);
    1.18 +qed"nexts_Cons";
    1.19 +
    1.20 +Addsimps [nexts_Nil,nexts_Cons];
    1.21 +
    1.22 +goalw Auto.thy [acc_prefix_def] "~acc_prefix A st []";
    1.23 +by(Simp_tac 1);
    1.24 +qed"acc_prefix_Nil";
    1.25 +Addsimps [acc_prefix_Nil];
    1.26 +
    1.27 +goalw Auto.thy [acc_prefix_def]
    1.28 + "acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)";
    1.29 +by(simp_tac (!simpset addsimps [prefix_Cons]) 1);
    1.30 +by(safe_tac HOL_cs);
    1.31 +  by(Asm_full_simp_tac 1);
    1.32 +  by (case_tac "zs=[]" 1);
    1.33 +   by(hyp_subst_tac 1);
    1.34 +   by(Asm_full_simp_tac 1);
    1.35 +  by(fast_tac (HOL_cs addSEs [Cons_neq_Nil]) 1);
    1.36 + by(res_inst_tac [("x","[x]")] exI 1);
    1.37 + by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    1.38 +by(res_inst_tac [("x","x#us")] exI 1);
    1.39 +by(Asm_simp_tac 1);
    1.40 +by (fast_tac HOL_cs 1);
    1.41 +qed"acc_prefix_Cons";
    1.42 +Addsimps [acc_prefix_Cons];
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Lex/Auto.thy	Sat Nov 18 14:55:44 1995 +0100
     2.3 @@ -0,0 +1,38 @@
     2.4 +(*  Title: 	HOL/Lex/Auto.thy
     2.5 +    ID:         $Id$
     2.6 +    Author: 	Tobias Nipkow
     2.7 +    Copyright   1995 TUM
     2.8 +
     2.9 +Automata expressed as triples of
    2.10 +  1. a start state,
    2.11 +  2. a transition function and
    2.12 +  3. a test for final states.
    2.13 +
    2.14 +NOTE: this functional representation is suitable for all kinds of automata,
    2.15 +      not just finite ones!
    2.16 +*)
    2.17 +
    2.18 +Auto = Prefix +
    2.19 +
    2.20 +types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)"
    2.21 +
    2.22 +consts
    2.23 +  start :: "('a, 'b)auto => 'b"
    2.24 +  next  :: "('a, 'b)auto => ('b => 'a => 'b)"
    2.25 +  fin   :: "('a, 'b)auto => ('b => bool)"
    2.26 +  nexts :: "('a, 'b)auto => 'b => 'a list => 'b"
    2.27 +  accepts :: "('a,'b) auto => 'a list => bool"  
    2.28 +  acc_prefix :: "('a, 'b)auto => 'b => 'a list => bool"
    2.29 +
    2.30 +defs
    2.31 +  start_def "start(A) == fst(A)"
    2.32 +  next_def  "next(A) == fst(snd(A))"
    2.33 +  fin_def   "fin(A) == snd(snd(A))"
    2.34 +  nexts_def "nexts(A) == foldl(next(A))"
    2.35 +
    2.36 +  accepts_def "accepts A xs == fin A (nexts A (start A) xs)"
    2.37 +
    2.38 +  acc_prefix_def
    2.39 +    "acc_prefix A st xs == ? us. us <= xs & us~=[] & fin A (nexts A st us)"
    2.40 +
    2.41 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Lex/AutoChopper.ML	Sat Nov 18 14:55:44 1995 +0100
     3.3 @@ -0,0 +1,241 @@
     3.4 +(*  Title: 	HOL/Lex/AutoChopper.ML
     3.5 +    ID:         $Id$
     3.6 +    Author: 	Richard Mayr & Tobias Nipkow
     3.7 +    Copyright   1995 TUM
     3.8 +
     3.9 +Main result: auto_chopper satisfies the is_auto_chopper specification.
    3.10 +*)
    3.11 +
    3.12 +open AutoChopper;
    3.13 +
    3.14 +infix repeat_RS;
    3.15 +fun th1 repeat_RS th2 = ((th1 RS th2) repeat_RS th2) handle _ => th1;
    3.16 +
    3.17 +Addsimps [Let_def];
    3.18 +
    3.19 +goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
    3.20 +by (list.induct_tac "xs" 1);
    3.21 +by (Simp_tac 1);
    3.22 +by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    3.23 +val accept_not_Nil = result() repeat_RS spec;
    3.24 +Addsimps [accept_not_Nil];
    3.25 +
    3.26 +goal AutoChopper.thy
    3.27 +"!st us. acc xs st [] us ([],ys) A = ([], zs) --> \
    3.28 +\        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
    3.29 +by (list.induct_tac "xs" 1);
    3.30 +by (simp_tac (!simpset addcongs [conj_cong]) 1);
    3.31 +by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    3.32 +by (strip_tac 1);
    3.33 +br conjI 1;
    3.34 +by (fast_tac HOL_cs 1);
    3.35 +by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
    3.36 +by (strip_tac 1);
    3.37 +by(REPEAT(eresolve_tac [conjE,exE] 1));
    3.38 +by(hyp_subst_tac 1);
    3.39 +by (Simp_tac 1);
    3.40 +by (case_tac "zsa = []" 1);
    3.41 +by (Asm_simp_tac 1);
    3.42 +by (fast_tac HOL_cs 1);
    3.43 +bind_thm("no_acc", result() RS spec RS spec RS mp);
    3.44 +
    3.45 +
    3.46 +val [prem] = goal HOL.thy "? x.P(f(x)) ==> ? y.P(y)";
    3.47 +by (cut_facts_tac [prem] 1);
    3.48 +by (fast_tac HOL_cs 1);
    3.49 +val ex_special = result();
    3.50 +
    3.51 +
    3.52 +goal AutoChopper.thy
    3.53 +"! r erk l rst st ys yss zs::'a list. \
    3.54 +\    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
    3.55 +\    ys@flat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@flat(l)@rst)";
    3.56 +by (list.induct_tac "xs" 1);
    3.57 + by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
    3.58 +by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    3.59 +by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
    3.60 +by(rename_tac "vss lrst" 1);  
    3.61 +by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    3.62 +by (res_inst_tac[("xs","vss")] list_eq_cases 1);
    3.63 + by(hyp_subst_tac 1);
    3.64 + by(Simp_tac 1);
    3.65 + by (fast_tac (HOL_cs addSDs [no_acc]) 1);
    3.66 +by(hyp_subst_tac 1);
    3.67 +by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    3.68 +val step2_a = (result() repeat_RS spec) RS mp;
    3.69 +
    3.70 +
    3.71 +goal AutoChopper.thy
    3.72 + "! st erk r l rest ys yss zs.\
    3.73 +\   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
    3.74 +\     (if acc_prefix A st xs \
    3.75 +\      then ys ~= [] \
    3.76 +\      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
    3.77 +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    3.78 +by (list.induct_tac "xs" 1);
    3.79 + by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
    3.80 + by (fast_tac HOL_cs 1);
    3.81 +by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
    3.82 +by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
    3.83 +by(rename_tac "vss lrst" 1);  
    3.84 +by(Asm_simp_tac 1);
    3.85 +by (strip_tac 1);
    3.86 +by (case_tac "acc_prefix A (next A st a) list" 1);
    3.87 + by(Asm_simp_tac 1);
    3.88 +by (subgoal_tac "r @ [a] ~= []" 1);
    3.89 + by (fast_tac HOL_cs 1);
    3.90 +by (Simp_tac 1);
    3.91 +val step2_b = (result() repeat_RS spec) RS mp;
    3.92 +
    3.93 +
    3.94 +goal AutoChopper.thy  
    3.95 + "! st erk r l rest ys yss zs. \
    3.96 +\   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
    3.97 +\     (if acc_prefix A st xs                   \
    3.98 +\      then ? g. ys=r@g & fin A (nexts A st g)  \
    3.99 +\      else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
   3.100 +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   3.101 +by (list.induct_tac "xs" 1);
   3.102 + by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   3.103 + by (fast_tac HOL_cs 1);
   3.104 +by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   3.105 +by (strip_tac 1);
   3.106 +br conjI 1;
   3.107 + by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   3.108 + by(rename_tac "vss lrst" 1);  
   3.109 + by(Asm_simp_tac 1);
   3.110 + by (case_tac "acc_prefix A (next A st a) list" 1);
   3.111 +  by (strip_tac 1);
   3.112 +  by (res_inst_tac [("f","%k.a#k")] ex_special 1);
   3.113 +  by (Simp_tac 1);
   3.114 +  by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
   3.115 +   by (Simp_tac 1);
   3.116 +  by (fast_tac HOL_cs 1);
   3.117 + by (strip_tac 1);
   3.118 + by (res_inst_tac [("x","[a]")] exI 1);
   3.119 + by (Asm_simp_tac 1);
   3.120 + by (subgoal_tac "r @ [a] ~= []" 1);
   3.121 +  br sym 1;
   3.122 +  by (fast_tac HOL_cs 1);
   3.123 + by (Simp_tac 1);
   3.124 +by (strip_tac 1);
   3.125 +by (res_inst_tac [("f","%k.a#k")] ex_special 1);
   3.126 +by (Simp_tac 1);
   3.127 +by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
   3.128 + by (Simp_tac 1);
   3.129 +by (fast_tac HOL_cs 1);
   3.130 +val step2_c = (result() repeat_RS spec) RS mp;
   3.131 +
   3.132 +
   3.133 +goal AutoChopper.thy
   3.134 + "! st erk r l rest ys yss zs. \
   3.135 +\   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
   3.136 +\     (if acc_prefix A st xs       \
   3.137 +\      then acc(flat(yss)@zs)(start A) [] [] ([],flat(yss)@zs) A = (yss,zs) \
   3.138 +\      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
   3.139 +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   3.140 +by (list.induct_tac "xs" 1);
   3.141 + by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   3.142 + by (fast_tac HOL_cs 1);
   3.143 +by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   3.144 +by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   3.145 +by(rename_tac "vss lrst" 1);  
   3.146 +by(Asm_simp_tac 1);
   3.147 +by (strip_tac 1);
   3.148 +by (case_tac "acc_prefix A (next A st a) list" 1);
   3.149 + by (Asm_simp_tac 1);
   3.150 +by (subgoal_tac "acc list (start A) [] [] ([],list) A = (yss,zs)" 1);
   3.151 + by (Asm_simp_tac 2);
   3.152 + by (subgoal_tac "r@[a] ~= []" 2);
   3.153 +  by (fast_tac HOL_cs 2);
   3.154 + by (Simp_tac 2);
   3.155 +by (subgoal_tac "flat(yss) @ zs = list" 1);
   3.156 + by (Asm_simp_tac 1);
   3.157 +by (case_tac "yss = []" 1);
   3.158 + by (Asm_simp_tac 1);
   3.159 + by (hyp_subst_tac 1);
   3.160 + by (fast_tac (HOL_cs addSDs [no_acc]) 1);
   3.161 +be ((neq_Nil_conv RS iffD1) RS exE) 1;
   3.162 +be exE 1;
   3.163 +by (hyp_subst_tac 1);
   3.164 +by (Simp_tac 1);
   3.165 +br trans 1;
   3.166 + be step2_a 1;
   3.167 +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   3.168 +val step2_d = (result() repeat_RS spec) RS mp;
   3.169 +
   3.170 +Delsimps [split_paired_All];
   3.171 +goal AutoChopper.thy 
   3.172 +"! st erk r p ys yss zs. \
   3.173 +\  acc xs st erk r p A = (ys#yss, zs) --> \
   3.174 +\  (if acc_prefix A st xs  \
   3.175 +\   then ? g.ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
   3.176 +\   else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
   3.177 +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   3.178 +by (list.induct_tac "xs" 1);
   3.179 + by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   3.180 + by (fast_tac HOL_cs 1);
   3.181 +by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   3.182 +by (strip_tac 1);
   3.183 +by (case_tac "acc_prefix A (next A st a) list" 1);
   3.184 + br conjI 1;
   3.185 +  by (strip_tac 1);
   3.186 +  by (res_inst_tac [("f","%k.a#k")] ex_special 1);
   3.187 +  by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
   3.188 +   by (Simp_tac 1);
   3.189 +  by (res_inst_tac [("P","%k.ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
   3.190 +   by (asm_simp_tac HOL_ss 1);
   3.191 +  by (res_inst_tac [("x","x")] exI 1);
   3.192 +  by (Asm_simp_tac 1);
   3.193 +  br list_cases 1;
   3.194 +   by (Simp_tac 1);
   3.195 +  by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
   3.196 + by (strip_tac 1);
   3.197 + by (res_inst_tac [("f","%k.a#k")] ex_special 1);
   3.198 + by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
   3.199 +  by (Simp_tac 1);
   3.200 + by (res_inst_tac [("P","%k.ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
   3.201 +  by (asm_simp_tac HOL_ss 1);
   3.202 + by (res_inst_tac [("x","x")] exI 1);
   3.203 + by (Asm_simp_tac 1);
   3.204 + br list_cases 1;
   3.205 +  by (Simp_tac 1);
   3.206 + by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
   3.207 +by (Asm_simp_tac 1);
   3.208 +by (strip_tac 1);
   3.209 +by (res_inst_tac [("x","[a]")] exI 1);
   3.210 +br conjI 1;
   3.211 + by (subgoal_tac "r @ [a] ~= []" 1);
   3.212 +  by (fast_tac HOL_cs 1);
   3.213 + by (Simp_tac 1);
   3.214 +br list_cases 1;
   3.215 + by (Simp_tac 1);
   3.216 +by (asm_full_simp_tac (!simpset addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
   3.217 +be thin_rl 1; (* speed up *)
   3.218 +by (fast_tac HOL_cs 1);
   3.219 +val step2_e = (result() repeat_RS spec) RS mp;
   3.220 +Addsimps[split_paired_All];
   3.221 +
   3.222 +goalw AutoChopper.thy [accepts_def, is_auto_chopper_def, auto_chopper_def,
   3.223 +                       Chopper.is_longest_prefix_chopper_def]
   3.224 + "is_auto_chopper(auto_chopper)";
   3.225 +by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
   3.226 + br mp 1;
   3.227 +  be step2_b 2;
   3.228 + by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   3.229 +br conjI 1;
   3.230 + br mp 1;
   3.231 +  be step2_c 2;
   3.232 + by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   3.233 + by (fast_tac HOL_cs 1);
   3.234 +br conjI 1;
   3.235 + by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
   3.236 +br conjI 1;
   3.237 + br mp 1;
   3.238 +  be step2_d 2;
   3.239 + by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   3.240 +br mp 1;
   3.241 + be step2_e 2;
   3.242 + by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   3.243 +by (fast_tac HOL_cs 1);
   3.244 +qed"auto_chopper_is_auto_chopper";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Lex/AutoChopper.thy	Sat Nov 18 14:55:44 1995 +0100
     4.3 @@ -0,0 +1,38 @@
     4.4 +(*  Title: 	HOL/Lex/AutoChopper.thy
     4.5 +    ID:         $Id$
     4.6 +    Author: 	Tobias Nipkow
     4.7 +    Copyright   1995 TUM
     4.8 +
     4.9 +auto_chopper turns an automaton into a chopper. Tricky, because primrec.
    4.10 +
    4.11 +is_auto_chopper requires its argument to produce longest_prefix_choppers
    4.12 +wrt the language accepted by the automaton.
    4.13 +
    4.14 +Main result: auto_chopper satisfies the is_auto_chopper specification.
    4.15 +*)
    4.16 +
    4.17 +AutoChopper = Auto + Chopper +
    4.18 +
    4.19 +consts
    4.20 +  is_auto_chopper :: "(('a,'b)auto => 'a chopper) => bool"
    4.21 +  auto_chopper :: "('a,'b)auto => 'a chopper"
    4.22 +  acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto] \
    4.23 +\	  => 'a list list * 'a list"
    4.24 +
    4.25 +defs
    4.26 +  is_auto_chopper_def "is_auto_chopper(chopperf) ==   \
    4.27 +\		       !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
    4.28 +
    4.29 +  auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
    4.30 +
    4.31 +primrec acc List.list
    4.32 +  acc_Nil  "acc [] st ys zs chopsr A =   \
    4.33 +\	      (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
    4.34 +  acc_Cons "acc(x#xs) st ys zs chopsr A =   \
    4.35 +\	  (let s0 = start(A); nxt = next(A); fin = fin(A)   \
    4.36 +\          in if fin(nxt st x)  \
    4.37 +\             then acc xs (nxt st x) (zs@[x]) (zs@[x]) \ 
    4.38 +\                      (acc xs s0 [] [] ([],xs) A) A \
    4.39 +\             else acc xs (nxt st x) ys (zs@[x]) chopsr A)"
    4.40 +
    4.41 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Lex/Chopper.thy	Sat Nov 18 14:55:44 1995 +0100
     5.3 @@ -0,0 +1,34 @@
     5.4 +(*  Title: 	HOL/Lex/Chopper.thy
     5.5 +    ID:         $Id$
     5.6 +    Author: 	Tobias Nipkow
     5.7 +    Copyright   1995 TUM
     5.8 +
     5.9 +A 'chopper' is a function which returns
    5.10 +  1. a chopped up prefix of the input string
    5.11 +  2. together with the remaining suffix.
    5.12 +
    5.13 +It is a longest_prefix_chopper if it
    5.14 +  1. chops up as much of the input as possible and
    5.15 +  2. chops it up into the longest substrings possible.
    5.16 +
    5.17 +A chopper is parametrized by a language ('a list => bool),
    5.18 +i.e. a set of strings.
    5.19 +*)
    5.20 +
    5.21 +Chopper = Prefix +
    5.22 +
    5.23 +types   'a chopper = "'a list => 'a list list * 'a list"
    5.24 +
    5.25 +consts
    5.26 +  is_longest_prefix_chopper :: "['a list => bool, 'a chopper] => bool"
    5.27 +
    5.28 +defs
    5.29 +  is_longest_prefix_chopper_def
    5.30 +    "is_longest_prefix_chopper L chopper == !xs.   \
    5.31 +\	 (!zs. chopper(xs) = ([],zs) --> \
    5.32 +\	       zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &  \
    5.33 +\ 	 (!ys yss zs. chopper(xs) = (ys#yss,zs) -->                \
    5.34 +\	    ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &   \
    5.35 +\           chopper(flat(yss)@zs) = (yss,zs) &     \
    5.36 +\           (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
    5.37 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Lex/Prefix.ML	Sat Nov 18 14:55:44 1995 +0100
     6.3 @@ -0,0 +1,43 @@
     6.4 +(*  Title: 	HOL/Lex/Prefix.thy
     6.5 +    ID:         $Id$
     6.6 +    Author: 	Richard Mayr & Tobias Nipkow
     6.7 +    Copyright   1995 TUM
     6.8 +*)
     6.9 +
    6.10 +open Prefix;
    6.11 +
    6.12 +val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l.Q(l)";
    6.13 +br allI 1;
    6.14 +by (list.induct_tac "l" 1);
    6.15 +br maj 1;
    6.16 +br min 1;
    6.17 +val list_cases = result();
    6.18 +
    6.19 +goalw Prefix.thy [prefix_def] "[] <= xs";
    6.20 +by (simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    6.21 +qed "Nil_prefix";
    6.22 +Addsimps[Nil_prefix];
    6.23 +
    6.24 +goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
    6.25 +by (list.induct_tac "xs" 1);
    6.26 +by (Simp_tac 1);
    6.27 +by (fast_tac HOL_cs 1);
    6.28 +by (Simp_tac 1);
    6.29 +qed "prefix_Nil";
    6.30 +Addsimps [prefix_Nil];
    6.31 +
    6.32 +(* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
    6.33 +goalw Prefix.thy [prefix_def]
    6.34 +   "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
    6.35 +by (list.induct_tac "xs" 1);
    6.36 +by (Simp_tac 1);
    6.37 +by (fast_tac HOL_cs 1);
    6.38 +by (Simp_tac 1);
    6.39 +by (fast_tac HOL_cs 1);
    6.40 +qed "prefix_Cons";
    6.41 +
    6.42 +goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
    6.43 +by(Simp_tac 1);
    6.44 +by (fast_tac HOL_cs 1);
    6.45 +qed"Cons_prefix_Cons";
    6.46 +Addsimps [Cons_prefix_Cons];
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Lex/Prefix.thy	Sat Nov 18 14:55:44 1995 +0100
     7.3 @@ -0,0 +1,13 @@
     7.4 +(*  Title: 	HOL/Lex/Prefix.thy
     7.5 +    ID:         $Id$
     7.6 +    Author: 	Tobias Nipkow
     7.7 +    Copyright   1995 TUM
     7.8 +*)
     7.9 +
    7.10 +Prefix = List +
    7.11 +
    7.12 +arities list :: (term)ord
    7.13 +
    7.14 +defs
    7.15 +	prefix_def     "xs <= zs  ==  ? ys. zs = xs@ys"
    7.16 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Lex/README.html	Sat Nov 18 14:55:44 1995 +0100
     8.3 @@ -0,0 +1,41 @@
     8.4 +<HTML><HEAD><TITLE>HOL/Lex/ReadMe</TITLE></HEAD>
     8.5 +<BODY>
     8.6 +
     8.7 +<H2>A Simplified Scanner Generator</H2>
     8.8 +
     8.9 +This is half of a simplified functional scanner generator. The overall design
    8.10 +is like this:
    8.11 +<PRE>
    8.12 +         regular expression
    8.13 +                  |
    8.14 +                  v
    8.15 +             -----------
    8.16 +             | mk_auto |
    8.17 +             -----------
    8.18 +                  |
    8.19 +        deterministic automaton
    8.20 +                  |
    8.21 +                  v
    8.22 +           ----------------
    8.23 +string --> | auto_chopper | --> chopped up string
    8.24 +           ----------------
    8.25 +</PRE>
    8.26 +A chopped up string is a pair of
    8.27 +<UL>
    8.28 +<LI>a prefix of the input string, chopped up into words of the language,
    8.29 +<LI>together with the remaining suffix.
    8.30 +</UL>
    8.31 +For example, if the language consists just of the word <KBD>ab</KBD>, the
    8.32 +input <KBD>ababaab</KBD> is partitioned into a chopped up prefix
    8.33 +<KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
    8.34 +<P>
    8.35 +
    8.36 +The auto_chopper is implemented in theory AutoChopper. The top part of the
    8.37 +diagram, i.e. the translation of regular expressions into deterministic
    8.38 +finite automata is still missing.  <P>
    8.39 +
    8.40 +<B>WANTED:</B> a theoretically inclined student to formalize a bit of
    8.41 +undergraduate level automata theory. This could be worth a "Diplom" or an
    8.42 +M.Sc. It could also be undertaken as a two-person "Fopra".
    8.43 +</BODY>
    8.44 +</HTML>
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Lex/ROOT.ML	Sat Nov 18 14:55:44 1995 +0100
     9.3 @@ -0,0 +1,13 @@
     9.4 +(*  Title: 	HOL/Lex/ROOT.ML
     9.5 +    ID:         $Id$
     9.6 +    Author: 	Tobias Nipkow
     9.7 +    Copyright   1995 TUM
     9.8 +*)
     9.9 +
    9.10 +HOL_build_completed;	(*Make examples fail if HOL did*)
    9.11 +
    9.12 +loadpath := ["Lex"];
    9.13 +
    9.14 +use_thy"AutoChopper";
    9.15 +
    9.16 +make_chart ();   (*make HTML chart*)