Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Journal/Paper.thy
changeset 265 d36be1e356c0
parent 218 16af5b8bd285
child 266 fff2e1b40dfc
equal deleted inserted replaced
264:e2828c4a1e23 265:d36be1e356c0 
     1 (*<*)
 
     1 (*<*)
 
     2 theory Paper
 
     2 theory Paper
 
     3 imports 
     3 imports 
     4    "../Lexer"
 
     4    "../Lexer"
 
     5    "../Simplifying" 
     5    "../Simplifying" 
     6    "../Sulzmann" 
     6    "../Positions" 
     7    "~~/src/HOL/Library/LaTeXsugar"
 
     7    "~~/src/HOL/Library/LaTeXsugar"
 
     8 begin
 
     8 begin
 
     9 
     9 
       
    10 lemma Suc_0_fold:
 
       
    11   "Suc 0 = 1"
 
       
    12 by simp
 
       
    13 
       
    14 
       
    15 
    10 declare [[show_question_marks = false]]
 
    16 declare [[show_question_marks = false]]
 
    11 
    17 
    12 abbreviation 
    18 abbreviation 
    13  "der_syn r c \<equiv> der c r"
 
    19   "der_syn r c \<equiv> der c r"
 
    14 
    20 
    15 abbreviation 
    21 abbreviation 
    16  "ders_syn r s \<equiv> ders s r"
 
    22   "ders_syn r s \<equiv> ders s r"
 
       
    23 
       
    24 
       
    25 abbreviation
 
       
    26   "nprec v1 v2 \<equiv> \<not>(v1 :\<sqsubset>val v2)"
 
       
    27 
    17 
    28 
    18 notation (latex output)
 
    29 notation (latex output)
 
    19   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
 
    30   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
 
    20   Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and  
    31   Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and  
    21 
    32 
    24   CHAR ("_" [1000] 80) and
 
    35   CHAR ("_" [1000] 80) and
 
    25   ALT ("_ + _" [77,77] 78) and
 
    36   ALT ("_ + _" [77,77] 78) and
 
    26   SEQ ("_ \<cdot> _" [77,77] 78) and
 
    37   SEQ ("_ \<cdot> _" [77,77] 78) and
 
    27   STAR ("_\<^sup>\<star>" [1000] 78) and
 
    38   STAR ("_\<^sup>\<star>" [1000] 78) and
 
    28   
    39   
    29   val.Void ("'(')" 1000) and
 
    40   val.Void ("Empty" 78) and
 
    30   val.Char ("Char _" [1000] 78) and
 
    41   val.Char ("Char _" [1000] 78) and
 
    31   val.Left ("Left _" [79] 78) and
 
    42   val.Left ("Left _" [79] 78) and
 
    32   val.Right ("Right _" [1000] 78) and
 
    43   val.Right ("Right _" [1000] 78) and
 
    33   val.Seq ("Seq _ _" [79,79] 78) and
 
    44   val.Seq ("Seq _ _" [79,79] 78) and
 
    34   val.Stars ("Stars _" [79] 78) and
 
    45   val.Stars ("Stars _" [79] 78) and
 
    54   F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and
 
    65   F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and
 
    55   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and
 
    66   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and
 
    56   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
 
    67   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
 
    57   slexer ("lexer\<^sup>+" 1000) and
 
    68   slexer ("lexer\<^sup>+" 1000) and
 
    58 
    69 
       
    70   at ("_\<^raw:\mbox{$\downharpoonleft$}>\<^bsub>_\<^esub>") and
 
       
    71   lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and
 
       
    72   PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and
 
       
    73   PosOrd_ex ("_ \<prec> _" [77,77] 77) and
 
       
    74   PosOrd_ex1 ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and
 
       
    75   pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and
 
       
    76   nprec ("_ \<^raw:\mbox{$\not\prec$}> _" [77,77] 77) 
       
    77 
       
    78   (*
 
    59   ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and
 
    79   ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and
 
    60   ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)
 
    80   ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)
 
       
    81   *)
 
    61 
    82 
    62 definition 
    83 definition 
    63   "match r s \<equiv> nullable (ders s r)"
 
    84   "match r s \<equiv> nullable (ders s r)"
 
    64 
    85 
    65 (*
 
    86 (*
 
    97 
   118 
    98 If a regular expression matches a string, then in general there is more than
 
   119 If a regular expression matches a string, then in general there is more than
 
    99 one way of how the string is matched. There are two commonly used
 
   120 one way of how the string is matched. There are two commonly used
 
   100 disambiguation strategies to generate a unique answer: one is called GREEDY
 
   121 disambiguation strategies to generate a unique answer: one is called GREEDY
 
   101 matching \cite{Frisch2004} and the other is POSIX
 
   122 matching \cite{Frisch2004} and the other is POSIX
 
   102 matching~\cite{Kuklewicz,Sulzmann2014,Vansummeren2006}. For example consider
 
   123 matching~\cite{POSIX,Kuklewicz,OkuiSuzuki2013,Sulzmann2014,Vansummeren2006}. For example consider
 
   103 the string @{term xy} and the regular expression \mbox{@{term "STAR (ALT
 
   124 the string @{term xy} and the regular expression \mbox{@{term "STAR (ALT
 
   104 (ALT x y) xy)"}}. Either the string can be matched in two `iterations' by
 
   125 (ALT x y) xy)"}}. Either the string can be matched in two `iterations' by
 
   105 the single letter-regular expressions @{term x} and @{term y}, or directly
 
   126 the single letter-regular expressions @{term x} and @{term y}, or directly
 
   106 in one iteration by @{term xy}. The first case corresponds to GREEDY
 
   127 in one iteration by @{term xy}. The first case corresponds to GREEDY
 
   107 matching, which first matches with the left-most symbol and only matches the
 
   128 matching, which first matches with the left-most symbol and only matches the
 
   112 In the context of lexing, where an input string needs to be split up into a
 
   133 In the context of lexing, where an input string needs to be split up into a
 
   113 sequence of tokens, POSIX is the more natural disambiguation strategy for
 
   134 sequence of tokens, POSIX is the more natural disambiguation strategy for
 
   114 what programmers consider basic syntactic building blocks in their programs.
 
   135 what programmers consider basic syntactic building blocks in their programs.
 
   115 These building blocks are often specified by some regular expressions, say
 
   136 These building blocks are often specified by some regular expressions, say
 
   116 @{text "r\<^bsub>key\<^esub>"} and @{text "r\<^bsub>id\<^esub>"} for recognising keywords and
 
   137 @{text "r\<^bsub>key\<^esub>"} and @{text "r\<^bsub>id\<^esub>"} for recognising keywords and
 
   117 identifiers, respectively. There are two underlying (informal) rules behind
 
   138 identifiers, respectively. There are a few underlying (informal) rules behind
 
   118 tokenising a string in a POSIX fashion according to a collection of regular
 
   139 tokenising a string in a POSIX \cite{POSIX} fashion according to a collection of regular
 
   119 expressions:
 
   140 expressions:
 
   120 
   141 
   121 \begin{itemize} 
   142 \begin{itemize} 
   122 \item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``maximal munch rule''}):
 
   143 \item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``{M}aximal {M}unch {R}ule''}):
 
   123 The longest initial substring matched by any regular expression is taken as
 
   144 The longest initial substring matched by any regular expression is taken as
 
   124 next token.\smallskip
 
   145 next token.\smallskip
 
   125 
   146 
   126 \item[$\bullet$] \emph{Priority Rule:}
 
   147 \item[$\bullet$] \emph{Priority Rule:}
 
   127 For a particular longest initial substring, the first regular expression
 
   148 For a particular longest initial substring, the first (leftmost) regular expression
 
   128 that can match determines the token.
 
   149 that can match determines the token.\smallskip
 
       
   150 
       
   151 \item[$\bullet$] \emph{Star Rule:} A subexpression repeated by ${}^\star$ shall 
       
   152 not match an empty string unless this is the only match for the repetition.\smallskip
 
       
   153 
       
   154 \item[$\bullet$] \emph{Empty String Rule:} An empty string shall be considered to 
       
   155 be longer than no match at all.
 
   129 \end{itemize}
 
   156 \end{itemize}
 
   130 
   157 
   131 \noindent Consider for example a regular expression @{text "r\<^bsub>key\<^esub>"} for recognising keywords
 
   158 \noindent Consider for example a regular expression @{text "r\<^bsub>key\<^esub>"} for recognising keywords
 
   132 such as @{text "if"}, @{text "then"} and so on; and @{text "r\<^bsub>id\<^esub>"}
 
   159 such as @{text "if"}, @{text "then"} and so on; and @{text "r\<^bsub>id\<^esub>"}
 
   133 recognising identifiers (say, a single character followed by
 
   160 recognising identifiers (say, a single character followed by
 
   155 r}, and to show that (once a string to be matched is chosen) there is
 
   182 r}, and to show that (once a string to be matched is chosen) there is
 
   156 a maximum element and that it is computed by their derivative-based
 
   183 a maximum element and that it is computed by their derivative-based
 
   157 algorithm. This proof idea is inspired by work of Frisch and Cardelli
 
   184 algorithm. This proof idea is inspired by work of Frisch and Cardelli
 
   158 \cite{Frisch2004} on a GREEDY regular expression matching
 
   185 \cite{Frisch2004} on a GREEDY regular expression matching
 
   159 algorithm. However, we were not able to establish transitivity and
 
   186 algorithm. However, we were not able to establish transitivity and
 
   160 totality for the ``order relation'' by Sulzmann and Lu. In Section
 
   187 totality for the ``order relation'' by Sulzmann and Lu. ??In Section
 
   161 \ref{argu} we identify some inherent problems with their approach (of
 
   188 \ref{argu} we identify some inherent problems with their approach (of
 
   162 which some of the proofs are not published in \cite{Sulzmann2014});
 
   189 which some of the proofs are not published in \cite{Sulzmann2014});
 
   163 perhaps more importantly, we give a simple inductive (and
 
   190 perhaps more importantly, we give a simple inductive (and
 
   164 algorithm-independent) definition of what we call being a {\em POSIX
 
   191 algorithm-independent) definition of what we call being a {\em POSIX
 
   165 value} for a regular expression @{term r} and a string @{term s}; we
 
   192 value} for a regular expression @{term r} and a string @{term s}; we
 
  1006   conclude in this case too.\qed   
  1033   conclude in this case too.\qed   
  1007 
  1034 
  1008   \end{proof} 
  1035   \end{proof} 
  1009 *}
 
  1036 *}
 
  1010 
  1037 
       
  1038 section {* Ordering of Values according to Okui and Suzuki*}
 
       
  1039 
       
  1040 text {*
 
       
  1041 
       
  1042  Positions are lists of natural numbers.
 
       
  1043 
       
  1044  The subvalue at position @{text p}, written @{term "at v p"}, is defined 
       
  1045   
       
  1046 
       
  1047  \begin{center}
 
       
  1048  \begin{tabular}{r@ {\hspace{0mm}}lcl}
 
       
  1049  @{term v} &  @{text "\<downharpoonleft>\<^bsub>[]\<^esub>"} & @{text "\<equiv>"}& @{thm (rhs) at.simps(1)}\\
 
       
  1050  @{term "Left v"} & @{text "\<downharpoonleft>\<^bsub>0::ps\<^esub>"} & @{text "\<equiv>"}& @{thm (rhs) at.simps(2)}\\
 
       
  1051  @{term "Right v"} & @{text "\<downharpoonleft>\<^bsub>1::ps\<^esub>"} & @{text "\<equiv>"} & 
       
  1052  @{thm (rhs) at.simps(3)[simplified Suc_0_fold]}\\
 
       
  1053  @{term "Seq v\<^sub>1 v\<^sub>2"} & @{text "\<downharpoonleft>\<^bsub>0::ps\<^esub>"} & @{text "\<equiv>"} & 
       
  1054  @{thm (rhs) at.simps(4)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} \\
 
       
  1055  @{term "Seq v\<^sub>1 v\<^sub>2"} & @{text "\<downharpoonleft>\<^bsub>1::ps\<^esub>"}
 
       
  1056  & @{text "\<equiv>"} & 
       
  1057  @{thm (rhs) at.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2", simplified Suc_0_fold]} \\
 
       
  1058  @{term "Stars vs"} & @{text "\<downharpoonleft>\<^bsub>n::ps\<^esub>"} & @{text "\<equiv>"}& @{thm (rhs) at.simps(6)}\\
 
       
  1059  \end{tabular} 
       
  1060  \end{center}
 
       
  1061 
       
  1062  \begin{center}
 
       
  1063  \begin{tabular}{lcl}
 
       
  1064  @{thm (lhs) Pos.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(1)}\\
 
       
  1065  @{thm (lhs) Pos.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(2)}\\
 
       
  1066  @{thm (lhs) Pos.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(3)}\\
 
       
  1067  @{thm (lhs) Pos.simps(4)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(4)}\\
 
       
  1068  @{thm (lhs) Pos.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
 
       
  1069   & @{text "\<equiv>"} 
       
  1070   & @{thm (rhs) Pos.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}\\
 
       
  1071  @{thm (lhs) Pos_stars} & @{text "\<equiv>"} & @{thm (rhs) Pos_stars}\\
 
       
  1072  \end{tabular}
 
       
  1073  \end{center}
 
       
  1074 
       
  1075  @{thm pflat_len_def}
 
       
  1076 
       
  1077 
       
  1078  \begin{center}
 
       
  1079  \begin{tabular}{ccc}
 
       
  1080  @{thm [mode=Axiom] lex_list.intros(1)}\hspace{1cm} &
 
       
  1081  @{thm [mode=Rule] lex_list.intros(2)[where ?ps1.0="ps\<^sub>1" and ?ps2.0="ps\<^sub>2"]}\hspace{1cm} &
 
       
  1082  @{thm [mode=Rule] lex_list.intros(3)[where ?p1.0="p\<^sub>1" and ?p2.0="p\<^sub>2" and
 
       
  1083                                             ?ps1.0="ps\<^sub>1" and ?ps2.0="ps\<^sub>2"]}
 
       
  1084  \end{tabular}
 
       
  1085  \end{center}
 
       
  1086 
       
  1087 
       
  1088  Main definition by Okui and Suzuki.
 
       
  1089 
       
  1090  \begin{center}
 
       
  1091  \begin{tabular}{ccl}
 
       
  1092  @{thm (lhs) PosOrd_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} &
 
       
  1093  @{text "\<equiv>"} &
 
       
  1094  @{term "pflat_len v\<^sub>1 p > pflat_len v\<^sub>2 p"}   and\\
 
       
  1095  & & @{term "(\<forall>q \<in> Pos v\<^sub>1 \<union> Pos v\<^sub>2. q \<sqsubset>lex p --> pflat_len v\<^sub>1 q = pflat_len v\<^sub>2 q)"}
 
       
  1096  \end{tabular}
 
       
  1097  \end{center}
 
       
  1098 
       
  1099  @{thm PosOrd_ex_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
 
       
  1100 
       
  1101  @{thm PosOrd_ex1_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
 
       
  1102 
       
  1103  Lemma 1
 
       
  1104 
       
  1105  @{thm [mode=IfThen] PosOrd_shorterE[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
 
       
  1106 
       
  1107  but in the other direction only
 
       
  1108 
       
  1109  @{thm [mode=IfThen] PosOrd_shorterI[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} 
       
  1110 
       
  1111  Lemma Transitivity:
 
       
  1112 
       
  1113  @{thm [mode=IfThen] PosOrd_trans[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and ?v3.0="v\<^sub>3"]} 
       
  1114 
       
  1115 
       
  1116 *}
 
       
  1117 
       
  1118 text {*
 
       
  1119 
       
  1120  Theorems:
 
       
  1121 
       
  1122  @{thm [mode=IfThen] Posix_CPT}
 
       
  1123 
       
  1124  @{thm [mode=IfThen] Posix_PosOrd[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
 
       
  1125 
       
  1126  Corrollary from the last one
 
       
  1127 
       
  1128  @{thm [mode=IfThen] Posix_PosOrd_stronger[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
 
       
  1129 
       
  1130  Theorem
 
       
  1131 
       
  1132  @{thm [mode=IfThen] PosOrd_Posix[where ?v1.0="v\<^sub>1"]}
 
       
  1133 *}
 
       
  1134 
       
  1135 
  1011 section {* The Correctness Argument by Sulzmann and Lu\label{argu} *}
 
  1136 section {* The Correctness Argument by Sulzmann and Lu\label{argu} *}
 
  1012 
  1137 
  1013 text {*
 
  1138 text {*
 
  1014 %  \newcommand{\greedy}{\succcurlyeq_{gr}}
 
  1139 %  \newcommand{\greedy}{\succcurlyeq_{gr}}
 
  1015  \newcommand{\posix}{>}
 
  1140  \newcommand{\posix}{>}
 
  1020   final form, we make no comment thereon, preferring to give general reasons
 
  1145   final form, we make no comment thereon, preferring to give general reasons
 
  1021   for our belief that the approach of \cite{Sulzmann2014} is problematic.
 
  1146   for our belief that the approach of \cite{Sulzmann2014} is problematic.
 
  1022   Their central definition is an ``ordering relation'' defined by the
 
  1147   Their central definition is an ``ordering relation'' defined by the
 
  1023   rules (slightly adapted to fit our notation):
 
  1148   rules (slightly adapted to fit our notation):
 
  1024 
  1149 
  1025 \begin{center}  
  1150   ??
 
  1026 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}	
       
  1027 @{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &
 
       
  1028 @{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\
 
       
  1029 
       
  1030 @{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\,(A1) &
 
       
  1031 @{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\,(A2)\smallskip\\
 
       
  1032 
       
  1033 @{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}\,(A3) &
 
       
  1034 @{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\,(A4)\smallskip\\
 
       
  1035 
       
  1036 @{thm[mode=Rule] K1[of "v" "vs" "r"]}\,(K1) &
 
       
  1037 @{thm[mode=Rule] K2[of "v" "vs" "r"]}\,(K2)\smallskip\\
 
       
  1038 
       
  1039 @{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\,(K3) &
 
       
  1040 @{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\,(K4)
 
       
  1041 \end{tabular}
 
       
  1042 \end{center}
 
       
  1043 
  1151 
  1044   \noindent The idea behind the rules (A1) and (A2), for example, is that a
 
  1152   \noindent The idea behind the rules (A1) and (A2), for example, is that a
 
  1045   @{text Left}-value is bigger than a @{text Right}-value, if the underlying
 
  1153   @{text Left}-value is bigger than a @{text Right}-value, if the underlying
 
  1046   string of the @{text Left}-value is longer or of equal length to the
 
  1154   string of the @{text Left}-value is longer or of equal length to the
 
  1047   underlying string of the @{text Right}-value. The order is reversed,
 
  1155   underlying string of the @{text Right}-value. The order is reversed,
 
  1060   string is. This seems to be only a very minor difference, but it has
 
  1168   string is. This seems to be only a very minor difference, but it has
 
  1061   drastic consequences in terms of what properties both orderings enjoy.
 
  1169   drastic consequences in terms of what properties both orderings enjoy.
 
  1062   What is interesting for our purposes is that the properties reflexivity,
 
  1170   What is interesting for our purposes is that the properties reflexivity,
 
  1063   totality and transitivity for this GREEDY ordering can be proved
 
  1171   totality and transitivity for this GREEDY ordering can be proved
 
  1064   relatively easily by induction.
 
  1172   relatively easily by induction.
 
  1065 
       
  1066   These properties of GREEDY, however, do not transfer to the POSIX
 
       
  1067   ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. 
       
  1068   To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is
 
       
  1069   not defined inductively, but as $($@{term "v\<^sub>1 = v\<^sub>2"}$)$ $\vee$ $($@{term "(v\<^sub>1 >r
 
       
  1070   v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}$)$. This means that @{term "v\<^sub>1
 
       
  1071   >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)
 
       
  1072   (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
 
       
  1073   formulation, for example:
 
       
  1074 
       
  1075   \begin{falsehood}
 
       
  1076   Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}.
 
       
  1077   If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
 
       
  1078   then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.
 
       
  1079   \end{falsehood}
 
       
  1080 
       
  1081   \noindent If formulated in this way, then there are various counter
 
       
  1082   examples: For example let @{term r} be @{text "a + ((a + a)\<cdot>(a + \<zero>))"}
 
       
  1083   then the @{term "v\<^sub>1"}, @{term "v\<^sub>2"} and @{term "v\<^sub>3"} below are values
 
       
  1084   of @{term r}:
 
       
  1085 
       
  1086   \begin{center}
 
       
  1087   \begin{tabular}{lcl}
 
       
  1088   @{term "v\<^sub>1"} & $=$ & @{term "Left(Char a)"}\\
 
       
  1089   @{term "v\<^sub>2"} & $=$ & @{term "Right(Seq (Left(Char a)) (Right Void))"}\\
 
       
  1090   @{term "v\<^sub>3"} & $=$ & @{term "Right(Seq (Right(Char a)) (Left(Char a)))"}
 
       
  1091   \end{tabular}
 
       
  1092   \end{center}
 
       
  1093 
       
  1094   \noindent Moreover @{term "v\<^sub>1 >(r::rexp) v\<^sub>2"} and @{term "v\<^sub>2 >(r::rexp)
 
       
  1095   v\<^sub>3"}, but \emph{not} @{term "v\<^sub>1 >(r::rexp) v\<^sub>3"}! The reason is that
 
       
  1096   although @{term "v\<^sub>3"} is a @{text "Right"}-value, it can match a longer
 
       
  1097   string, namely @{term "flat v\<^sub>3 = [a,a]"}, while @{term "flat v\<^sub>1"} (and
 
       
  1098   @{term "flat v\<^sub>2"}) matches only @{term "[a]"}. So transitivity in this
 
       
  1099   formulation does not hold---in this example actually @{term "v\<^sub>3
 
       
  1100   >(r::rexp) v\<^sub>1"}!
 
       
  1101 
       
  1102   Sulzmann and Lu ``fix'' this problem by weakening the transitivity
 
       
  1103   property. They require in addition that the underlying strings are of the
 
       
  1104   same length. This excludes the counter example above and any
 
       
  1105   counter-example we were able to find (by hand and by machine). Thus the
 
       
  1106   transitivity lemma should be formulated as:
 
       
  1107 
       
  1108   \begin{conject}
 
       
  1109   Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"},
 
       
  1110   and also @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}.\\
 
       
  1111   If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
 
       
  1112   then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.
 
       
  1113   \end{conject}
 
       
  1114 
       
  1115   \noindent While we agree with Sulzmann and Lu that this property
 
       
  1116   probably(!) holds, proving it seems not so straightforward: although one
 
       
  1117   begins with the assumption that the values have the same flattening, this
 
       
  1118   cannot be maintained as one descends into the induction. This is a problem
 
       
  1119   that occurs in a number of places in the proofs by Sulzmann and Lu.
 
       
  1120 
       
  1121   Although they do not give an explicit proof of the transitivity property,
 
       
  1122   they give a closely related property about the existence of maximal
 
       
  1123   elements. They state that this can be verified by an induction on @{term r}. We
 
       
  1124   disagree with this as we shall show next in case of transitivity. The case
 
       
  1125   where the reasoning breaks down is the sequence case, say @{term "SEQ r\<^sub>1 r\<^sub>2"}.
 
       
  1126   The induction hypotheses in this case are
 
       
  1127 
       
  1128 \begin{center}
 
       
  1129 \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 
       
  1130 \begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}
 
       
  1131 IH @{term "r\<^sub>1"}:\\
 
       
  1132 @{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."} \\
 
       
  1133   & @{term "\<turnstile> v\<^sub>1 : r\<^sub>1"}\;@{text "\<and>"}
 
       
  1134     @{term "\<turnstile> v\<^sub>2 : r\<^sub>1"}\;@{text "\<and>"}
 
       
  1135     @{term "\<turnstile> v\<^sub>3 : r\<^sub>1"}\\
 
       
  1136   & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\
 
       
  1137   & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>1::rexp) v\<^sub>3"}\medskip\\
 
       
  1138   & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>3"}
 
       
  1139 \end{tabular} &
 
       
  1140 \begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}
 
       
  1141 IH @{term "r\<^sub>2"}:\\
 
       
  1142 @{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."}\\ 
       
  1143   & @{term "\<turnstile> v\<^sub>1 : r\<^sub>2"}\;@{text "\<and>"}
 
       
  1144     @{term "\<turnstile> v\<^sub>2 : r\<^sub>2"}\;@{text "\<and>"}
 
       
  1145     @{term "\<turnstile> v\<^sub>3 : r\<^sub>2"}\\
 
       
  1146   & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\
 
       
  1147   & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>2::rexp) v\<^sub>3"}\medskip\\
 
       
  1148   & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>3"}
 
       
  1149 \end{tabular}
 
       
  1150 \end{tabular}
 
       
  1151 \end{center} 
       
  1152 
       
  1153   \noindent We can assume that
 
       
  1154   %
 
       
  1155   \begin{equation}
 
       
  1156   @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}
 
       
  1157   \qquad\textrm{and}\qquad
 
       
  1158   @{term "(Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}
 
       
  1159   \label{assms}
 
       
  1160   \end{equation}
 
       
  1161 
       
  1162   \noindent hold, and furthermore that the values have equal length, namely:
 
       
  1163   %
 
       
  1164   \begin{equation}
 
       
  1165   @{term "flat (Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) = flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}
 
       
  1166   \qquad\textrm{and}\qquad
 
       
  1167   @{term "flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) = flat (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}
 
       
  1168   \label{lens}
 
       
  1169   \end{equation} 
       
  1170 
       
  1171   \noindent We need to show that @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2)
 
       
  1172   (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"} holds. We can proceed by analysing how the
 
       
  1173   assumptions in \eqref{assms} have arisen. There are four cases. Let us
 
       
  1174   assume we are in the case where we know
 
       
  1175 
       
  1176   \[
 
       
  1177   @{term "v\<^sub>1\<^sub>l >(r\<^sub>1::rexp) v\<^sub>2\<^sub>l"}
 
       
  1178   \qquad\textrm{and}\qquad
 
       
  1179   @{term "v\<^sub>2\<^sub>l >(r\<^sub>1::rexp) v\<^sub>3\<^sub>l"}
 
       
  1180   \]
 
       
  1181 
       
  1182   \noindent and also know the corresponding inhabitation judgements. This is
 
       
  1183   exactly a case where we would like to apply the induction hypothesis
 
       
  1184   IH~$r_1$. But we cannot! We still need to show that @{term "flat (v\<^sub>1\<^sub>l) =
 
       
  1185   flat(v\<^sub>2\<^sub>l)"} and @{term "flat(v\<^sub>2\<^sub>l) = flat(v\<^sub>3\<^sub>l)"}. We know from
 
       
  1186   \eqref{lens} that the lengths of the sequence values are equal, but from
 
       
  1187   this we cannot infer anything about the lengths of the component values.
 
       
  1188   Indeed in general they will be unequal, that is
 
       
  1189 
       
  1190   \[
 
       
  1191   @{term "flat(v\<^sub>1\<^sub>l) \<noteq> flat(v\<^sub>2\<^sub>l)"}  
       
  1192   \qquad\textrm{and}\qquad
 
       
  1193   @{term "flat(v\<^sub>1\<^sub>r) \<noteq> flat(v\<^sub>2\<^sub>r)"}
 
       
  1194   \]
 
       
  1195 
       
  1196   \noindent but still \eqref{lens} will hold. Now we are stuck, since the IH
 
       
  1197   does not apply. As said, this problem where the induction hypothesis does
 
       
  1198   not apply arises in several places in the proof of Sulzmann and Lu, not
 
       
  1199   just for proving transitivity.
 
       
  1200 
       
  1201 *}
 
  1173 *}
 
       
  1174 
  1202 
  1175 
  1203 section {* Conclusion *}
 
  1176 section {* Conclusion *}
 
  1204 
  1177 
  1205 text {*
 
  1178 text {*
 
  1206 
  1179
lexing