--- a/progs/Matcher2.thy	Fri Oct 23 00:16:00 2015 +0100
+++ b/progs/Matcher2.thy	Fri Oct 23 08:35:17 2015 +0100
@@ -24,9 +24,8 @@
 | PLUS rexp
 | OPT rexp
 | NTIMES rexp nat
-| NMTIMES rexp nat nat
 | NMTIMES2 rexp nat nat
-
+(*
 fun M :: "rexp \<Rightarrow> nat"
 where
   "M (NULL) = 0"
@@ -39,9 +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 (NMTIMES r n m) = Suc (M r) * 2 * (Suc n + Suc m)"
-| "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc n + Suc m)"
-
+| "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc m - Suc n)"
+*)
 section {* Sequential Composition of Sets *}
 
 definition
@@ -161,7 +159,6 @@
 | "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..n+m} . ((L r) \<up> i))" 
 | "L (NMTIMES2 r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
 
 
@@ -169,56 +166,6 @@
 apply(simp)
 done
 
-lemma "L (NMTIMES r (Suc n) m) = L (SEQ r (NMTIMES r n m))"
-apply(simp add:  Suc_reduce_Union Seq_def)
-apply(auto)
-done
-
-lemma "L (NMTIMES2 r (Suc n) (Suc m)) = L (SEQ r (NMTIMES2 r n m))"
-apply(simp add:  Suc_reduce_Union Seq_def)
-apply(auto)
-done
-
-lemma "L (NMTIMES2 r 0 0) = {[]}"
-apply(simp add: Suc_reduce_Union Seq_def)
-done
-
-lemma t: "\<lbrakk>n \<le> i; i \<le> m\<rbrakk> \<Longrightarrow> L (NMTIMES2 r n m) = L (NMTIMES2 r n i) \<union> L (NMTIMES2 r i m)"
-apply(auto)
-apply (metis atLeastAtMost_iff nat_le_linear)
-apply (metis atLeastAtMost_iff le_trans)
-by (metis atLeastAtMost_iff le_trans)
-
-
-lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \<union> L (NMTIMES2 r 1 (Suc m))"
-apply(rule t)
-apply(auto)
-done
-
-lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \<union> L (NMTIMES2 r 1 (Suc m))"
-apply(rule t)
-apply(auto)
-done
-
-lemma "L (NMTIMES2 r 0 1) = {[]} \<union> L r"
-apply(simp)
-apply(auto)
-apply(case_tac xa)
-apply(auto)
-done
-
-
-lemma "L (NMTIMES2 r n n) = L (NTIMES r n)"
-apply(simp)
-done
-
-lemma "n < m \<Longrightarrow> L (NMTIMES2 r n m) = L (NTIMES r n) \<union> L (NMTIMES2 r (Suc n) m)"
-apply(simp)
-apply(auto)
-apply (metis Suc_leI atLeastAtMost_iff le_eq_less_or_eq)
-apply (metis atLeastAtMost_iff le_eq_less_or_eq)
-by (metis Suc_leD atLeastAtMost_iff)
-
 section {* The Matcher *}
 
 fun
@@ -234,11 +181,23 @@
 | "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 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))"
 
-function
- der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
+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))"
+
+function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
   "der c (NULL) = NULL"
 | "der c (EMPTY) = NULL"
@@ -251,17 +210,16 @@
 | "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 (NMTIMES r 0 0) = NULL"
-| "der c (NMTIMES r 0 (Suc m)) = ALT (der c (NTIMES r (Suc m))) (der c (NMTIMES r 0 m))"
-| "der c (NMTIMES r (Suc n) m) = der c  (SEQ r (NMTIMES r n m))"
 | "der c (NMTIMES2 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))))"
 by pat_completeness auto
 
 termination der 
+apply(relation "measure (\<lambda>(c, r). M r)") 
+apply(simp_all)
 sorry
-(*by (relation "measure (\<lambda>(c, r). M r)") (simp_all)*)
+
 
 
 fun