Journal/Paper.thy
author urbanc
Mon, 25 Jul 2011 13:33:38 +0000
changeset 170 b1258b7d2789
parent 167 61d0a412a3ae
child 172 21ee3a852a02
permissions -rw-r--r--
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
     1
(*<*)
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
     2
theory Paper
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
     3
imports "../Closure" 
24
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
     4
begin
39
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
     5
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
     6
declare [[show_question_marks = false]]
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
     7
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
     8
consts
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
     9
 REL :: "(string \<times> string) \<Rightarrow> bool"
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
    10
 UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
    11
70
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
    12
abbreviation
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
    13
  "EClass x R \<equiv> R `` {x}"
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
    14
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
    15
abbreviation 
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
    16
  "Append_rexp2 r_itm r \<equiv> Append_rexp r r_itm"
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
    17
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
    18
39
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
    19
notation (latex output)
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
    20
  str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
    21
  str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
    22
  Seq (infixr "\<cdot>" 100) and
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
    23
  Star ("_\<^bsup>\<star>\<^esup>") and
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
    24
  pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
58
0d4d5bb321dc a little bit in the introduction
urbanc
parents: 54
diff changeset
    25
  Suc ("_+1" [100] 100) and
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
    26
  quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
    27
  REL ("\<approx>") and
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
    28
  UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    29
  L_rexp ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
    30
  Lam ("\<lambda>'(_')" [100] 100) and 
89
42af13d194c9 a bit more on the paper
urbanc
parents: 88
diff changeset
    31
  Trn ("'(_, _')" [100, 100] 100) and 
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
    32
  EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
88
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
    33
  transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
    34
  Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
    35
  Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
    36
  Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    37
  uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    38
  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
121
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
    39
  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
    40
  tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
    41
  tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
    42
  tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
    43
  tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    44
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    45
lemma meta_eq_app:
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    46
  shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    47
  by auto
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    48
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    49
(* THEOREMS *)
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    50
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    51
notation (Rule output)
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    52
  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    53
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    54
syntax (Rule output)
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    55
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    56
  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    57
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    58
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    59
  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    60
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    61
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    62
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    63
notation (Axiom output)
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    64
  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    65
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    66
notation (IfThen output)
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    67
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    68
syntax (IfThen output)
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    69
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    70
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    71
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    72
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    73
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    74
notation (IfThenNoBox output)
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    75
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    76
syntax (IfThenNoBox output)
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    77
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    78
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    79
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    80
  "_asm" :: "prop \<Rightarrow> asms" ("_")
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    81
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    82
24
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
    83
(*>*)
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
    84
70
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
    85
24
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
    86
section {* Introduction *}
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
    87
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
    88
text {*
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
    89
  \noindent
58
0d4d5bb321dc a little bit in the introduction
urbanc
parents: 54
diff changeset
    90
  Regular languages are an important and well-understood subject in Computer
60
fb08f41ca33d a bit more tuning on the introduction
urbanc
parents: 59
diff changeset
    91
  Science, with many beautiful theorems and many useful algorithms. There is a
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
    92
  wide range of textbooks on this subject, many of which are aimed at students
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
    93
  and contain very detailed `pencil-and-paper' proofs
60
fb08f41ca33d a bit more tuning on the introduction
urbanc
parents: 59
diff changeset
    94
  (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
    95
  formalising the theorems and by verifying formally the algorithms.
170
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents: 167
diff changeset
    96
  Some of the popular theorem provers are based on Higher-Order Logic (HOL).
59
fc35eb54fdc9 more on the intro
urbanc
parents: 58
diff changeset
    97
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
    98
  There is however a problem: the typical approach to regular languages is to
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
    99
  introduce finite automata and then define everything in terms of them.  For
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   100
  example, a regular language is normally defined as one whose strings are
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   101
  recognised by a finite deterministic automaton. This approach has many
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   102
  benefits. Among them is the fact that it is easy to convince oneself that
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   103
  regular languages are closed under complementation: one just has to exchange
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   104
  the accepting and non-accepting states in the corresponding automaton to
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   105
  obtain an automaton for the complement language.  The problem, however, lies with
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   106
  formalising such reasoning in a HOL-based theorem prover, in our case
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   107
  Isabelle/HOL. Automata are built up from states and transitions that 
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   108
  need to be represented as graphs, matrices or functions, none
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   109
  of which can be defined as an inductive datatype. 
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   110
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   111
  In case of graphs and matrices, this means we have to build our own
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   112
  reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   113
  HOLlight support them with libraries. Even worse, reasoning about graphs and
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   114
  matrices can be a real hassle in HOL-based theorem provers.  Consider for
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   115
  example the operation of sequencing two automata, say $A_1$ and $A_2$, by
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   116
  connecting the accepting states of $A_1$ to the initial state of $A_2$:
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   117
  %  
60
fb08f41ca33d a bit more tuning on the introduction
urbanc
parents: 59
diff changeset
   118
  \begin{center}
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   119
  \begin{tabular}{ccc}
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   120
  \begin{tikzpicture}[scale=0.8]
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   121
  %\draw[step=2mm] (-1,-1) grid (1,1);
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   122
  
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   123
  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   124
  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   125
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   126
  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   127
  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   128
  
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   129
  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   130
  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   131
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   132
  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   133
  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   134
  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   135
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   136
  \draw (-0.6,0.0) node {\footnotesize$A_1$};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   137
  \draw ( 0.6,0.0) node {\footnotesize$A_2$};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   138
  \end{tikzpicture}
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   139
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   140
  & 
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   141
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   142
  \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   143
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   144
  &
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   145
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   146
  \begin{tikzpicture}[scale=0.8]
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   147
  %\draw[step=2mm] (-1,-1) grid (1,1);
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   148
  
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   149
  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   150
  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   151
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   152
  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   153
  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   154
  
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   155
  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   156
  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   157
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   158
  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   159
  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   160
  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   161
  
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   162
  \draw (C) to [very thick, bend left=45] (B);
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   163
  \draw (D) to [very thick, bend right=45] (B);
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   164
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   165
  \draw (-0.6,0.0) node {\footnotesize$A_1$};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   166
  \draw ( 0.6,0.0) node {\footnotesize$A_2$};
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   167
  \end{tikzpicture}
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   168
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   169
  \end{tabular}
60
fb08f41ca33d a bit more tuning on the introduction
urbanc
parents: 59
diff changeset
   170
  \end{center}
fb08f41ca33d a bit more tuning on the introduction
urbanc
parents: 59
diff changeset
   171
fb08f41ca33d a bit more tuning on the introduction
urbanc
parents: 59
diff changeset
   172
  \noindent
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   173
  On `paper' we can define the corresponding graph in terms of the disjoint 
88
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
   174
  union of the state nodes. Unfortunately in HOL, the standard definition for disjoint 
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   175
  union, namely 
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   176
  %
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   177
  \begin{equation}\label{disjointunion}
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   178
  @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"}
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   179
  \end{equation}
60
fb08f41ca33d a bit more tuning on the introduction
urbanc
parents: 59
diff changeset
   180
61
070f543e2560 more to the intro
urbanc
parents: 60
diff changeset
   181
  \noindent
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   182
  changes the type---the disjoint union is not a set, but a set of pairs. 
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
   183
  Using this definition for disjoint union means we do not have a single type for automata
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   184
  and hence will not be able to state certain properties about \emph{all}
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   185
  automata, since there is no type quantification available in HOL (unlike in Coq, for example). An
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   186
  alternative, which provides us with a single type for automata, is to give every 
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   187
  state node an identity, for example a natural
70
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
   188
  number, and then be careful to rename these identities apart whenever
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   189
  connecting two automata. This results in clunky proofs
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   190
  establishing that properties are invariant under renaming. Similarly,
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   191
  connecting two automata represented as matrices results in very adhoc
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   192
  constructions, which are not pleasant to reason about.
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   193
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   194
  Functions are much better supported in Isabelle/HOL, but they still lead to similar
88
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
   195
  problems as with graphs.  Composing, for example, two non-deterministic automata in parallel
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   196
  requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98} 
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   197
  dismisses for this the option of using identities, because it leads according to 
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   198
  him to ``messy proofs''. He
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   199
  opts for a variant of \eqref{disjointunion} using bit lists, but writes 
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   200
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   201
  \begin{quote}
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   202
  \it%
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   203
  \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   204
  `` & All lemmas appear obvious given a picture of the composition of automata\ldots
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   205
       Yet their proofs require a painful amount of detail.''
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   206
  \end{tabular}
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   207
  \end{quote}
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   208
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   209
  \noindent
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   210
  and
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   211
  
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   212
  \begin{quote}
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   213
  \it%
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   214
  \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   215
  `` & If the reader finds the above treatment in terms of bit lists revoltingly
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   216
       concrete, I cannot disagree. A more abstract approach is clearly desirable.''
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   217
  \end{tabular}
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   218
  \end{quote}
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   219
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   220
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   221
  \noindent
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   222
  Moreover, it is not so clear how to conveniently impose a finiteness condition 
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   223
  upon functions in order to represent \emph{finite} automata. The best is
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   224
  probably to resort to more advanced reasoning frameworks, such as \emph{locales}
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   225
  or \emph{type classes},
