diff -r 210df4cd512b -r 0cce1aee0fb2 thys2/SizeBound6CT.thy --- 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"\dersset. ( (finite dersset) \ (\s. (rders_simp r s) \ dersset) )" - sorry - - @@ -475,6 +470,24 @@ shows "rsimp (rsimp r) = rsimp r" sorry +corollary rsimp_inner_idem1: + shows "rsimp r = RSEQ r1 r2 \ rsimp r1 = r1 \ rsimp r2 = r2" + + sorry + +corollary rsimp_inner_idem2: + shows "rsimp r = RALTS rs \ \r' \ (set rs). rsimp r' = r'" + sorry + +corollary rsimp_inner_idem3: + shows "rsimp r = RALTS rs \ map rsimp rs = rs" + by (meson map_idI rsimp_inner_idem2) + +corollary rsimp_inner_idem4: + shows "rsimp r = RALTS rs \ 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) \ 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 []} \ {RZERO} \ {RONE} \ { (RCHAR c) |c. c \ set (all_chars 255)}" |"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \ (rexp_enum i) \ r2 \ (rexp_enum j) \ i + j = n}" - + lemma finite_sized_rexp_forms_finite_set: shows " \SN. ( \r.( rsize r < N \ r \ SN)) \ (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 " \Ss. rders_simp (RSTAR r) [c] = rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)" + shows " \Ss. rders_simp (RSTAR r) [c] = rsimp (RALTS ( (map (\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 \ rrexp \ 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) \ star_update c r (s # Ss) = (s @ [c]) # [c] # (star_update c r Ss)" + + by force + +lemma star_update_case2: + shows "\rnullable (rders_simp r s) \ 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 (\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 (\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 (\s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = + rsimp (rsimp_ALTs (map (\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 (\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 (\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 (\s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss) ) = rsimp (rsimp_ALTs (map (\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 ( (\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 (\s. f s) Ss) = map (\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 "\Ssa. rsimp (rder x (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) = - rsimp_ALTs (map (\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 (\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 " \xs \ [] \ \Ss. rders_simp (RSTAR r) xs = rsimp (RALTS (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)); + xs @ [x] \ []; xs \ []\ \ + \Ss. rders_simp (RSTAR r ) (xs @ [x]) = + rsimp (RALTS (map (\s1. (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) ) Ss) )" + apply(subgoal_tac "\Ss. rders_simp (RSTAR r) xs = rsimp (RALTS (map (\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 (\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 (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) = + rsimp (rsimp (rder x (RALTS (map (\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 (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) = + rsimp (rsimp (RALTS (map (rder x) (map (\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 (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) = + rsimp (rsimp (RALTS (map (\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 (\s1. (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) ) Ss) ) = +rsimp (RALTS (map (\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 \ [] \ \Ss. rders_simp (RSTAR r) s = rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)" + shows "s \ [] \ \Ss. rders_simp (RSTAR r) s = rsimp (RALTS( (map (\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 "\Ss. rders_simp (RSTAR r) (xs @ [x]) = + rsimp (RALTS (map (\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"\dersset. ( (finite dersset) \ (\s. (rders_simp r s) \ dersset) )" + sorry + + unused_thms lemma seq_ders_shape: