--- a/thys2/SizeBound6CT.thy Sun Feb 20 22:39:56 2022 +0000
+++ b/thys2/SizeBound6CT.thy Mon Feb 21 23:38:26 2022 +0000
@@ -80,7 +80,7 @@
| "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)
@@ -88,7 +88,7 @@
sorry
-
+*)
datatype rrexp =
RZERO
@@ -215,11 +215,6 @@
by(meson neq_Nil_conv)
-lemma finite_list_of_ders:
- shows"\<exists>dersset. ( (finite dersset) \<and> (\<forall>s. (rders_simp r s) \<in> dersset) )"
- sorry
-
-
@@ -475,6 +470,24 @@
shows "rsimp (rsimp r) = rsimp r"
sorry
+corollary rsimp_inner_idem1:
+ shows "rsimp r = RSEQ r1 r2 \<Longrightarrow> rsimp r1 = r1 \<and> rsimp r2 = r2"
+
+ sorry
+
+corollary rsimp_inner_idem2:
+ shows "rsimp r = RALTS rs \<Longrightarrow> \<forall>r' \<in> (set rs). rsimp r' = r'"
+ sorry
+
+corollary rsimp_inner_idem3:
+ shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs"
+ by (meson map_idI rsimp_inner_idem2)
+
+corollary rsimp_inner_idem4:
+ shows "rsimp r = RALTS rs \<Longrightarrow> flts rs = rs"
+ sorry
+
+
lemma head_one_more_simp:
shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"
by (simp add: rsimp_idem)
@@ -558,7 +571,17 @@
shows " rnullable (rders_simp r1 s) \<Longrightarrow>
rsimp (rder c (RALTS ( (RSEQ (rders_simp r1 s) r2) # (cond_list r1 r2 s)) )) =
rsimp (RALTS ( (RSEQ (rders_simp r1 (s @ [c])) r2) # (cond_list r1 r2 (s @ [c])) ) )"
- by (metis LHS1_def_der_seq append.left_neutral append_Cons first_elem_seqder_nullable simp_flatten)
+ using RHS1 LHS1_def_der_seq cond_list_head_last simp_flatten
+ by (metis append.left_neutral append_Cons)
+
+
+(*^^^^^^^^^nullable_seq_with_list1 related ^^^^^^^^^^^^^^^^*)
+
+
+
+
+
+
@@ -683,7 +706,7 @@
|"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}"
-
+
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)
@@ -782,8 +805,6 @@
apply (meson order_le_less)
apply(erule exE)
apply(erule exE)
- apply(erule exE)
- apply(rule_tac x = "N3a + Nr'" in exI)
sorry
lemma alts_simp_bounded_by_sloppy1_version:
@@ -933,8 +954,9 @@
apply(rule allI)
apply(case_tac "s = []")
prefer 2
- apply (metis add_2_eq_Suc' le_imp_less_Suc less_SucI max.strict_coboundedI1 shape_derssimp_seq(2))
- by (metis add.assoc less_Suc_eq max.strict_coboundedI2 plus_1_eq_Suc rders_simp.simps(1) rsize.simps(5))
+ apply (metis add_2_eq_Suc' le_imp_less_Suc less_SucI max.strict_coboundedI1 shape_derssimp_seq)
+ by (metis add.assoc less_Suc_eq less_max_iff_disj plus_1_eq_Suc rders_simp.simps(1) rsize.simps(5))
+
(* apply (simp add: less_SucI shape_derssimp_seq(2))
apply (meson less_SucI less_max_iff_disj)
apply simp
@@ -951,11 +973,34 @@
(*For star related 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)"
+ shows " \<exists>Ss. rders_simp (RSTAR r) [c] = rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))"
apply simp
apply(rule_tac x = "[[c]]" in exI)
apply auto
- done
+ apply(case_tac "rsimp (rder c r)")
+ apply simp
+ apply auto
+ apply(subgoal_tac "rsimp (RSEQ x41 x42) = RSEQ x41 x42")
+ prefer 2
+ apply (metis rsimp_idem)
+ apply(subgoal_tac "rsimp x41 = x41")
+ prefer 2
+ using rsimp_inner_idem1 apply blast
+ apply(subgoal_tac "rsimp x42 = x42")
+ prefer 2
+ using rsimp_inner_idem1 apply blast
+ apply simp
+ apply(subgoal_tac "map rsimp x5 = x5")
+ prefer 2
+ using rsimp_inner_idem3 apply blast
+ apply simp
+ apply(subgoal_tac "rflts x5 = x5")
+ prefer 2
+ using rsimp_inner_idem4 apply blast
+ apply simp
+ using rsimp_inner_idem4 by auto
+
+
lemma rder_rsimp_ALTs_commute:
shows " (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)"
@@ -966,16 +1011,7 @@
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
+
fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list => char list list" where
"star_update c r [] = []"
@@ -983,12 +1019,67 @@
then (s@[c]) # [c] # (star_update c r Ss)
else s # (star_update c r Ss) )"
+lemma star_update_case1:
+ shows "rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # [c] # (star_update c r Ss)"
+
+ by force
+
+lemma star_update_case2:
+ shows "\<not>rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = s # (star_update c r Ss)"
+ by simp
+
+lemma rsimp_alts_idem:
+ shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs (a # [(rsimp (rsimp_ALTs as))] ))"
+ sorry
+
+lemma rsimp_alts_idem2:
+ shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs ((rsimp a) # [(rsimp (rsimp_ALTs as))] ))"
+ sorry
+
+lemma evolution_step1:
+ shows "rsimp
+ (rsimp_ALTs
+ (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) =
+ rsimp
+ (rsimp_ALTs
+ (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # [(rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)))])) "
+ using rsimp_alts_idem by auto
+
+lemma evolution_step2:
+ assumes " rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) =
+ rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))"
+ shows "rsimp
+ (rsimp_ALTs
+ (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) =
+ rsimp
+ (rsimp_ALTs
+ (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # [ rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])) "
+ by (simp add: assms rsimp_alts_idem)
+
+
+(*
+proof (prove)
+goal (1 subgoal):
+ 1. map f (a # s) = f a # map f s
+Auto solve_direct: the current goal can be solved directly with
+ HOL.nitpick_simp(115): map ?f (?x21.0 # ?x22.0) = ?f ?x21.0 # map ?f ?x22.0
+ List.list.map(2): map ?f (?x21.0 # ?x22.0) = ?f ?x21.0 # map ?f ?x22.0
+ List.list.simps(9): map ?f (?x21.0 # ?x22.0) = ?f ?x21.0 # map ?f ?x22.0
+*)
lemma starseq_list_evolution:
fixes r :: rrexp and Ss :: "char list list" and x :: char
shows "rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss) ) =
rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)) )"
apply(induct Ss)
- apply simp
+ apply simp
+ apply(subst List.list.map(2))
+ apply(subst evolution_step2)
+ apply simp
+ apply(case_tac "rnullable (rders_simp r a)")
+ apply(subst star_update_case1)
+ apply simp
+ apply(subst List.list.map)+
+ sledgehammer
sorry
@@ -997,32 +1088,75 @@
= 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"
- oops
+lemma map_der_lambda_composition:
+ shows "map (rder x) (map (\<lambda>s. f s) Ss) = map (\<lambda>s. (rder x (f s))) Ss"
+ by force
+
+lemma ralts_vs_rsimpalts:
+ shows "rsimp (RALTS rs) = rsimp (rsimp_ALTs rs)"
+ sorry
lemma linearity_of_list_of_star_or_starseqs:
fixes r::rrexp and Ss::"char list list" and x::char
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))
+ rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)))"
+ apply(subst rder_rsimp_ALTs_commute)
+ apply(subst map_der_lambda_composition)
+ using starseq_list_evolution
+ apply(rule_tac x = "star_update x r Ss" in exI)
+ apply(subst ralts_vs_rsimpalts)
+ by simp
+
- sorry
+(*certified correctness---does not depend on any previous sorry*)
+lemma star_list_push_der: shows " \<lbrakk>xs \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSTAR r) xs = rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss));
+ xs @ [x] \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow>
+ \<exists>Ss. rders_simp (RSTAR r ) (xs @ [x]) =
+ rsimp (RALTS (map (\<lambda>s1. (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) ) Ss) )"
+ apply(subgoal_tac "\<exists>Ss. rders_simp (RSTAR r) xs = rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))")
+ prefer 2
+ apply blast
+ apply(erule exE)
+ apply(subgoal_tac "rders_simp (RSTAR r) (xs @ [x]) = rsimp (rder x (rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))))")
+ prefer 2
+ using rders_simp_append
+ using rders_simp_one_char apply presburger
+ apply(rule_tac x= "Ss" in exI)
+ apply(subgoal_tac " rsimp (rder x (rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) =
+ rsimp (rsimp (rder x (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))))")
+ prefer 2
+ using inside_simp_removal rsimp_idem apply presburger
+ apply(subgoal_tac "rsimp (rsimp (rder x (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) =
+ rsimp (rsimp (RALTS (map (rder x) (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))))")
+ prefer 2
+ using rder.simps(4) apply presburger
+ apply(subgoal_tac "rsimp (rsimp (RALTS (map (rder x) (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) =
+ rsimp (rsimp (RALTS (map (\<lambda>s1. (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss)))")
+ apply (metis rsimp_idem)
+ by (metis map_der_lambda_composition)
+
+lemma simp_in_lambdas :
+ shows "
+rsimp (RALTS (map (\<lambda>s1. (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) ) Ss) ) =
+rsimp (RALTS (map (\<lambda>s1. (rsimp (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))))) Ss))"
+ by (metis (no_types, lifting) comp_apply list.map_comp map_eq_conv rsimp.simps(2) rsimp_idem)
+
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)"
+ shows "s \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSTAR r) s = rsimp (RALTS( (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
+ apply(simp)
+ apply(subgoal_tac "\<exists>Ss. rders_simp (RSTAR r) (xs @ [x]) =
+ rsimp (RALTS (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))")
+ prefer 2
+ using star_list_push_der apply presburger
+
+
+ sorry
lemma finite_star:
@@ -1067,6 +1201,12 @@
apply (simp add: finite_star)
sorry
+lemma finite_list_of_ders:
+ fixes r
+ shows"\<exists>dersset. ( (finite dersset) \<and> (\<forall>s. (rders_simp r s) \<in> dersset) )"
+ sorry
+
+
unused_thms
lemma seq_ders_shape: