lexing: comparison thys2/SizeBound6CT.thy

equal deleted inserted replaced

-:210df4cd512b
+:0cce1aee0fb2
 |   "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
+*)
 datatype rrexp =
 RZERO
 | RONE
 | RCHAR char
 apply(erule exE)+
 apply simp
 apply simp
 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
 lemma rsimp_idem:
 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)
 lemma head_one_more_dersimp:
 lemma nullable_seq_with_list1:
 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 ^^^^^^^^^^^^^^^^*)
 lemma nullable_seq_with_list:
 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}"
 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
 apply(subgoal_tac "\<exists>Nr'. \<forall>s. rsize (RSEQ  (rders_simp r1 s) r2) \<le> Nr'")
 prefer 2
 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:
 shows "\<forall>s. rsize (rsimp (RALTS  ((RSEQ (rders_simp r1 s) r2) #
 (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s))) )) \<le>
 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 (metis add_2_eq_Suc' le_imp_less_Suc less_SucI max.strict_coboundedI1 shape_derssimp_seq(2))
+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 max.strict_coboundedI2 plus_1_eq_Suc rders_simp.simps(1) rsize.simps(5))
+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
 done*)
 apply simp
 done*)
 (*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)"
 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
 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list => char list list" where
 "star_update c r [] = []"
 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s))
 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(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
 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:
+lemma map_der_lambda_composition:
-shows "rder x (RSEQ r1 r2) = RSEQ r3 r4"
+shows "map (rder x) (map (\<lambda>s. f s) Ss) = map (\<lambda>s. (rder x (f s))) Ss"
-oops
+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)"
+rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)))"
-apply(simp add: rder_rsimp_ALTs_commute)
+apply(subst rder_rsimp_ALTs_commute)
-apply(induct Ss)
+apply(subst map_der_lambda_composition)
-apply simp
+using starseq_list_evolution
-apply (metis list.simps(8) rsimp_ALTs.simps(1))
+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(subgoal_tac "\<exists>Ss. rders_simp (RSTAR r) (xs @ [x]) =
-apply(simp add: rders_simp_append)
+rsimp (RALTS (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))")
-using linearity_of_list_of_star_or_starseqs by blast
+prefer 2
+using star_list_push_der apply presburger
+sorry
 lemma finite_star:
 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 )
 \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3"
 prefer 2
 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:
 shows "E"

changeset 434	0cce1aee0fb2
parent 433	210df4cd512b
child 435	65e786a58365
child 436	222333d2bdc2