--- a/thys/SpecExt.thy	Wed Sep 18 16:35:57 2019 +0100
+++ b/thys/SpecExt.thy	Sat Oct 24 12:13:39 2020 +0100
@@ -163,7 +163,11 @@
 using assms
 apply(induct n arbitrary: s)
 apply(auto simp add: Sequ_def)
-done
+  done
+
+lemma
+  assumes "[] \<in> A" "n \<noteq> 0" "A \<noteq> {}"
+  shows "A \<up> (Suc n) = A \<up> n"
 
 lemma Der_Pow_0:
   shows "Der c (A \<up> 0) = {}"
@@ -225,6 +229,7 @@
 | NTIMES rexp nat
 | FROMNTIMES rexp nat
 | NMTIMES rexp nat nat
+| NOT rexp
 
 section {* Semantics of Regular Expressions *}
  
@@ -241,6 +246,7 @@
 | "L (NTIMES r n) = (L r) \<up> n"
 | "L (FROMNTIMES r n) = (\<Union>i\<in>{n..} . (L r) \<up> i)"
 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" 
+| "L (NOT r) = ((UNIV:: string set)  - L r)"
 
 section {* Nullable, Derivatives *}
 
@@ -257,6 +263,7 @@
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 | "nullable (FROMNTIMES 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 (NOT r) = (\<not> nullable r)"
 
 fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -281,6 +288,7 @@
       else (if n = 0 then (if m = 0 then ZERO else 
                            SEQ (der c r) (UPNTIMES r (m - 1))) else 
                            SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 
+| "der c (NOT r) = NOT (der c r)"
 
 lemma
  "L(der c (UPNTIMES r m))  =
@@ -295,6 +303,26 @@
   apply blast
   oops
 
+
+
+lemma 
+  assumes "der c r = ONE \<or> der c r = ZERO"
+  shows "L (der c (NOT r)) \<noteq> L(if (der c r = ZERO) then ONE else 
+                               if (der c r = ONE) then ZERO
+                               else NOT(der c r))"
+  using assms
+  apply(simp)
+  apply(auto)
+  done
+
+lemma 
+  "L (der c (NOT r)) = L(if (der c r = ZERO) then ONE else 
+                         if (der c r = ONE) then ZERO
+                         else NOT(der c r))"
+  apply(simp)
+  apply(auto)
+  oops
+
 lemma pow_add:
   assumes "s1 \<in> A \<up> n" "s2 \<in> A \<up> m"
   shows "s1 @ s2 \<in> A \<up> (n + m)"
@@ -344,6 +372,16 @@
   apply(auto simp add: Sequ_def)
   using SpecExt.Pow_empty by blast 
 
+abbreviation "FROM \<equiv> FROMNTIMES"
+
+lemma
+  shows "L (der c (FROM r n)) = 
+         L (if n <= 0 then SEQ (der c r) (ALT ONE (FROM r 0))
+                      else SEQ (der c r) (ALT ZERO (FROM r (n -1))))"
+  apply(auto simp add: Sequ_def)
+  oops
+
+
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 where
@@ -365,7 +403,15 @@
 apply(simp add: nullable_correctness del: Der_UNION)
 apply(simp add: nullable_correctness del: Der_UNION)
 apply(simp add: nullable_correctness del: Der_UNION)
-prefer 2
+      prefer 2
+      apply(simp only: der.simps)
+      apply(case_tac "x2 = 0")
+       apply(simp)
+      apply(simp del: Der_Sequ L.simps)
+      apply(subst L.simps)
+  apply(subst (2) L.simps)
+  thm Der_UNION
+
 apply(simp add: nullable_correctness del: Der_UNION)
 apply(simp add: nullable_correctness del: Der_UNION)
 apply(rule impI)