Commit 163a6b08 authored by lammich's avatar lammich
Browse files

merged

5dd878a5f54a7d1cdbcb41a70dab21c4554d7791 Isabelle2011-1
......@@ -7,3 +7,4 @@
2009-1 = 2009-12-02
2009-2 = 2010-06-23
2011 = 2011-02-11
2011-1 = 2011-10-10
......@@ -22,6 +22,7 @@ afp-ArrowImpossibilityGS-2009-09-29.tar.gz
afp-ArrowImpossibilityGS-2009-12-12.tar.gz
afp-ArrowImpossibilityGS-2010-06-30.tar.gz
afp-ArrowImpossibilityGS-2011-02-11.tar.gz
afp-AutoFocus-Stream-2011-02-24.tar.gz
afp-BDD-2008-03-07.tar.gz
afp-BDD-2008-06-10.tar.gz
afp-BDD-2009-04-29.tar.gz
......@@ -217,6 +218,7 @@ afp-Functional-Automata-2009-04-29.tar.gz
afp-Functional-Automata-2009-12-12.tar.gz
afp-Functional-Automata-2010-07-01.tar.gz
afp-Functional-Automata-2011-02-11.tar.gz
afp-Gauss-Jordan-Elim-Fun-2011-08-19.tar.gz
afp-GenClock-2005-06-24.tar.gz
afp-GenClock-2005-10-14.tar.gz
afp-GenClock-2007-11-27.tar.gz
......@@ -225,6 +227,7 @@ afp-GenClock-2009-04-29.tar.gz
afp-GenClock-2009-12-12.tar.gz
afp-GenClock-2010-07-01.tar.gz
afp-GenClock-2011-02-11.tar.gz
afp-General-Triangle-2011-04-01.tar.gz
afp-GraphMarkingIBP-2010-05-28.tar.gz
afp-GraphMarkingIBP-2010-07-01.tar.gz
afp-GraphMarkingIBP-2011-02-11.tar.gz
......@@ -288,8 +291,10 @@ afp-JiveDataStoreModel-2009-04-29.tar.gz
afp-JiveDataStoreModel-2009-12-12.tar.gz
afp-JiveDataStoreModel-2010-07-01.tar.gz
afp-JiveDataStoreModel-2011-02-11.tar.gz
afp-KBPs-2011-05-19.tar.gz
afp-Lam-ml-Normalization-2010-09-01.tar.gz
afp-Lam-ml-Normalization-2011-02-11.tar.gz
afp-LatticeProperties-2011-09-27.tar.gz
afp-Lazy-Lists-II-2004-04-27.tar.gz
afp-Lazy-Lists-II-2004-05-21.tar.gz
afp-Lazy-Lists-II-2005-10-14.tar.gz
......@@ -299,6 +304,7 @@ afp-Lazy-Lists-II-2009-04-29.tar.gz
afp-Lazy-Lists-II-2009-12-12.tar.gz
afp-Lazy-Lists-II-2010-07-01.tar.gz
afp-Lazy-Lists-II-2011-02-11.tar.gz
afp-LightweightJava-2011-03-02.tar.gz
afp-LinearQuantifierElim-2008-01-11.tar.gz
afp-LinearQuantifierElim-2008-01-24.tar.gz
afp-LinearQuantifierElim-2008-02-12.tar.gz
......@@ -310,6 +316,7 @@ afp-LinearQuantifierElim-2011-02-11.tar.gz
afp-List-Index-2010-02-20.tar.gz
afp-List-Index-2010-07-01.tar.gz
afp-List-Index-2011-02-11.tar.gz
afp-List-Infinite-2011-02-24.tar.gz
afp-Locally-Nameless-Sigma-2010-05-03.tar.gz
afp-Locally-Nameless-Sigma-2010-07-01.tar.gz
afp-Locally-Nameless-Sigma-2011-02-11.tar.gz
......@@ -319,6 +326,8 @@ afp-Marriage-2011-02-11.tar.gz
afp-Matrix-2010-06-17.tar.gz
afp-Matrix-2010-07-01.tar.gz
afp-Matrix-2011-02-11.tar.gz
afp-Max-Card-Matching-2011-08-15.tar.gz
afp-Max-Card-Matching-2011-08-19.tar.gz
afp-MiniML-2004-03-23.tar.gz
afp-MiniML-2004-04-20.tar.gz
afp-MiniML-2004-05-21.tar.gz
......@@ -329,12 +338,14 @@ afp-MiniML-2009-04-29.tar.gz
afp-MiniML-2009-12-12.tar.gz
afp-MiniML-2010-07-01.tar.gz
afp-MiniML-2011-02-11.tar.gz
afp-MonoBoolTranAlgebra-2011-09-27.tar.gz
afp-MuchAdoAboutTwo-2007-11-27.tar.gz
afp-MuchAdoAboutTwo-2008-06-10.tar.gz
afp-MuchAdoAboutTwo-2009-04-29.tar.gz
afp-MuchAdoAboutTwo-2009-12-12.tar.gz
afp-MuchAdoAboutTwo-2010-07-01.tar.gz
afp-MuchAdoAboutTwo-2011-02-11.tar.gz
afp-Nat-Interval-Logic-2011-02-24.tar.gz
afp-NormByEval-2008-02-18.tar.gz
afp-NormByEval-2008-02-22.tar.gz
afp-NormByEval-2008-06-10.tar.gz
......@@ -375,6 +386,7 @@ afp-Program-Conflict-Analysis-2009-04-29.tar.gz
afp-Program-Conflict-Analysis-2009-12-12.tar.gz
afp-Program-Conflict-Analysis-2010-07-01.tar.gz
afp-Program-Conflict-Analysis-2011-02-11.tar.gz
afp-PseudoHoops-2011-09-27.tar.gz
afp-RIPEMD-160-SPARK-2011-01-19.tar.gz
afp-RIPEMD-160-SPARK-2011-02-11.tar.gz
afp-RSAPSS-2005-10-14.tar.gz
......@@ -461,6 +473,7 @@ afp-Topology-2009-04-29.tar.gz
afp-Topology-2009-12-12.tar.gz
afp-Topology-2010-07-01.tar.gz
afp-Topology-2011-02-11.tar.gz
afp-Transitive-Closure-2011-03-14.tar.gz
afp-Tree-Automata-2009-11-29.tar.gz
afp-Tree-Automata-2009-12-12.tar.gz
afp-Tree-Automata-2009-12-13.tar.gz
......
......@@ -36,6 +36,10 @@ begin
lemma trancl_mono_set: "r \<subseteq> s \<Longrightarrow> r^+ \<subseteq> s^+"
by (blast intro: trancl_mono)
lemma rel_pow_mono: assumes "(r :: ('a \<times> 'a)set) \<subseteq> r'" shows "r ^^ n \<subseteq> r' ^^ n"
by (induct n, insert assms, auto)
text {*
An abstract rewrite system (ARS) is a binary endorelation, i.e., a binary
relation where domain and codomain coincide.
......
......@@ -45,8 +45,7 @@ on
<tr><td class="datahead" valign="top">Abstract:</td>
<td class="abstract">
There are many proofs of the Myhill-Nerode theorem using automata. In this library we give a proof of this theorem entirely based on regular expressions, since regularity of languages can be conveniently defined using regular expressions (it is more painful in HOL to define regularity in terms of automata). We prove the first direction of the Myhill-Nerode theorem by solving equational systems that involve regular expressions. For the second direction we give two proofs: one using tagging-functions and another using partial derivatives. We also establish various closure properties of regular languages, including closure under complement and building the set of sub- and super-strings of a language. Most details of the theories are described
in our ITP 2011 paper.
There are many proofs of the Myhill-Nerode theorem using automata. In this library we give a proof entirely based on regular expressions, since regularity of languages can be conveniently defined using regular expressions (it is more painful in HOL to define regularity in terms of automata). We prove the first direction of the Myhill-Nerode theorem by solving equational systems that involve regular expressions. For the second direction we give two proofs: one using tagging-functions and another using partial derivatives. We also establish various closure properties of regular languages. Most details of the theories are described in our ITP 2011 paper.
</td></tr>
<tr><td class="datahead">License:</td>
......
......@@ -35,19 +35,7 @@ and larger scientific developments, mechanically checked in the theorem prover
<a href="http://isabelle.in.tum.de/">Isabelle</a>. It is organized in the way
of a scientific journal and has an ISSN: 2150-914x. Submissions are refereed. The preferred citation style
is available <a href="citing.shtml">[here]</a>.
</td></tr>
</tbody>
</table>
<p>&nbsp;</p>
<table width="80%" class="entries">
<tbody>
<tr><td><strong>This is the development version of the AFP.</strong> It is
provided as a preview of the next upcoming release and might
contain entries that are currently broken and that might change
without notice over time. Use at your own risk. Please refer to
the <a href="index.shtml">release version</a> only in citations.
</td></tr>
</tbody>
A <a href="devel.shtml">development version</a> of the archive is available as well.</td></tr>
</table>
<p>&nbsp;</p>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment