diff -r 2416fdec6396 -r ec08181c1f42 thys2/SizeBound5CT.thy
--- a/thys2/SizeBound5CT.thy	Wed Feb 09 00:29:04 2022 +0000
+++ b/thys2/SizeBound5CT.thy	Wed Feb 09 00:30:04 2022 +0000
@@ -1672,6 +1672,20 @@
 | "rsize (RSTAR  r) = Suc (rsize r)"
 
 
+
+
+lemma rsimp_aalts_smaller:
+  shows "rsize (rsimp_ALTs  rs) \<le> rsize (RALTS rs)"
+  apply(induct rs)
+   apply simp
+  sorry
+
+lemma finite_list_of_ders:
+  shows"\<exists>dersset. ( (finite dersset) \<and> (\<forall>s. (rders_simp r s) \<in> dersset) )"
+  sorry
+
+
+
 lemma rerase_bsimp:
   shows "rerase (bsimp r) = rsimp (rerase r)"
   apply(induct r)
@@ -1698,18 +1712,7 @@
   sorry
 *)
 
-lemma ders_simp_comm_onechar:
-  shows " rerase  (bders_simp r [c]) = rerase (bsimp (bders r [c]))"
-and " rders_simp (RSEQ r1 r2) [c] = 
-         rsimp (RALTS  ((RSEQ (rders r1 [c]) r2) #
-           (map (rders r2) (orderedSuf [c]))) )"
-   apply simp
-  apply(simp add: rders.simps)
-  apply(case_tac "rsimp (rder c r1) = RZERO")
-   apply simp
-  apply auto
-  sledgehammer
-  oops
+
 
 fun rders_cond_list :: "rrexp \<Rightarrow> bool list \<Rightarrow> char list list \<Rightarrow> rrexp list"
   where
@@ -1723,9 +1726,146 @@
 "nullable_bools r (s#strs) = (rnullable (rders r s)) # (nullable_bools r strs) "
 |"nullable_bools r [] = []"
 
+thm rsimp_SEQ.simps
+
+lemma idiot:
+  shows "rsimp_SEQ RONE r = r"
+  apply(case_tac r)
+       apply simp_all
+  done
+
+lemma no_dup_after_simp:
+  shows "RALTS rs = rsimp r \<Longrightarrow> distinct rs"
+  sorry
+
+lemma no_further_dB_after_simp:
+  shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"
+  sorry
+
+lemma longlist_withstands_rsimp_alts:
+  shows "length rs \<ge> 2 \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+  sorry
+
+lemma no_alt_short_list_after_simp:
+  shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+  sorry
+
+lemma idiot2:
+  shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk>
+    \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2"
+  apply(case_tac r1)
+       apply(case_tac r2)
+  apply simp_all
+     apply(case_tac r2)
+  apply simp_all
+     apply(case_tac r2)
+  apply simp_all
+   apply(case_tac r2)
+  apply simp_all
+  apply(case_tac r2)
+       apply simp_all
+  done
+
+lemma rsimp_aalts_another:
+  shows "\<forall>r \<in> (set  (map rsimp  ((RSEQ (rders r1 s) r2) #
+           (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s))  )) ). (rsize r) < N "
+  sorry
+
+
+
+lemma shape_derssimpseq_onechar:
+  shows " rerase  (bders_simp r [c]) = rerase (bsimp (bders r [c]))"
+and "rders_simp (RSEQ r1 r2) [c] = 
+         rsimp (RALTS  ((RSEQ (rders r1 [c]) r2) #
+           (rders_cond_list r2 (nullable_bools r1 (orderedPref [c]))  (orderedSuf [c]))) )"
+   apply simp
+  apply(simp add: rders.simps)
+  apply(case_tac "rsimp (rder c r1) = RZERO")
+   apply auto
+  apply(case_tac "rsimp (rder c r1) = RONE")
+   apply auto
+   apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp r2")
+  prefer 2
+  using idiot
+    apply simp
+   apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp r2]) {})")
+    prefer 2
+    apply auto
+   apply(case_tac "rsimp r2")
+        apply auto
+   apply(subgoal_tac "rdistinct x5 {} = x5")
+  prefer 2
+  using no_further_dB_after_simp
+    apply metis
+   apply(subgoal_tac "rsimp_ALTs (rdistinct x5 {}) = rsimp_ALTs x5")
+    prefer 2
+    apply fastforce  
+   apply auto
+   apply (metis no_alt_short_list_after_simp)
+  apply (case_tac "rsimp r2 = RZERO")
+   apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RZERO")
+    prefer 2
+    apply(case_tac "rsimp ( rder c r1)")
+         apply auto
+  apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RSEQ (rsimp (rder c r1)) (rsimp r2)")
+   prefer 2
+   apply auto
+  apply(metis idiot2)
+  done
+
+lemma rders__onechar:
+  shows " (rders_simp r [c]) =  (rsimp (rders r [c]))"
+  by simp
+
+lemma rders_append:
+  "rders c (s1 @ s2) = rders (rders c s1) s2"
+  apply(induct s1 arbitrary: c s2)
+  apply(simp_all)
+  done
+
+lemma rders_simp_append:
+  "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2"
+  apply(induct s1 arbitrary: c s2)
+  apply(simp_all)
+  done
+
+lemma inside_simp_removal:
+  shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
   
