--- a/progs/Matcher2.thy	Fri Oct 23 00:16:00 2015 +0100
+++ b/progs/Matcher2.thy	Fri Oct 23 08:35:17 2015 +0100
@@ -24,9 +24,8 @@
 | PLUS rexp
 | OPT rexp
 | NTIMES rexp nat
-| NMTIMES rexp nat nat
 | NMTIMES2 rexp nat nat
-
+(*
 fun M :: "rexp \<Rightarrow> nat"
 where
   "M (NULL) = 0"
@@ -39,9 +38,8 @@
 | "M (PLUS r) = Suc (M r)"
 | "M (OPT r) = Suc (M r)"
 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
-| "M (NMTIMES r n m) = Suc (M r) * 2 * (Suc n + Suc m)"
-| "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc n + Suc m)"
-
+| "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc m - Suc n)"
+*)
 section {* Sequential Composition of Sets *}
 
 definition
@@ -161,7 +159,6 @@
 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 | "L (OPT r) = (L r) \<union> {[]}"
 | "L (NTIMES r n) = (L r) \<up> n"
-| "L (NMTIMES r n m) = (\<Union>i\<in> {n..n+m} . ((L r) \<up> i))" 
 | "L (NMTIMES2 r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
 
 
@@ -169,56 +166,6 @@
 apply(simp)
 done
 
-lemma "L (NMTIMES r (Suc n) m) = L (SEQ r (NMTIMES r n m))"
-apply(simp add:  Suc_reduce_Union Seq_def)
-apply(auto)
-done
-
-lemma "L (NMTIMES2 r (Suc n) (Suc m)) = L (SEQ r (NMTIMES2 r n m))"
-apply(simp add:  Suc_reduce_Union Seq_def)
-apply(auto)
-done
-
-lemma "L (NMTIMES2 r 0 0) = {[]}"
-apply(simp add: Suc_reduce_Union Seq_def)
-done
-
-lemma t: "\<lbrakk>n \<le> i; i \<le> m\<rbrakk> \<Longrightarrow> L (NMTIMES2 r n m) = L (NMTIMES2 r n i) \<union> L (NMTIMES2 r i m)"
-apply(auto)
-apply (metis atLeastAtMost_iff nat_le_linear)
-apply (metis atLeastAtMost_iff le_trans)
-by (metis atLeastAtMost_iff le_trans)
-
-
-lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \<union> L (NMTIMES2 r 1 (Suc m))"
-apply(rule t)
-apply(auto)
-done
-
-lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \<union> L (NMTIMES2 r 1 (Suc m))"
-apply(rule t)
-apply(auto)
-done
-
-lemma "L (NMTIMES2 r 0 1) = {[]} \<union> L r"
-apply(simp)
-apply(auto)
-apply(case_tac xa)
-apply(auto)
-done
-
-
-lemma "L (NMTIMES2 r n n) = L (NTIMES r n)"
-apply(simp)
-done
-
-lemma "n < m \<Longrightarrow> L (NMTIMES2 r n m) = L (NTIMES r n) \<union> L (NMTIMES2 r (Suc n) m)"
-apply(simp)
-apply(auto)
-apply (metis Suc_leI atLeastAtMost_iff le_eq_less_or_eq)
-apply (metis atLeastAtMost_iff le_eq_less_or_eq)
-by (metis Suc_leD atLeastAtMost_iff)
-
 section {* The Matcher *}
 
 fun
@@ -234,11 +181,23 @@
 | "nullable (PLUS r) = (nullable r)"
 | "nullable (OPT r) = True"
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
-| "nullable (NMTIMES r n m) = (if n = 0 then True else nullable r)"
 | "nullable (NMTIMES2 r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
-function
- der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
+fun M :: "rexp \<Rightarrow> nat"
+where
+  "M (NULL) = 0"
+| "M (EMPTY) = 0"
+| "M (CHAR char) = 0"
+| "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"
+| "M (ALT r1 r2) = Suc ((M r1) + (M r2))"
+| "M (STAR r) = Suc (M r)"
+| "M (NOT r) = Suc (M r)"
+| "M (PLUS r) = Suc (M r)"
+| "M (OPT r) = Suc (M r)"
+| "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
+| "M (NMTIMES2 r n m) = 3 * (Suc (M r) + n) * 3 * (Suc n) * (Suc (Suc m) - (Suc n))"
+
+function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
   "der c (NULL) = NULL"
 | "der c (EMPTY) = NULL"
@@ -251,17 +210,16 @@
 | "der c (OPT r) = der c r"
 | "der c (NTIMES r 0) = NULL"
 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
