
diff -r cf7a5c863831 -r 6c13f76c070b thys3/ClosedForms.thy
--- a/thys3/ClosedForms.thy	Wed Feb 15 11:52:22 2023 +0000
+++ b/thys3/ClosedForms.thy	Thu Feb 16 23:23:22 2023 +0000
@@ -1,9 +1,20 @@
 theory ClosedForms 
-  imports "HarderProps"
+  imports "BasicIdentities"
 begin
 
+lemma flts_middle0:
+  shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
+  apply(induct rsa)
+  apply simp
+  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
 
+
+lemma simp_flatten_aux0:
+  shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))"
+  by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts)
+  
+
 inductive 
   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
 where
@@ -56,8 +67,44 @@
   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
 
+lemma simp_removes_duplicate1:
+  shows  " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) =  rsimp (RALTS (rsa))"
+and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
+  apply(induct rsa arbitrary: a1)
+     apply simp
+    apply simp
+  prefer 2
+  apply(case_tac "a = aa")
+     apply simp
+    apply simp
+  apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2))
+  apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9))
+  by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2))
+  
+lemma simp_removes_duplicate2:
+  shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))"
+  apply(induct rsb arbitrary: rsa)
+   apply simp
+  using distinct_removes_duplicate_flts apply auto[1]
+  by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1))
 
+lemma simp_removes_duplicate3:
+  shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
+  using simp_removes_duplicate2 by auto
 
+(*
+lemma distinct_removes_middle4:
+  shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"
+  using distinct_removes_middle(1) by fastforce
+*)
+
+(*
+lemma distinct_removes_middle_list:
+  shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"
+  apply(induct x)
+   apply simp
+  by (simp add: distinct_removes_middle3)
+*)
 
 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
   where
@@ -212,6 +259,11 @@
   using grewrites_append apply blast   
   by (meson greal_trans grewrites.simps grewrites_concat)
 
+fun alt_set:: "rrexp \<Rightarrow> rrexp set"
+  where
+  "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))"
+| "alt_set r = {r}"
+
 
 lemma grewrite_cases_middle:
   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 
@@ -226,6 +278,216 @@
   by blast
 
 
+lemma good_singleton:
+  shows "good a \<and> nonalt a  \<Longrightarrow> rflts [a] = [a]"
+  using good.simps(1) k0b by blast
+
+
+
+
+
+
+
+lemma all_that_same_elem:
+  shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>
+       \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset"
+  apply(induct rs)
+   apply simp
+  apply(subgoal_tac "aa = a")
+   apply simp
+  by (metis empty_iff insert_iff list.discI rdistinct.simps(2))
+
+lemma distinct_early_app1:
+  shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
+  apply(induct rs arbitrary: rset rset1)
+   apply simp
+  apply simp
+  apply(case_tac "a \<in> rset1")
+   apply simp
+   apply(case_tac "a \<in> rset")
+    apply simp+
+  
+   apply blast
+  apply(case_tac "a \<in> rset1")
+   apply simp+
+  apply(case_tac "a \<in> rset")
+   apply simp
+   apply (metis insert_subsetI)
+  apply simp
+  by (meson insert_mono)
+
+
+lemma distinct_early_app:
+  shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"
+  apply(induct rsb)
+   apply simp
+  using distinct_early_app1 apply blast
+  by (metis distinct_early_app1 distinct_once_enough empty_subsetI)
+
+
+lemma distinct_eq_interesting1:
+  shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"
+  apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")
+   apply(simp only:)
+  using distinct_early_app apply blast 
+  by (metis append_Cons distinct_early_app rdistinct.simps(2))
+
+
+
+lemma good_flatten_aux_aux1:
+  shows "\<lbrakk> size rs \<ge>2; 
+\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
+       \<Longrightarrow> rdistinct (rs @ rsb) rset =
+           rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
+  apply(induct rs arbitrary: rset)
+   apply simp
+  apply(case_tac "a \<in> rset")
+   apply simp
+   apply(case_tac "rdistinct rs {a}")
+    apply simp
+    apply(subst good_singleton)
+     apply force
+  apply simp
+    apply (meson all_that_same_elem)
+   apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ")
+  prefer 2
+  using k0a rsimp_ALTs.simps(3) apply presburger
+  apply(simp only:)
+  apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ")
+    apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2))
+   apply (meson distinct_eq_interesting1)
+  apply simp
+  apply(case_tac "rdistinct rs {a}")
+  prefer 2
+   apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})")
+  apply(simp only:)
+  apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) =
+           rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset")
+   apply simp
+  apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2))
+  using rsimp_ALTs.simps(3) apply presburger
+  by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left)
+
+
+
+  
+
+lemma good_flatten_aux_aux:
+  shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista; 
+\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
+       \<Longrightarrow> rdistinct (rs @ rsb) rset =
+           rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
+  apply(erule exE)+
+  apply(subgoal_tac "size rs \<ge> 2")
+   apply (metis good_flatten_aux_aux1)
+  by (simp add: Suc_leI length_Cons less_add_Suc1)
+
+
+
+lemma good_flatten_aux:
+  shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO; 
+           \<forall>r\<in>set rsb. good r \<or> r = RZERO;
+     rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {});
+     rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
+     rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {});
+     map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs;
+     rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =
+     rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa));
+     rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =
+     rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk>
+    \<Longrightarrow>    rdistinct (rflts rs @ rflts rsb) rset =
+           rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset"
+  apply simp
+  apply(case_tac "rflts rs ")
+   apply simp
+  apply(case_tac "list")
+   apply simp
+   apply(case_tac "a \<in> rset")
+    apply simp
+  apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2))
+   apply simp
+  apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left)
+  apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")
+   prefer 2
+  apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1)  
+  apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r")
+   prefer 2
+  apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1)  
+  by (smt (verit, ccfv_threshold) good_flatten_aux_aux)
+
+  
+
+
+lemma good_flatten_middle:
+  shows "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO; \<forall>r \<in> set rsa. good r \<or> r = RZERO; \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow>
+rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))"
+  apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 
+map rsimp rs @ map rsimp rsb)) {})")
+  prefer 2
+  apply simp
+  apply(simp only:)
+    apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 
+[rsimp (RALTS rs)] @ map rsimp rsb)) {})")
+  prefer 2
+   apply simp
+  apply(simp only:)
+  apply(subgoal_tac "map rsimp rsa = rsa")
+  prefer 2
+  apply (metis map_idI rsimp.simps(3) test)
+  apply(simp only:)
+  apply(subgoal_tac "map rsimp rsb = rsb")
+   prefer 2
+  apply (metis map_idI rsimp.simps(3) test)
+  apply(simp only:)
+  apply(subst k00)+
+  apply(subgoal_tac "map rsimp rs = rs")
+   apply(simp only:)
+   prefer 2
+  apply (metis map_idI rsimp.simps(3) test)
+  apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = 
+rdistinct (rflts rsa) {} @ rdistinct  (rflts rs @ rflts rsb) (set (rflts rsa))")
+   apply(simp only:)
+  prefer 2
+  using rdistinct_concat_general apply blast
+  apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = 
+rdistinct (rflts rsa) {} @ rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
+   apply(simp only:)
+  prefer 2
+  using rdistinct_concat_general apply blast
+  apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = 
+                     rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
+   apply presburger
+  using good_flatten_aux by blast
+
+
+lemma simp_flatten3:
+  shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
+  apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = 
+                     rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")
+  prefer 2
+   apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0)
+  apply (simp only:)
+  apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = 
+rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))")
+  prefer 2
+   apply (metis map_append simp_flatten_aux0)
+  apply(simp only:)
+  apply(subgoal_tac "rsimp  (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) =
+ rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))")
+  
+   apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0)
+  apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO")
+   apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO")
+    apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO")
+  
+  using good_flatten_middle apply presburger
+  
+  apply (simp add: good1)
+  apply (simp add: good1)
+  apply (simp add: good1)
+
+  done
+
 
 
   
