
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"\<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:




