--- a/progs/Matcher2.thy	Fri Oct 23 14:45:57 2015 +0100
+++ b/progs/Matcher2.thy	Sat Oct 31 11:16:52 2015 +0000
@@ -196,9 +196,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 n m) = (if m < n then NULL else 
+| "der c (NMTIMES r n m) = 
+     (if m < n then NULL else 
+     (if m = 0 then NULL else
+     (der c (SEQ r (NMTIMES r (n - 1) (m - 1))))))"
+(*
+
+  (if m < n then NULL else 
                               (if n = m then der c (NTIMES r n) else
                                 ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
+*)
 by pat_completeness auto
 
 termination der 
@@ -294,8 +301,25 @@
   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
 by (auto simp add: Der_def)
 
+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(case_tac "[] \<in> L r")
+apply(simp)
+apply(case_tac n)
+apply(auto)[1]
+apply(case_tac m)
+apply(simp)
+apply(auto simp add: )[1]
+apply (metis (full_types, hide_lams) Der_pow Der_seq Suc_le_mono UnCI atLeast0AtMost atMost_iff not_less_eq_eq)
 
+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 der_correctness:
   shows "L (der c r) = Der c (L r)"
 apply(induct rule: der.induct) 
@@ -308,7 +332,7 @@
 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:
   shows "matcher r s \<longleftrightarrow> s \<in> L r"
@@ -316,4 +340,88 @@
    (simp_all add: nullable_correctness der_correctness Der_def)
 
 
+lemma "L (der c (NMTIMES r n m)) = 
+  L ((if m < n then NULL else 
+     (if m = 0 then NULL else
+     (der c (SEQ r (NMTIMES r (n - 1) (m - 1)))))))"
+apply(subst der.simps(12))
+apply(auto simp del: der.simps)
+apply(simp)
+apply(auto)[1]
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(subst (asm) der.simps(12))
+apply(auto)[1]
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply(auto simp del: der.simps(12))[1]
+apply(subst (asm) der.simps(12))
+apply(case_tac n)
+apply(simp)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(case_tac "Suc nat = nata")
+apply(simp)
+apply(auto simp del: der.simps(12))[1]
+apply(auto)[1]
+apply(case_tac n)
+apply(simp)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(simp add: Seq_def)
+apply(auto)[1]
+apply (metis atLeastAtMost_iff le_eq_less_or_eq linorder_neqE_nat)
+apply(simp (no_asm) del: der.simps(12))
+apply(auto simp del: der.simps(12))[1]
+apply(case_tac "m = Suc n")
+apply(simp)
+apply(case_tac n)
+apply(simp)
+apply(simp)
+apply(auto simp add: Seq_def del: der.simps(12))[1]
+
+apply(case_tac n)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(simp add: Seq_def)
+apply(auto)[1]
+apply(case_tac "nat = 0")
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply(case_tac "Suc 0 = nat")
+apply(simp)
+apply(auto simp del: der.simps(12))[1]
+apply(simp)
+apply(case_tac "Suc 0 = nat")
+apply(simp)
+apply(auto simp add: Seq_def del: der.simps(12))[1]
+apply(rule_tac x="s1" in exI)
+apply(rule_tac x="s2" in exI)
+apply(simp)
+apply(rule_tac x="1" in bexI)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(auto simp add: Seq_def)[1]
+apply(case_tac m)
+apply(simp)
+apply(simp)
+
 end    
\ No newline at end of file