zhang [Sat, 05 Feb 2011 13:56:50 +0000] rev 68
Check in Myhill.thy before trying another way to explain DFA
urbanc [Sat, 05 Feb 2011 09:54:52 +0000] rev 67
more intro
urbanc [Fri, 04 Feb 2011 22:54:29 +0000] rev 66
more on the introduction
urbanc [Fri, 04 Feb 2011 13:33:18 +0000] rev 65
exercise about arden from TU Munich
zhang [Fri, 04 Feb 2011 13:02:00 +0000] rev 64
Added something to Myhill.thy, trying to explain the relationship between finite automata and language partition.
zhang [Thu, 03 Feb 2011 12:44:46 +0000] rev 63
Myhill_2.thy added
zhang [Thu, 03 Feb 2011 12:00:06 +0000] rev 62
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
urbanc [Thu, 03 Feb 2011 09:54:19 +0000] rev 61
more to the intro
urbanc [Thu, 03 Feb 2011 05:38:47 +0000] rev 60
a bit more tuning on the introduction
urbanc [Wed, 02 Feb 2011 15:43:22 +0000] rev 59
more on the intro
urbanc [Wed, 02 Feb 2011 13:54:07 +0000] rev 58
a little bit in the introduction
zhang [Wed, 02 Feb 2011 13:25:09 +0000] rev 57
Myhill.pdf modified
urbanc [Wed, 02 Feb 2011 06:05:12 +0000] rev 56
removed the inductive definition of Star and replaced it by a definition in terms of pow
zhang [Mon, 31 Jan 2011 14:51:47 +0000] rev 55
Myhill.thy IsabelleMakefile modified
urbanc [Mon, 31 Jan 2011 12:54:31 +0000] rev 54
a bit more on the paper
urbanc [Sun, 30 Jan 2011 17:24:37 +0000] rev 53
small typo
urbanc [Sun, 30 Jan 2011 17:21:53 +0000] rev 52
tuning of the syntax; needs the stmaryrd latex package
urbanc [Sun, 30 Jan 2011 17:09:02 +0000] rev 51
some tuning of the paper
urbanc [Sun, 30 Jan 2011 16:59:57 +0000] rev 50
revised proof of Ardens lemma
zhang [Sun, 30 Jan 2011 12:22:07 +0000] rev 49
Illustration added together with renewed explainations for case STAR.
zhang [Sat, 29 Jan 2011 11:41:17 +0000] rev 48
Myhill.thy and Myhill_1.thy changed.
urbanc [Fri, 28 Jan 2011 19:17:40 +0000] rev 47
slightly tuned the main lemma and the finiteness proofs
wu [Fri, 28 Jan 2011 12:53:01 +0000] rev 46
test
zhang [Fri, 28 Jan 2011 11:52:11 +0000] rev 45
More improvement
wu [Thu, 27 Jan 2011 17:37:20 +0000] rev 44
added a recent paper about reg exps and automata
urbanc [Thu, 27 Jan 2011 16:58:11 +0000] rev 43
added my changes again
zhang [Thu, 27 Jan 2011 12:35:06 +0000] rev 42
Trying to solve the confict
zhang [Thu, 27 Jan 2011 11:50:58 +0000] rev 41
a newer version
wu [Thu, 27 Jan 2011 05:39:19 +0000] rev 40
tuned a bit more the last STAR-proof
urbanc [Thu, 27 Jan 2011 00:51:46 +0000] rev 39
tuned a little bit the section about finite partitions
zhang [Wed, 26 Jan 2011 23:39:42 +0000] rev 38
Delete generated
wu [Wed, 26 Jan 2011 22:58:24 +0000] rev 37
ITP-Paper loads Myhill.thy
wu [Wed, 26 Jan 2011 22:51:51 +0000] rev 36
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
urbanc [Wed, 26 Jan 2011 22:23:56 +0000] rev 35
made the theory work under both Isabelle 2009 and 2011
zhang [Wed, 26 Jan 2011 14:13:18 +0000] rev 34
Just checkin
zhang [Wed, 26 Jan 2011 14:12:36 +0000] rev 33
Small modification
zhang [Wed, 26 Jan 2011 13:21:16 +0000] rev 32
ok
zhang [Tue, 25 Jan 2011 12:14:31 +0000] rev 31
1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML
zhang [Mon, 24 Jan 2011 11:29:55 +0000] rev 30
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
wu [Fri, 07 Jan 2011 14:25:23 +0000] rev 29
Beautifying of the Other Direction is finished.
wu [Fri, 31 Dec 2010 13:47:53 +0000] rev 28
Rewritten of hard direction once more. To make it looking better.
wu [Tue, 14 Dec 2010 14:31:31 +0000] rev 27
Add new file for the new definition of the hard direction's simplification.
Merging Operation is deleted
All definitions are done. Proof still undone.
urbanc [Fri, 26 Nov 2010 12:34:34 +0000] rev 26
added a recent paper by Tobias Nipkow on regular expressions
urbanc [Fri, 26 Nov 2010 10:53:14 +0000] rev 25
added interesting paper by rutten
urbanc [Thu, 25 Nov 2010 18:54:45 +0000] rev 24
added paper
wu [Thu, 18 Nov 2010 11:39:17 +0000] rev 23
All cases of the Other direction finished
urbanc [Wed, 10 Nov 2010 11:59:29 +0000] rev 22
added a test file
urbanc [Wed, 10 Nov 2010 11:53:07 +0000] rev 21
my slides from the talk in Cambridge
urbanc [Wed, 10 Nov 2010 11:49:45 +0000] rev 20
added my slides
urbanc [Mon, 08 Nov 2010 01:13:09 +0000] rev 19
slight tuning of proof by Chunhan
wu [Sat, 06 Nov 2010 23:31:53 +0000] rev 18
the ALT case is done;
the other two cases:
the relation is defined by not proved on inj part.
urbanc [Wed, 03 Nov 2010 22:08:50 +0000] rev 17
added more experiments
urbanc [Wed, 03 Nov 2010 21:42:44 +0000] rev 16
added initial slides for informal talk in Cambridge
urbanc [Tue, 26 Oct 2010 23:09:31 +0000] rev 15
added slides of chunhan
urbanc [Tue, 26 Oct 2010 13:01:22 +0000] rev 14
more experiments
urbanc [Sun, 24 Oct 2010 01:17:44 +0000] rev 13
a few more experiments, but no proof for the ALT-case
wu [Sat, 23 Oct 2010 12:51:38 +0000] rev 12
add some proofs about the other direction
1: the NULL case
2: the EMPTY case
3: the atomic CHAR c case
urbanc [Fri, 22 Oct 2010 19:43:56 +0000] rev 11
deleted two unnecessary lemmas
urbanc [Fri, 22 Oct 2010 10:45:01 +0000] rev 10
added a paper by Constable about the Myhill-Nerode in Nuprl using DFA and a paper by tobias about RegExp->DFA translation
urbanc [Thu, 21 Oct 2010 15:35:03 +0000] rev 9
deleted the test
urbanc [Thu, 21 Oct 2010 15:06:30 +0000] rev 8
tried at the end to prove the other direction (failed at the moment)
urbanc [Thu, 21 Oct 2010 13:42:08 +0000] rev 7
deleted the matcher ate the beginning; made it to work with stable Isabelle and the development version
wu [Wed, 20 Oct 2010 14:11:14 +0000] rev 6
former version has a ugly usage of "overloaded";
changing this using "overloading"
by chunhan
urbanc [Tue, 19 Oct 2010 11:51:05 +0000] rev 5
added a file about the easy closure properties of regular sets (the difficult parts, like complement, are missing)
wu [Thu, 07 Oct 2010 05:30:21 +0000] rev 4
Add a test file, after testing, this file can be deleted.
chunhan, 2010-10-7, in nanjing
urbanc [Sun, 03 Oct 2010 08:12:48 +0000] rev 3
added simple regexp matcher from Slind et al
urbanc [Sun, 03 Oct 2010 06:55:21 +0000] rev 2
test
urbanc [Sun, 03 Oct 2010 06:42:01 +0000] rev 1
added literature
urbanc [Sun, 03 Oct 2010 06:32:12 +0000] rev 0
added initial version by Chunhan