# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1456178971 0
# Node ID cf3ca219c727948b139723839c312af1217de1e4
# Parent  4cd75c619e06838072aac04266c9ca62bc21bbdf
updated

diff -r 4cd75c619e06 -r cf3ca219c727 handouts/scala-ho.pdf
Binary file handouts/scala-ho.pdf has changed
diff -r 4cd75c619e06 -r cf3ca219c727 handouts/scala-ho.tex
--- a/handouts/scala-ho.tex	Tue Jan 12 02:49:26 2016 +0000
+++ b/handouts/scala-ho.tex	Mon Feb 22 22:09:31 2016 +0000
@@ -932,11 +932,17 @@
 \item \url{http://www.scala-lang.org/docu/files/ScalaByExample.pdf}
 \item \url{http://www.scala-lang.org/docu/files/ScalaTutorial.pdf}
 \item \url{https://www.youtube.com/user/ShadowofCatron}
+\item \url{http://docs.scala-lang.org/tutorials}
 \end{itemize}
 
 \noindent There is also a course at Coursera on Functional
 Programming Principles in Scala by Martin Odersky, the main
-developer of the Scala language.
+developer of the Scala language. And a document that explains
+Scala for Java programmers
+
+\begin{itemize}
+\item \small\url{http://docs.scala-lang.org/tutorials/scala-for-java-programmers.html}
+\end{itemize}
 
 While I am quite enthusiastic about Scala, I am also happy to
 admit that it has more than its fair share of faults. The
diff -r 4cd75c619e06 -r cf3ca219c727 progs/Matcher2.thy
--- a/progs/Matcher2.thy	Tue Jan 12 02:49:26 2016 +0000
+++ b/progs/Matcher2.thy	Mon Feb 22 22:09:31 2016 +0000
@@ -1,4 +1,4 @@
-ytheory Matcher2
+theory Matcher2
   imports "Main" 
 begin
 
@@ -26,19 +26,6 @@
 | NTIMES rexp nat
 | NMTIMES rexp nat nat
 
-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 (NMTIMES r n m) = Suc (M r) * 2 * (Suc m - Suc n)"
 
 section {* Sequential Composition of Sets *}
 
@@ -183,6 +170,21 @@
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
+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 (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
+
+
 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
   "der c (NULL) = NULL"
@@ -197,23 +199,59 @@
 | "der c (NTIMES r 0) = NULL"
 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
 | "der c (NMTIMES r n m) = 
-     (if m < n then NULL else 
-     (if m = 0 then NULL else
-     (der c (SEQ r (NMTIMES r (n - 1) (m - 1))))))"
-(*
+        (if m < n then NULL else 
+        (if n = m then der c (NTIMES r n) else
+                       ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
+by pat_completeness auto
 
-  (if m < n then NULL else 
-                              (if n = m then der c (NTIMES r n) else
-                                ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
-*)
-by pat_completeness auto
+lemma bigger1:
+  "\<lbrakk>c < (d::nat); a < b; 0 < a; 0 < c\<rbrakk> \<Longrightarrow> c * a < d * b"
+by (metis le0 mult_strict_mono')
 
 termination der 
 apply(relation "measure (\<lambda>(c, r). M r)") 
-apply(simp_all)
-sorry
-
-
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp_all del: M.simps)
+apply(simp_all only: M.simps)
+defer
+apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
+prefer 2
+apply(auto)[1]
+apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
+apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
+prefer 2
+apply(auto)[1]
+apply(subgoal_tac "Suc n < Suc m")
+prefer 2
+apply(auto)[1]
+apply(subgoal_tac "Suc (M r) * 2 * Suc n < Suc (Suc (M r)) * 2 * Suc m")
+prefer 2
+apply(subgoal_tac "Suc (M r) * 2 < Suc (Suc (M r)) * 2")
+prefer 2
+apply(auto)[1]
+apply(rule bigger1)
+apply(assumption)
+apply(simp)
+apply (metis zero_less_Suc)
+apply (metis mult_is_0 neq0_conv old.nat.distinct(2))
+apply(rotate_tac 4)
+apply(drule_tac a="1" and b="(Suc (Suc m) - Suc n)" in bigger1)
+prefer 4
+apply(simp)
+apply(simp)
+apply (metis zero_less_one)
+apply(simp)
+done
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -306,122 +344,14 @@
 apply(induct rule: der.induct) 
 apply(simp_all add: nullable_correctness 
     Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
-apply(case_tac "[] \<in> L r")
-apply(simp)
-apply(case_tac n)
-apply(auto)[1]
-apply(case_tac m)
-apply(simp)
-apply(auto simp add: )[1]
-apply (metis (full_types, hide_lams) Der_pow Der_seq Suc_le_mono UnCI atLeast0AtMost atMost_iff not_less_eq_eq)
-
-apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl)
-apply (metis Suc_leD atLeastAtMost_iff)
-by (metis atLeastAtMost_iff le_antisym not_less_eq_eq)
-
-(*
-lemma der_correctness:
-  shows "L (der c r) = Der c (L r)"
-apply(induct rule: der.induct) 
-apply(simp_all add: nullable_correctness 
-    Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
-apply(case_tac m)
-apply(simp)
-apply(simp)
+apply(rule impI)+
+apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
 apply(auto)
-apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl)
-apply (metis Suc_leD atLeastAtMost_iff)
-by (metis atLeastAtMost_iff le_antisym not_less_eq_eq)
-*)
+done
 
 lemma matcher_correctness:
   shows "matcher r s \<longleftrightarrow> s \<in> L r"
 by (induct s arbitrary: r)
    (simp_all add: nullable_correctness der_correctness Der_def)
 
-
-lemma "L (der c (NMTIMES r n m)) = 
-  L ((if m < n then NULL else 
-     (if m = 0 then NULL else
-     (der c (SEQ r (NMTIMES r (n - 1) (m - 1)))))))"
-apply(subst der.simps(12))
-apply(auto simp del: der.simps)
-apply(simp)
-apply(auto)[1]
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(subst (asm) der.simps(12))
-apply(auto)[1]
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(auto simp del: der.simps(12))[1]
-apply(subst (asm) der.simps(12))
-apply(case_tac n)
-apply(simp)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(case_tac "Suc nat = nata")
-apply(simp)
-apply(auto simp del: der.simps(12))[1]
-apply(auto)[1]
-apply(case_tac n)
-apply(simp)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(simp add: Seq_def)
-apply(auto)[1]
-apply (metis atLeastAtMost_iff le_eq_less_or_eq linorder_neqE_nat)
-apply(simp (no_asm) del: der.simps(12))
-apply(auto simp del: der.simps(12))[1]
-apply(case_tac "m = Suc n")
-apply(simp)
-apply(case_tac n)
-apply(simp)
-apply(simp)
-apply(auto simp add: Seq_def del: der.simps(12))[1]
-
-apply(case_tac n)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(simp add: Seq_def)
-apply(auto)[1]
-apply(case_tac "nat = 0")
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(case_tac "Suc 0 = nat")
-apply(simp)
-apply(auto simp del: der.simps(12))[1]
-apply(simp)
-apply(case_tac "Suc 0 = nat")
-apply(simp)
-apply(auto simp add: Seq_def del: der.simps(12))[1]
-apply(rule_tac x="s1" in exI)
-apply(rule_tac x="s2" in exI)
-apply(simp)
-apply(rule_tac x="1" in bexI)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(auto simp add: Seq_def)[1]
-apply(case_tac m)
-apply(simp)
-apply(simp)
-
 end    
\ No newline at end of file
diff -r 4cd75c619e06 -r cf3ca219c727 progs/pow.scala
--- a/progs/pow.scala	Tue Jan 12 02:49:26 2016 +0000
+++ b/progs/pow.scala	Mon Feb 22 22:09:31 2016 +0000
@@ -12,6 +12,9 @@
 val B = Set("a", "b", "c", "")
 pow(B, 4).size                            // -> 121
 
+val B2 = Set("a", "b", "c", "")
+pow(B2, 3).size                           // -> 40
+
 val C = Set("a", "b", "")
 pow(C, 2)
 pow(C, 2).size                            // -> 7