134
08afbed1c8c7 chunhan's comments
urbanc
parents: 133
diff changeset
   226
  which are \emph{not} available in all HOL-based theorem provers.
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   227
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   228
  {\bf add commnets from Brozowski}
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   229
66
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   230
  Because of these problems to do with representing automata, there seems
828ea293b61f more on the introduction
urbanc
parents: 61
diff changeset
   231
  to be no substantial formalisation of automata theory and regular languages 
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   232
  carried out in HOL-based theorem provers. Nipkow  \cite{Nipkow98} establishes
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   233
  the link between regular expressions and automata in
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   234
  the context of lexing. Berghofer and Reiter \cite{BerghoferReiter09} 
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   235
  formalise automata working over 
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   236
  bit strings in the context of Presburger arithmetic.
114
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   237
  The only larger formalisations of automata theory 
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   238
  are carried out in Nuprl \cite{Constable00} and in Coq \cite{Filliatre97}.
58
0d4d5bb321dc a little bit in the introduction
urbanc
parents: 54
diff changeset
   239
  
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   240
  In this paper, we will not attempt to formalise automata theory in
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   241
  Isabelle/HOL, but take a different approach to regular
82
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   242
  languages. Instead of defining a regular language as one where there exists
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   243
  an automaton that recognises all strings of the language, we define a
14b12b5de6d3 added coments about functions
urbanc
parents: 79
diff changeset
   244
  regular language as:
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   245
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   246
  \begin{dfntn}
77
63bc9f9d96ba small additions
urbanc
parents: 75
diff changeset
   247
  A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   248
  strings of @{text "A"}.
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   249
  \end{dfntn}
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   250
  
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   251
  \noindent
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   252
  The reason is that regular expressions, unlike graphs, matrices and functions, can
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   253
  be easily defined as inductive datatype. Consequently a corresponding reasoning 
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   254
  infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   255
  of regular expression matching based on derivatives \cite{OwensSlind08} and
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   256
  with an equivalence checker for regular expressions in Isabelle/HOL \cite{KraussNipkow11}.  
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   257
  The purpose of this paper is to
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   258
  show that a central result about regular languages---the Myhill-Nerode theorem---can 
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   259
  be recreated by only using regular expressions. This theorem gives necessary
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   260
  and sufficient conditions for when a language is regular. As a corollary of this
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   261
  theorem we can easily establish the usual closure properties, including 
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   262
  complementation, for regular languages.\smallskip
61
070f543e2560 more to the intro
urbanc
parents: 60
diff changeset
   263
  
070f543e2560 more to the intro
urbanc
parents: 60
diff changeset
   264
  \noindent
88
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
   265
  {\bf Contributions:} 
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
   266
  There is an extensive literature on regular languages.
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   267
  To our best knowledge, our proof of the Myhill-Nerode theorem is the
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   268
  first that is based on regular expressions, only. We prove the part of this theorem 
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   269
  stating that a regular expression has only finitely many partitions using certain 
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
   270
  tagging-functions. Again to our best knowledge, these tagging-functions have
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   271
  not been used before to establish the Myhill-Nerode theorem.
24
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
   272
*}
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
   273
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   274
section {* Preliminaries *}
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   275
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   276
text {*
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   277
  Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   278
  being represented by the empty list, written @{term "[]"}.  \emph{Languages}
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   279
  are sets of strings. The language containing all strings is written in
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   280
  Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages 
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   281
  is written @{term "A \<cdot> B"} and a language raised to the power @{text n} is written 
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   282
  @{term "A \<up> n"}. They are defined as usual
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   283
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   284
  \begin{center}
58
0d4d5bb321dc a little bit in the introduction
urbanc
parents: 54
diff changeset
   285
  @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
0d4d5bb321dc a little bit in the introduction
urbanc
parents: 54
diff changeset
   286
  \hspace{7mm}
0d4d5bb321dc a little bit in the introduction
urbanc
parents: 54
diff changeset
   287
  @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}
0d4d5bb321dc a little bit in the introduction
urbanc
parents: 54
diff changeset
   288
  \hspace{7mm}
0d4d5bb321dc a little bit in the introduction
urbanc
parents: 54
diff changeset
   289
  @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   290
  \end{center}
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   291
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   292
  \noindent
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   293
  where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   294
  is defined as the union over all powers, namely @{thm Star_def}. In the paper
88
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
   295
  we will make use of the following properties of these constructions.
58
0d4d5bb321dc a little bit in the introduction
urbanc
parents: 54
diff changeset
   296
  
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   297
  \begin{prpstn}\label{langprops}\mbox{}\\
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   298
  \begin{tabular}{@ {}ll}
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   299
  (i)   & @{thm star_cases}     \\ 
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   300
  (ii)  & @{thm[mode=IfThen] pow_length}\\
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   301
  (iii) & @{thm seq_Union_left} \\ 
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   302
  \end{tabular}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   303
  \end{prpstn}
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   304
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   305
  \noindent
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   306
  In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   307
  string; this property states that if \mbox{@{term "[] \<notin> A"}} then the lengths of
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   308
  the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}.  We omit
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   309
  the proofs for these properties, but invite the reader to consult our
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   310
  formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}}
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   311
90
97b783438316 added an example
urbanc
parents: 89
diff changeset
   312
  The notation in Isabelle/HOL for the quotient of a language @{text A} according to an 
97b783438316 added an example
urbanc
parents: 89
diff changeset
   313
  equivalence relation @{term REL} is @{term "A // REL"}. We will write 
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   314
  @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined 
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   315
  as \mbox{@{text "{y | y \<approx> x}"}}.
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   316
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   317
51
6cfb92de4654 some tuning of the paper
urbanc
parents: 50
diff changeset
   318
  Central to our proof will be the solution of equational systems
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   319
  involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64},
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   320
  which solves equations of the form @{term "X = A \<cdot> X \<union> B"} provided
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   321
  @{term "[] \<notin> A"}. However we will need the following `reverse' 
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   322
  version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A \<cdot> X"} to
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   323
  \mbox{@{term "X \<cdot> A"}}).
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   324
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   325
  \begin{lmm}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
86
6457e668dee5 tuned comments and names in Myhill_1
urbanc
parents: 83
diff changeset
   326
  If @{thm (prem 1) arden} then
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   327
  @{thm (lhs) arden} if and only if
86
6457e668dee5 tuned comments and names in Myhill_1
urbanc
parents: 83
diff changeset
   328
  @{thm (rhs) arden}.
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   329
  \end{lmm}
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   330
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   331
  \begin{proof}
86
6457e668dee5 tuned comments and names in Myhill_1
urbanc
parents: 83
diff changeset
   332
  For the right-to-left direction we assume @{thm (rhs) arden} and show
6457e668dee5 tuned comments and names in Myhill_1
urbanc
parents: 83
diff changeset
   333
  that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"} 
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   334
  we have @{term "A\<star> = {[]} \<union> A \<cdot> A\<star>"},
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   335
  which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both 
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   336
  sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   337
  is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. This completes this direction. 
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   338
86
6457e668dee5 tuned comments and names in Myhill_1
urbanc
parents: 83
diff changeset
   339
  For the other direction we assume @{thm (lhs) arden}. By a simple induction
51
6cfb92de4654 some tuning of the paper
urbanc
parents: 50
diff changeset
   340
  on @{text n}, we can establish the property
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   341
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   342
  \begin{center}
86
6457e668dee5 tuned comments and names in Myhill_1
urbanc
parents: 83
diff changeset
   343
  @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   344
  \end{center}
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   345
  
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   346
  \noindent
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   347
  Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   348
  all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   349
  of @{text "\<star>"}.
51
6cfb92de4654 some tuning of the paper
urbanc
parents: 50
diff changeset
   350
  For the inclusion in the other direction we assume a string @{text s}
134
08afbed1c8c7 chunhan's comments
urbanc
parents: 133
diff changeset
   351
  with length @{text k} is an element in @{text X}. Since @{thm (prem 1) arden}
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   352
  we know by Prop.~\ref{langprops}@{text "(ii)"} that 
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   353
  @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   354
  (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer). 
53
da85feadb8e3 small typo
urbanc
parents: 52
diff changeset
   355
  From @{text "(*)"} it follows then that
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   356
  @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   357
  implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} 
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   358
  this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.\qed
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   359
  \end{proof}
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   360
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   361
  \noindent
88
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
   362
  Regular expressions are defined as the inductive datatype
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   363
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   364
  \begin{center}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   365
  @{text r} @{text "::="}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   366
  @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   367
  @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   368
  @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   369
  @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   370
  @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   371
  @{term "STAR r"}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   372
  \end{center}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   373
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   374
  \noindent
88
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
   375
  and the language matched by a regular expression is defined as
67
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   376
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   377
  \begin{center}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   378
  \begin{tabular}{c@ {\hspace{10mm}}c}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   379
  \begin{tabular}{rcl}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   380
  @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   381
  @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   382
  @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   383
  \end{tabular}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   384
  &
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   385
  \begin{tabular}{rcl}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   386
  @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   387
       @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   388
  @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   389
       @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   390
  @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   391
      @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   392
  \end{tabular}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   393
  \end{tabular}
7478be786f87 more intro
urbanc
parents: 66
diff changeset
   394
  \end{center}
70
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
   395
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   396
  Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating 
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
   397
  a regular expression that matches the union of all languages of @{text rs}. We only need to know the 
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
   398
  existence
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   399
  of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   400
  @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the 
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   401
  set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   402
  %
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   403
  \begin{equation}\label{uplus}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   404
  \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   405
  \end{equation}
88
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
   406
1436fc451bb9 added something about Setalt and folds
urbanc
parents: 86
diff changeset
   407
  \noindent
90
97b783438316 added an example
urbanc
parents: 89
diff changeset
   408
  holds, whereby @{text "\<calL> ` rs"} stands for the 
97b783438316 added an example
urbanc
parents: 89
diff changeset
   409
  image of the set @{text rs} under function @{text "\<calL>"}.
50
32bff8310071 revised proof of Ardens lemma
urbanc
parents: 39
diff changeset
   410
*}
39
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
   411
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
   412
133
3ab755a96cef minor change
urbanc
parents: 132
diff changeset
   413
section {* The Myhill-Nerode Theorem, First Part *}
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   414
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   415
text {*
77
63bc9f9d96ba small additions
urbanc
parents: 75
diff changeset
   416
  The key definition in the Myhill-Nerode theorem is the
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   417
  \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two 
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   418
  strings are related, provided there is no distinguishing extension in this
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   419
  language. This can be defined as a tertiary relation.
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   420
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   421
  \begin{dfntn}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   422
  @{text y} are Myhill-Nerode related provided
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   423
  \begin{center}
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   424
  @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   425
  \end{center}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   426
  \end{dfntn}
70
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
   427
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   428
  \noindent
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   429
  It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   430
  partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   431
  equivalence classes. To illustrate this quotient construction, let us give a simple 
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   432
  example: consider the regular language containing just
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   433
  the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   434
  into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and  @{text "X\<^isub>3"}
90
97b783438316 added an example
urbanc
parents: 89
diff changeset
   435
  as follows
97b783438316 added an example
urbanc
parents: 89
diff changeset
   436
  
97b783438316 added an example
urbanc
parents: 89
diff changeset
   437
  \begin{center}
97b783438316 added an example
urbanc
parents: 89
diff changeset
   438
  @{text "X\<^isub>1 = {[]}"}\hspace{5mm}
97b783438316 added an example
urbanc
parents: 89
diff changeset
   439
  @{text "X\<^isub>2 = {[c]}"}\hspace{5mm}
97b783438316 added an example
urbanc
parents: 89
diff changeset
   440
  @{text "X\<^isub>3 = UNIV - {[], [c]}"}
97b783438316 added an example
urbanc
parents: 89
diff changeset
   441
  \end{center}
97b783438316 added an example
urbanc
parents: 89
diff changeset
   442
97b783438316 added an example
urbanc
parents: 89
diff changeset
   443
  One direction of the Myhill-Nerode theorem establishes 
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   444
  that if there are finitely many equivalence classes, like in the example above, then 
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   445
  the language is regular. In our setting we therefore have to show:
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   446
  
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   447
  \begin{thrm}\label{myhillnerodeone}
96
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   448
  @{thm[mode=IfThen] Myhill_Nerode1}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   449
  \end{thrm}
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   450
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   451
  \noindent
90
97b783438316 added an example
urbanc
parents: 89
diff changeset
   452
  To prove this theorem, we first define the set @{term "finals A"} as those equivalence
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   453
  classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   454
  %
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   455
  \begin{equation} 
70
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
   456
  @{thm finals_def}
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   457
  \end{equation}
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   458
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   459
  \noindent
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
   460
  In our running example, @{text "X\<^isub>2"} is the only 
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
   461
  equivalence class in @{term "finals {[c]}"}.
90
97b783438316 added an example
urbanc
parents: 89
diff changeset
   462
  It is straightforward to show that in general @{thm lang_is_union_of_finals} and 
79
bba9c80735f9 started to define things more directly
urbanc
parents: 77
diff changeset
   463
  @{thm finals_in_partitions} hold. 
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   464
  Therefore if we know that there exists a regular expression for every
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   465
  equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   466
  a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression 
98
36f9d19be0e6 included comments by Xingyuan
urbanc
parents: 96
diff changeset
   467
  that matches every string in @{text A}.
70
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
   468
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   469
90
97b783438316 added an example
urbanc
parents: 89
diff changeset
   470
  Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a
79
bba9c80735f9 started to define things more directly
urbanc
parents: 77
diff changeset
   471
  regular expression for \emph{every} equivalence class, not just the ones 
77
63bc9f9d96ba small additions
urbanc
parents: 75
diff changeset
   472
  in @{term "finals A"}. We
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   473
  first define the notion of \emph{one-character-transition} between 
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   474
  two equivalence classes
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   475
  %
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   476
  \begin{equation} 
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   477
  @{thm transition_def}
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   478
  \end{equation}
70
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
   479
71
426070e68b21 more on the paper
urbanc
parents: 70
diff changeset
   480
  \noindent
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   481
  which means that if we concatenate the character @{text c} to the end of all 
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   482
  strings in the equivalence class @{text Y}, we obtain a subset of 
77
63bc9f9d96ba small additions
urbanc
parents: 75
diff changeset
   483
  @{text X}. Note that we do not define an automaton here, we merely relate two sets
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   484
  (with the help of a character). In our concrete example we have 
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   485
  @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any 
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   486
  other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   487
  
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   488
  Next we construct an \emph{initial equational system} that
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   489
  contains an equation for each equivalence class. We first give
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   490
  an informal description of this construction. Suppose we have 
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   491
  the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   492
  contains the empty string @{text "[]"} (since equivalence classes are disjoint).
77
63bc9f9d96ba small additions
urbanc
parents: 75
diff changeset
   493
  Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   494
  
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   495
  \begin{center}
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   496
  \begin{tabular}{rcl}
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   497
  @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   498
  @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   499
  & $\vdots$ \\
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   500
  @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   501
  \end{tabular}
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   502
  \end{center}
70
8ab3a06577cf slightly more on the paper
urbanc
parents: 67
diff changeset
   503
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   504
  \noindent
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   505
  where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   506
  stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   507
  X\<^isub>i"}. 
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   508
  %The intuition behind the equational system is that every 
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   509
  %equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   510
  %corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states 
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   511
  %are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these 
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   512
  %predecessor states to @{text X\<^isub>i}. 
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   513
  There can only be
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   514
  finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side 
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   515
  since by assumption there are only finitely many
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   516
  equivalence classes and only finitely many characters.
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   517
  The term @{text "\<lambda>(EMPTY)"} in the first equation acts as a marker for the initial state, that
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   518
  is the equivalence class
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   519
  containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   520
  single `initial' state in the equational system, which is different from
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   521
  the method by Brzozowski \cite{Brzozowski64}, where he marks the
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   522
  `terminal' states. We are forced to set up the equational system in our
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   523
  way, because the Myhill-Nerode relation determines the `direction' of the
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   524
  transitions---the successor `state' of an equivalence class @{text Y} can
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   525
  be reached by adding a character to the end of @{text Y}. This is also the
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   526
  reason why we have to use our reverse version of Arden's Lemma.}
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   527
  %In our initial equation system there can only be
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   528
  %finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side 
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   529
  %since by assumption there are only finitely many
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   530
  %equivalence classes and only finitely many characters. 
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   531
  Overloading the function @{text \<calL>} for the two kinds of terms in the
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   532
  equational system, we have
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   533
  
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   534
  \begin{center}
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   535
  @{text "\<calL>(Y, r) \<equiv>"} %
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   536
  @{thm (rhs) L_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   537
  @{thm L_trm.simps(1)[where r="r", THEN eq_reflection]}
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   538
  \end{center}
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   539
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   540
  \noindent
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   541
  and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   542
  %
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   543
  \begin{equation}\label{inv1}
83
f438f4dbaada a bit more on the paper
urbanc
parents: 82
diff changeset
   544
  @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   545
  \end{equation}
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   546
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   547
  \noindent
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   548
  hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   549
  %
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   550
  \begin{equation}\label{inv2}
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   551
  @{text "X\<^isub>1 = \<calL>(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   552
  \end{equation}
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   553
d63baacbdb16 parts of the 3 section
urbanc
parents: 71
diff changeset
   554
  \noindent
160
ea2e5acbfe4a added comments from Chunhan
urbanc
parents: 159
diff changeset
   555
  holds. The reason for adding the @{text \<lambda>}-marker to our initial equational system is 
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   556
  to obtain this equation: it only holds with the marker, since none of 
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   557
  the other terms contain the empty string. The point of the initial equational system is
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   558
  that solving it means we will be able to extract a regular expression for every equivalence class. 
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   559
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   560
  Our representation for the equations in Isabelle/HOL are pairs,
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   561
  where the first component is an equivalence class (a set of strings)
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   562
  and the second component
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   563
  is a set of terms. Given a set of equivalence
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   564
  classes @{text CS}, our initial equational system @{term "Init CS"} is thus 
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   565
  formally defined as
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   566
  %
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   567
  \begin{equation}\label{initcs}
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   568
  \mbox{\begin{tabular}{rcl}     
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   569
  @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} & 
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   570
  @{text "if"}~@{term "[] \<in> X"}\\
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   571
  & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   572
  & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   573
  @{thm (lhs) Init_def}     & @{text "\<equiv>"} & @{thm (rhs) Init_def}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   574
  \end{tabular}}
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   575
  \end{equation}
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   576
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   577
  
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   578
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   579
  \noindent
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   580
  Because we use sets of terms 
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   581
  for representing the right-hand sides of equations, we can 
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   582
  prove \eqref{inv1} and \eqref{inv2} more concisely as
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   583
  %
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   584
  \begin{lmm}\label{inv}
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   585
  If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   586
  \end{lmm}
77
63bc9f9d96ba small additions
urbanc
parents: 75
diff changeset
   587
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   588
  \noindent
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   589
  Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   590
  initial equational system into one in \emph{solved form} maintaining the invariant
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   591
  in Lem.~\ref{inv}. From the solved form we will be able to read
89
42af13d194c9 a bit more on the paper
urbanc
parents: 88
diff changeset
   592
  off the regular expressions. 
42af13d194c9 a bit more on the paper
urbanc
parents: 88
diff changeset
   593
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   594
  In order to transform an equational system into solved form, we have two 
89
42af13d194c9 a bit more on the paper
urbanc
parents: 88
diff changeset
   595
  operations: one that takes an equation of the form @{text "X = rhs"} and removes
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   596
  any recursive occurrences of @{text X} in the @{text rhs} using our variant of Arden's 
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   597
  Lemma. The other operation takes an equation @{text "X = rhs"}
89
42af13d194c9 a bit more on the paper
urbanc
parents: 88
diff changeset
   598
  and substitutes @{text X} throughout the rest of the equational system
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   599
  adjusting the remaining regular expressions appropriately. To define this adjustment 
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   600
  we define the \emph{append-operation} taking a term and a regular expression as argument
89
42af13d194c9 a bit more on the paper
urbanc
parents: 88
diff changeset
   601
42af13d194c9 a bit more on the paper
urbanc
parents: 88
diff changeset
   602
  \begin{center}
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   603
  @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   604
  @{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
89
42af13d194c9 a bit more on the paper
urbanc
parents: 88
diff changeset
   605
  \end{center}
42af13d194c9 a bit more on the paper
urbanc
parents: 88
diff changeset
   606
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
   607
  \noindent
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   608
  We lift this operation to entire right-hand sides of equations, written as
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   609
  @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   610
  the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   611
  %
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   612
  \begin{equation}\label{arden_def}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   613
  \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
94
5b12cd0a3b3c latest on the paper
urbanc
parents: 93
diff changeset
   614
  @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\ 
5b12cd0a3b3c latest on the paper
urbanc
parents: 93
diff changeset
   615
   & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
5b12cd0a3b3c latest on the paper
urbanc
parents: 93
diff changeset
   616
   & & @{text "r' ="}   & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
5b12cd0a3b3c latest on the paper
urbanc
parents: 93
diff changeset
   617
   & &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\ 
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   618
  \end{tabular}}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   619
  \end{equation}
93
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   620
2aa3756dcc9f more on the paper
urbanc
parents: 92
diff changeset
   621
  \noindent
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   622
  In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   623
  then we calculate the combined regular expressions for all @{text r} coming 
94
5b12cd0a3b3c latest on the paper
urbanc
parents: 93
diff changeset
   624
  from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
5b12cd0a3b3c latest on the paper
urbanc
parents: 93
diff changeset
   625
  finally we append this regular expression to @{text rhs'}. It can be easily seen 
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   626
  that this operation mimics Arden's Lemma on the level of equations. To ensure
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   627
  the non-emptiness condition of Arden's Lemma we say that a right-hand side is
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   628
  @{text ardenable} provided
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   629
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   630
  \begin{center}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   631
  @{thm ardenable_def}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   632
  \end{center}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   633
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   634
  \noindent
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   635
  This allows us to prove a version of Arden's Lemma on the level of equations.
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   636
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   637
  \begin{lmm}\label{ardenable}
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   638
  Given an equation @{text "X = rhs"}.
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   639
  If @{text "X = \<Union>\<calL> ` rhs"},
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   640
  @{thm (prem 2) Arden_keeps_eq}, and
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   641
  @{thm (prem 3) Arden_keeps_eq}, then
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
   642
  @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   643
  \end{lmm}
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   644
  
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   645
  \noindent
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   646
  Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   647
  but we can still ensure that it holds troughout our algorithm of transforming equations
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   648
  into solved form. The \emph{substitution-operation} takes an equation
95
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   649
  of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
94
5b12cd0a3b3c latest on the paper
urbanc
parents: 93
diff changeset
   650
5b12cd0a3b3c latest on the paper
urbanc
parents: 93
diff changeset
   651
  \begin{center}
95
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   652
  \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   653
  @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\ 
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   654
   & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   655
   & & @{text "r' ="}   & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   656
   & &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> append_rhs_rexp xrhs r'"}}\\ 
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   657
  \end{tabular}
94
5b12cd0a3b3c latest on the paper
urbanc
parents: 93
diff changeset
   658
  \end{center}
95
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   659
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   660
  \noindent
134
08afbed1c8c7 chunhan's comments
urbanc
parents: 133
diff changeset
   661
  We again delete first all occurrences of @{text "(X, r)"} in @{text rhs}; we then calculate
95
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   662
  the regular expression corresponding to the deleted terms; finally we append this
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   663
  regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
9540c2f2ea77 more things
urbanc
parents: 94
diff changeset
   664
  the substitution operation we will arrange it so that @{text "xrhs"} does not contain
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   665
  any occurrence of @{text X}.
96
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   666
134
08afbed1c8c7 chunhan's comments
urbanc
parents: 133
diff changeset
   667
  With these two operations in place, we can define the operation that removes one equation
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   668
  from an equational systems @{text ES}. The operation @{const Subst_all}
96
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   669
  substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES}; 
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   670
  @{const Remove} then completely removes such an equation from @{text ES} by substituting 
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   671
  it to the rest of the equational system, but first eliminating all recursive occurrences
96
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   672
  of @{text X} by applying @{const Arden} to @{text "xrhs"}.
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   673
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   674
  \begin{center}
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   675
  \begin{tabular}{rcl}
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   676
  @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   677
  @{thm (lhs) Remove_def}    & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   678
  \end{tabular}
3b9deda4f459 simplified a bit the proof
urbanc
parents: 95
diff changeset
   679
  \end{center}
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   680
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   681
  \noindent
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   682
  Finally, we can define how an equational system should be solved. For this 
107
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   683
  we will need to iterate the process of eliminating equations until only one equation
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   684
  will be left in the system. However, we do not just want to have any equation
107
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   685
  as being the last one, but the one involving the equivalence class for 
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   686
  which we want to calculate the regular 
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   687
  expression. Let us suppose this equivalence class is @{text X}. 
107
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   688
  Since @{text X} is the one to be solved, in every iteration step we have to pick an
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   689
  equation to be eliminated that is different from @{text X}. In this way 
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   690
  @{text X} is kept to the final step. The choice is implemented using Hilbert's choice 
107
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   691
  operator, written @{text SOME} in the definition below.
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   692
  
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   693
  \begin{center}
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   694
  \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   695
  @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\ 
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   696
   & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   697
   & &  \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\ 
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   698
  \end{tabular}
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   699
  \end{center}
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   700
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   701
  \noindent
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   702
  The last definition we need applies @{term Iter} over and over until a condition 
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   703
  @{text Cond} is \emph{not} satisfied anymore. This condition states that there
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   704
  are more than one equation left in the equational system @{text ES}. To solve
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   705
  an equational system we use Isabelle/HOL's @{text while}-operator as follows:
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   706
  
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   707
  \begin{center}
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   708
  @{thm Solve_def}
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   709
  \end{center}
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   710
101
d3fe0597080a updated paper
urbanc
parents: 100
diff changeset
   711
  \noindent
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   712
  We are not concerned here with the definition of this operator
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   713
  (see Berghofer and Nipkow \cite{BerghoferNipkow00}), but note that we eliminate
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   714
  in each @{const Iter}-step a single equation, and therefore 
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   715
  have a well-founded termination order by taking the cardinality 
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   716
  of the equational system @{text ES}. This enables us to prove
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
   717
  properties about our definition of @{const Solve} when we `call' it with
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   718
  the equivalence class @{text X} and the initial equational system 
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   719
  @{term "Init (UNIV // \<approx>A)"} from
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   720
  \eqref{initcs} using the principle:
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   721
  %
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   722
  \begin{equation}\label{whileprinciple}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   723
  \mbox{\begin{tabular}{l}
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   724
  @{term "invariant (Init (UNIV // \<approx>A))"} \\
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   725
  @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   726
  @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   727
  @{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   728
  \hline
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   729
  \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   730
  \end{tabular}}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   731
  \end{equation}
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   732
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   733
  \noindent
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   734
  This principle states that given an invariant (which we will specify below) 
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   735
  we can prove a property
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   736
  @{text "P"} involving @{const Solve}. For this we have to discharge the following
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   737
  proof obligations: first the
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   738
  initial equational system satisfies the invariant; second the iteration
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   739
  step @{text "Iter"} preserves the invariant as long as the condition @{term Cond} holds;
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   740
  third @{text "Iter"} decreases the termination order, and fourth that
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   741
  once the condition does not hold anymore then the property @{text P} must hold.
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   742
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   743
  The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   744
  returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   745
  that this equational system still satisfies the invariant. In order to get
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   746
  the proof through, the invariant is composed of the following six properties:
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   747
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   748
  \begin{center}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   749
  \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   750
  @{text "invariant ES"} & @{text "\<equiv>"} &
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   751
      @{term "finite ES"} & @{text "(finiteness)"}\\
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   752
  & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   753
  & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   754
  & @{text "\<and>"} & @{thm (rhs) distinctness_def}\\
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   755
  &             &  & @{text "(distinctness)"}\\
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   756
  & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\   
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   757
  & @{text "\<and>"} & @{thm (rhs) validity_def} & @{text "(validity)"}\\
103
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   758
  \end{tabular}
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   759
  \end{center}
f460d5f75cb5 updated
urbanc
parents: 101
diff changeset
   760
 
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   761
  \noindent
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   762
  The first two ensure that the equational system is always finite (number of equations
160
ea2e5acbfe4a added comments from Chunhan
urbanc
parents: 159
diff changeset
   763
  and number of terms in each equation); the third makes sure the `meaning' of the 
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   764
  equations is preserved under our transformations. The other properties are a bit more
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   765
  technical, but are needed to get our proof through. Distinctness states that every
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   766
  equation in the system is distinct. @{text Ardenable} ensures that we can always
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   767
  apply the @{text Arden} operation. 
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   768
  The last property states that every @{text rhs} can only contain equivalence classes
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   769
  for which there is an equation. Therefore @{text lhss} is just the set containing 
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   770
  the first components of an equational system,
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   771
  while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the 
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   772
  form @{term "Trn X r"}. That means formally @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"} 
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   773
  and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}.
108
212bfa431fa5 filled details in one place
urbanc
parents: 107
diff changeset
   774
  
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   775
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   776
  It is straightforward to prove that the initial equational system satisfies the
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   777
  invariant.
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   778
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   779
  \begin{lmm}\label{invzero}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   780
  @{thm[mode=IfThen] Init_ES_satisfies_invariant}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   781
  \end{lmm}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   782
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   783
  \begin{proof}
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   784
  Finiteness is given by the assumption and the way how we set up the 
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   785
  initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   786
  follows from the fact that the equivalence classes are disjoint. The @{text ardenable}
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   787
  property also follows from the setup of the initial equational system, as does 
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   788
  validity.\qed
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   789
  \end{proof}
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   790
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   791
  \noindent
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   792
  Next we show that @{text Iter} preserves the invariant.
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   793
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   794
  \begin{lmm}\label{iterone}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   795
  @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   796
  \end{lmm}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   797
107
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   798
  \begin{proof} 
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   799
  The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   800
  and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"} 
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   801
  preserves the invariant.
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   802
  We prove this as follows:
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   803
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   804
  \begin{center}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   805
  @{text "\<forall> ES."} @{thm (prem 1) Subst_all_satisfies_invariant} implies
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   806
  @{thm (concl) Subst_all_satisfies_invariant}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   807
  \end{center}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   808
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   809
  \noindent
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   810
  Finiteness is straightforward, as the @{const Subst} and @{const Arden} operations 
116
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   811
  keep the equational system finite. These operations also preserve soundness 
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   812
  and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   813
  The property @{text ardenable} is clearly preserved because the append-operation
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   814
  cannot make a regular expression to match the empty string. Validity is
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   815
  given because @{const Arden} removes an equivalence class from @{text yrhs}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   816
  and then @{const Subst_all} removes @{text Y} from the equational system.
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
   817
  Having proved the implication above, we can instantiate @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   818
  which matches with our proof-obligation of @{const "Subst_all"}. Since
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
   819
  \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption 
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   820
  to complete the proof.\qed 
107
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   821
  \end{proof}
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   822
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   823
  \noindent
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   824
  We also need the fact that @{text Iter} decreases the termination measure.
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   825
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   826
  \begin{lmm}\label{itertwo}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   827
  @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   828
  \end{lmm}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   829
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   830
  \begin{proof}
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   831
  By assumption we know that @{text "ES"} is finite and has more than one element.
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   832
  Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with 
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   833
  @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   834
  that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   835
  removes the equation @{text "Y = yrhs"} from the system, and therefore 
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   836
  the cardinality of @{const Iter} strictly decreases.\qed
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   837
  \end{proof}
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   838
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   839
  \noindent
134
08afbed1c8c7 chunhan's comments
urbanc
parents: 133
diff changeset
   840
  This brings us to our property we want to establish for @{text Solve}.
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   841
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   842
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   843
  \begin{lmm}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   844
  If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   845
  a @{text rhs} such that  @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   846
  and @{term "invariant {(X, rhs)}"}.
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   847
  \end{lmm}
104
5bd73aa805a7 updated paper
urbanc
parents: 103
diff changeset
   848
107
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   849
  \begin{proof} 
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   850
  In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   851
  stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition 
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   852
  that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   853
  in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}.
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   854
  Therefore our invariant cannot be just @{term "invariant ES"}, but must be 
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   855
  @{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption 
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   856
  @{thm (prem 2) Solve} and Lem.~\ref{invzero}, the more general invariant holds for
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   857
  the initial equational system. This is premise 1 of~\eqref{whileprinciple}.
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   858
  Premise 2 is given by Lem.~\ref{iterone} and the fact that @{const Iter} might
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   859
  modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it.
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   860
  Premise 3 of~\eqref{whileprinciple} is by Lem.~\ref{itertwo}. Now in premise 4
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   861
  we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   862
  and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   863
  does not holds. By the stronger invariant we know there exists such a @{text "rhs"}
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   864
  with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   865
  of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"},
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   866
  for which the invariant holds. This allows us to conclude that 
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   867
  @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold,
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   868
  as needed.\qed
107
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   869
  \end{proof}
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   870
106
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   871
  \noindent
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   872
  With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   873
  there exists a regular expression.
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   874
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   875
  \begin{lmm}\label{every_eqcl_has_reg}
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   876
  @{thm[mode=IfThen] every_eqcl_has_reg}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   877
  \end{lmm}
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   878
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   879
  \begin{proof}
138
2dfe13bc1443 three typos
urbanc
parents: 137
diff changeset
   880
  By the preceding lemma, we know that there exists a @{text "rhs"} such
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   881
  that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   882
  and that the invariant holds for this equation. That means we 
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   883
  know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
109
79b37ef9505f minor updated
urbanc
parents: 108
diff changeset
   884
  this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the 
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   885
  invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
   886
  we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation
106
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   887
  removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
   888
  This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   889
  So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = L (\<Uplus>rs)"}.
106
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   890
  With this we can conclude the proof.\qed
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   891
  \end{proof}
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   892
106
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   893
  \noindent
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   894
  Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   895
  of the Myhill-Nerode theorem.
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   896
106
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   897
  \begin{proof}[of Thm.~\ref{myhillnerodeone}]
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   898
  By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular expression for
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   899
  every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
110
e500cab16be4 completed first direction
urbanc
parents: 109
diff changeset
   900
  a subset of  @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   901
  in @{term "finals A"} there exists a regular expression. Moreover by assumption 
106
91dc591de63f updated paper
urbanc
parents: 105
diff changeset
   902
  we know that @{term "finals A"} must be finite, and therefore there must be a finite
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   903
  set of regular expressions @{text "rs"} such that
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   904
  @{term "\<Union>(finals A) = L (\<Uplus>rs)"}.
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   905
  Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"} 
107
6f4f9b7b9891 updated paper
urbanc
parents: 106
diff changeset
   906
  as the regular expression that is needed in the theorem.\qed
105
ae6ad1363eb9 updated paper
urbanc
parents: 104
diff changeset
   907
  \end{proof}
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   908
*}
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
   909
