diff -r 53889239df4a -r fa3e3d00b802 progs/Matcher2.thy
--- a/progs/Matcher2.thy	Sat Nov 08 09:51:49 2025 +0000
+++ b/progs/Matcher2.thy	Thu Nov 13 23:41:39 2025 +0000
@@ -14,6 +14,7 @@
 | ALT rexp rexp
 | STAR rexp
 
+| AND rexp rexp
 | NOT rexp
 | PLUS rexp
 | OPT rexp
@@ -135,6 +136,7 @@
 | "L (CH c) = {[c]}"
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
+| "L (AND r1 r2) = (L r1) \<inter> (L r2)"
 | "L (STAR r) = (L r)\<star>"
 | "L (NOT r) = UNIV - (L r)"
 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
@@ -156,6 +158,7 @@
 | "nullable (ONE) = True"
 | "nullable (CH c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
+| "nullable (AND r1 r2) = (nullable r1 \<and> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 | "nullable (STAR r) = True"
 | "nullable (NOT r) = (\<not>(nullable r))"
@@ -172,6 +175,7 @@
 | "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 (AND r1 r2) = AND (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 ZERO)"
 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 | "der c (NOT r) = NOT(der c r)"
@@ -229,7 +233,12 @@
 lemma Der_union [simp]:
   shows "Der c (A \<union> B) = Der c A \<union> Der c B"
 unfolding Der_def
-by auto
+  by auto
+
+lemma Der_inter [simp]:
+  shows "Der c (A \<inter> B) = Der c A \<inter> Der c B"
+unfolding Der_def
+  by auto
 
 lemma Der_insert_nil [simp]:
   shows "Der c (insert [] A) = Der c A"
@@ -329,6 +338,9 @@
   case (ALT r1 r2)
   then show ?case by simp
 next
+  case (AND r1 r2)
+  then show ?case by(simp)
+next
   case (STAR r)
   then show ?case
     by simp 
@@ -383,4 +395,11 @@
 by (induct s arbitrary: r)
    (simp_all add: nullable_correctness der_correctness Der_def)
 
+
+lemma
+  "L(AND r ZERO) = {}" and
+  "L(AND r r) = L(r)" 
+  by(auto)
+
+
 end    
\ No newline at end of file