--- 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:
--- 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
--- 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._
Binary file slides/slides03.pdf has changed
--- 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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
{