100
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   910
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   911
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   912
2409827d8eb8 updated
urbanc
parents: 98
diff changeset
   913
section {* Myhill-Nerode, Second Part *}
39
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
   914
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
   915
text {*
116
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   916
  We will prove in this section the second part of the Myhill-Nerode
160
ea2e5acbfe4a added comments from Chunhan
urbanc
parents: 159
diff changeset
   917
  theorem. It can be formulated in our setting as follows:
39
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
   918
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   919
  \begin{thrm}
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
   920
  Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   921
  \end{thrm}  
39
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
   922
116
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   923
  \noindent
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   924
  The proof will be by induction on the structure of @{text r}. It turns out
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   925
  the base cases are straightforward.
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   926
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   927
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   928
  \begin{proof}[Base Cases]
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   929
  The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because 
149
e122cb146ecc added the most current versions of the theories.
urbanc
parents: 145
diff changeset
   930
  we can easily establish that
39
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
   931
114
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   932
  \begin{center}
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   933
  \begin{tabular}{l}
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   934
  @{thm quot_null_eq}\\
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   935
  @{thm quot_empty_subset}\\
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   936
  @{thm quot_char_subset}
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   937
  \end{tabular}
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   938
  \end{center}
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   939
116
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   940
  \noindent
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   941
  hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed
114
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
   942
  \end{proof}
109
79b37ef9505f minor updated
urbanc
parents: 108
diff changeset
   943
116
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
   944
  \noindent
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
   945
  Much more interesting, however, are the inductive cases. They seem hard to solve 
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   946
  directly. The reader is invited to try. 
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   947
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
   948
  Our proof will rely on some
138
2dfe13bc1443 three typos
urbanc
parents: 137
diff changeset
   949
  \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will 
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
   950
  be easy to prove that the \emph{range} of these tagging-functions is finite
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   951
  (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}).
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
   952
  With this we will be able to infer that the tagging-functions, seen as relations,
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   953
  give rise to finitely many equivalence classes of @{const UNIV}. Finally we 
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
   954
  will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   955
  implies that @{term "UNIV // \<approx>(L r)"} must also be finite (a relation @{text "R\<^isub>1"} 
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   956
  is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}).
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   957
  We formally define the notion of a \emph{tagging-relation} as follows.
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   958
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   959
  \begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   960
  and @{text y} are \emph{tag-related} provided
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   961
  \begin{center}
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
   962
  @{text "x =tag= y \<equiv> tag x = tag y"}\;.
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   963
  \end{center}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   964
  \end{dfntn}
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   965
145
099e20f25b25 corrected small typo
urbanc
parents: 143
diff changeset
   966
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   967
  In order to establish finiteness of a set @{text A}, we shall use the following powerful
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   968
  principle from Isabelle/HOL's library.
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   969
  %
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   970
  \begin{equation}\label{finiteimageD}
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   971
  @{thm[mode=IfThen] finite_imageD}
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   972
  \end{equation}
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   973
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   974
  \noindent
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   975
  It states that if an image of a set under an injective function @{text f} (injective over this set) 
