--- a/progs/Matcher2.thy	Sun Oct 12 12:50:16 2025 +0100
+++ b/progs/Matcher2.thy	Fri Oct 17 11:20:49 2025 +0100
@@ -186,7 +186,7 @@
 | "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"
+fun der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
   "der c (NULL) = NULL"
 | "der c (EMPTY) = NULL"
@@ -197,70 +197,12 @@
 | "der c (NOT r) = NOT(der c r)"
 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 | "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 (NTIMES r n) = (if n = 0 then NULL else (SEQ (der c r) (NTIMES r (n - 1))))"
 | "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 (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:
-  "\<lbrakk>c < (d::nat); a < b; 0 < a; 0 < c\<rbrakk> \<Longrightarrow> c * a < d * b"
-by (metis le0 mult_strict_mono')
-
-termination der 
-apply(relation "measure (\<lambda>(c, r). M r)") 
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-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
-apply(auto)[1]
-apply(subgoal_tac "Suc n < Suc m")
-prefer 2
-apply(auto)[1]
-apply(subgoal_tac "Suc (M r) * 2 * Suc n < Suc (Suc (M r)) * 2 * Suc m")
-prefer 2
-apply(subgoal_tac "Suc (M r) * 2 < Suc (Suc (M r)) * 2")
-prefer 2
-apply(auto)[1]
-apply(rule bigger1)
-apply(assumption)
-apply(simp)
-apply (metis zero_less_Suc)
-apply (metis mult_is_0 neq0_conv old.nat.distinct(2))
-apply(rotate_tac 4)
-apply(drule_tac a="1" and b="(Suc (Suc m) - Suc n)" in bigger1)
-prefer 4
-apply(simp)
-apply(simp)
-apply (metis zero_less_one)
-apply(simp)
-done
-*)
-sorry
+        (if m = 0 then NULL else 
+        (if n = 0 then SEQ (der c r) (UPNTIMES r (m - 1))
+         else SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))"
+| "der c (UPNTIMES r n) = (if n = 0 then NULL else SEQ (der c r) (UPNTIMES r (n - 1)))"
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -369,6 +311,7 @@
 unfolding Der_def 
 by(auto simp add: Cons_eq_append_conv Seq_def)
 
+
 lemma Der_UNION [simp]: 
   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
   by (auto simp add: Der_def)
@@ -412,22 +355,24 @@
 next
   case (NTIMES r n)
   then show ?case
-    apply(induct n)
-     apply(simp)
-    apply(simp only: L.simps)
-    apply(simp only: Der_pow)
-    apply(simp only: der.simps L.simps)
-    apply(simp only: nullable_correctness)
-    apply(simp only: if_f)
-    by simp
+    apply(auto simp add: Seq_def)
+    using Der_ntimes Matcher2.Seq_def less_iff_Suc_add apply fastforce
+    using Der_ntimes Matcher2.Seq_def less_iff_Suc_add by auto
 next
   case (NMTIMES r n m)
   then show ?case 
+    apply(auto simp add: Seq_def)
+    sledgeham mer[timeout=1000]
     apply(case_tac n)
     sorry
 next
   case (UPNTIMES r x2)
-  then show ?case sorry
+  then show ?case 
+    apply(auto simp add: Seq_def)
+    apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atMost_iff
+        mem_Collect_eq)
+sledgehammer[timeout=1000]
+    sorry
 qed