@@ -277,8 +539,10 @@
      apply (simp add: frewrites_alt)
   apply (simp add: frewrites_cons)
    apply (simp add: frewrites_append)
-  by (simp add: frewrites_cons)
-
+  apply (simp add: frewrites_cons)
+  apply (auto simp add: frewrites_cons)
+  using frewrite.intros(1) many_steps_later by blast
+  
 
 lemma gstar0:
   shows "rsa @ (rdistinct rs (set rsa)) \<leadsto>g* rsa @ (rdistinct rs (insert RZERO (set rsa)))"
@@ -380,7 +644,8 @@
   apply(induct r)
   apply simp+
    apply (metis list.set_intros(1))
-  by blast
+  apply blast
+  by simp
   
 
 
@@ -604,8 +869,39 @@
   by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts)
 
 
+lemma basic_regex_property1:
+  shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO"
+  apply(induct r rule: rsimp.induct)
+  apply(auto)
+  apply (metis idiot idiot2 rrexp.distinct(5))
+  by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
 
 
+lemma inside_simp_seq_nullable:
+  shows 
+"\<And>r1 r2.
+       \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2);
+        rnullable r1\<rbrakk>
+       \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) =
+           rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})"
+  apply(case_tac "rsimp r1 = RONE")
+   apply(simp)
+  apply(subst basic_rsimp_SEQ_property1)
+   apply (simp add: idem_after_simp1)
+  apply(case_tac "rsimp r1 = RZERO")
+  
+  using basic_regex_property1 apply blast
+  apply(case_tac "rsimp r2 = RZERO")
+  
+  apply (simp add: basic_rsimp_SEQ_property3)
+  apply(subst idiot2)
+     apply simp+
+  apply(subgoal_tac "rnullable (rsimp r1)")
+   apply simp
+  using rsimp_idem apply presburger
+  using der_simp_nullability by presburger
+  
+
 
 lemma grewrite_ralts:
   shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
@@ -754,7 +1050,7 @@
     apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)
 
    apply (simp add: grewrites_ralts hrewrites_list)
-  by simp
+  by simp_all
 
 lemma interleave_aux1:
   shows " RALT (RSEQ RZERO r1) r h\<leadsto>*  r"
@@ -815,30 +1111,6 @@
 
 
 
-lemma inside_simp_seq_nullable:
-  shows 
-"\<And>r1 r2.
-       \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2);
-        rnullable r1\<rbrakk>
-       \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) =
-           rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})"
-  apply(case_tac "rsimp r1 = RONE")
-   apply(simp)
-  apply(subst basic_rsimp_SEQ_property1)
-   apply (simp add: idem_after_simp1)
-  apply(case_tac "rsimp r1 = RZERO")
-  using basic_regex_property1 apply blast
-  apply(case_tac "rsimp r2 = RZERO")
-  apply (simp add: basic_rsimp_SEQ_property3)
-  apply(subst idiot2)
-     apply simp+
-  apply(subgoal_tac "rnullable (rsimp r1)")
-   apply simp
-  using rsimp_idem apply presburger
-  using der_simp_nullability by presburger
-  
-
-
 lemma inside_simp_removal:
   shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
   apply(induct r)
@@ -852,7 +1124,7 @@
    apply(subgoal_tac "rder x (RALTS xa) h\<leadsto>* rder x (rsimp (RALTS xa))")
   using hrewrites_simpeq apply presburger
   using interleave_star1 simp_hrewrites apply presburger
-  by simp
+  by simp_all
   
 
 
@@ -887,16 +1159,14 @@
   using rders_simp_same_simpders rsimp_idem by auto
 
 lemma repeated_altssimp:
