# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1760859844 -7200
# Node ID 31e011ce66e32bde7c95e3c969e3bfcedb5f013a
# Parent  ae9ffbf979ffd374a8a862493a305bec239b67f1
updated

diff -r ae9ffbf979ff -r 31e011ce66e3 progs/Matcher2.thy
--- a/progs/Matcher2.thy	Fri Oct 17 11:20:49 2025 +0100
+++ b/progs/Matcher2.thy	Sun Oct 19 09:44:04 2025 +0200
@@ -2,30 +2,24 @@
   imports "Main" 
 begin
 
-lemma Suc_Union:
-  "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))"
-by (metis UN_insert atMost_Suc)
-
-lemma Suc_reduce_Union:
-  "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"
-by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)
 
 
 section \<open>Regular Expressions\<close>
 
 datatype rexp =
-  NULL
-| EMPTY
+  ZERO
+| ONE
 | CH char
 | SEQ rexp rexp
 | ALT rexp rexp
 | STAR rexp
+
 | NOT rexp
 | PLUS rexp
 | OPT rexp
 | NTIMES rexp nat
-| NMTIMES rexp nat nat
-| UPNTIMES rexp nat
+| BETWEEN rexp nat nat
+| UPTO rexp nat
 
 
 section \<open>Sequential Composition of Sets\<close>
@@ -136,8 +130,8 @@
 fun
   L :: "rexp \<Rightarrow> string set"
 where
-  "L (NULL) = {}"
-| "L (EMPTY) = {[]}"
+  "L (ZERO) = {}"
+| "L (ONE) = {[]}"
 | "L (CH c) = {[c]}"
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
@@ -146,10 +140,10 @@
 | "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..m} . ((L r) \<up> i))" 
-| "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"
+| "L (BETWEEN r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
+| "L (UPTO r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"
 
-lemma "L (NOT NULL) = UNIV"
+lemma "L (NOT ZERO) = UNIV"
 apply(simp)
 done
 
@@ -158,8 +152,8 @@
 fun
  nullable :: "rexp \<Rightarrow> bool"
 where
-  "nullable (NULL) = False"
-| "nullable (EMPTY) = True"
+  "nullable (ZERO) = False"
+| "nullable (ONE) = True"
 | "nullable (CH c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
@@ -168,41 +162,27 @@
 | "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 m < n then False else (if n = 0 then True else nullable r))"
-| "nullable (UPNTIMES r n) = True"
+| "nullable (BETWEEN r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
+| "nullable (UPTO r n) = True"
 
-fun M :: "rexp \<Rightarrow> nat"
-where
-  "M (NULL) = 0"
-| "M (EMPTY) = 0"
-| "M (CH 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)"
-| "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
 fun der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
-  "der c (NULL) = NULL"
-| "der c (EMPTY) = NULL"
-| "der c (CH d) = (if c = d then EMPTY else NULL)"
+  "der c (ZERO) = ZERO"
+| "der c (ONE) = ZERO"
+| "der c (CH d) = (if c = d then ONE else ZERO)"
 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
-| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
+| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else ZERO)"
 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 | "der c (NOT r) = NOT(der c r)"
 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 | "der c (OPT r) = der c r"
-| "der c (NTIMES r n) = (if n = 0 then NULL else (SEQ (der c r) (NTIMES r (n - 1))))"
-| "der c (NMTIMES r n m) = 
-        (if m = 0 then NULL else 
-        (if n = 0 then SEQ (der c r) (UPNTIMES r (m - 1))
-         else SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))"
-| "der c (UPNTIMES r n) = (if n = 0 then NULL else SEQ (der c r) (UPNTIMES r (n - 1)))"
+| "der c (NTIMES r n) = (if n = 0 then ZERO else (SEQ (der c r) (NTIMES r (n - 1))))"
+| "der c (BETWEEN r n m) = 
+        (if m = 0 then ZERO else 
+        (if n = 0 then SEQ (der c r) (UPTO r (m - 1))
+         else SEQ (der c r) (BETWEEN r (n - 1) (m - 1))))"
+| "der c (UPTO r n) = (if n = 0 then ZERO else SEQ (der c r) (UPTO r (n - 1)))"
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -287,6 +267,7 @@
   apply blast
   by force
 
