--- a/thys2/SizeBound5CT.thy Wed Feb 09 15:14:58 2022 +0000
+++ b/thys2/SizeBound5CT.thy Wed Feb 09 18:21:15 2022 +0000
@@ -1,6 +1,6 @@
theory SizeBound5CT
- imports "Lexer" "PDerivs"
+ imports "Lexer" "PDerivs"
begin
section \<open>Bit-Encodings\<close>
@@ -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,34 +1882,167 @@
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
+(*
+fun rexp_encode :: "rrexp \<Rightarrow> nat"
+ where
+"rexp_encode RZERO = 0"
+|"rexp_encode RONE = 1"
+|"rexp_encode (RCHAR c) = 2"
+|"rexp_encode (RSEQ r1 r2) = ( 2 ^ (rexp_encode r1)) "
+*)
+lemma finite_chars:
+ shows " \<exists>N. ( (\<forall>r \<in> (set rs). \<exists>c. r = RCHAR c) \<and> (distinct rs) \<longrightarrow> length rs < N)"
+ apply(rule_tac x = "Suc 256" in exI)
+ sorry
+
+fun all_chars :: "nat \<Rightarrow> char list"
+ where
+"all_chars 0 = [CHR 0x00]"
+|"all_chars (Suc i) = (char_of (Suc i)) # (all_chars i)"
+
+
+fun rexp_enum :: "nat \<Rightarrow> rrexp list"
+ where
+"rexp_enum 0 = []"
+|"rexp_enum 1 = RZERO # (RONE # (map RCHAR (all_chars 255)))"
+
+lemma finite_sized_rexp_forms_finite_set:
+ shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)"
+ apply(induct N)
+ apply simp
+ apply auto
+ (*\<lbrakk>\<forall>r. rsize r < N \<longrightarrow> r \<in> SN; finite SN\<rbrakk> \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*)
+ (* \<And>N. \<exists>SN. (\<forall>r. rsize r < N \<longrightarrow> r \<in> SN) \<and> finite SN \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*)
+ 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
+ shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) "
+ apply(frule finite_sized_rexp_forms_finite_set)
(*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))"
+ by (meson comp_apply)
+
+lemma der_seqstar_res:
+ shows "rder x (RSEQ r1 r2) = RSEQ r3 r4"
+
+
+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))
+
+
+ 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 +2078,6 @@
prefer 2
apply (simp add: finite_star)
-sledgehammer
sorry