+  sorry
+
+lemma set_related_list:
+  shows "distinct rs  \<Longrightarrow> length rs = card (set rs)"
+  by (simp add: distinct_card)
+(*this section deals with the property of distinctBy: creates a list without duplicates*)
+lemma rdistinct_never_added_twice:
+  shows "rdistinct (a # rs) {a} = rdistinct rs {a}"
+  by force
+
+
+lemma rdistinct_does_the_job:
+  shows "distinct (rdistinct rs s)"
+  apply(induct rs arbitrary: s)
+   apply simp
+  apply simp
+  sorry
+
+
+
+
+(*this section deals with the property of distinctBy: creates a list without duplicates*)
+
+lemma rders_simp_same_simpders:
+  shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(case_tac "xs = []")
+   apply simp
+  apply(simp add: rders_append rders_simp_append)
+  using inside_simp_removal by blast
+
 lemma shape_derssimp_seq:
-  shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow> rerase  (bders_simp r s) = rerase (bsimp (bders r s))"
+  shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow>  (rders_simp r s) = (rsimp (rders r s))"
 and "\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = 
          rsimp (RALTS  ((RSEQ (rders r1 s) r2) #
            (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s))) )"
@@ -1742,11 +1882,17 @@
    
     apply(subgoal_tac "xs \<noteq> [] \<Longrightarrow> rsimp (rder x (rerase (bders_simp r xs))) = rsimp (rder x (rerase (bsimp (bders r xs))))")
   prefer 2
-  apply presburger
+     apply presburger
+  apply(case_tac "xs = []")
   sorry
 
+
 lemma shape_derssimp_alts:
-  shows "rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))"
+  shows "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))"
+  apply(case_tac "s")
+   apply simp
+  apply simp
+  sorry
 
 
 lemma finite_size_finite_regx:
@@ -1757,19 +1903,115 @@
 (*below  probably needs proved concurrently*)
 
 lemma finite_r1r2_ders_list:
-  shows "\<forall>r1 r2. \<exists>l. 
-(length (rdistinct  (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s)) {})) < l "
+  shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2)
+           \<Longrightarrow>  \<exists>l. \<forall>s.
+(length (rdistinct  (map rsimp (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s))) {}) )  < l "
   sorry
 
+(*
+\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = 
+         rsimp (RALTS  ((RSEQ (rders r1 s) r2) #
+           (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s))) )
+*)
+
+lemma finite_width_alt:
+  shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) 
+      \<Longrightarrow> \<exists>N3. \<forall>s.  rsize (rsimp (RALTS  ((RSEQ (rders r1 s) r2) #
+           (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s))) )) < N3"
+
+  sorry
+
+
+lemma empty_diff:
+  shows "s = [] \<Longrightarrow>
+        (rsize (rders_simp (RSEQ r1 r2) s)) \<le> 
+        (max 
+        (rsize (rsimp (RALTS (RSEQ (rders r1 s) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)))))
+        (Suc (rsize r1 + rsize r2)) ) "
+  apply simp
+  done
+
 lemma finite_seq:
   shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2)
            \<Longrightarrow> \<exists>N3.\<forall>s.(rsize (rders_simp (RSEQ r1 r2) s)) < N3"
+  apply(frule finite_width_alt)
+  apply(erule exE)
+  apply(rule_tac x = "max (N3+2) (Suc (Suc (rsize r1) + (rsize r2)))" in exI)
+  apply(rule allI)
+  apply(case_tac "s = []")
+  prefer 2
+   apply (simp add: less_SucI shape_derssimp_seq(2))
+   apply (meson less_SucI less_max_iff_disj)
+  apply simp
+  done
+
+
+(*For star related error bound*)
+
+lemma star_is_a_singleton_list_derc:
+  shows " \<exists>Ss.  rders_simp (RSTAR r) [c] = rsimp_ALTs (map (\<lambda>s1.  rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)"
+  apply simp
+  apply(rule_tac x = "[[c]]" in exI)
+  apply auto
+  done
+
+lemma rder_rsimp_ALTs_commute:
+  shows "  (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)"
+  apply(induct rs)
+   apply simp
+  apply(case_tac rs)
+   apply simp
+  apply auto
+  done
+
+lemma double_nested_ALTs_under_rsimp:
+  shows "rsimp (rsimp_ALTs ((RALTS rs1) # rs)) = rsimp (RALTS (rs1 @ rs))"
+  apply(case_tac rs1)
+  apply simp
+  
+   apply (metis list.simps(8) list.simps(9) neq_Nil_conv rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+  apply(case_tac rs)
+   apply simp
+  apply auto
   sorry
 
+lemma star_seqs_produce_star_seqs:
+  shows "rsimp (rsimp_ALTs (map (rder x \<circ> (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))
+       = rsimp (rsimp_ALTs (map ( (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss))"
+  sledgehammer
+  by (meson comp_apply)
+
+lemma der_seqstar_res:
+  shows "rder x "
+
+
+lemma linearity_of_list_of_star_or_starseqs:
+  shows "\<exists>Ssa. rsimp (rder x (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) =
+                 rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)"
+  apply(simp add: rder_rsimp_ALTs_commute)
+  apply(induct Ss)
+   apply simp
+   apply (metis list.simps(8) rsimp_ALTs.simps(1))
+
+  sledgehammer
+  sorry
+
+lemma starder_is_a_list_of_stars_or_starseqs:
+  shows "s \<noteq> [] \<Longrightarrow> \<exists>Ss.  rders_simp (RSTAR r) s = rsimp_ALTs (map (\<lambda>s1.  rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)"
+  apply(induct s rule: rev_induct)
+  apply simp
+  apply(case_tac "xs = []")
+  using star_is_a_singleton_list_derc
+  apply(simp)
+  apply auto
+  apply(simp add: rders_simp_append)
+  using linearity_of_list_of_star_or_starseqs by blast
+
 
 lemma finite_star:
   shows "(\<forall>s. rsize (rders_simp r0 s) < N0 )
            \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3"
+
   sorry
 
 
@@ -1805,7 +2047,6 @@
    prefer 2
 
    apply (simp add: finite_star)
-sledgehammer
   sorry