+
 lemma Der_ntimes [simp]:
   shows "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
 proof -    
@@ -311,6 +292,14 @@
 unfolding Der_def 
 by(auto simp add: Cons_eq_append_conv Seq_def)
 
+lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs \<in> A \<Longrightarrow> xs \<in> A ;; B"
+  using Matcher2.Seq_def by auto
+
+lemma Der_pow2:
+  shows "Der c (A \<up> n) = (if n = 0 then {} else (Der c A) ;; (A \<up> (n - 1)))"
+  apply(induct n arbitrary: A)
+  using Der_ntimes by auto
+
 
 lemma Der_UNION [simp]: 
   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
@@ -324,10 +313,10 @@
 lemma der_correctness:
   shows "L (der c r) = Der c (L r)"
 proof(induct r)
-  case NULL
+  case ZERO
   then show ?case by simp
 next
-  case EMPTY
+  case ONE
   then show ?case by simp
 next
   case (CH x)
@@ -359,99 +348,34 @@
     using Der_ntimes Matcher2.Seq_def less_iff_Suc_add apply fastforce
     using Der_ntimes Matcher2.Seq_def less_iff_Suc_add by auto
 next
-  case (NMTIMES r n m)
+  case (BETWEEN r n m)
   then show ?case 
     apply(auto simp add: Seq_def)
-    sledgeham mer[timeout=1000]
-    apply(case_tac n)
-    sorry
+    apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_pred atLeast0AtMost atMost_iff diff_Suc_Suc
+        diff_is_0_eq mem_Collect_eq)
+      apply(subst (asm) Der_pow2)
+      apply(case_tac xa)
+       apply(simp)
+      apply(auto simp add: Seq_def)[1]
+    apply (metis atMost_iff diff_Suc_1' diff_le_mono)
+    apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atLeastAtMost_iff
+        mem_Collect_eq)
+    apply(subst (asm) Der_pow2)
+      apply(case_tac xa)
+       apply(simp)
+    apply(auto simp add: Seq_def)[1]
+    by force
 next
-  case (UPNTIMES r x2)
+  case (UPTO r x2)
   then show ?case 
     apply(auto simp add: Seq_def)
     apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atMost_iff
         mem_Collect_eq)
-sledgehammer[timeout=1000]
-    sorry
-qed
-
-
-
-
-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(rule impI)+
-apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
-apply(auto simp add: Seq_def)
-done
-
-lemma L_der_NTIMES:
-  shows "L(der c (NTIMES r n)) = L (if n = 0 then NULL else if nullable r then 
-         SEQ (der c r) (UPNTIMES r (n - 1)) else SEQ (der c r) (NTIMES r (n - 1)))"
-apply(induct n)
-apply(simp)
-apply(simp)
-apply(auto)
-apply(auto simp add: Seq_def)
-apply(rule_tac x="s1" in exI)
-apply(simp)
-apply(rule_tac x="xa" in bexI)
-apply(simp)
-apply(simp)
-apply(rule_tac x="s1" in exI)
-apply(simp)
-by (metis Suc_pred atMost_iff le_Suc_eq)
-
-lemma "L(der c (UPNTIMES r 0)) = {}"
-by simp
-
-lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
-proof(induct n)
-  case 0 show ?case by simp
-next
-  case (Suc n)
-  have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact
-  { assume a: "nullable r"
-    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
-    by (simp only: der_correctness)
-    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
-    by(simp only: L.simps Suc_Union)
-    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
-    by (simp only: der_correctness)
-    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
-    by(auto simp add: Seq_def)
-    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
-    using IH by simp
-    also have "... = L (SEQ (der c r) (UPNTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
-    using a unfolding L_der_NTIMES by simp
-    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
-    by (auto, metis Suc_Union Un_iff seq_Union)
-    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
-    } 
-  moreover
-  { assume a: "\<not>nullable r"
-    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
-    by (simp only: der_correctness)
-    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
-    by(simp only: L.simps Suc_Union)
-    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
-    by (simp only: der_correctness)
-    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
-    by(auto simp add: Seq_def)
-    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
-    using IH by simp
-    also have "... = L (SEQ (der c r) (NTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
-    using a unfolding L_der_NTIMES by simp
-    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
-    by (simp add: Suc_Union seq_union(1))
-    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
-  }
-  ultimately  
-  show "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))"
-  by blast
+    apply(subst (asm) Der_pow2)
+    apply(case_tac xa)
+     apply(simp)
+    apply(auto simp add: Seq_def)
+    by (metis atMost_iff diff_Suc_1' diff_le_mono)
 qed
 
 lemma matcher_correctness:
diff -r ae9ffbf979ff -r 31e011ce66e3 progs/lexer/lex.sc
--- a/progs/lexer/lex.sc	Fri Oct 17 11:20:49 2025 +0100
+++ b/progs/lexer/lex.sc	Sun Oct 19 09:44:04 2025 +0200
@@ -51,9 +51,6 @@
   def ~ (s: Rexp) = SEQ(r, s)
 }
 
