# HG changeset patch
# User Chengsong
# Date 1644280707 0
# Node ID d9e1df9ae58f12f8ff230a02d4bcd2e694a33fbe
# Parent  b66a4305749c70f87f9fd6eeb980cf622feb3d3a
size

diff -r b66a4305749c -r d9e1df9ae58f thys2/SizeBound5CT.thy
--- a/thys2/SizeBound5CT.thy	Mon Feb 07 14:22:08 2022 +0000
+++ b/thys2/SizeBound5CT.thy	Tue Feb 08 00:38:27 2022 +0000
@@ -1482,8 +1482,7 @@
 
 fun orderedSufAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list"
   where
-"orderedSufAux (Suc 0) ss = Nil"
-|"orderedSufAux (Suc i) ss = (drop i ss) # (orderedSufAux i ss)"
+ "orderedSufAux (Suc i) ss = (drop i ss) # (orderedSufAux i ss)"
 |"orderedSufAux 0 ss = Nil"
 
 fun 
@@ -1491,16 +1490,78 @@
 where
 "orderedSuf s = orderedSufAux (length s) s"
 
-lemma shape_of_suf_2list:
-  shows "orderedSuf [c1, c2] = [[c2]]"
+fun orderedPrefAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list"
+  where
+"orderedPrefAux (Suc i) ss = (take i ss) # (orderedPrefAux i ss)"
+|"orderedPrefAux 0 ss = Nil"
+
+
+fun orderedPref :: "char list \<Rightarrow> char list list"
+  where
+"orderedPref s = orderedPrefAux (length s) s"
+
+lemma shape_of_pref_1list:
+  shows "orderedPref [c] = [[]]"
   apply auto
   done
 
+lemma shape_of_suf_1list:
+  shows "orderedSuf [c] = [[c]]"
+  by auto
+
+lemma shape_of_suf_2list:
+  shows "orderedSuf [c2, c3] = [[c3], [c2,c3]]"
+  by auto
+
+lemma shape_of_prf_2list:
+  shows "orderedPref [c1, c2] = [[c1], []]"
+  by auto
+
 
 lemma shape_of_suf_3list:
-  shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3]]"
-  apply auto
-  done
+  shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]"
+  by auto
+
+lemma throwing_elem_around:
+  shows "orderedSuf (s1 @ [a] @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf ( s1 @ [a]) ))"
+and "orderedSuf (s1 @ [a] @ s) = (orderedSuf ([a] @ s) @ (map (\<lambda>s11. s11 @ ([a] @ s))) (orderedSuf s1) )"
+  sorry
+
+
+lemma suf_cons:
+  shows "orderedSuf (s1 @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf s1))"
+  apply(induct s arbitrary: s1)
+   apply simp
+  apply(subgoal_tac "s1 @ a # s = (s1 @ [a]) @ s")
+  prefer 2
+   apply simp
+  apply(subgoal_tac "orderedSuf (s1 @ a # s) = orderedSuf ((s1 @ [a]) @ s)")
+  prefer 2
+   apply presburger
+  apply(drule_tac x="s1 @ [a]" in meta_spec)
+  sorry
+
+
+
+lemma shape_of_prf_3list:
+  shows "orderedPref [c1, c2, c3] = [[c1, c2], [c1], []]"
+  by auto
+
+fun zip_concat :: "char list list \<Rightarrow> char list list \<Rightarrow> char list list"
+  where 
+    "zip_concat (s1#ss1) (s2#ss2) = (s1@s2) # (zip_concat ss1 ss2)"
+  |   "zip_concat [] [] = []"
+  | "zip_concat [] (s2#ss2) = s2 # (zip_concat [] ss2)"
+  | "zip_concat (s1#ss1) [] = s1 # (zip_concat ss1 [])"
+
+
+
+lemma compliment_pref_suf:
+  shows "zip_concat (orderedPref s) (orderedSuf s) = replicate (length s) s "
+  apply(induct s)
+   apply auto[1]
+  sorry
+
 
 
 
@@ -1602,6 +1663,14 @@
   "rders_simp r [] = r"
 | "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s"
 
+fun rsize :: "rrexp \<Rightarrow> nat" where
+  "rsize RZERO = 1"
+| "rsize (RONE) = 1" 
+| "rsize (RCHAR  c) = 1"
+| "rsize (RALTS  rs) = Suc (sum_list (map rsize rs))"
+| "rsize (RSEQ  r1 r2) = Suc (rsize r1 + rsize r2)"
+| "rsize (RSTAR  r) = Suc (rsize r)"
+
 
 lemma rerase_bsimp:
   shows "rerase (bsimp r) = rsimp (rerase r)"
@@ -1611,30 +1680,92 @@
 
   sorry
 
+
 lemma rerase_bder:
   shows "rerase (bder c r) = rder c (rerase r)"
   apply(induct r)
        apply auto
   sorry
-
+(*
 lemma rders_shape:
-  shows "rders_simp (RSEQ r1 r2) s = 
+  shows "s \<noteq> [] \<Longrightarrow> rders_simp (RSEQ r1 r2) s = 
          rsimp (RALTS  ((RSEQ (rders r1 s) r2) #
            (map (rders r2) (orderedSuf s))) )"
+  apply(induct s arbitrary: r1 r2 rule: rev_induct)
+   apply simp
+  apply simp
+
   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
+"rders_cond_list r2 (True # bs) (s # strs) = (rders r2 s) # (rders_cond_list r2 bs strs)"
+| "rders_cond_list r2 (False # bs) (s # strs) = rders_cond_list r2 bs strs"
+| "rders_cond_list r2 [] s = []"
+| "rders_cond_list r2 bs [] = []"
+
+fun nullable_bools :: "rrexp \<Rightarrow> char list list \<Rightarrow> bool list"
+  where
+"nullable_bools r (s#strs) = (rnullable (rders r s)) # (nullable_bools r strs) "
+|"nullable_bools r [] = []"
 
   
 lemma ders_simp_commute:
-  shows "rerase (bsimp (bders_simp r s)) = rerase (bsimp (bders r s))"
-  apply(induct s arbitrary: r rule: rev_induct)
-   apply simp
-  apply (simp add: bders_simp_append bders_append )
-  apply (simp add: rerase_bsimp)
-  apply (simp add: rerase_bder)
-  apply (simp add: rders_shape)
-  sledgehammer
-  oops
+  shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow> rerase  (bders_simp r s) = rerase (bsimp (bders 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))) )"
+  apply(induct s arbitrary: r r1 r2 rule: rev_induct)
+     apply simp
+  apply simp
+   apply(case_tac "xs = []")
+
+   apply (simp add: bders_simp_append )
+   apply(subgoal_tac "rerase (bsimp (bder x (bders_simp r xs))) = (rsimp (rerase (bder x (bders_simp r xs)))) ")
+    prefer 2
+    apply (simp add: rerase_bsimp)
+   apply(subgoal_tac "(rsimp (rerase (bder x (bders_simp r xs)))) = (rsimp (rder x (rerase (bders_simp r xs))))")
+   
+    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
+  sorry
 
+lemma finite_size_finite_regx:
+  shows "\<forall>N. \<exists>l. (\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<Longrightarrow> (length rs) < l "
+  sorry
+
+
+(*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 "
+  sorry
+
+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"
+  sorry
+
+
+lemma finite_size_ders:
+  shows "\<forall>r. \<exists>Nr. \<forall>s. rsize (rders_simp r s) < Nr"
+  sorry
 
 
 unused_thms