-  shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> 
-           rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =
+  shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =
            rsimp_ALTs (rdistinct (rflts rs) {})"
   by (metis map_idI rsimp.simps(2) rsimp_idem)
 
 
 
 lemma alts_closed_form: 
-  shows "rsimp (rders_simp (RALTS rs) s) = 
-         rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
+  shows "rsimp (rders_simp (RALTS rs) s) = rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
   apply(induct s rule: rev_induct)
    apply simp
   apply simp
@@ -981,11 +1251,15 @@
   apply simp+
   
   using created_by_seq.cases apply blast
-  
-  apply (meson created_by_seq.cases rrexp.distinct(19) rrexp.distinct(21))
-  apply (metis created_by_seq.simps rder.simps(5))
-   apply (smt (verit, ccfv_threshold) created_by_seq.simps list.set_intros(1) list.simps(8) list.simps(9) rder.simps(4) rrexp.distinct(25) rrexp.inject(3))
-  using created_by_seq.intros(1) by force
+      apply(auto)
+  apply (meson created_by_seq.cases rrexp.distinct(23) rrexp.distinct(25))
+  using created_by_seq.simps apply blast
+  apply (meson created_by_seq.simps)
+  using created_by_seq.intros(1) apply blast
+  apply (metis (no_types, lifting) created_by_seq.simps k0a list.set_intros(1) list.simps(8) list.simps(9) rrexp.distinct(31))
+  apply (simp add: created_by_seq.intros(1))
+  using created_by_seq.simps apply blast
+  by (simp add: created_by_seq.intros(1))
 
 lemma createdbyseq_left_creatable:
   shows "created_by_seq (RALT r1 r2) \<Longrightarrow> created_by_seq r1"
@@ -1030,16 +1304,6 @@
   by fastforce
 
 
-fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list" where
-"vsuf [] _ = []"
-|"vsuf (c#cs) r1 = (if (rnullable r1) then  (vsuf cs (rder c r1)) @ [c # cs]
-                                      else  (vsuf cs (rder c r1))
-                   ) "
-
-
-
-
-
 lemma vsuf_prop1:
   shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) 
                                 then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) )
@@ -1071,75 +1335,44 @@
   apply simp
   by (simp add: rders_append)
   
-thm sfau_idem_der
 
