--- a/progs/Matcher2.thy	Fri Oct 16 14:27:20 2015 +0100
+++ b/progs/Matcher2.thy	Sat Oct 17 11:24:41 2015 +0100
@@ -2,6 +2,15 @@
   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 {* Regular Expressions *}
 
 datatype rexp =
@@ -16,6 +25,7 @@
 | OPT rexp
 | NTIMES rexp nat
 | NMTIMES rexp nat nat
+| NMTIMES2 rexp nat nat
 
 fun M :: "rexp \<Rightarrow> nat"
 where
@@ -30,6 +40,7 @@
 | "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)"
 
 section {* Sequential Composition of Sets *}
 
@@ -151,11 +162,62 @@
 | "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))" 
+
 
 lemma "L (NOT NULL) = UNIV"
 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 *}
 
@@ -173,6 +235,7 @@
 | "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"
@@ -191,10 +254,14 @@
 | "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 
-by (relation "measure (\<lambda>(c, r). M r)") (simp_all)
+sorry
+(*by (relation "measure (\<lambda>(c, r). M r)") (simp_all)*)
 
 
 fun 
@@ -213,8 +280,9 @@
 
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-by(induct r) (auto simp add: Seq_def) 
-
+apply(induct r) 
+apply(auto simp add: Seq_def) 
+done
 
 section {* Left-Quotient of a Set *}
 
@@ -282,20 +350,20 @@
   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
 by (auto simp add: Der_def)
 
-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)
 
 
 lemma der_correctness:
   shows "L (der c r) = Der c (L r)"
-by (induct rule: der.induct) 
-   (simp_all add: nullable_correctness 
+apply(induct rule: der.induct) 
+apply(simp_all add: nullable_correctness 
     Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(auto)
+apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl)
+apply (metis Suc_leD atLeastAtMost_iff)
+by (metis atLeastAtMost_iff le_antisym not_less_eq_eq)
 
 
 lemma matcher_correctness: