Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys3/ClosedForms.thy
changeset 555 aecf1ddf3541
parent 554 15d182ffbc76
child 557 812e5d112f49
equal deleted inserted replaced
554:15d182ffbc76 555:aecf1ddf3541 
     1 theory ClosedForms 
     1 theory ClosedForms 
     2   imports "BasicIdentities"
 
     2   imports "HarderProps"
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 
     5 
     6 lemma flts_middle0:
 
       
     7   shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
 
       
     8   apply(induct rsa)
 
       
     9   apply simp
 
       
    10   by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
    11 
       
    12 
       
    13 
       
    14 lemma simp_flatten_aux0:
 
       
    15   shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))"
 
       
    16   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)
 
       
    17   
       
    18 
     6 
    19 inductive 
     7 inductive 
    20   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
 
     8   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
 
    21 where
 
     9 where
 
    22   "RSEQ  RZERO r2 h\<leadsto> RZERO"
 
    10   "RSEQ  RZERO r2 h\<leadsto> RZERO"
 
    66 lemma hrewrites_seq_contexts:
 
    54 lemma hrewrites_seq_contexts:
 
    67   shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4"
 
    55   shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4"
 
    68   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
    56   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
    69 
    57 
    70 
    58 
    71 lemma simp_removes_duplicate1:
 
    59 
    72   shows  " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) =  rsimp (RALTS (rsa))"
 
    60 
    73 and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
 
       
    74   apply(induct rsa arbitrary: a1)
 
       
    75      apply simp
 
       
    76     apply simp
 
       
    77   prefer 2
 
       
    78   apply(case_tac "a = aa")
 
       
    79      apply simp
 
       
    80     apply simp
 
       
    81   apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2))
 
       
    82   apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9))
 
       
    83   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))
 
       
    84   
       
    85 lemma simp_removes_duplicate2:
 
       
    86   shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))"
 
       
    87   apply(induct rsb arbitrary: rsa)
 
       
    88    apply simp
 
       
    89   using distinct_removes_duplicate_flts apply auto[1]
 
       
    90   by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1))
 
       
    91 
       
    92 lemma simp_removes_duplicate3:
 
       
    93   shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
 
       
    94   using simp_removes_duplicate2 by auto
 
       
    95 
       
    96 (*
 
       
    97 lemma distinct_removes_middle4:
 
       
    98   shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"
 
       
    99   using distinct_removes_middle(1) by fastforce
 
       
   100 *)
 
       
   101 
       
   102 (*
 
       
   103 lemma distinct_removes_middle_list:
 
       
   104   shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"
 
       
   105   apply(induct x)
 
       
   106    apply simp
 
       
   107   by (simp add: distinct_removes_middle3)
 
       
   108 *)
 
       
   109 
    61 
   110 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
 
    62 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
 
   111   where
 
    63   where
 
   112   "(RZERO # rs) \<leadsto>f rs"
 
    64   "(RZERO # rs) \<leadsto>f rs"
 
   113 | "((RALTS rs) # rsa) \<leadsto>f (rs @ rsa)"
 
    65 | "((RALTS rs) # rsa) \<leadsto>f (rs @ rsa)"
 
   258    apply(case_tac rs)
 
   210    apply(case_tac rs)
 
   259     apply simp
 
   211     apply simp
 
   260   using grewrites_append apply blast   
   212   using grewrites_append apply blast   
   261   by (meson greal_trans grewrites.simps grewrites_concat)
 
   213   by (meson greal_trans grewrites.simps grewrites_concat)
 
   262 
   214 
   263 fun alt_set:: "rrexp \<Rightarrow> rrexp set"
 
       
   264   where
 
       
   265   "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))"
 
       
   266 | "alt_set r = {r}"
 
       
   267 
       
   268 
   215 
   269 lemma grewrite_cases_middle:
 
   216 lemma grewrite_cases_middle:
 
   270   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 
   217   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 
   271 (\<exists>rsa rsb rsc. rs1 =  (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or>
 
   218 (\<exists>rsa rsb rsc. rs1 =  (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or>
 
   272 (\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc) \<or>
 
   219 (\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc) \<or>
 
   276   apply blast
 
   223   apply blast
 
   277   apply (metis append_Cons append_Nil)
 
   224   apply (metis append_Cons append_Nil)
 
   278   apply (metis append_Cons)
 
   225   apply (metis append_Cons)
 
   279   by blast
 
   226   by blast
 
   280 
   227 
   281 
       
   282 lemma good_singleton:
 
       
   283   shows "good a \<and> nonalt a  \<Longrightarrow> rflts [a] = [a]"
 
       
   284   using good.simps(1) k0b by blast
 
       
   285 
       
   286 
       
   287 
       
   288 
       
   289 
       
   290 
       
   291 
       
   292 
       
   293 lemma distinct_early_app1:
 
       
   294   shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
 
       
   295   apply(induct rs arbitrary: rset rset1)
 
       
   296    apply simp
 
       
   297   apply simp
 
       
   298   apply(case_tac "a \<in> rset1")
 
       
   299    apply simp
 
       
   300    apply(case_tac "a \<in> rset")
 
       
   301     apply simp+
 
       
   302   
       
   303    apply blast
 
       
   304   apply(case_tac "a \<in> rset1")
 
       
   305    apply simp+
 
       
   306   apply(case_tac "a \<in> rset")
 
       
   307    apply simp
 
       
   308    apply (metis insert_subsetI)
 
       
   309   apply simp
 
       
   310   by (meson insert_mono)
 
       
   311 
       
   312 
       
   313 lemma distinct_early_app:
 
       
   314   shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"
 
       
   315   apply(induct rsb)
 
       
   316    apply simp
 
       
   317   using distinct_early_app1 apply blast
 
       
   318   by (metis distinct_early_app1 distinct_once_enough empty_subsetI)
 
       
   319 
       
   320 
       
   321 lemma distinct_eq_interesting1:
 
       
   322   shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"
 
       
   323   apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")
 
       
   324    apply(simp only:)
 
       
   325   using distinct_early_app apply blast 
       
   326   by (metis append_Cons distinct_early_app rdistinct.simps(2))
 
       
   327 
       
   328 
       
   329 
       
   330 lemma good_flatten_aux_aux1:
 
       
   331   shows "\<lbrakk> size rs \<ge>2; 
       
   332 \<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>
 
       
   333        \<Longrightarrow> rdistinct (rs @ rsb) rset =
 
       
   334            rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
 
       
   335   apply(induct rs arbitrary: rset)
 
       
   336    apply simp
 
       
   337   apply(case_tac "a \<in> rset")
 
       
   338    apply simp
 
       
   339    apply(case_tac "rdistinct rs {a}")
 
       
   340     apply simp
 
       
   341     apply(subst good_singleton)
 
       
   342      apply force
 
       
   343   apply simp
 
       
   344     apply (meson all_that_same_elem)
 
       
   345    apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ")
 
       
   346   prefer 2
 
       
   347   using k0a rsimp_ALTs.simps(3) apply presburger
 
       
   348   apply(simp only:)
 
       
   349   apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ")
 
       
   350     apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2))
 
       
   351    apply (meson distinct_eq_interesting1)
 
       
   352   apply simp
 
       
   353   apply(case_tac "rdistinct rs {a}")
 
       
   354   prefer 2
 
       
   355    apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})")
 
       
   356   apply(simp only:)
 
       
   357   apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) =
 
       
   358            rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset")
 
       
   359    apply simp
 
       
   360   apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2))
 
       
   361   using rsimp_ALTs.simps(3) apply presburger
 
       
   362   by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left)
 
       
   363 
       
   364 
       
   365 
       
   366   
       
   367 
       
   368 lemma good_flatten_aux_aux:
 
       
   369   shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista; 
       
   370 \<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>
 
       
   371        \<Longrightarrow> rdistinct (rs @ rsb) rset =
 
       
   372            rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
 
       
   373   apply(erule exE)+
 
       
   374   apply(subgoal_tac "size rs \<ge> 2")
 
       
   375    apply (metis good_flatten_aux_aux1)
 
       
   376   by (simp add: Suc_leI length_Cons less_add_Suc1)
 
       
   377 
       
   378 
       
   379 
       
   380 lemma good_flatten_aux:
 
       
   381   shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO; 
       
   382            \<forall>r\<in>set rsb. good r \<or> r = RZERO;
 
       
   383      rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {});
 
       
   384      rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
 
       
   385      rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {});
 
       
   386      map rsimp rsa = rsa; 
       
   387      map rsimp rsb = rsb; 
       
   388      map rsimp rs = rs;
 
       
   389      rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =
 
       
   390      rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa));
 
       
   391      rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =
 
       
   392      rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk>
 
       
   393     \<Longrightarrow>    rdistinct (rflts rs @ rflts rsb) rset =
 
       
   394            rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset"
 
       
   395   apply simp
 
       
   396   apply(case_tac "rflts rs ")
 
       
   397    apply simp
 
       
   398   apply(case_tac "list")
 
       
   399    apply simp
 
       
   400    apply(case_tac "a \<in> rset")
 
       
   401     apply simp
 
       
   402   apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2))
 
       
   403    apply simp
 
       
   404   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)
 
       
   405   apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")
 
       
   406    prefer 2
 
       
   407   apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1)  
       
   408   apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r")
 
       
   409    prefer 2
 
       
   410   apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1)  
       
   411   by (smt (verit, ccfv_threshold) good_flatten_aux_aux)
 
       
   412 
       
   413   
       
   414 
       
   415 
       
   416 lemma good_flatten_middle:
 
       
   417   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>
 
       
   418 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))"
 
       
   419   apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 
       
   420 map rsimp rs @ map rsimp rsb)) {})")
 
       
   421   prefer 2
 
       
   422   apply simp
 
       
   423   apply(simp only:)
 
       
   424     apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 
       
   425 [rsimp (RALTS rs)] @ map rsimp rsb)) {})")
 
       
   426   prefer 2
 
       
   427    apply simp
 
       
   428   apply(simp only:)
 
       
   429   apply(subgoal_tac "map rsimp rsa = rsa")
 
       
   430   prefer 2
 
       
   431   apply (metis map_idI rsimp.simps(3) test)
 
       
   432   apply(simp only:)
 
       
   433   apply(subgoal_tac "map rsimp rsb = rsb")
 
       
   434    prefer 2
 
       
   435   apply (metis map_idI rsimp.simps(3) test)
 
       
   436   apply(simp only:)
 
       
   437   apply(subst flts_append)+
 
       
   438   apply(subgoal_tac "map rsimp rs = rs")
 
       
   439    apply(simp only:)
 
       
   440    prefer 2
 
       
   441   apply (metis map_idI rsimp.simps(3) test)
 
       
   442   apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = 
       
   443 rdistinct (rflts rsa) {} @ rdistinct  (rflts rs @ rflts rsb) (set (rflts rsa))")
 
       
   444    apply(simp only:)
 
       
   445   prefer 2
 
       
   446   using rdistinct_concat_general apply blast
 
       
   447   apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = 
       
   448 rdistinct (rflts rsa) {} @ rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
 
       
   449    apply(simp only:)
 
       
   450   prefer 2
 
       
   451   using rdistinct_concat_general apply blast
 
       
   452   apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = 
       
   453                      rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
 
       
   454    apply presburger
 
       
   455   using good_flatten_aux by blast
 
       
   456 
       
   457 
       
   458 
       
   459 lemma simp_flatten3:
 
       
   460   shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
 
       
   461   apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = 
       
   462                      rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")
 
       
   463   prefer 2
 
       
   464    apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0)
 
       
   465   apply (simp only:)
 
       
   466   apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = 
       
   467 rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))")
 
       
   468   prefer 2
 
       
   469    apply (metis map_append simp_flatten_aux0)
 
       
   470   apply(simp only:)
 
       
   471   apply(subgoal_tac "rsimp  (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) =
 
       
   472  rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))")
 
       
   473   
       
   474    apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0)
 
       
   475   apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO")
 
       
   476    apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO")
 
       
   477     apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO")
 
       
   478   
       
   479   using good_flatten_middle apply presburger
 
       
   480   
       
   481   apply (simp add: good1)
 
       
   482   apply (simp add: good1)
 
       
   483   apply (simp add: good1)
 
       
   484 
       
   485   done
 
       
   486 
   228 
   487 
   229 
   488 
   230 
   489   
   231   
   490 
   232 
  1282 lemma sfau_head:
 
  1024 lemma sfau_head:
 
  1283   shows " created_by_seq r \<Longrightarrow> \<exists>ra rb rs. sflat_aux r = RSEQ ra rb # rs"
 
  1025   shows " created_by_seq r \<Longrightarrow> \<exists>ra rb rs. sflat_aux r = RSEQ ra rb # rs"
 
  1284   apply(induction r rule: created_by_seq.induct)
 
  1026   apply(induction r rule: created_by_seq.induct)
 
  1285   apply simp
 
  1027   apply simp
 
  1286   by fastforce
 
  1028   by fastforce
 
       
  1029 
       
  1030 
       
  1031 fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list" where
 
       
  1032 "vsuf [] _ = []"
 
       
  1033 |"vsuf (c#cs) r1 = (if (rnullable r1) then  (vsuf cs (rder c r1)) @ [c # cs]
 
       
  1034                                       else  (vsuf cs (rder c r1))
 
       
  1035                    ) "
 
       
  1036 
       
  1037 
       
  1038 
  1287 
  1039 
  1288 
  1040 
  1289 lemma vsuf_prop1:
 
  1041 lemma vsuf_prop1:
 
  1290   shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) 
  1042   shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) 
  1291                                 then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) )
 
  1043                                 then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) )
 
  1531   qed
 
  1283   qed
 
  1532 
  1284 
  1533 (*AALTS [a\x . b.c, b\x .c,  c \x]*)
 
  1285 (*AALTS [a\x . b.c, b\x .c,  c \x]*)
 
  1534 (*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*)
 
  1286 (*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*)
 
  1535 
  1287 
       
  1288 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where
 
       
  1289 "star_update c r [] = []"
 
       
  1290 |"star_update c r (s # Ss) = (if (rnullable (rders r s)) 
       
  1291                                 then (s@[c]) # [c] # (star_update c r Ss) 
       
  1292                                else   (s@[c]) # (star_update c r Ss) )"
 
       
  1293 
       
  1294 
       
  1295 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list"
 
       
  1296   where
 
       
  1297 "star_updates [] r Ss = Ss"
 
       
  1298 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"
 
       
  1299 
       
  1300 
       
  1301 lemma stupdates_append: shows 
       
  1302 "star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)"
 
       
  1303   apply(induct s arbitrary: Ss)
 
       
  1304    apply simp
 
       
  1305   apply simp
 
       
  1306   done
 
       
  1307 
       
  1308 
       
  1309 
       
  1310 
       
  1311 
  1536 lemma stupdate_induct1:
 
  1312 lemma stupdate_induct1:
 
  1537   shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
 
  1313   shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
 
  1538           map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"
 
  1314           map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"
 
  1539   apply(induct Ss)
 
  1315   apply(induct Ss)
 
  1540    apply simp+
 
  1316    apply simp+
lexing