diff -r cc8e231529fb -r e1b74d618f1b thys/SpecExt.thy
--- a/thys/SpecExt.thy	Tue Jan 25 13:12:50 2022 +0000
+++ b/thys/SpecExt.thy	Thu Jan 27 23:25:26 2022 +0000
@@ -1,6 +1,6 @@
    
 theory SpecExt
-  imports Main (*"~~/src/HOL/Library/Sublist"*)
+  imports Main "HOL-Library.Sublist" (*"~~/src/HOL/Library/Sublist"*)
 begin
 
 section {* Sequential Composition of Languages *}
@@ -165,10 +165,6 @@
 apply(auto simp add: Sequ_def)
   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) = {}"
 by(simp add: Der_def)
@@ -221,7 +217,7 @@
 datatype rexp =
   ZERO
 | ONE
-| CHAR char
+| CH char
 | SEQ rexp rexp
 | ALT rexp rexp
 | STAR rexp
@@ -238,7 +234,7 @@
 where
   "L (ZERO) = {}"
 | "L (ONE) = {[]}"
-| "L (CHAR c) = {[c]}"
+| "L (CH c) = {[c]}"
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 | "L (STAR r) = (L r)\<star>"
@@ -255,7 +251,7 @@
 where
   "nullable (ZERO) = False"
 | "nullable (ONE) = True"
-| "nullable (CHAR c) = False"
+| "nullable (CH c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 | "nullable (STAR r) = True"
@@ -270,7 +266,7 @@
 where
   "der c (ZERO) = ZERO"
 | "der c (ONE) = ZERO"
