--- a/progs/Matcher2.thy	Tue Oct 18 11:13:37 2016 +0100
+++ b/progs/Matcher2.thy	Tue Oct 18 19:14:33 2016 +0100
@@ -25,6 +25,7 @@
 | OPT rexp
 | NTIMES rexp nat
 | NMTIMES rexp nat nat
+| UPNTIMES rexp nat
 
 
 section {* Sequential Composition of Sets *}
@@ -147,7 +148,7 @@
 | "L (OPT r) = (L r) \<union> {[]}"
 | "L (NTIMES r n) = (L r) \<up> n"
 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
-
+| "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"
 
 lemma "L (NOT NULL) = UNIV"
 apply(simp)
@@ -169,6 +170,7 @@
 | "nullable (OPT r) = True"
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
+| "nullable (UPNTIMES r n) = True"
 
 fun M :: "rexp \<Rightarrow> nat"
 where
@@ -183,7 +185,7 @@
 | "M (OPT r) = Suc (M r)"
 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
 | "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
-
+| "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
@@ -202,6 +204,8 @@
         (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))))"
+| "der c (UPNTIMES r 0) = NULL"
+| "der c (UPNTIMES r (Suc n)) = der c (ALT (NTIMES r (Suc n)) (UPNTIMES r n))"
 by pat_completeness auto
 
 lemma bigger1:
@@ -224,9 +228,12 @@
 apply(simp_all del: M.simps)
 apply(simp_all only: M.simps)
 defer
+defer
+defer
 apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
 prefer 2
 apply(auto)[1]
+(*
 apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
 apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
 prefer 2
@@ -252,6 +259,8 @@
 apply (metis zero_less_one)
 apply(simp)
 done
+*)
+sorry
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -346,8 +355,73 @@
     Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
 apply(rule impI)+
 apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
+apply(auto simp add: Seq_def)
+done
+
+lemma L_der_NTIMES:
+  shows "L(der c (NTIMES r n)) = (if n = 0 then {} else if nullable r then 
+       L(SEQ (der c r) (UPNTIMES r (n - 1)))
+       else L(SEQ (der c r) (NTIMES r (n - 1))))"
+apply(induct n)
+apply(simp)
+apply(simp)
 apply(auto)
-done
+apply(auto simp add: Seq_def)
+apply(rule_tac x="s1" in exI)
+apply(simp)
+apply(rule_tac x="xa" in bexI)
+apply(simp)
+apply(simp)
+apply(rule_tac x="s1" in exI)
+apply(simp)
+by (metis Suc_pred atMost_iff le_Suc_eq)
+
+lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
+using assms
+proof(induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact
+  { assume a: "nullable r"
+    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
+    by (simp only: der_correctness)
+    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
+    by(simp only: L.simps Suc_Union)
+    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
+    by (simp only: der_correctness)
+    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
+    by(auto simp add: Seq_def)
+    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
+    using IH by simp
+    also have "... = L (SEQ (der c r) (UPNTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
+    using a unfolding L_der_NTIMES by simp
+    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
+    by (auto, metis Suc_Union Un_iff seq_Union)
+    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
+    } 
+  moreover
+  { assume a: "\<not>nullable r"
+    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
+    by (simp only: der_correctness)
+    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
+    by(simp only: L.simps Suc_Union)
+    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
+    by (simp only: der_correctness)
+    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
+    by(auto simp add: Seq_def)
+    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
+    using IH by simp
+    also have "... = L (SEQ (der c r) (NTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
+    using a unfolding L_der_NTIMES by simp
+    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
+    by (simp add: Suc_Union seq_union(1))
+    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
+  }
+  ultimately  
+  show "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))"
+  by blast
+qed
 
 lemma matcher_correctness:
   shows "matcher r s \<longleftrightarrow> s \<in> L r"