--- 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