Binary file hws/hw07.pdf has changed

--- a/hws/hw07.tex	Fri Nov 15 10:29:04 2013 +0000
+++ b/hws/hw07.tex	Sun Nov 17 18:16:20 2013 +0000
@@ -13,11 +13,21 @@
 \section*{Homework 7}
 
 \begin{enumerate}
-\item Suppose the following grammar for positive numbers
+\item Suppose the context-sensitive grammar
 
 \begin{center}
+\begin{tabular}{lcl}
+$S$ & $\rightarrow$ &  $bSAA\;|\; \epsilon$\\
+$A$ & $\rightarrow$ & $a$\\
+$bA$ & $\rightarrow$ & $Ab$\\
+\end{tabular}
+\end{center}
 
-\end{center}
+where $S$ is the starting symbol of the grammar. 
+Give a derivation  of the string $"\!aaabaaabb"$. 
+What can you say about the number of as and bs in the
+strings recognised by this grammar.
+
 
 \item Consider the following grammar 
 
@@ -41,14 +51,27 @@
 \texttt{The trainer trains the student team}
 \end{center}
 
-\item {\bf (Optional)} The task is to match strings where the letters are in alphabetical order---for example, 
-\texttt{abcfjz} would pass, but \texttt{acb} would not. Whitespace should be ignored---for example
-\texttt{ab c d} should pass. The point is to try to get the regular expression as short as possible!
-See:
+\item Transform the grammar
 
 \begin{center}
-\url{http://callumacrae.github.com/regex-tuesday/challenge11.html}
+\begin{tabular}{lcl}
+$A$ & $\rightarrow$ & $0A1 \;|\; BB$\\
+$B$ & $\rightarrow$ & $\epsilon \;|\; 2B$
+\end{tabular}
 \end{center}
+
+\noindent
+into Chomsky normal form.
+
+
+%\item {\bf (Optional)} The task is to match strings where the letters are in alphabetical order---for example, 
+%\texttt{abcfjz} would pass, but \texttt{acb} would not. Whitespace should be ignored---for example
+%\texttt{ab c d} should pass. The point is to try to get the regular expression as short as possible!
+%See:
+
+%\begin{center}
+%\url{http://callumacrae.github.com/regex-tuesday/challenge11.html}
+%\end{center}
 \end{enumerate}
 
 \end{document}

--- a/progs/Matcher2.thy	Fri Nov 15 10:29:04 2013 +0000
+++ b/progs/Matcher2.thy	Sun Nov 17 18:16:20 2013 +0000
@@ -52,6 +52,7 @@
 
 lemma seq_union:
   shows "A ;; (B \<union> C) = A ;; B \<union> A ;; C"
+  and   "(B \<union> C) ;; A = B ;; A \<union> C ;; A"
 by (auto simp add: Seq_def)
 
 lemma seq_Union:
@@ -62,6 +63,30 @@
   "[] \<in> A ;; B \<longleftrightarrow> ([] \<in> A \<and> [] \<in> B)"
 by (simp add: Seq_def)
 
+lemma seq_assoc: 
+  shows "A ;; (B ;; C) = (A ;; B) ;; C" 
+apply(auto simp add: Seq_def)
+apply(metis append_assoc)
+apply(metis)
+done
+
+
+section {* Power for Sets *}
+
+fun 
+  pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101)
+where
+   "A \<up> 0 = {[]}"
+|  "A \<up> (Suc n) = A ;; (A \<up> n)"
+
+lemma pow_empty [simp]:
+  shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"
+by (induct n) (auto)
+
+lemma pow_plus:
+  "A \<up> (n + m) = A \<up> n ;; A \<up> m"
+by (induct n) (simp_all add: seq_assoc)
+
 section {* Kleene Star for Sets *}
 
 inductive_set
@@ -71,33 +96,43 @@
   start[intro]: "[] \<in> A\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
 
-
 text {* A Standard Property of Star *}
 
-lemma star_cases:
-  shows "A\<star> = {[]} \<union> A ;; A\<star>"
-unfolding Seq_def
-by (auto) (metis Star.simps)
-
 lemma star_decomp: 
   assumes a: "c # x \<in> A\<star>" 
   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
+using a 
 using a
 by (induct x\<equiv>"c # x" rule: Star.induct) 
    (auto simp add: append_eq_Cons_conv)
 
-section {* Power for Sets *}
+lemma star_cases:
+  shows "A\<star> = {[]} \<union> A ;; A\<star>"
+unfolding Seq_def 
+by (auto) (metis Star.simps)
 
-fun 
-  pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101)
-where
-   "A \<up> 0 = {[]}"
-|  "A \<up> (Suc n) = A ;; (A \<up> n)"
+lemma Star_in_Pow:
+  assumes a: "s \<in> A\<star>"
+  shows "\<exists>n. s \<in> A \<up> n"
+using a
+apply(induct)
+apply(auto)
+apply(rule_tac x="Suc n" in exI)
+apply(auto simp add: Seq_def)
+done
+
+lemma Pow_in_Star:
+  assumes a: "s \<in> A \<up> n"
+  shows "s \<in> A\<star>"
+using a
+by (induct n arbitrary: s) (auto simp add: Seq_def)
 
 
-lemma pow_empty [simp]:
-  shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"
-by (induct n) (auto)
+lemma Star_def2: 
+  shows "A\<star> = (\<Union>n. A \<up> n)"
+using Star_in_Pow Pow_in_Star
+by (auto)
+
 
 
 section {* Semantics of Regular Expressions *}
@@ -265,4 +300,39 @@
    (simp_all add: nullable_correctness der_correctness Der_def)
 
 
+
+
+lemma bb: "A \<up> n ;; A\<star> \<subseteq> A\<star>"
+apply(induct n)
+apply(simp)
+apply(simp)
+apply(subst aa[symmetric])
+apply(subst Seq_def)
+apply(auto)
+done
+
+lemma cc: "(\<Union>i\<in>{..n}. A \<up> i) ;; A\<star> \<subseteq> A\<star>"
+apply(induct n)
+apply(simp)
+apply(simp add: Suc_Union del: pow.simps)
+apply(simp only: seq_union)
+apply(rule Un_least)
+defer
+apply(simp)
+apply(rule bb)
+done
+
+lemma "A\<star> ;; A\<star> = A\<star>"
+apply(simp add: Seq_def)
+apply(rule subset_antisym)
+defer
+apply(auto)[1]
+apply(auto simp add: Star_def2)
+
+apply(subst (asm) Star_def2)
+apply(subst (asm) Star_def2)
+apply(auto)
+
+
+
 end    
\ No newline at end of file