131
6b4c20714b4f chunhan's comments
urbanc
parents: 130
diff changeset
   976
  is finite, then the set @{text A} itself must be finite. We can use it to establish the following 
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   977
  two lemmas.
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   978
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   979
  \begin{lmm}\label{finone}
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   980
  @{thm[mode=IfThen] finite_eq_tag_rel}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   981
  \end{lmm}
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   982
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   983
  \begin{proof}
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   984
  We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   985
  @{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   986
  finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   987
  and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   988
  assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
149
e122cb146ecc added the most current versions of the theories.
urbanc
parents: 145
diff changeset
   989
  From the assumptions we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with 
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   990
  @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in 
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   991
  turn means that the equivalence classes @{text X}
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   992
  and @{text Y} must be equal.\qed
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   993
  \end{proof}
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
   994
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
   995
  \begin{lmm}\label{fintwo} 
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
   996
  Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   997
  @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   998
  If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
   999
  then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1000
  \end{lmm}
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
  1001
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
  1002
  \begin{proof}
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1003
  We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
  1004
  be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that 
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1005
  @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"},
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
  1006
  which is finite by assumption. What remains to be shown is that @{text f} is injective
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
  1007
  on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence 
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
  1008
  classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
  1009
  @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
  1010
  @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1011
  We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}. 
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1012
  From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1013
  and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1014
  such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
  1015
  are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
  1016
  they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
  1017
  \end{proof}
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
  1018
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
  1019
  \noindent
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1020
  Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1021
  that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging-function whose
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1022
  range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1023
  Let us attempt the @{const ALT}-case first.
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1024
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1025
  \begin{proof}[@{const "ALT"}-Case] 
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1026
  We take as tagging-function 
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1027
  %
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1028
  \begin{center}
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1029
  @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1030
  \end{center}
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
  1031
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1032
  \noindent
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1033
  where @{text "A"} and @{text "B"} are some arbitrary languages.
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1034
  We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1035
  then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1036
  @{term "tag_str_ALT A B"} is a subset of this product set---so finite. It remains to be shown
