--- a/progs/Matcher2.thy	Fri Oct 23 08:35:17 2015 +0100
+++ b/progs/Matcher2.thy	Fri Oct 23 14:45:57 2015 +0100
@@ -24,8 +24,8 @@
 | PLUS rexp
 | OPT rexp
 | NTIMES rexp nat
-| NMTIMES2 rexp nat nat
-(*
+| NMTIMES rexp nat nat
+
 fun M :: "rexp \<Rightarrow> nat"
 where
   "M (NULL) = 0"
@@ -38,8 +38,8 @@
 | "M (PLUS r) = Suc (M r)"
 | "M (OPT r) = Suc (M r)"
 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
-| "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc m - Suc n)"
-*)
+| "M (NMTIMES r n m) = Suc (M r) * 2 * (Suc m - Suc n)"
+
 section {* Sequential Composition of Sets *}
 
 definition
@@ -159,7 +159,7 @@
 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 | "L (OPT r) = (L r) \<union> {[]}"
 | "L (NTIMES r n) = (L r) \<up> n"
-| "L (NMTIMES2 r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
+| "L (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
 
 
 lemma "L (NOT NULL) = UNIV"
@@ -181,21 +181,7 @@
 | "nullable (PLUS r) = (nullable r)"
 | "nullable (OPT r) = True"
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
-| "nullable (NMTIMES2 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 (NMTIMES2 r n m) = 3 * (Suc (M r) + n) * 3 * (Suc n) * (Suc (Suc m) - (Suc n))"
+| "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
@@ -210,9 +196,9 @@
 | "der c (OPT r) = der c r"
 | "der c (NTIMES r 0) = NULL"
 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
-| "der c (NMTIMES2 r n m) = (if m < n then NULL else 
+| "der c (NMTIMES r n m) = (if m < n then NULL else 
                               (if n = m then der c (NTIMES r n) else
-                                ALT (der c (NTIMES r n)) (der c (NMTIMES2 r (Suc n) m))))"
+                                ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
 by pat_completeness auto
 
 termination der