-| "der c (NMTIMES r 0 0) = NULL"
-| "der c (NMTIMES r 0 (Suc m)) = ALT (der c (NTIMES r (Suc m))) (der c (NMTIMES r 0 m))"
-| "der c (NMTIMES r (Suc n) m) = der c  (SEQ r (NMTIMES r n m))"
 | "der c (NMTIMES2 r n m) = (if m < n then NULL else 
                               (if n = m then der c (NTIMES r n) else
                                 ALT (der c (NTIMES r n)) (der c (NMTIMES2 r (Suc n) m))))"
 by pat_completeness auto
 
 termination der 
+apply(relation "measure (\<lambda>(c, r). M r)") 
+apply(simp_all)
 sorry
-(*by (relation "measure (\<lambda>(c, r). M r)") (simp_all)*)
+
 
 
 fun 

Binary file slides/slides05.pdf has changed

--- a/slides/slides05.tex	Fri Oct 23 00:16:00 2015 +0100
+++ b/slides/slides05.tex	Fri Oct 23 08:35:17 2015 +0100
@@ -179,14 +179,76 @@
 \end{center}
 
 \small
-\hspace{4.5cm}\bl{$(\varnothing \cdot (b \cdot c)) + ((\varnothing \cdot c) + \epsilon)$}
+\hspace{4.5cm}\bl{$(b \cdot c) + (\varnothing + \epsilon)$}
 $\mapsto$
-\bl{$\epsilon$}
+\bl{$(b \cdot c) + \epsilon$}
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+
+\begin{center}
+\bl{$\only<1>{(b \cdot c)}%
+     \only<2-3>{(\underline{b \cdot c})}%
+     \only<1-3>{+}% 
+     \only<1>{(\varnothing + \epsilon)}%
+     \only<2-3>{(\underline{\varnothing + \epsilon})}$}%
+\only<4->{%
+\bl{$\underline{(b \cdot c) + (\varnothing + \epsilon)}$}%
+}
+$\mapsto$
+\bl{$(b \cdot c) + \epsilon$}
+\end{center}\bigskip
+
+\onslide<3->{%
+\begin{center}
+\begin{tabular}{lcl}
+\bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
+\bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
+\end{tabular}
+\end{center}}
+
+\only<4>{%
+\begin{center}
+\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
+\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
+\quad \bl{$\lambda v.\,$} 
+        case \bl{$v = Left(v')$}: 
+      & return \bl{$Left(f_{s1}(v'))$}\\
+\quad \phantom{$\lambda v.\,$} 
+        case \bl{$v = Right(v')$}: 
+      & return \bl{$Right(f_{s2}(v'))$}\\ 
+\end{tabular}
+\end{center}}%
+\only<5->{%
+\begin{center}
+\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
+\only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
+\quad \bl{$\lambda v.\,$} 
+        case \bl{$v = Left(v')$}: 
+      & return \bl{$Left(v')$}\\
+\quad \phantom{$\lambda v.\,$} 
+        case \bl{$v = Right(v')$}: 
+      & return \bl{$Right(Right(v'))$}\\ 
+\end{tabular}
+\end{center}}%
+
+\only<6->{%
+\begin{center}
+\begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
+\bl{$\textit{mkeps}$} simplified case: &
+\bl{$\textit{Right}(\textit{Empty})$}\\
+rectified case: &
+\bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
+\end{tabular}
+\end{center}}%
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{Records}
 
@@ -315,39 +377,6 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-
-\begin{itemize}
-\item Regular expression for email addresses
-
-\begin{center}
-\begin{tabular}{l}
-(name: \bl{$[a\mbox{-}z0\mbox{-}9\_\!\_\,.-]^+$})\bl{$\cdot @\cdot$}\\ 
-\qquad(domain: \bl{$[a\mbox{-}z0\mbox{-}9\,.-]^+$}) \bl{$\cdot .\cdot$}\\ 
-\qquad\qquad(top\_level: \bl{$[a\mbox{-}z\,.]^{\{2,6\}}$})
-\end{tabular}
-\end{center}
-
-\bl{\[
-\texttt{christian.urban@kcl.ac.uk}
-\]}
-
-\item result environment:
-
-\begin{center}
-\begin{tabular}{l}
-\bl{$[(name:\texttt{christian.urban}),$}\\ 
-\bl{$\phantom{[}(domain:\texttt{kcl}),$}\\ 
-\bl{$\phantom{[}(top\_level:\texttt{ac.uk})]$}
-\end{tabular}
-\end{center}
-\end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{Coursework}