-lemma oneCharvsuf:
-  shows "breakHead [rder x (RSEQ r1 r2)] = RSEQ (rder x r1) r2 # map (rders r2)  (vsuf [x] r1)"
-  by simp
-
-
-lemma vsuf_compose2:
-  shows "(map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1)) = 
-          map (rders r2) (vsuf (xs @ [x]) r1)"
-proof(induct xs arbitrary: r1)
-  case Nil
-  then show ?case 
-    by simp
-next
-  case (Cons a xs)
-  have "rnullable (rders r1 xs) \<longrightarrow>        map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) =
-       map (rders r2) (vsuf ((a # xs) @ [x]) r1)"
-  proof
-    assume nullableCond: "rnullable (rders r1 xs)"
-    have "rnullable r1 \<longrightarrow> rder x (rders (rder a r2) xs) = rders (rder a r2) (xs @ [x])"
-        by (simp add: rders_append)
-    show " map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) =
-       map (rders r2) (vsuf ((a # xs) @ [x]) r1)"
-      using \<open>rnullable r1 \<longrightarrow> rder x (rders (rder a r2) xs) = rders (rder a r2) (xs @ [x])\<close> local.Cons by auto
-  qed
-  then have "\<not> rnullable (rders r1 xs) \<longrightarrow> map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = 
-            map (rders r2) (vsuf ((a # xs) @ [x]) r1)"
-    apply simp
-  by (smt (verit, ccfv_threshold) append_Cons append_Nil list.map_comp list.simps(8) list.simps(9) local.Cons rders.simps(1) rders.simps(2) rders_append vsuf.simps(1) vsuf.simps(2))
-  then show ?case 
-    using \<open>rnullable (rders r1 xs) \<longrightarrow> map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = map (rders r2) (vsuf ((a # xs) @ [x]) r1)\<close> by blast
-qed
 
 
 lemma seq_sfau0:
   shows  "sflat_aux (rders (RSEQ r1 r2) s) = (RSEQ (rders r1 s) r2) #
                                        (map (rders r2) (vsuf s r1)) "
-proof(induct s rule: rev_induct)
-  case Nil
-  then show ?case 
-    by simp
-next
-  case (snoc x xs)
-  then have LHS1:"sflat_aux (rders (RSEQ r1 r2) (xs @ [x]))  = sflat_aux (rder x (rders (RSEQ r1 r2) xs)) "
-    by (simp add: rders_append)
-  then have LHS1A: "... = breakHead (map (rder x) (sflat_aux (rders (RSEQ r1 r2) xs)))"
-    using recursively_derseq sfau_idem_der by auto
-  then have LHS1B: "... = breakHead (map (rder x)  (RSEQ (rders r1 xs) r2 # map (rders r2) (vsuf xs r1)))"
-    using snoc by auto
-  then have LHS1C: "... = breakHead (rder x (RSEQ (rders r1 xs) r2) # map (rder x) (map (rders r2) (vsuf xs r1)))"
-    by simp
-  then have LHS1D: "... = breakHead [rder x (RSEQ (rders r1 xs) r2)] @ map (rder x) (map (rders r2) (vsuf xs r1))"
-    by simp
-  then have LHS1E: "... = RSEQ (rder x (rders r1 xs)) r2 # (map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1))"
-    by force
-  then have LHS1F: "... = RSEQ (rder x (rders r1 xs)) r2 # (map (rders r2) (vsuf (xs @ [x]) r1))"
-    using vsuf_compose2 by blast
-  then have LHS1G: "... = RSEQ (rders r1 (xs @ [x])) r2 # (map (rders r2) (vsuf (xs @ [x]) r1))"
-    using rders.simps(1) rders.simps(2) rders_append by presburger
-  then show ?case
-    using LHS1 LHS1A LHS1C LHS1D LHS1E LHS1F snoc by presburger
-qed
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(subst rders_append)+
+  apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) xs)")
+  prefer 2
+  using recursively_derseq1 apply blast
+  apply simp
+  apply(subst sfau_idem_der)
+  
+   apply blast
+  apply(case_tac "rnullable (rders r1 xs)")
+   apply simp
+   apply(subst vsuf_prop1)
+  apply simp
+  apply (simp add: rders_append)
+  apply simp
+  using vsuf_compose1 by blast
 
 
 
 
 
 
+
+
+
+thm sflat.elims
+
+
+
+
+
 lemma sflat_rsimpeq:
   shows "created_by_seq r1 \<Longrightarrow> sflat_aux r1 =  rs \<Longrightarrow> rsimp r1 = rsimp (RALTS rs)"
   apply(induct r1 arbitrary: rs rule:  created_by_seq.induct)
@@ -1225,8 +1458,7 @@
 lemma seq_closed_form_variant: 
   assumes "s \<noteq> []"
   shows "rders_simp (RSEQ r1 r2) s = 
-             rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # 
-        (map (rders_simp r2) (vsuf s r1))))"
+             rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # (map (rders_simp r2) (vsuf s r1))))"
   using assms q seq_closed_form by force
 
 
@@ -1243,20 +1475,9 @@
   "created_by_star (RSEQ ra (RSTAR rb))"
 | "\<lbrakk>created_by_star r1; created_by_star r2\<rbrakk> \<Longrightarrow> created_by_star (RALT r1 r2)"
 
-
-
-fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where
-"star_update c r [] = []"
-|"star_update c r (s # Ss) = (if (rnullable (rders r s)) 
-                                then (s@[c]) # [c] # (star_update c r Ss) 
-                               else   (s@[c]) # (star_update c r Ss) )"
-
-
-fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list"
-  where
-"star_updates [] r Ss = Ss"
-| "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"
-
+fun hElem :: "rrexp  \<Rightarrow> rrexp list" where
+  "hElem (RALT r1 r2) = (hElem r1 ) @ (hElem r2)"
+| "hElem r = [r]"
 
 
 lemma cbs_ders_cbs:
@@ -1277,38 +1498,20 @@
 
 
 
-
 lemma hfau_pushin: 
-  shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))"
-proof(induct r rule: created_by_star.induct)
-  case (1 ra rb)
-  then show ?case by simp
-next
-  case (2 r1 r2)
-  then have "created_by_star (rder c r1)"
-    using cbs_ders_cbs by blast
-  then have "created_by_star (rder c r2)"
-    using "2.hyps"(3) cbs_ders_cbs by auto
-  then show ?case
-    by (simp add: "2.hyps"(2) "2.hyps"(4))
-  qed
-
-(*AALTS [a\x . b.c, b\x .c,  c \x]*)
-(*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*)
-
-lemma stupdates_append: shows 
-"star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)"
-  apply(induct s arbitrary: Ss)
+  shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hElem (map (rder c) (hflat_aux r)))"
+  apply(induct r rule: created_by_star.induct)
    apply simp
+  apply(subgoal_tac "created_by_star (rder c r1)")
+  prefer 2
+  apply(subgoal_tac "created_by_star (rder c r2)")
+  using cbs_ders_cbs apply blast
+  using cbs_ders_cbs apply auto[1]
   apply simp
   done
 
-
-
-
-
 lemma stupdate_induct1:
-  shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
+  shows " concat (map (hElem \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
           map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"
   apply(induct Ss)
    apply simp+
@@ -1317,11 +1520,8 @@
 
 
 lemma stupdates_join_general:
-  shows  "concat 
-            (map hflat_aux (map (rder x) 
-                (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))
-             ) =
-          map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)"
+  shows  "concat (map hElem (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))) =
+           map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)"
   apply(induct xs arbitrary: Ss)
    apply (simp)
   prefer 2
@@ -1341,14 +1541,16 @@
   apply (simp add: star_ders_cbs)
   apply(subst hfau_pushin)
    apply simp
-  apply(subgoal_tac "concat (map hflat_aux (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) =
-                     concat (map hflat_aux (map (rder x) ( map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ")
+  apply(subgoal_tac "concat (map hElem (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) =
+                     concat (map hElem (map (rder x) ( map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ")
    apply(simp only:)
   prefer 2
    apply presburger
   apply(subst stupdates_append[symmetric])
   using stupdates_join_general by blast
 
+
+
 lemma starders_hfau_also1:
   shows "hflat_aux (rders (RSTAR r) (c # xs)) = map (\<lambda>s1. RSEQ (rders r s1) (RSTAR r)) (star_updates xs r [[c]])"
   using star_hfau_induct by force
@@ -1366,7 +1568,7 @@
   apply simp
   apply (metis (no_types, lifting) append_Cons append_eq_append_conv2 gmany_steps_later greal_trans grewrite.intros(2) grewrites_append self_append_conv)
   apply simp
-  by simp
+  by simp_all
   
 
 
@@ -1380,10 +1582,29 @@
 
 lemma hfau_rsimpeq2:
   shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))"
-  apply(induct rule: created_by_star.induct)
+  apply(induct r)
+       apply simp+
+  
+    apply (metis rsimp_seq_equal1)
+  prefer 2
+   apply simp
+  apply(case_tac x)
+   apply simp
+  apply(case_tac "list")
    apply simp
-  apply (metis rsimp.simps(6) rsimp_seq_equal1)
-  using cbs_hfau_rsimpeq1 hflat_aux.simps(1) by presburger
+  
+  apply (metis idem_after_simp1)
+  apply(case_tac "lista")
+  prefer 2
+   apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2))
+  apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))")
+  apply simp
+  apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))")
+  using hflat_aux.simps(1) apply presburger
+  apply simp
+  using cbs_hfau_rsimpeq1 apply(fastforce)
+  by simp
+  
 
 lemma star_closed_form1:
   shows "rsimp (rders (RSTAR r0) (c#s)) = 
@@ -1427,8 +1648,11 @@
   using hrewrites_simpeq srewritescf_alt1 apply fastforce
   using star_closed_form6_hrewrites by blast
 
+
+
+
 lemma stupdate_nonempty:
-  shows "\<forall>s \<in> set  Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []"
+  shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []"
   apply(induct Ss)
   apply simp
   apply(case_tac "rnullable (rders r a)")
@@ -1454,12 +1678,518 @@
 lemma star_closed_form:
   shows "rders_simp (RSTAR r0) (c#s) = 
 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
-  apply(induct s)
+  apply(case_tac s)
    apply simp
    apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem)
   using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger
 
 
-unused_thms
+
+
+fun nupdate :: "char \<Rightarrow> rrexp \<Rightarrow>  (string * nat) option  list \<Rightarrow> (string * nat) option  list" where
+  "nupdate c r [] = []"
+| "nupdate c r (Some (s, Suc n) # Ss) = (if (rnullable (rders r s)) 
+                                          then Some (s@[c], Suc n) # Some ([c], n) # (nupdate c r Ss) 
+                                          else Some ((s@[c]), Suc n)  # (nupdate c r Ss) 
+                                        )"
+| "nupdate c r (Some (s, 0) # Ss) =  (if (rnullable (rders r s)) 
+                                        then Some (s@[c], 0) # None # (nupdate c r Ss) 
+                                        else Some ((s@[c]), 0)  # (nupdate c r Ss) 
+                                      ) "
+| "nupdate c r (None # Ss) = (None # nupdate c r Ss)"
+
+
+fun nupdates :: "char list \<Rightarrow> rrexp \<Rightarrow> (string * nat) option list \<Rightarrow> (string * nat) option list"
+  where
+  "nupdates [] r Ss = Ss"
+| "nupdates (c # cs) r Ss = nupdates cs r (nupdate c r Ss)"
+
+fun ntset :: "rrexp \<Rightarrow> nat \<Rightarrow> string \<Rightarrow> (string * nat) option list" where
+  "ntset r (Suc n)  (c # cs) = nupdates cs r [Some ([c], n)]"
+| "ntset r 0 _ = [None]"
+| "ntset r _ [] = []"
+
+inductive created_by_ntimes :: "rrexp \<Rightarrow> bool" where
+  "created_by_ntimes RZERO"
+| "created_by_ntimes (RSEQ ra (RNTIMES rb n))"
+| "\<lbrakk>created_by_ntimes r1; created_by_ntimes r2\<rbrakk> \<Longrightarrow> created_by_ntimes (RALT r1 r2)"
+| "\<lbrakk>created_by_ntimes r \<rbrakk> \<Longrightarrow> created_by_ntimes (RALT r RZERO)"
+
+fun highest_power_aux :: "(string * nat) option list \<Rightarrow> nat \<Rightarrow> nat" where
+  "highest_power_aux [] n = n"
+| "highest_power_aux (None # rs) n = highest_power_aux rs n"
+| "highest_power_aux (Some (s, n) # rs) m = highest_power_aux rs (max n m)"
+
+fun hpower :: "(string * nat) option list \<Rightarrow> nat" where
+  "hpower rs =  highest_power_aux rs 0"
+                        
+
+lemma nupdate_mono:
+  shows " (highest_power_aux (nupdate c r optlist) m) \<le> (highest_power_aux optlist m)"
+  apply(induct optlist arbitrary: m)
+   apply simp
+  apply(case_tac a)
+   apply simp
+  apply(case_tac aa)
+  apply(case_tac b)
+   apply simp+
+  done
+
+lemma nupdate_mono1:
+  shows "hpower (nupdate c r optlist) \<le> hpower optlist"
+  by (simp add: nupdate_mono)
+
+
+
+lemma cbn_ders_cbn:
+  shows "created_by_ntimes r \<Longrightarrow> created_by_ntimes (rder c r)"
+  apply(induct r rule: created_by_ntimes.induct)
+    apply simp
+
+  using created_by_ntimes.intros(1) created_by_ntimes.intros(2) created_by_ntimes.intros(3) apply presburger
+  
+  apply (metis created_by_ntimes.simps rder.simps(5) rder.simps(7))
+  using created_by_star.intros(1) created_by_star.intros(2) apply auto[1]
+  using created_by_ntimes.intros(1) created_by_ntimes.intros(3) apply auto[1]
+  by (metis (mono_tags, lifting) created_by_ntimes.simps list.simps(8) list.simps(9) rder.simps(1) rder.simps(4))
+
+lemma ntimes_ders_cbn:
+  shows "created_by_ntimes (rders (RSEQ r' (RNTIMES r n)) s)"
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply (simp add: created_by_ntimes.intros(2))
+  apply(subst rders_append)
+  using cbn_ders_cbn by auto
+
+lemma always0:
+  shows "rders RZERO s = RZERO"
+  apply(induct s)
+  by simp+
+
+lemma ntimes_ders_cbn1:
+  shows "created_by_ntimes (rders (RNTIMES r n) (c#s))"
+  apply(case_tac n)
+   apply simp
+  using always0 created_by_ntimes.intros(1) apply auto[1]
+  by (simp add: ntimes_ders_cbn)
+
+
+lemma ntimes_hfau_pushin: 
+  shows "created_by_ntimes r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))"
+  apply(induct r rule: created_by_ntimes.induct)
+  apply simp+
+  done
+
+
+abbreviation
+  "opterm r SN \<equiv>     case SN of
+                                Some (s, n) \<Rightarrow> RSEQ (rders r s) (RNTIMES r n)
+                            |   None \<Rightarrow> RZERO
+                     
+              
+"
+
+fun nonempty_string :: "(string * nat) option \<Rightarrow> bool" where
+  "nonempty_string None = True"
+| "nonempty_string (Some ([], n)) = False"
+| "nonempty_string (Some (c#s, n)) = True"
+
+
+lemma nupdate_nonempty:
+  shows "\<lbrakk>\<forall>opt \<in> set Ss. nonempty_string opt \<rbrakk> \<Longrightarrow> \<forall>opt \<in> set (nupdate c r Ss). nonempty_string opt"
+  apply(induct c r Ss rule: nupdate.induct)
+     apply(auto)
+  apply (metis Nil_is_append_conv neq_Nil_conv nonempty_string.simps(3))
+  by (metis Nil_is_append_conv neq_Nil_conv nonempty_string.simps(3))
+
+
+
+lemma nupdates_nonempty:
+  shows "\<lbrakk>\<forall>opt \<in> set Ss. nonempty_string opt \<rbrakk> \<Longrightarrow> \<forall>opt \<in> set (nupdates s r Ss). nonempty_string opt"
+  apply(induct s arbitrary: Ss)
+   apply simp
+  apply simp
+  using nupdate_nonempty by presburger
+
+lemma nullability1: shows "rnullable (rders r s) = rnullable (rders_simp r s)"
+  by (metis der_simp_nullability rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders)
+
+lemma nupdate_induct1:
+  shows 
+  "concat (map (hflat_aux \<circ> (rder c \<circ> (opterm r)))  sl ) = 
+   map (opterm r) (nupdate c r sl)"
+  apply(induct sl)
+   apply simp
+  apply(simp add: rders_append)
+  apply(case_tac "a")
+   apply simp+
+  apply(case_tac "aa")
+  apply(case_tac "b")
+  apply(case_tac "rnullable (rders r ab)")
+  apply(subgoal_tac "rnullable (rders_simp r ab)")
+    apply simp
+  using rders.simps(1) rders.simps(2) rders_append apply presburger
+  using nullability1 apply blast
+   apply simp
+  using rders.simps(1) rders.simps(2) rders_append apply presburger
+  apply simp
+  using rders.simps(1) rders.simps(2) rders_append by presburger
+
+
+lemma nupdates_join_general:
+  shows  "concat (map hflat_aux (map (rder x) (map (opterm r) (nupdates xs r Ss))  )) =
+           map (opterm r) (nupdates (xs @ [x]) r Ss)"
+  apply(induct xs arbitrary: Ss)
+   apply (simp)
+  prefer 2
+   apply auto[1]
+  using nupdate_induct1 by blast
+
+
+lemma nupdates_join_general1:
+  shows  "concat (map (hflat_aux \<circ> (rder x) \<circ> (opterm r)) (nupdates xs r Ss)) =
+           map (opterm r) (nupdates (xs @ [x]) r Ss)"
+  by (metis list.map_comp nupdates_join_general)
+
+lemma nupdates_append: shows 
+"nupdates (s @ [c]) r Ss = nupdate c r (nupdates s r Ss)"
+  apply(induct s arbitrary: Ss)
+   apply simp
+  apply simp
+  done
+
+lemma nupdates_mono:
+  shows "highest_power_aux (nupdates s r optlist) m \<le> highest_power_aux optlist m"
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(subst nupdates_append)
+  by (meson le_trans nupdate_mono)
+
+lemma nupdates_mono1:
+  shows "hpower (nupdates s r optlist) \<le> hpower optlist"
+  by (simp add: nupdates_mono)
+
+
+(*"\<forall>r \<in> set (nupdates s r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"*)
+lemma nupdates_mono2:
+  shows "hpower (nupdates s r [Some ([c], n)]) \<le> n"
+  by (metis highest_power_aux.simps(1) highest_power_aux.simps(3) hpower.simps max_nat.right_neutral nupdates_mono1)
+
+lemma hpow_arg_mono:
+  shows "m \<ge> n \<Longrightarrow> highest_power_aux rs m \<ge> highest_power_aux rs n"
+  apply(induct rs arbitrary: m n)
+   apply simp
+  apply(case_tac a)
+   apply simp
+  apply(case_tac aa)
+  apply simp
+  done
+
+
+lemma hpow_increase:
+  shows "highest_power_aux (a # rs') m \<ge> highest_power_aux rs' m"
+  apply(case_tac a)
+   apply simp
+  apply simp
+  apply(case_tac aa)
+  apply(case_tac b)
+   apply simp+
+  apply(case_tac "Suc nat > m")
+  using hpow_arg_mono max.cobounded2 apply blast
+  using hpow_arg_mono max.cobounded2 by blast
+
+lemma hpow_append:
+  shows "highest_power_aux (rsa @ rsb) m  = highest_power_aux rsb (highest_power_aux rsa m)"
+  apply (induct rsa arbitrary: rsb m)
+   apply simp
+  apply simp
+  apply(case_tac a)
+   apply simp
+  apply(case_tac aa)
+  apply simp
+  done
+
+lemma hpow_aux_mono:
+  shows "highest_power_aux (rsa @ rsb) m \<ge> highest_power_aux rsb m"
+  apply(induct rsa arbitrary: rsb rule: rev_induct)
+  apply simp
+  apply simp
+  using hpow_increase order.trans by blast
+ 
+
+
+
+lemma hpow_mono:
+  shows "hpower (rsa @ rsb) \<le> n \<Longrightarrow> hpower rsb \<le> n"
+  apply(induct rsb arbitrary: rsa)
+   apply simp
+  apply(subgoal_tac "hpower rsb \<le> n")
+  apply simp
+  apply (metis dual_order.trans hpow_aux_mono)
+  by (metis hpow_append hpow_increase hpower.simps nat_le_iff_add trans_le_add1)
+
+
+lemma hpower_rs_elems_aux:
+  shows "highest_power_aux rs k \<le> n \<Longrightarrow> \<forall>r\<in>set rs. r = None \<or> (\<exists>s' m. r = Some (s', m) \<and> m \<le> n)"
+apply(induct rs k arbitrary: n rule: highest_power_aux.induct)
+    apply(auto)
+  by (metis dual_order.trans highest_power_aux.simps(1) hpow_append hpow_aux_mono linorder_le_cases max.absorb1 max.absorb2)
+
 