120
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1037
  that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to 
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1038
  showing
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1039
  %
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1040
  \begin{center}
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1041
  @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1042
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1043
  %
120
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1044
  \noindent
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1045
  which by unfolding the Myhill-Nerode relation is identical to
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1046
  %
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1047
  \begin{equation}\label{pattern}
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1048
  @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1049
  \end{equation}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1050
  %
120
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1051
  \noindent
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1052
  since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
142
f1fea2c2713f changed one occurence of tagging function into tagging relation
urbanc
parents: 138
diff changeset
  1053
  \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse 
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1054
  in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. 
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1055
  The definition of the tagging-function will give us in each case the
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1056
  information to infer that @{text "y @ z \<in> A \<union> B"}.
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1057
  Finally we
120
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
  1058
  can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1059
  \end{proof}
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
  1060
109
79b37ef9505f minor updated
urbanc
parents: 108
diff changeset
  1061
121
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
  1062
  \noindent
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
  1063
  The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1064
  they are slightly more complicated. In the @{const SEQ}-case we essentially have
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1065
  to be able to infer that 
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1066
  %
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1067
  \begin{center}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1068
  @{text "\<dots>"}@{term "x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1069
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1070
  %
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1071
  \noindent
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1072
  using the information given by the appropriate tagging-function. The complication 
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1073
  is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A \<cdot> B"}
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1074
  (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the
124
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1075
  notions of \emph{string prefixes} 
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1076
  %
124
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1077
  \begin{center}
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1078
  @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1079
  @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1080
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1081
  %
124
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1082
  \noindent
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1083
  and \emph{string subtraction}:
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1084
  %
124
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1085
  \begin{center}
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1086
  @{text "[] - y \<equiv> []"}\hspace{10mm}
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1087
  @{text "x - [] \<equiv> x"}\hspace{10mm}
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1088
  @{text "cx - dy \<equiv> if c = d then x - y else cx"}
124
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1089
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1090
  %
124
8233510cab6c added definition of string prefix and string subtraction
urbanc
parents: 123
diff changeset
  1091
  \noindent
142
f1fea2c2713f changed one occurence of tagging function into tagging relation
urbanc
parents: 138
diff changeset
  1092
  where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. 
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1093
  
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1094
  Now assuming  @{term "x @ z \<in> A \<cdot> B"} there are only two possible ways of how to `split' 
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1095
  this string to be in @{term "A \<cdot> B"}:
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1096
  %
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1097
  \begin{center}
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1098
  \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1099
  \scalebox{0.7}{
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1100
  \begin{tikzpicture}
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1101
    \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1102
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1103
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1104
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1105
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1106
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1107
               node[midway, above=0.5em]{@{text x}};
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1108
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1109
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1110
           (z.north west) -- ($(z.north east)+(0em,0em)$)
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1111
               node[midway, above=0.5em]{@{text z}};
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1112
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1113
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1114
           ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1115
               node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1116
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1117
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1118
           ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1119
               node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1120
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1121
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1122
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1123
               node[midway, below=0.5em]{@{term "x' \<in> A"}};
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1124
  \end{tikzpicture}}
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1125
  &
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1126
  \scalebox{0.7}{
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1127
  \begin{tikzpicture}
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1128
    \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1129
    \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1130
    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z - z'"}\hspace{2.6em}$  };
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1131
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1132
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1133
           (x.north west) -- ($(za.north west)+(0em,0em)$)
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1134
               node[midway, above=0.5em]{@{text x}};
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1135
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1136
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1137
           ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1138
               node[midway, above=0.5em]{@{text z}};
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1139
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1140
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1141
           ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1142
               node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1143
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1144
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1145
           ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1146
               node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1147
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1148
    \draw[decoration={brace,transform={yscale=3}},decorate]
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1149
           ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1150
               node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1151
  \end{tikzpicture}}
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1152
  \end{tabular}
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1153
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1154
  %
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1155
  \noindent
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
  1156
  Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
  1157
  or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1158
  In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. For this we use the 
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1159
  following tagging-function
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1160
  %
121
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
  1161
  \begin{center}
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
  1162
  @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
  1163
  \end{center}
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1164
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1165
  \noindent
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1166
  with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1167
  is in the language @{text B}.
125
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1168
62925473bf6b added pictures for seq-case
urbanc
parents: 124
diff changeset
  1169
  \begin{proof}[@{const SEQ}-Case]
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1170
  If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1171
  then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1172
  @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
130
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1173
  We have to show injectivity of this tagging-function as
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1174
  %
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1175
  \begin{center}
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1176
  @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1177
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1178
  %
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1179
  \noindent
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1180
  There are two cases to be considered (see pictures above). First, there exists 
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1181
  a @{text "x'"} such that
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1182
  @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1183
  %
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1184
  \begin{center}
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1185
  @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1186
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1187
  %
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1188
  \noindent
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1189
  and by the assumption about @{term "tag_str_SEQ A B"} also 
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1190
  %
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1191
  \begin{center}
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1192
  @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1193
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1194
  %
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1195
  \noindent
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1196
  That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and 
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1197
  @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1198
  @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1199
  relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1200
  have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1201
  @{term "y @ z \<in> A \<cdot> B"}, as needed in this case.
127
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1202
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1203
  Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1204
  By the assumption about @{term "tag_str_SEQ A B"} we have
8440863a9900 seq case finished
urbanc
parents: 126
diff changeset
  1205
  @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
134
08afbed1c8c7 chunhan's comments
urbanc
parents: 133
diff changeset
  1206
  relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1207
  with @{term "y @ z \<in> A \<cdot> B"}. We again can complete the @{const SEQ}-case
129
urbanc
parents: 128
diff changeset
  1208
  by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed 
121
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
  1209
  \end{proof}
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1210
  
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1211
  \noindent
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1212
  The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When
137
06bafc710423 one further polishing
urbanc
parents: 136
diff changeset
  1213
  we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the 
130
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1214
  empty string, we 
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1215
  have the following picture:
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1216
  %
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1217
  \begin{center}
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1218
  \scalebox{0.7}{
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1219
  \begin{tikzpicture}
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1220
    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ };
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1221
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ };
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1222
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1223
    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1224
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1225
    \draw[decoration={brace,transform={yscale=3}},decorate]
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1226
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1227
               node[midway, above=0.5em]{@{text x}};
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1228
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1229
    \draw[decoration={brace,transform={yscale=3}},decorate]
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1230
           (za.north west) -- ($(zb.north east)+(0em,0em)$)
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1231
               node[midway, above=0.5em]{@{text z}};
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1232
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1233
    \draw[decoration={brace,transform={yscale=3}},decorate]
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1234
           ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1235
               node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}};
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1236
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1237
    \draw[decoration={brace,transform={yscale=3}},decorate]
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1238
           ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1239
               node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}};
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1240
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1241
    \draw[decoration={brace,transform={yscale=3}},decorate]
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1242
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
136
13b0f3dac9a2 final final polishing
urbanc
parents: 135
diff changeset
  1243
               node[midway, below=0.5em]{@{term "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1244
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1245
    \draw[decoration={brace,transform={yscale=3}},decorate]
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1246
           ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
136
13b0f3dac9a2 final final polishing
urbanc
parents: 135
diff changeset
  1247
               node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}};
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1248
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1249
    \draw[decoration={brace,transform={yscale=3}},decorate]
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1250
           ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
136
13b0f3dac9a2 final final polishing
urbanc
parents: 135
diff changeset
  1251
               node[midway, below=0.5em]{@{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1252
  \end{tikzpicture}}
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1253
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1254
  %
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1255
  \noindent
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1256
  We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1257
  @{text "x' < x"} and the rest @{term "(x - x') @ z \<in> A\<star>"}. For example the empty string 
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1258
  @{text "[]"} would do.
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1259
  There are potentially many such prefixes, but there can only be finitely many of them (the 
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1260
  string @{text x} is finite). Let us therefore choose the longest one and call it 
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1261
  @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1262
  know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, we can separate
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1263
  this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1264
  and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1265
  otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a}
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1266
  `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1267
   @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1268
  @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1269
  such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
145
099e20f25b25 corrected small typo
urbanc
parents: 143
diff changeset
  1270
  `border' of @{text x} and @{text z}. This string is @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a"}.
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1271
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1272
  In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1273
  the following tagging-function:
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1274
  %
121
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
  1275
  \begin{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1276
  @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
121
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
  1277
  \end{center}
128
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1278
6d2693c78c37 finished picture
urbanc
parents: 127
diff changeset
  1279
  \begin{proof}[@{const STAR}-Case]
130
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1280
  If @{term "finite (UNIV // \<approx>A)"} 
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1281
  then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1282
  @{term "tag_str_STAR A"} is a subset of this set, and therefore finite.
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1283
  Again we have to show injectivity of this tagging-function as  
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1284
  %
130
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1285
  \begin{center}
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1286
  @{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1287
  \end{center}  
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1288
  %
130
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1289
  \noindent
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1290
  We first need to consider the case that @{text x} is the empty string.
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1291
  From the assumption we can infer @{text y} is the empty string and
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1292
  clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
134
08afbed1c8c7 chunhan's comments
urbanc
parents: 133
diff changeset
  1293
  string, we can divide the string @{text "x @ z"} as shown in the picture 
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1294
  above. By the tagging-function we have
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1295
  %
130
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1296
  \begin{center}
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1297
  @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"}
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1298
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1299
  %
130
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1300
  \noindent
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1301
  which by assumption is equal to
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1302
  %
130
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1303
  \begin{center}
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1304
  @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1305
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1306
  %
130
3e4ad22193e7 pre-final version
urbanc
parents: 129
diff changeset
  1307
  \noindent 
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1308
  and we know that we have a @{term "y' \<in> A\<star>"} and @{text "y' < y"}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1309
  and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode
135
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1310
  relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1311
  Therefore @{term "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
604518f0127f final polished
urbanc
parents: 134
diff changeset
  1312
  @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "L r"} and
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1313
  complete the proof.\qed
121
1cf12a107b03 added directory with the small files and numbers of lines
urbanc
parents: 120
diff changeset
  1314
  \end{proof}
39
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
  1315
*}
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
  1316
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1317
section {* Second Part based on Partial Derivatives *}
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1318
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1319
text {*
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1320
   We briefly considered using the method Brzozowski presented in the
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1321
  Appendix of~\cite{Brzozowski64} in order to prove the second
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1322
  direction of the Myhill-Nerode theorem. There he calculates the
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1323
  derivatives for regular expressions and shows that for every
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1324
  language there can be only finitely many of them %derivations (if
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1325
  regarded equal modulo ACI). We could have used as tagging-function
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1326
  the set of derivatives of a regular expression with respect to a
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1327
  language.  Using the fact that two strings are Myhill-Nerode related
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1328
  whenever their derivative is the same, together with the fact that
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1329
  there are only finitely such derivatives would give us a similar
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1330
  argument as ours. However it seems not so easy to calculate the set
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1331
  of derivatives modulo ACI. Therefore we preferred our direct method
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1332
  of using tagging-functions. 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1333
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1334
*}
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1335
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1336
section {* Closure Properties *}
39
a59473f0229d tuned a little bit the section about finite partitions
urbanc
parents: 37
diff changeset
  1337
117
22ba25b808c8 updated second direction
urbanc
parents: 116
diff changeset
  1338
54
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
  1339
section {* Conclusion and Related Work *}
c19d2fc2cc69 a bit more on the paper
urbanc
parents: 53
diff changeset
  1340
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
  1341
text {*
112
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1342
  In this paper we took the view that a regular language is one where there
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
  1343
  exists a regular expression that matches all of its strings. Regular
145
099e20f25b25 corrected small typo
urbanc
parents: 143
diff changeset
  1344
  expressions can conveniently be defined as a datatype in HOL-based theorem
099e20f25b25 corrected small typo
urbanc
parents: 143
diff changeset
  1345
  provers. For us it was therefore interesting to find out how far we can push
154
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
  1346
  this point of view. We have established in Isabelle/HOL both directions 
7c68b9ad4486 implemented most suggestions from the reviewers
urbanc
parents: 149
diff changeset
  1347
  of the Myhill-Nerode theorem.
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1348
  %
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1349
  \begin{thrm}[The Myhill-Nerode Theorem]\mbox{}\\
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1350
  A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
167
61d0a412a3ae added a journal version
urbanc
parents: 162
diff changeset
  1351
  \end{thrm}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1352
  %
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1353
  \noindent
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1354
  Having formalised this theorem means we
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1355
  pushed our point of view quite far. Using this theorem we can obviously prove when a language
112
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1356
  is \emph{not} regular---by establishing that it has infinitely many
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1357
  equivalence classes generated by the Myhill-Nerode relation (this is usually
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1358
  the purpose of the pumping lemma \cite{Kozen97}).  We can also use it to
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1359
  establish the standard textbook results about closure properties of regular
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1360
  languages. Interesting is the case of closure under complement, because
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1361
  it seems difficult to construct a regular expression for the complement
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
  1362
  language by direct means. However the existence of such a regular expression
ec774952190c polished everything
urbanc
parents: 112
diff changeset
  1363
  can be easily proved using the Myhill-Nerode theorem since 
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1364
  %
112
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1365
  \begin{center}
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1366
  @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1367
  \end{center}
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1368
  %
112
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1369
  \noindent
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1370
  holds for any strings @{text "s\<^isub>1"} and @{text
114
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
  1371
  "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
159
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1372
  partitions.  Proving the existence of such a regular expression via automata 
990c12ab1562 edits; sqeezed to 16 pages
urbanc
parents: 157
diff changeset
  1373
  using the standard method would 
114
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
  1374
  be quite involved. It includes the
112
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1375
  steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1376
  "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1377
  regular expression.
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1378
116
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
  1379
  While regular expressions are convenient in formalisations, they have some
122
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1380
  limitations. One is that there seems to be no method of calculating a
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1381
  minimal regular expression (for example in terms of length) for a regular
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1382
  language, like there is
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1383
  for automata. On the other hand, efficient regular expression matching,
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1384
  without using automata, poses no problem \cite{OwensReppyTuron09}.
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1385
  For an implementation of a simple regular expression matcher,
122
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1386
  whose correctness has been formally established, we refer the reader to
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1387
  Owens and Slind \cite{OwensSlind08}.
116
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
  1388
342983676c8f included comments by Chunhan
urbanc
parents: 115
diff changeset
  1389
143
1cc87efb3b53 formalisation of first direction is now only 780 loc
urbanc
parents: 142
diff changeset
  1390
  Our formalisation consists of 780 lines of Isabelle/Isar code for the first
149
e122cb146ecc added the most current versions of the theories.
urbanc
parents: 145
diff changeset
  1391
  direction and 460 for the second, plus around 300 lines of standard material about
122
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1392
  regular languages. While this might be seen as too large to count as a
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1393
  concise proof pearl, this should be seen in the context of the work done by
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1394
  Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1395
  in Nuprl using automata. They write that their four-member team needed
134
08afbed1c8c7 chunhan's comments
urbanc
parents: 133
diff changeset
  1396
  something on the magnitude of 18 months for their formalisation. The
122
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1397
  estimate for our formalisation is that we needed approximately 3 months and
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1398
  this included the time to find our proof arguments. Unlike Constable et al,
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1399
  who were able to follow the proofs from \cite{HopcroftUllman69}, we had to
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1400
  find our own arguments.  So for us the formalisation was not the
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1401
  bottleneck. It is hard to gauge the size of a formalisation in Nurpl, but
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1402
  from what is shown in the Nuprl Math Library about their development it
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1403
  seems substantially larger than ours. The code of ours can be found in the
ab6637008963 my latest version (SEQ and STAR still missing)
urbanc
parents: 121
diff changeset
  1404
  Mercurial Repository at
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 131
diff changeset
  1405
  \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
  1406
112
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1407
62fdb4bf7239 more on the conclusion
urbanc
parents: 111
diff changeset
  1408
  Our proof of the first direction is very much inspired by \emph{Brzozowski's
134
08afbed1c8c7 chunhan's comments
urbanc
parents: 133
diff changeset
  1409
  algebraic method} used to convert a finite automaton to a regular
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
  1410
  expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence
111
d65d071798ff first ideas about conclusion
urbanc
parents: 110
diff changeset
  1411
  classes as the states of the minimal automaton for the regular language.
114
c5eb5f3065ae updated bib
urbanc
parents: 113
diff changeset
  1412
  However there are some subtle differences. Since we identify equivalence
111
d65d071798ff first ideas about conclusion
urbanc
parents: 110
diff changeset
  1413
  classes with the states of the automaton, then the most natural choice is to
d65d071798ff first ideas about conclusion
urbanc
parents: 110
diff changeset
  1414
  characterise each state with the set of strings starting from the initial
113
ec774952190c polished everything
urbanc
parents: 112
diff changeset
  1415
  state leading up to that state. Usually, however, the states are characterised as the
123
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1416
  strings starting from that state leading to the terminal states.  The first
23c0e6f2929d polished everywhere...two cases still missing
urbanc
parents: 122
diff changeset
  1417
  choice has consequences about how the initial equational system is set up. We have
115
c5f138b5fc88 added comment from Larry
urbanc
parents: 114
diff changeset
  1418
  the $\lambda$-term on our `initial state', while Brzozowski has it on the
111
d65d071798ff first ideas about conclusion
urbanc
parents: 110
diff changeset
  1419
  terminal states. This means we also need to reverse the direction of Arden's
156
fd39492b187c a few more changes
urbanc
parents: 154
diff changeset
  1420
  Lemma.
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
  1421
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1422
  This is also where our method shines, because we can completely
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1423
  side-step the standard argument \cite{Kozen97} where automata need
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1424
  to be composed, which as stated in the Introduction is not so easy
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1425
  to formalise in a HOL-based theorem prover. However, it is also the
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1426
  direction where we had to spend most of the `conceptual' time, as
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1427
  our proof-argument based on tagging-functions is new for
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1428
  establishing the Myhill-Nerode theorem. All standard proofs of this
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1429
  direction proceed by arguments over automata.\medskip
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1430
  
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1431
  \noindent
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1432
  {\bf Acknowledgements:} We are grateful for the comments we received from Larry
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
  1433
  Paulson.
111
d65d071798ff first ideas about conclusion
urbanc
parents: 110
diff changeset
  1434
92
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
  1435
*}
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
  1436
a9ebc410a5c8 more on paper
urbanc
parents: 90
diff changeset
  1437
24
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
  1438
(*<*)
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
  1439
end
f72c82bf59e5 added paper
urbanc
parents:
diff changeset
  1440
(*>*)