--- a/thys2/SizeBound6CT.thy Tue Mar 01 11:14:17 2022 +0000
+++ b/thys2/SizeBound6CT.thy Wed Mar 02 23:13:59 2022 +0000
@@ -21,6 +21,12 @@
|"orderedPrefAux 0 ss = Nil"
+fun ordsuf :: "char list \<Rightarrow> char list list"
+ where
+ "ordsuf [] = []"
+| "ordsuf (x # xs) = (ordsuf xs) @ [(x # xs)]"
+
+
fun orderedPref :: "char list \<Rightarrow> char list list"
where
"orderedPref s = orderedPrefAux (length s) s"
@@ -46,6 +52,26 @@
lemma shape_of_suf_3list:
shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]"
by auto
+
+
+lemma ordsuf_last:
+ shows "ordsuf (xs @ [x]) = [x] # (map (\<lambda>s. s @ [x]) (ordsuf xs))"
+ apply(induct xs)
+ apply(auto)
+ done
+
+lemma ordsuf_append:
+ shows "ordsuf (s1 @ s) = (ordsuf s) @ (map (\<lambda>s11. s11 @ s) (ordsuf s1))"
+apply(induct s1 arbitrary: s rule: rev_induct)
+ apply(simp)
+ apply(drule_tac x="[x] @ s" in meta_spec)
+ apply(simp)
+ apply(subst ordsuf_last)
+ apply(simp)
+ done
+
+
+
(*
lemma throwing_elem_around:
shows "orderedSuf (s1 @ [a] @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf ( s1 @ [a]) ))"
@@ -90,10 +116,16 @@
*)
+datatype cchar =
+Achar
+|Bchar
+|Cchar
+|Dchar
+
datatype rrexp =
RZERO
| RONE
-| RCHAR char
+| RCHAR cchar
| RSEQ rrexp rrexp
| RALTS "rrexp list"
| RSTAR rrexp
@@ -113,13 +145,19 @@
| "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)"
| "rnullable (RSTAR r) = True"
+fun convert_cchar_char :: "cchar \<Rightarrow> char"
+ where
+"convert_cchar_char Achar = (CHR 0x41) "
+| "convert_cchar_char Bchar = (CHR 0x42) "
+| "convert_cchar_char Cchar = (CHR 0x43) "
+| "convert_cchar_char Dchar = (CHR 0x44) "
fun
rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"
where
"rder c (RZERO) = RZERO"
| "rder c (RONE) = RZERO"
-| "rder c (RCHAR d) = (if c = d then RONE else RZERO)"
+| "rder c (RCHAR d) = (if c = (convert_cchar_char d) then RONE else RZERO)"
| "rder c (RALTS rs) = RALTS (map (rder c) rs)"
| "rder c (RSEQ r1 r2) =
(if rnullable r1
@@ -252,6 +290,12 @@
"cond_list r1 r2 s = rders_cond_list r2 (nullable_bools r1 (orderedPref s) ) (orderedSuf s)"
+fun seq_update :: " char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list"
+ where
+"seq_update c r Ss = (if (rnullable r) then ([c] # (map (\<lambda>s1. s1 @ [c]) Ss)) else (map (\<lambda>s1. s1 @ [c]) Ss))"
+
+
+
lemma rSEQ_mono:
shows "rsize (rsimp_SEQ r1 r2) \<le>rsize ( RSEQ r1 r2)"
apply auto
@@ -378,7 +422,7 @@
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 "
@@ -424,8 +468,55 @@
prefer 2
apply auto
sorry
+*)
+(*
+lemma shape_derssimpseq_onechar2:
+ shows "rders_simp (RSEQ r1 r2) [c] =
+ rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) #
+ (rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )"
+ sorry
+*)
+
+lemma shape_derssimpseq_onechar:
+ shows " (rders_simp r [c]) = (rsimp (rders 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
+ sorry
lemma shape_derssimpseq_onechar2:
shows "rders_simp (RSEQ r1 r2) [c] =
@@ -433,6 +524,31 @@
(rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )"
sorry
+(*
+lemma simp_helps_der_pierce_dB:
+ shows " rsimp
+ (rsimp_ALTs
+ (map (rder x)
+ (rdistinct rs {}))) =
+ rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
+
+ sorry
+*)
+(*
+lemma simp_helps_der_pierce_flts:
+ shows " rsimp
+ (rsimp_ALTs
+ (rdistinct
+ (map (rder x)
+ (rflts rs )
+ ) {}
+ )
+ ) =
+ rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}) )"
+
+ sorry
+
+*)
lemma rders__onechar:
shows " (rders_simp r [c]) = (rsimp (rders r [c]))"
@@ -484,29 +600,6 @@
)"
sorry
-lemma simp_helps_der_pierce_dB:
- shows " rsimp
- (rsimp_ALTs
- (map (rder x)
- (rdistinct rs {}))) =
- rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
-
- sorry
-
-lemma simp_helps_der_pierce_flts:
- shows " rsimp
- (rsimp_ALTs
- (rdistinct
- (map (rder x)
- (rflts rs )
- ) {}
- )
- ) =
- rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}) )"
-
- sorry
-
-
lemma unfold_ders_simp_inside_only:
shows " (rders_simp (RSEQ r1 r2) xs =
rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs))))
@@ -594,6 +687,55 @@
sorry
+
+
+lemma seq_update_seq_ders:
+ shows "rsimp (rder c ( rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) #
+(map (rders_simp r2) Ss))))) =
+ rsimp (RALTS ((RSEQ (rders_simp r1 (s @ [c])) r2) #
+(map (rders_simp r2) (seq_update c (rders_simp r1 s) Ss)))) "
+ sorry
+
+lemma seq_ders_closed_form1:
+ shows "\<exists>Ss. rders_simp (RSEQ r1 r2) [c] = rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) #
+(map ( rders_simp r2 ) Ss)))"
+ apply(case_tac "rnullable r1")
+ apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] =
+rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [[c]])))")
+ prefer 2
+ apply (simp add: rsimp_idem)
+ apply(rule_tac x = "[[c]]" in exI)
+ apply simp
+ apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] =
+rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [])))")
+ apply blast
+ apply(simp add: rsimp_idem)
+ sorry
+
+
+
+lemma seq_ders_closed_form:
+ shows "s \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSEQ r1 r2) s = rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) #
+(map ( rders_simp r2 ) Ss)))"
+ apply(induct s rule: rev_induct)
+ apply simp
+ apply(case_tac xs)
+ using seq_ders_closed_form1 apply auto[1]
+ apply(subgoal_tac "\<exists>Ss. rders_simp (RSEQ r1 r2) xs = rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # map (rders_simp r2) Ss))")
+ prefer 2
+
+ apply blast
+ apply(erule exE)
+ apply(rule_tac x = "seq_update x (rders_simp r1 xs) Ss" in exI)
+ apply(subst rders_simp_append)
+ apply(subgoal_tac "rders_simp (rders_simp (RSEQ r1 r2) xs) [x] = rsimp (rder x (rders_simp (RSEQ r1 r2) xs))")
+ apply(simp only:)
+ apply(subst seq_update_seq_ders)
+ apply blast
+ using rders_simp_one_char by presburger
+
+
+
(*nullable_seq_with_list1 related *)
lemma LHS0_def_der_alt:
shows "rsimp (rder x (RALTS ( (RSEQ (rders_simp r1 xs) r2) # (cond_list r1 r2 xs)))) =
@@ -710,32 +852,6 @@
apply simp
using r1r2ders_whole rders_simp_append rders_simp_one_char by presburger
-(*
-
- apply(subgoal_tac " rsimp
- (rder x
- (rsimp_ALTs
- (rdistinct
- (rflts
- (rsimp_SEQ (rsimp (rders_simp r1 xs)) (rsimp r2) #
- map rsimp
- (rders_cond_list r2 (nullable_bools r1 (orderedPrefAux (length xs) xs)) (orderedSufAux (length xs) xs))))
- {}))) =
- rsimp
- (
- (rsimp_ALTs
- (map (rder x)
- (rdistinct
- (rflts
- (rsimp_SEQ (rsimp (rders_simp r1 xs)) (rsimp r2) #
- map rsimp
- (rders_cond_list r2 (nullable_bools r1 (orderedPrefAux (length xs) xs)) (orderedSufAux (length xs) xs))))
- {})
- )
- )
- ) ")
- prefer 2
-*)
lemma shape_derssimp_alts:
shows "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))"
@@ -751,13 +867,10 @@
|"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
+
-definition all_chars :: "int \<Rightarrow> char list"
- where "all_chars n = map char_of [0..n]"
+
+
(*
fun rexp_enum :: "nat \<Rightarrow> rrexp list"
where
@@ -766,26 +879,150 @@
|"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]"
*)
-
-fun rexp_enum :: "nat \<Rightarrow> rrexp set"
+context notes rev_conj_cong[fundef_cong] begin
+function (sequential) rexp_enum :: "nat \<Rightarrow> rrexp set"
where
"rexp_enum 0 = {}"
-|"rexp_enum (Suc 0) = {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c. c \<in> set (all_chars 255)}"
-|"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = n}"
+|"rexp_enum (Suc 0) = {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c. c \<in>{Achar, Bchar, Cchar, Dchar} }"
+|"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = n} \<union>
+{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union>
+{RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
+(rexp_enum n)"
+ by pat_completeness auto
+termination
+ by (relation "measure size") auto
+end
+
+lemma rexp_enum_inclusion:
+ shows "(rexp_enum n) \<subseteq> (rexp_enum (Suc n))"
+ apply(induct n)
+ apply auto[1]
+ apply(simp)
+ done
+
+lemma rexp_enum_mono:
+ shows "n \<le> m \<Longrightarrow> (rexp_enum n) \<subseteq> (rexp_enum m)"
+ by (simp add: lift_Suc_mono_le rexp_enum_inclusion)
+
+lemma enum_inductive_cases:
+ shows "rsize (RSEQ r1 r2) = Suc n \<Longrightarrow> \<exists>i j. rsize r1 = i \<and> rsize r2 = j\<and> i + j = n"
+ by (metis Suc_inject rsize.simps(5))
+thm rsize.simps(5)
+
+lemma enumeration_finite:
+ shows "\<exists>Nn. card (rexp_enum n) < Nn"
+ apply(simp add:no_top_class.gt_ex)
+ done
+
+lemma size1_rexps:
+ shows "RCHAR x \<in> rexp_enum 1"
+ apply(cases x)
+ apply auto
+ done
+
+lemma non_zero_size:
+ shows "rsize r \<ge> Suc 0"
+ apply(induct r)
+ apply auto done
+
+corollary size_geq1:
+ shows "rsize r \<ge> 1"
+ by (simp add: non_zero_size)
+
+
+lemma rexp_size_induct:
+ shows "\<And>N r x5 a list.
+ \<lbrakk> rsize r = Suc N; r = RALTS x5;
+ x5 = a # list\<rbrakk> \<Longrightarrow>\<exists>i j. rsize a = i \<and> rsize (RALTS list) = j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N"
+ apply(rule_tac x = "rsize a" in exI)
+ apply(rule_tac x = "rsize (RALTS list)" in exI)
+ apply(subgoal_tac "rsize a \<ge> 1")
+ prefer 2
+ using One_nat_def non_zero_size apply presburger
+ apply(subgoal_tac "rsize (RALTS list) \<ge> 1 ")
+ prefer 2
+ using size_geq1 apply blast
+ apply simp
+ done
-
-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)
+lemma rexp_enum_case3:
+ shows "N \<ge> Suc 0 \<Longrightarrow> rexp_enum (Suc N) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = N} \<union>
+{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N} \<union>
+{RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
+(rexp_enum N)"
+ apply(case_tac 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*)
+ apply auto
+ done
+
+
+
+lemma def_enum_alts:
+ shows "\<lbrakk> r = RALTS x5; x5 = a # list;
+ rsize a = i \<and> rsize (RALTS list) = j \<and> i + j = Suc N \<and> a \<in> (rexp_enum i) \<and> (RALTS list) \<in> (rexp_enum j) \<rbrakk>
+ \<Longrightarrow> r \<in> rexp_enum (Suc N)"
+ apply(subgoal_tac "N \<ge> 1")
+ prefer 2
+ apply (metis One_nat_def add_is_1 less_Suc0 linorder_le_less_linear non_zero_size)
+ apply(subgoal_tac " rexp_enum (Suc N) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = N} \<union>
+{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N\<and> i \<le> N \<and> j \<le> N} \<union>
+{RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
+(rexp_enum N)")
+ prefer 2
+ using One_nat_def rexp_enum_case3 apply presburger
+ apply(subgoal_tac "i \<le> N \<and> j \<le> N")
+ prefer 2
+ using non_zero_size apply auto[1]
+ apply(subgoal_tac "r \<in> {uu.
+ \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
+ apply auto[1]
+ apply(subgoal_tac "RALTS (a # list) \<in> {uu.
+ \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
+
+
+ apply fastforce
+ apply(subgoal_tac "a \<in> rexp_enum i")
+ prefer 2
+
+ apply linarith
+ by blast
+
+lemma rexp_enum_covers:
+ shows " rsize r \<le> N \<Longrightarrow> r \<in> rexp_enum N \<and> r \<in> rexp_enum (rsize r)"
+ apply(induct N arbitrary : r)
+ apply simp
+
+ using rsize.elims apply auto[1]
+ apply(case_tac "rsize r \<le> N")
+ using enumeration_finite
+
+ apply (meson in_mono rexp_enum_inclusion)
+ apply(subgoal_tac "rsize r = Suc N")
+ prefer 2
+ using le_Suc_eq apply blast
+
+ apply(case_tac r)
+ prefer 5
+ apply(case_tac x5)
+ apply(subgoal_tac "rsize r =1")
+ prefer 2
+ using hand_made_def_rlist_size rlist_size.simps(2) rsize.simps(4) apply presburger
+ apply simp
+ apply(subgoal_tac "a \<in> rexp_enum (rsize a)")
+ apply(subgoal_tac "RALTS list \<in> rexp_enum (rsize (RALTS list))")
+
+ apply (meson def_enum_alts rexp_size_induct)
+ apply(subgoal_tac "rsize (RALTS list) \<le> N")
+ apply(subgoal_tac "RALTS list \<in> rexp_enum N")
+ prefer 2
+ apply presburger
+
sorry
lemma finite_size_finite_regx:
shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) "
+
sorry
(*below probably needs proved concurrently*)