+lemma hpower_rs_elems:
+  shows "hpower rs \<le> n \<Longrightarrow> \<forall>r \<in> set rs. r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"
+  by (simp add: hpower_rs_elems_aux)
+
+lemma nupdates_elems_leqn:
+  shows "\<forall>r \<in> set (nupdates s r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"
+  by (meson hpower_rs_elems nupdates_mono2)
+
+lemma ntimes_hfau_induct:
+  shows "hflat_aux (rders (RSEQ (rder c r) (RNTIMES r n)) s) =   
+      map (opterm r) (nupdates s r [Some ([c], n)])"
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(subst rders_append)+
+  apply simp
+  apply(subst nupdates_append)
+  apply(subgoal_tac "created_by_ntimes (rders (RSEQ (rder c r) (RNTIMES r n)) xs)")
+  prefer 2
+  apply (simp add: ntimes_ders_cbn)
+  apply(subst ntimes_hfau_pushin)
+   apply simp
+  apply(subgoal_tac "concat (map hflat_aux (map (rder x) (hflat_aux (rders (RSEQ (rder c r) (RNTIMES r n)) xs)))) =
+                     concat (map hflat_aux (map (rder x) ( map (opterm r) (nupdates xs r [Some ([c], n)])))) ")
+   apply(simp only:)
+  prefer 2
+   apply presburger
+  apply(subst nupdates_append[symmetric])  
+  using nupdates_join_general by blast
+
+
+(*nupdates s r [Some ([c], n)]*)
+lemma ntimes_ders_hfau_also1:
+  shows "hflat_aux (rders (RNTIMES r (Suc n)) (c # xs)) = map (opterm r) (nupdates xs r [Some ([c], n)])"
+  using ntimes_hfau_induct by force
+
+
+
+lemma hfau_rsimpeq2_ntimes:
+  shows "created_by_ntimes r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))"
+  apply(induct r)
+       apply simp+
+  
+    apply (metis rsimp_seq_equal1)
+  prefer 2
+   apply simp
+  apply(case_tac x)
+   apply simp
+  apply(case_tac "list")
+   apply simp
+  
+  apply (metis idem_after_simp1)
+  apply(case_tac "lista")
+  prefer 2
+   apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2))
+  apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))")
+  apply simp
+  apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))")
+  using hflat_aux.simps(1) apply presburger
+  apply simp
+  using cbs_hfau_rsimpeq1 apply(fastforce)
+  by simp
+  
+
+lemma ntimes_closed_form1:
+  shows "rsimp (rders (RNTIMES r (Suc n)) (c#s)) = 
+rsimp ( ( RALTS (  map (opterm r) (nupdates s r [Some ([c], n)]) )))"
+  apply(subgoal_tac "created_by_ntimes (rders (RNTIMES r (Suc n)) (c#s))")
+   apply(subst hfau_rsimpeq2_ntimes)
+  apply linarith
+  using ntimes_ders_hfau_also1 apply auto[1]
+  using ntimes_ders_cbn1 by blast
+
+
+lemma ntimes_closed_form2:
+  shows  "rsimp (rders_simp (RNTIMES r (Suc n)) (c#s) ) = 
+rsimp ( ( RALTS ( (map (opterm r ) (nupdates s r [Some ([c], n)]) ) )))"
+  by (metis list.distinct(1) ntimes_closed_form1 rders_simp_same_simpders rsimp_idem)
+
+
+lemma ntimes_closed_form3:
+  shows  "rsimp (rders_simp (RNTIMES r n) (c#s)) =   (rders_simp (RNTIMES r n) (c#s))"
+  by (metis list.distinct(1) rders_simp_same_simpders rsimp_idem)
+
+
+lemma ntimes_closed_form4:
+  shows " (rders_simp (RNTIMES r (Suc n)) (c#s)) = 
+rsimp ( ( RALTS ( (map (opterm r ) (nupdates s r [Some ([c], n)]) )  )))"
+  using ntimes_closed_form2 ntimes_closed_form3 
+  by metis
+
+
+
+
+lemma ntimes_closed_form5:
+  shows " rsimp (  RALTS (map (\<lambda>s1. RSEQ (rders r0 s1) (RNTIMES r n) )         Ss)) = 
+          rsimp (  RALTS (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r n)) ) Ss))"
+  by (smt (verit, ccfv_SIG) list.map_comp map_eq_conv o_apply simp_flatten_aux0)
+
+
+
+lemma ntimes_closed_form6_hrewrites:
+  shows "  
+(map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss )
+ scf\<leadsto>*
+(map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss )"
+  apply(induct Ss)
+  apply simp
+  apply (simp add: ss1)
+  by (metis (no_types, lifting) list.simps(9) rsimp.simps(1) rsimp_idem simp_hrewrites ss2)
+
+
+
+lemma ntimes_closed_form6:
+  shows " rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss )))) = 
+          rsimp ( ( RALTS ( (map (\<lambda>s1.  (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss ))))"
+  apply(subgoal_tac " map (\<lambda>s1.  (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss  scf\<leadsto>*
+                      map (\<lambda>s1.  rsimp (RSEQ  (rders r0 s1) (RNTIMES r0 n)) ) Ss ")
+  using hrewrites_simpeq srewritescf_alt1 apply fastforce
+  using ntimes_closed_form6_hrewrites by blast
+
+abbreviation
+  "optermsimp r SN \<equiv>     case SN of
+                                Some (s, n) \<Rightarrow> RSEQ (rders_simp r s) (RNTIMES r n)
+                            |   None \<Rightarrow> RZERO
+                     
+              
+"
+
+abbreviation
+  "optermOsimp r SN \<equiv>     case SN of
+                                Some (s, n) \<Rightarrow> rsimp (RSEQ (rders r s) (RNTIMES r n))
+                            |   None \<Rightarrow> RZERO
+                     
+              
+"
+
+abbreviation
+  "optermosimp r SN \<equiv> case SN of
+                              Some (s, n) \<Rightarrow> RSEQ (rsimp (rders r s)) (RNTIMES r n)
+                            | None \<Rightarrow> RZERO
+"
+
+lemma ntimes_closed_form51:
+  shows "rsimp (RALTS (map (opterm r) (nupdates s r [Some ([c], n)]))) =
+         rsimp (RALTS (map (rsimp \<circ> (opterm r)) (nupdates s r [Some ([c], n)])))"
+  by (metis map_map simp_flatten_aux0)
+
+
+
+lemma osimp_Osimp:
+  shows " nonempty_string sn \<Longrightarrow> optermosimp r sn = optermsimp r sn"
+  apply(induct rule: nonempty_string.induct)
+  apply force
+   apply auto[1]
+  apply simp
+  by (metis list.distinct(1) rders.simps(2) rders_simp.simps(2) rders_simp_same_simpders)
+
+
+
+lemma osimp_Osimp_list:
+  shows "\<forall>sn \<in> set snlist. nonempty_string sn \<Longrightarrow> map (optermosimp r) snlist = map (optermsimp r) snlist"
+  by (simp add: osimp_Osimp)
+
+
+lemma ntimes_closed_form8:
+  shows  
+"rsimp (RALTS (map (optermosimp r) (nupdates s r [Some ([c], n)]))) =
+ rsimp (RALTS (map (optermsimp r) (nupdates s r [Some ([c], n)])))"
+  apply(subgoal_tac "\<forall>opt \<in> set (nupdates s r [Some ([c], n)]). nonempty_string opt")
+  using osimp_Osimp_list apply presburger
+  by (metis list.distinct(1) list.set_cases nonempty_string.simps(3) nupdates_nonempty set_ConsD)
+
+
+
+lemma ntimes_closed_form9aux:
+  shows "\<forall>snopt \<in> set (nupdates s r [Some ([c], n)]). nonempty_string snopt"
+  by (metis list.distinct(1) list.set_cases nonempty_string.simps(3) nupdates_nonempty set_ConsD)
+
+lemma ntimes_closed_form9aux1:
+  shows  "\<forall>snopt \<in> set snlist. nonempty_string snopt \<Longrightarrow> 
+rsimp (RALTS (map (optermosimp r) snlist)) =
+rsimp (RALTS (map (optermOsimp r) snlist))"
+  apply(induct snlist)
+   apply simp+
+  apply(case_tac "a")
+   apply simp+
+  by (smt (z3) case_prod_conv idem_after_simp1 map_eq_conv nonempty_string.elims(2) o_apply option.simps(4) option.simps(5) rsimp.simps(1) rsimp.simps(7) rsimp_idem)
+  
+
+
+
+lemma ntimes_closed_form9:
+  shows  
+"rsimp (RALTS (map (optermosimp r) (nupdates s r [Some ([c], n)]))) =
+ rsimp (RALTS (map (optermOsimp r) (nupdates s r [Some ([c], n)])))"
+  using ntimes_closed_form9aux ntimes_closed_form9aux1 by presburger
+
+
+lemma ntimes_closed_form10rewrites_aux:
+  shows "  map (rsimp \<circ> (opterm r)) optlist scf\<leadsto>* 
+           map (optermOsimp r)      optlist"
+  apply(induct optlist)
+   apply simp
+   apply (simp add: ss1)
+  apply simp
+  apply(case_tac a)
+  using ss2 apply fastforce
+  using ss2 by force
+  
+
+lemma ntimes_closed_form10rewrites:
+  shows "  map (rsimp \<circ> (opterm r)) (nupdates s r [Some ([c], n)]) scf\<leadsto>* 
+           map (optermOsimp r) (nupdates s r [Some ([c], n)])"
+  using ntimes_closed_form10rewrites_aux by blast
+
+lemma ntimes_closed_form10:
+  shows "rsimp (RALTS (map (rsimp \<circ> (opterm r)) (nupdates s r [Some ([c], n)]))) = 
+         rsimp (RALTS (map (optermOsimp r) (nupdates s r [Some ([c], n)])))"
+  by (smt (verit, best) case_prod_conv hpower_rs_elems map_eq_conv nupdates_mono2 o_apply option.case(2) option.simps(4) rsimp.simps(3))
+
+
+lemma rders_simp_cons:
+  shows "rders_simp r (c # s) = rders_simp (rsimp (rder c r)) s"
+  by simp
+
+lemma rder_ntimes:
+  shows "rder c (RNTIMES r (Suc n)) = RSEQ (rder c r) (RNTIMES r n)"
+  by simp
+
+
+lemma ntimes_closed_form:
+  shows "rders_simp (RNTIMES r0 (Suc n)) (c#s) = 
+rsimp ( RALTS ( (map (optermsimp r0 ) (nupdates s r0 [Some ([c], n)]) ) ))"
+  apply (subst rders_simp_cons)
+  apply(subst rder_ntimes)  
+  using ntimes_closed_form10 ntimes_closed_form4 ntimes_closed_form51 ntimes_closed_form8 ntimes_closed_form9 by force
+
+
+
+
+
+
+(*
+lemma ntimes_closed_form:
+  assumes "s \<noteq> []"
+  shows "rders_simp (RNTIMES r (Suc n)) s = 
+rsimp ( RALTS  (     map 
+                     (\<lambda> optSN. case optSN of
+                                Some (s, n) \<Rightarrow> RSEQ (rders_simp r s) (RNTIMES r n)
+                            |   None \<Rightarrow> RZERO
+                     ) 
+                     (ntset r n s) 
+               )
+      )"
+  
+*)
 end
\ No newline at end of file




