Half a lexical analyzer generator.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Auto.ML Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,39 @@
+(* Title: HOL/Lex/Auto.ML
+ ID: $Id$
+ Author: Richard Mayr & Tobias Nipkow
+ Copyright 1995 TUM
+*)
+
+open Auto;
+
+goalw Auto.thy [nexts_def] "nexts A st [] = st";
+by(Simp_tac 1);
+qed"nexts_Nil";
+
+goalw Auto.thy [nexts_def] "nexts A st (x#xs) = nexts A (next A st x) xs";
+by(Simp_tac 1);
+qed"nexts_Cons";
+
+Addsimps [nexts_Nil,nexts_Cons];
+
+goalw Auto.thy [acc_prefix_def] "~acc_prefix A st []";
+by(Simp_tac 1);
+qed"acc_prefix_Nil";
+Addsimps [acc_prefix_Nil];
+
+goalw Auto.thy [acc_prefix_def]
+ "acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)";
+by(simp_tac (!simpset addsimps [prefix_Cons]) 1);
+by(safe_tac HOL_cs);
+ by(Asm_full_simp_tac 1);
+ by (case_tac "zs=[]" 1);
+ by(hyp_subst_tac 1);
+ by(Asm_full_simp_tac 1);
+ by(fast_tac (HOL_cs addSEs [Cons_neq_Nil]) 1);
+ by(res_inst_tac [("x","[x]")] exI 1);
+ by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by(res_inst_tac [("x","x#us")] exI 1);
+by(Asm_simp_tac 1);
+by (fast_tac HOL_cs 1);
+qed"acc_prefix_Cons";
+Addsimps [acc_prefix_Cons];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Auto.thy Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,38 @@
+(* Title: HOL/Lex/Auto.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1995 TUM
+
+Automata expressed as triples of
+ 1. a start state,
+ 2. a transition function and
+ 3. a test for final states.
+
+NOTE: this functional representation is suitable for all kinds of automata,
+ not just finite ones!
+*)
+
+Auto = Prefix +
+
+types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)"
+
+consts
+ start :: "('a, 'b)auto => 'b"
+ next :: "('a, 'b)auto => ('b => 'a => 'b)"
+ fin :: "('a, 'b)auto => ('b => bool)"
+ nexts :: "('a, 'b)auto => 'b => 'a list => 'b"
+ accepts :: "('a,'b) auto => 'a list => bool"
+ acc_prefix :: "('a, 'b)auto => 'b => 'a list => bool"
+
+defs
+ start_def "start(A) == fst(A)"
+ next_def "next(A) == fst(snd(A))"
+ fin_def "fin(A) == snd(snd(A))"
+ nexts_def "nexts(A) == foldl(next(A))"
+
+ accepts_def "accepts A xs == fin A (nexts A (start A) xs)"
+
+ acc_prefix_def
+ "acc_prefix A st xs == ? us. us <= xs & us~=[] & fin A (nexts A st us)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/AutoChopper.ML Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,241 @@
+(* Title: HOL/Lex/AutoChopper.ML
+ ID: $Id$
+ Author: Richard Mayr & Tobias Nipkow
+ Copyright 1995 TUM
+
+Main result: auto_chopper satisfies the is_auto_chopper specification.
+*)
+
+open AutoChopper;
+
+infix repeat_RS;
+fun th1 repeat_RS th2 = ((th1 RS th2) repeat_RS th2) handle _ => th1;
+
+Addsimps [Let_def];
+
+goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
+by (list.induct_tac "xs" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+val accept_not_Nil = result() repeat_RS spec;
+Addsimps [accept_not_Nil];
+
+goal AutoChopper.thy
+"!st us. acc xs st [] us ([],ys) A = ([], zs) --> \
+\ zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
+by (list.induct_tac "xs" 1);
+by (simp_tac (!simpset addcongs [conj_cong]) 1);
+by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (strip_tac 1);
+br conjI 1;
+by (fast_tac HOL_cs 1);
+by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
+by (strip_tac 1);
+by(REPEAT(eresolve_tac [conjE,exE] 1));
+by(hyp_subst_tac 1);
+by (Simp_tac 1);
+by (case_tac "zsa = []" 1);
+by (Asm_simp_tac 1);
+by (fast_tac HOL_cs 1);
+bind_thm("no_acc", result() RS spec RS spec RS mp);
+
+
+val [prem] = goal HOL.thy "? x.P(f(x)) ==> ? y.P(y)";
+by (cut_facts_tac [prem] 1);
+by (fast_tac HOL_cs 1);
+val ex_special = result();
+
+
+goal AutoChopper.thy
+"! r erk l rst st ys yss zs::'a list. \
+\ acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
+\ ys@flat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@flat(l)@rst)";
+by (list.induct_tac "xs" 1);
+ by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by(rename_tac "vss lrst" 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (res_inst_tac[("xs","vss")] list_eq_cases 1);
+ by(hyp_subst_tac 1);
+ by(Simp_tac 1);
+ by (fast_tac (HOL_cs addSDs [no_acc]) 1);
+by(hyp_subst_tac 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+val step2_a = (result() repeat_RS spec) RS mp;
+
+
+goal AutoChopper.thy
+ "! st erk r l rest ys yss zs.\
+\ acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
+\ (if acc_prefix A st xs \
+\ then ys ~= [] \
+\ else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (list.induct_tac "xs" 1);
+ by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+ by (fast_tac HOL_cs 1);
+by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by(rename_tac "vss lrst" 1);
+by(Asm_simp_tac 1);
+by (strip_tac 1);
+by (case_tac "acc_prefix A (next A st a) list" 1);
+ by(Asm_simp_tac 1);
+by (subgoal_tac "r @ [a] ~= []" 1);
+ by (fast_tac HOL_cs 1);
+by (Simp_tac 1);
+val step2_b = (result() repeat_RS spec) RS mp;
+
+
+goal AutoChopper.thy
+ "! st erk r l rest ys yss zs. \
+\ acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
+\ (if acc_prefix A st xs \
+\ then ? g. ys=r@g & fin A (nexts A st g) \
+\ else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (list.induct_tac "xs" 1);
+ by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+ by (fast_tac HOL_cs 1);
+by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+by (strip_tac 1);
+br conjI 1;
+ by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+ by(rename_tac "vss lrst" 1);
+ by(Asm_simp_tac 1);
+ by (case_tac "acc_prefix A (next A st a) list" 1);
+ by (strip_tac 1);
+ by (res_inst_tac [("f","%k.a#k")] ex_special 1);
+ by (Simp_tac 1);
+ by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+ by (Simp_tac 1);
+ by (fast_tac HOL_cs 1);
+ by (strip_tac 1);
+ by (res_inst_tac [("x","[a]")] exI 1);
+ by (Asm_simp_tac 1);
+ by (subgoal_tac "r @ [a] ~= []" 1);
+ br sym 1;
+ by (fast_tac HOL_cs 1);
+ by (Simp_tac 1);
+by (strip_tac 1);
+by (res_inst_tac [("f","%k.a#k")] ex_special 1);
+by (Simp_tac 1);
+by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+ by (Simp_tac 1);
+by (fast_tac HOL_cs 1);
+val step2_c = (result() repeat_RS spec) RS mp;
+
+
+goal AutoChopper.thy
+ "! st erk r l rest ys yss zs. \
+\ acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
+\ (if acc_prefix A st xs \
+\ then acc(flat(yss)@zs)(start A) [] [] ([],flat(yss)@zs) A = (yss,zs) \
+\ else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (list.induct_tac "xs" 1);
+ by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+ by (fast_tac HOL_cs 1);
+by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by(rename_tac "vss lrst" 1);
+by(Asm_simp_tac 1);
+by (strip_tac 1);
+by (case_tac "acc_prefix A (next A st a) list" 1);
+ by (Asm_simp_tac 1);
+by (subgoal_tac "acc list (start A) [] [] ([],list) A = (yss,zs)" 1);
+ by (Asm_simp_tac 2);
+ by (subgoal_tac "r@[a] ~= []" 2);
+ by (fast_tac HOL_cs 2);
+ by (Simp_tac 2);
+by (subgoal_tac "flat(yss) @ zs = list" 1);
+ by (Asm_simp_tac 1);
+by (case_tac "yss = []" 1);
+ by (Asm_simp_tac 1);
+ by (hyp_subst_tac 1);
+ by (fast_tac (HOL_cs addSDs [no_acc]) 1);
+be ((neq_Nil_conv RS iffD1) RS exE) 1;
+be exE 1;
+by (hyp_subst_tac 1);
+by (Simp_tac 1);
+br trans 1;
+ be step2_a 1;
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+val step2_d = (result() repeat_RS spec) RS mp;
+
+Delsimps [split_paired_All];
+goal AutoChopper.thy
+"! st erk r p ys yss zs. \
+\ acc xs st erk r p A = (ys#yss, zs) --> \
+\ (if acc_prefix A st xs \
+\ then ? g.ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
+\ else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (list.induct_tac "xs" 1);
+ by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+ by (fast_tac HOL_cs 1);
+by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+by (strip_tac 1);
+by (case_tac "acc_prefix A (next A st a) list" 1);
+ br conjI 1;
+ by (strip_tac 1);
+ by (res_inst_tac [("f","%k.a#k")] ex_special 1);
+ by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+ by (Simp_tac 1);
+ 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);
+ by (asm_simp_tac HOL_ss 1);
+ by (res_inst_tac [("x","x")] exI 1);
+ by (Asm_simp_tac 1);
+ br list_cases 1;
+ by (Simp_tac 1);
+ by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
+ by (strip_tac 1);
+ by (res_inst_tac [("f","%k.a#k")] ex_special 1);
+ by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+ by (Simp_tac 1);
+ 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);
+ by (asm_simp_tac HOL_ss 1);
+ by (res_inst_tac [("x","x")] exI 1);
+ by (Asm_simp_tac 1);
+ br list_cases 1;
+ by (Simp_tac 1);
+ by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
+by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (res_inst_tac [("x","[a]")] exI 1);
+br conjI 1;
+ by (subgoal_tac "r @ [a] ~= []" 1);
+ by (fast_tac HOL_cs 1);
+ by (Simp_tac 1);
+br list_cases 1;
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
+be thin_rl 1; (* speed up *)
+by (fast_tac HOL_cs 1);
+val step2_e = (result() repeat_RS spec) RS mp;
+Addsimps[split_paired_All];
+
+goalw AutoChopper.thy [accepts_def, is_auto_chopper_def, auto_chopper_def,
+ Chopper.is_longest_prefix_chopper_def]
+ "is_auto_chopper(auto_chopper)";
+by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
+ br mp 1;
+ be step2_b 2;
+ by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+br conjI 1;
+ br mp 1;
+ be step2_c 2;
+ by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by (fast_tac HOL_cs 1);
+br conjI 1;
+ by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
+br conjI 1;
+ br mp 1;
+ be step2_d 2;
+ by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+br mp 1;
+ be step2_e 2;
+ by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (fast_tac HOL_cs 1);
+qed"auto_chopper_is_auto_chopper";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/AutoChopper.thy Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,38 @@
+(* Title: HOL/Lex/AutoChopper.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1995 TUM
+
+auto_chopper turns an automaton into a chopper. Tricky, because primrec.
+
+is_auto_chopper requires its argument to produce longest_prefix_choppers
+wrt the language accepted by the automaton.
+
+Main result: auto_chopper satisfies the is_auto_chopper specification.
+*)
+
+AutoChopper = Auto + Chopper +
+
+consts
+ is_auto_chopper :: "(('a,'b)auto => 'a chopper) => bool"
+ auto_chopper :: "('a,'b)auto => 'a chopper"
+ acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto] \
+\ => 'a list list * 'a list"
+
+defs
+ is_auto_chopper_def "is_auto_chopper(chopperf) == \
+\ !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
+
+ auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
+
+primrec acc List.list
+ acc_Nil "acc [] st ys zs chopsr A = \
+\ (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))"
+ acc_Cons "acc(x#xs) st ys zs chopsr A = \
+\ (let s0 = start(A); nxt = next(A); fin = fin(A) \
+\ in if fin(nxt st x) \
+\ then acc xs (nxt st x) (zs@[x]) (zs@[x]) \
+\ (acc xs s0 [] [] ([],xs) A) A \
+\ else acc xs (nxt st x) ys (zs@[x]) chopsr A)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Chopper.thy Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,34 @@
+(* Title: HOL/Lex/Chopper.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1995 TUM
+
+A 'chopper' is a function which returns
+ 1. a chopped up prefix of the input string
+ 2. together with the remaining suffix.
+
+It is a longest_prefix_chopper if it
+ 1. chops up as much of the input as possible and
+ 2. chops it up into the longest substrings possible.
+
+A chopper is parametrized by a language ('a list => bool),
+i.e. a set of strings.
+*)
+
+Chopper = Prefix +
+
+types 'a chopper = "'a list => 'a list list * 'a list"
+
+consts
+ is_longest_prefix_chopper :: "['a list => bool, 'a chopper] => bool"
+
+defs
+ is_longest_prefix_chopper_def
+ "is_longest_prefix_chopper L chopper == !xs. \
+\ (!zs. chopper(xs) = ([],zs) --> \
+\ zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) & \
+\ (!ys yss zs. chopper(xs) = (ys#yss,zs) --> \
+\ ys ~= [] & L(ys) & xs=ys@flat(yss)@zs & \
+\ chopper(flat(yss)@zs) = (yss,zs) & \
+\ (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Prefix.ML Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,43 @@
+(* Title: HOL/Lex/Prefix.thy
+ ID: $Id$
+ Author: Richard Mayr & Tobias Nipkow
+ Copyright 1995 TUM
+*)
+
+open Prefix;
+
+val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l.Q(l)";
+br allI 1;
+by (list.induct_tac "l" 1);
+br maj 1;
+br min 1;
+val list_cases = result();
+
+goalw Prefix.thy [prefix_def] "[] <= xs";
+by (simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+qed "Nil_prefix";
+Addsimps[Nil_prefix];
+
+goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
+by (list.induct_tac "xs" 1);
+by (Simp_tac 1);
+by (fast_tac HOL_cs 1);
+by (Simp_tac 1);
+qed "prefix_Nil";
+Addsimps [prefix_Nil];
+
+(* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
+goalw Prefix.thy [prefix_def]
+ "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
+by (list.induct_tac "xs" 1);
+by (Simp_tac 1);
+by (fast_tac HOL_cs 1);
+by (Simp_tac 1);
+by (fast_tac HOL_cs 1);
+qed "prefix_Cons";
+
+goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
+by(Simp_tac 1);
+by (fast_tac HOL_cs 1);
+qed"Cons_prefix_Cons";
+Addsimps [Cons_prefix_Cons];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Prefix.thy Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,13 @@
+(* Title: HOL/Lex/Prefix.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1995 TUM
+*)
+
+Prefix = List +
+
+arities list :: (term)ord
+
+defs
+ prefix_def "xs <= zs == ? ys. zs = xs@ys"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/README.html Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,41 @@
+<HTML><HEAD><TITLE>HOL/Lex/ReadMe</TITLE></HEAD>
+<BODY>
+
+<H2>A Simplified Scanner Generator</H2>
+
+This is half of a simplified functional scanner generator. The overall design
+is like this:
+<PRE>
+ regular expression
+ |
+ v
+ -----------
+ | mk_auto |
+ -----------
+ |
+ deterministic automaton
+ |
+ v
+ ----------------
+string --> | auto_chopper | --> chopped up string
+ ----------------
+</PRE>
+A chopped up string is a pair of
+<UL>
+<LI>a prefix of the input string, chopped up into words of the language,
+<LI>together with the remaining suffix.
+</UL>
+For example, if the language consists just of the word <KBD>ab</KBD>, the
+input <KBD>ababaab</KBD> is partitioned into a chopped up prefix
+<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>
+
+<B>WANTED:</B> a theoretically inclined student to formalize a bit of
+undergraduate level automata theory. This could be worth a "Diplom" or an
+M.Sc. It could also be undertaken as a two-person "Fopra".
+</BODY>
+</HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/ROOT.ML Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,13 @@
+(* Title: HOL/Lex/ROOT.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1995 TUM
+*)
+
+HOL_build_completed; (*Make examples fail if HOL did*)
+
+loadpath := ["Lex"];
+
+use_thy"AutoChopper";
+
+make_chart (); (*make HTML chart*)