-| "der c (CHAR d) = (if c = d then ONE else ZERO)"
+| "der c (CH d) = (if c = d then ONE else ZERO)"
 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 | "der c (SEQ r1 r2) = 
      (if nullable r1
@@ -340,48 +336,6 @@
   by (metis append.assoc)
   
 
-
-lemma
- "L(FROMNTIMES r n) = L(SEQ (NTIMES r n) (STAR r))"
-  apply(auto simp add: Sequ_def)
-  defer
-   apply(subgoal_tac "\<exists>m. s2 \<in> (L r) \<up> m")
-  prefer 2
-    apply (simp add: Star_Pow)
-  apply(auto)
-  apply(rule_tac x="n + m" in bexI)
-    apply (simp add: pow_add)
-   apply simp
-  apply(subgoal_tac "\<exists>m. m + n = xa")
-   apply(auto)
-   prefer 2
-  using le_add_diff_inverse2 apply auto[1]
-  by (smt Pow_Star Sequ_def add.commute mem_Collect_eq pow_add2)
-  
-lemma
-   "L (der c (FROMNTIMES r n)) = 
-     L (SEQ (der c r) (FROMNTIMES r (n - 1)))"
-  apply(auto simp add: Sequ_def)
-  using Star_Pow apply blast
-  using Pow_Star by blast
-  
-lemma
- "L (der c (UPNTIMES r n)) = 
-    L(if n = 0 then ZERO  else 
-      ALT (der c r) (SEQ (der c r) (UPNTIMES r (n - 1))))"
-  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
@@ -454,8 +408,10 @@
 apply(auto simp add: Sequ_def Der_def Cons_eq_append_conv)[1]
 apply(rule_tac x="Suc xa" in bexI)
 apply(auto simp add: Sequ_def)[2]
-apply (metis append_Cons)
-apply (metis (no_types, hide_lams) Pow_decomp atMost_iff diff_Suc_eq_diff_pred diff_is_0_eq)
+     apply (metis append_Cons)
+ apply(rule_tac x="xa - 1" in bexI)
+     apply(auto simp add: Sequ_def)[2]
+  apply (metis One_nat_def Pow_decomp)
 apply(rule impI)+
 apply(subst Sequ_Union_in)
 apply(subst Der_Pow_Sequ[symmetric])
@@ -485,7 +441,7 @@
 | Right val
 | Left val
 | Stars "val list"
-
+| Nt val
 
 section {* The string behind a value *}
 
@@ -499,6 +455,7 @@
 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
 | "flat (Stars []) = []"
 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
+| "flat (Nt v) = flat v"
 
 abbreviation
   "flats vs \<equiv> concat (map flat vs)"
@@ -597,7 +554,7 @@
 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 | "\<Turnstile> Void : ONE"
-| "\<Turnstile> Char c : CHAR c"
+| "\<Turnstile> Char c : CH c"
 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs \<le> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : UPNTIMES r n"
 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; 
@@ -622,7 +579,7 @@
   "\<Turnstile> v : SEQ r1 r2"
   "\<Turnstile> v : ALT r1 r2"
   "\<Turnstile> v : ONE"
-  "\<Turnstile> v : CHAR c"
+  "\<Turnstile> v : CH c"
   "\<Turnstile> vs : STAR r"
   "\<Turnstile> vs : UPNTIMES r n"
   "\<Turnstile> vs : NTIMES r n"
@@ -867,7 +824,10 @@
   then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" "length vs \<le> n"
   using IH flats_cval_nonempty by (smt order.trans) 
   then show "\<exists>v. \<Turnstile> v : UPNTIMES r n \<and> flat v = s"
-  using Prf.intros(7) flat_Stars by blast
+    using Prf.intros(7) flat_Stars by blast
+next 
+  case (NOT r)
+  then show ?case sorry
 qed (auto intro: Prf.intros)
 
 
@@ -917,7 +877,7 @@
 lemma LV_simps:
   shows "LV ZERO s = {}"
   and   "LV ONE s = (if s = [] then {Void} else {})"
-  and   "LV (CHAR c) s = (if s = [c] then {Char c} else {})"
+  and   "LV (CH c) s = (if s = [c] then {Char c} else {})"
   and   "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
 unfolding LV_def
 apply(auto intro: Prf.intros elim: Prf.cases)
@@ -1226,8 +1186,8 @@
   case (ONE s)
   show "finite (LV ONE s)" by (simp add: LV_simps)
 next
-  case (CHAR c s)
-  show "finite (LV (CHAR c) s)" by (simp add: LV_simps)
+  case (CH c s)
+  show "finite (LV (CH c) s)" by (simp add: LV_simps)
 next 
   case (ALT r1 r2 s)
   then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
@@ -1270,7 +1230,10 @@
   case (NMTIMES r n m s)
   have "\<And>s. finite (LV r s)" by fact
   then show "finite (LV (NMTIMES r n m) s)"
-    by (simp add: LV_NMTIMES_6)         
+    by (simp add: LV_NMTIMES_6)    
+next 
+  case (NOT r s)
+  then show ?case sorry
 qed
 
 
@@ -1281,7 +1244,7 @@
   Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 where
   Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
-| Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
+| Posix_CHAR: "[c] \<in> (CH c) \<rightarrow> (Char c)"
 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
@@ -1320,7 +1283,7 @@
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
   "s \<in> ONE \<rightarrow> v"
-  "s \<in> CHAR c \<rightarrow> v"
+  "s \<in> CH c \<rightarrow> v"
   "s \<in> ALT r1 r2 \<rightarrow> v"
   "s \<in> SEQ r1 r2 \<rightarrow> v"
   "s \<in> STAR r \<rightarrow> v"
@@ -1396,7 +1359,7 @@
   then show "Void = v2" by cases auto
 next 
   case (Posix_CHAR c v2)
-  have "[c] \<in> CHAR c \<rightarrow> v2" by fact
+  have "[c] \<in> CH c \<rightarrow> v2" by fact
   then show "Char c = v2" by cases auto
 next 
   case (Posix_ALT1 s r1 v r2 v2)
@@ -1503,14 +1466,9 @@
     using Posix1(1) Posix1(2) apply blast 
      apply(case_tac n)
       apply(simp)
-      apply(simp)
-    apply(drule_tac x="va" in meta_spec)
-    apply(drule_tac x="vs" in meta_spec)
-    apply(simp)
-     apply(drule meta_mp)
-    apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil diff_Suc_1 local.Posix_FROMNTIMES1(4) val.inject(5))
-    apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil)
-    by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) self_append_conv self_append_conv2)
+     apply(simp)
+    apply (smt (verit, ccfv_threshold) L.simps(9) Posix1(1) UN_E append_eq_append_conv2)
+    by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) append_Nil2 append_self_conv2)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1555,18 +1513,8 @@
        apply(case_tac m)
       apply(simp)
      apply(simp)
-    apply(drule_tac x="va" in meta_spec)
-    apply(drule_tac x="vs" in meta_spec)
-    apply(simp)
-     apply(drule meta_mp)
-      apply(drule Posix1(1))
-      apply(drule Posix1(1))
-      apply(drule Posix1(1))
-      apply(frule Posix1(1))
-      apply(simp)
-    using Posix_NMTIMES1.hyps(4) apply force
-     apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2)
-    by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil)      
+    apply (metis L.simps(10) Posix1(1) UN_E append.right_neutral append_Nil)
+    by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append_Nil self_append_conv)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1616,7 +1564,6 @@
      apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2]
   apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq)
      apply(simp)
-     apply(clarify)
      apply(case_tac n)
       apply(simp)
      apply(simp)
@@ -1632,7 +1579,6 @@
       apply(simp)
      apply(simp)
     apply(simp)
-   apply(clarify)
    apply(erule Prf_elims)
       apply(simp)
   apply(rule Prf.intros)  
@@ -1660,7 +1606,6 @@
   apply(simp)
   apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
   apply(simp)
-  apply(clarify)
   apply(rotate_tac 6)
   apply(erule Prf_elims)
    apply(simp)
@@ -1675,7 +1620,6 @@
   apply(simp)
   apply(simp)
   apply(simp)
-  apply(clarify)
   apply(rotate_tac 6)
   apply(erule Prf_elims)
    apply(simp)