-// to use & for records, instead of $ which had
-// its precedence be changed in Scala 3
-
 val TEST = ("ab" | "ba").%
 
 def nullable(r: Rexp) : Boolean = r match {
@@ -148,18 +145,6 @@
 
 println(lex(STAR(STAR("a")), "aaa".toList))
 
-val re = ("a" | "ab") ~ ("c" | "bc")
-
-println(pders1("abc", re).toList.mkString("\n"))
-pders('a', pder('a', re))))
-draw(simp(der('a', der('a', der('a', re)))))
-
-size(simp(ders(, re)))
-size(simp(der('a', der('a', re))))
-size(simp(der('a', der('a', der('a', re)))))
-
-
-lex(re, "aaaaa".toList)
 
 // The Lexing Rules for the WHILE Language
 
@@ -190,21 +175,22 @@
 }
 import TAGS._
 
+
 extension (t: TAGS) {
-  def & (r: Rexp) = RECD[TAGS](t, r)
+  def $ (r: Rexp) = RECD[TAGS](t, r)
 }
 
 def lexing(r: Rexp, s: String) = 
   env[TAGS](lex(r, s.toList))
 
-val WHILE_REGS = ((Key & KEYWORD) | 
-                  (Id & ID) | 
-                  (Op & OP) | 
-                  (Num & NUM) | 
-                  (Semi & SEMI) | 
-                  (Str & STRING) |
-                  (Paren & (LPAREN | RPAREN)) | 
-                  (Wht & WHITESPACE)).%
+val WHILE_REGS = ((Key $ KEYWORD) | 
+                  (Id $ ID) | 
+                  (Op $ OP) | 
+                  (Num $ NUM) | 
+                  (Semi $ SEMI) | 
+                  (Str $ STRING) |
+                  (Paren $ (LPAREN | RPAREN)) | 
+                  (Wht $ WHITESPACE)).%
 
 
 // Two Simple While Tests
diff -r ae9ffbf979ff -r 31e011ce66e3 progs/lexer/lexer.sc
--- a/progs/lexer/lexer.sc	Fri Oct 17 11:20:49 2025 +0100
+++ b/progs/lexer/lexer.sc	Sun Oct 19 09:44:04 2025 +0200
@@ -329,12 +329,6 @@
 
 
 /*
-// Ammonite still provides 
-//
-//    scala.reflect.runtime.universe._
-//
-// which has been removed in Scala 3.
-//
 // for escaping strings in Scala 3 use this equivalent code
 
 import scala.quoted._
diff -r ae9ffbf979ff -r 31e011ce66e3 slides/slides03.pdf
Binary file slides/slides03.pdf has changed
diff -r ae9ffbf979ff -r 31e011ce66e3 slides/slides03.tex
--- a/slides/slides03.tex	Fri Oct 17 11:20:49 2025 +0100
+++ b/slides/slides03.tex	Sun Oct 19 09:44:04 2025 +0200
@@ -67,6 +67,7 @@
 
 
 
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 
@@ -227,6 +228,22 @@
 %\end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Coursework}
+
+\begin{itemize}
+\item CW1 : Week 2
+\item CW2 : Week 4
+\item CW3 : Week 5 + 6
+\item CW4 : Week 7 + 8
+\item CW5 : Week 10
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
 
 
 {