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.
thys2/SizeBound6CT.thy
changeset 436 222333d2bdc2
parent 434 0cce1aee0fb2
child 437 43b87bab0dac
equal deleted inserted replaced
434:0cce1aee0fb2 436:222333d2bdc2 
    45 
    45 
    46 lemma shape_of_suf_3list:
 
    46 lemma shape_of_suf_3list:
 
    47   shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]"
 
    47   shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]"
 
    48   by auto
 
    48   by auto
 
    49 
    49 
       
    50 
       
    51 fun ordsuf :: "char list \<Rightarrow> char list list"
 
       
    52   where
 
       
    53   "ordsuf [] = []"
 
       
    54 | "ordsuf (x # xs) = (ordsuf xs) @ [(x # xs)]" 
       
    55 
       
    56 lemma 
       
    57   shows "ordsuf [c] = [[c]]"
 
       
    58   and "ordsuf [c2, c3] = [[c3], [c2,c3]]"
 
       
    59   and "ordsuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]"
 
       
    60   by auto
 
       
    61 
       
    62 lemma ordsuf_last:
 
       
    63   shows "ordsuf (xs @ [x]) = [x] # (map (\<lambda>s. s @ [x]) (ordsuf xs))" 
       
    64   apply(induct xs)
 
       
    65   apply(auto)
 
       
    66   done
 
       
    67 
       
    68 lemma ordsuf_append:
 
       
    69   shows "ordsuf (s1 @ s) = (ordsuf s) @ (map (\<lambda>s11. s11 @ s) (ordsuf s1))"
 
       
    70 apply(induct s1 arbitrary: s rule: rev_induct)
 
       
    71   apply(simp)
 
       
    72   apply(drule_tac x="[x] @ s" in meta_spec)
 
       
    73   apply(simp)
 
       
    74   apply(subst ordsuf_last)
 
       
    75   apply(simp)
 
       
    76   done
 
       
    77 
       
    78 
       
    79 lemma 
       
    80   "orderedSuf xs = ordsuf xs"
 
       
    81   apply(induct xs rule: rev_induct)
 
       
    82    apply(simp)
 
       
    83   apply(simp)
 
       
    84   apply(subst ordsuf_last)
 
       
    85   apply(simp)
 
       
    86   oops  
       
    87 
       
    88 (*
 
       
    89 (*
 
    50 lemma throwing_elem_around:
 
    90 lemma throwing_elem_around:
 
    51   shows "orderedSuf (s1 @ [a] @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf ( s1 @ [a]) ))"
 
    91   shows "orderedSuf (s1 @ [a] @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf ( s1 @ [a]) ))"
 
    52 and "orderedSuf (s1 @ [a] @ s) = (orderedSuf ([a] @ s) @ (map (\<lambda>s11. s11 @ ([a] @ s))) (orderedSuf s1) )"
 
    92 and "orderedSuf (s1 @ [a] @ s) = (orderedSuf ([a] @ s) @ (map (\<lambda>s11. s11 @ ([a] @ s))) (orderedSuf s1) )"
 
    53   sorry
 
    93    apply(auto)
 
    54 
    94    prefer 2
 
       
    95   
       
    96   sorry
 
       
    97 *)
 
    55 
    98 
    56 lemma suf_cons:
 
    99 lemma suf_cons:
 
    57   shows "orderedSuf (s1 @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf s1))"
 
   100   shows "orderedSuf (s1 @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf s1))"
 
       
   101   apply(induct s1 arbitrary: s rule: rev_induct)
 
       
   102    apply(simp)
 
       
   103   apply(drule_tac x="[x] @ s" in meta_spec)
 
       
   104   apply(simp)
 
       
   105   
       
   106   
    58   apply(induct s arbitrary: s1)
 
   107   apply(induct s arbitrary: s1)
 
    59    apply simp
 
   108    apply simp
 
    60   apply(subgoal_tac "s1 @ a # s = (s1 @ [a]) @ s")
 
       
    61   prefer 2
 
       
    62    apply simp
 
       
    63   apply(subgoal_tac "orderedSuf (s1 @ a # s) = orderedSuf ((s1 @ [a]) @ s)")
 
       
    64   prefer 2
 
       
    65    apply presburger
 
       
    66   apply(drule_tac x="s1 @ [a]" in meta_spec)
 
   109   apply(drule_tac x="s1 @ [a]" in meta_spec)
 
    67   sorry
 
   110   apply(simp only: append_assoc append.simps)
 
       
   111   
       
   112   using throwing_elem_around(2) by force
 
    68 
   113 
    69 
   114 
    70 
   115 
    71 lemma shape_of_prf_3list:
 
   116 lemma shape_of_prf_3list:
 
    72   shows "orderedPref [c1, c2, c3] = [[c1, c2], [c1], []]"
 
   117   shows "orderedPref [c1, c2, c3] = [[c1, c2], [c1], []]"
 
   139   "rdistinct [] acc = []"
 
   184   "rdistinct [] acc = []"
 
   140 | "rdistinct (x#xs)  acc = 
   185 | "rdistinct (x#xs)  acc = 
   141      (if x \<in> acc then rdistinct xs  acc 
   186      (if x \<in> acc then rdistinct xs  acc 
   142       else x # (rdistinct xs  ({x} \<union> acc)))"
 
   187       else x # (rdistinct xs  ({x} \<union> acc)))"
 
   143 
   188 
   144 lemma rdistinct_idem:
 
       
   145   shows "rdistinct (x # (rdistinct rs {x})) {} = x # (rdistinct rs {x})"
 
       
   146   
       
   147   sorry
 
       
   148 
       
   149 
   189 
   150 
   190 
   151 
   191 
   152 
   192 
   153 fun rflts :: "rrexp list \<Rightarrow> rrexp list"
 
   193 fun rflts :: "rrexp list \<Rightarrow> rrexp list"
 
   197 fun rlist_size :: "rrexp list \<Rightarrow> nat" where
 
   237 fun rlist_size :: "rrexp list \<Rightarrow> nat" where
 
   198 "rlist_size (r # rs) = rsize r + rlist_size rs" 
   238 "rlist_size (r # rs) = rsize r + rlist_size rs" 
   199 | "rlist_size [] = 0"
 
   239 | "rlist_size [] = 0"
 
   200 
   240 
   201 thm neq_Nil_conv
 
   241 thm neq_Nil_conv
 
   202 
   242 lemma hand_made_def_rlist_size:
 
       
   243   shows "rlist_size rs = sum_list (map rsize rs)"
 
       
   244 proof (induct rs)
 
       
   245   case Nil show ?case by simp
 
       
   246 next
 
       
   247   case (Cons a rs) thus ?case
 
       
   248     by simp
 
       
   249 qed
 
   203 
   250 
   204 lemma rsimp_aalts_smaller:
 
   251 lemma rsimp_aalts_smaller:
 
   205   shows "rsize (rsimp_ALTs  rs) \<le> rsize (RALTS rs)"
 
   252   shows "rsize (rsimp_ALTs  rs) \<le> rsize (RALTS rs)"
 
   206   apply(induct rs)
 
   253   apply(induct rs)
 
   207    apply simp
 
   254    apply simp
 
   247 
   294 
   248 fun cond_list :: "rrexp \<Rightarrow> rrexp \<Rightarrow> char list \<Rightarrow> rrexp list"
 
   295 fun cond_list :: "rrexp \<Rightarrow> rrexp \<Rightarrow> char list \<Rightarrow> rrexp list"
 
   249   where
 
   296   where
 
   250 "cond_list r1 r2 s = rders_cond_list r2 (nullable_bools r1 (orderedPref s) ) (orderedSuf s)"
 
   297 "cond_list r1 r2 s = rders_cond_list r2 (nullable_bools r1 (orderedPref s) ) (orderedSuf s)"
 
   251 
   298 
   252 thm rsimp_SEQ.simps
 
   299 
   253 lemma rSEQ_mono:
 
   300 lemma rSEQ_mono:
 
   254   shows "rsize (rsimp_SEQ r1 r2) \<le>rsize ( RSEQ r1 r2)"
 
   301   shows "rsize (rsimp_SEQ r1 r2) \<le>rsize ( RSEQ r1 r2)"
 
   255   apply auto
 
   302   apply auto
 
   256   apply(induct r1)
 
   303   apply(induct r1)
 
   257        apply auto
 
   304        apply auto
 
   265         apply simp_all
 
   312         apply simp_all
 
   266      apply(case_tac r2)
 
   313      apply(case_tac r2)
 
   267   apply simp_all
 
   314   apply simp_all
 
   268   done
 
   315   done
 
   269 
   316 
       
   317 lemma ralts_cap_mono:
 
       
   318   shows "rsize (RALTS rs) \<le> Suc ( sum_list (map rsize rs)) "
 
       
   319   by simp
 
       
   320 
       
   321 lemma rflts_def_idiot:
 
       
   322   shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk>
 
       
   323        \<Longrightarrow> rflts (a # rs) = a # rflts rs"
 
       
   324   apply(case_tac a)
 
       
   325        apply simp_all
 
       
   326   done
 
       
   327 
       
   328 
       
   329 lemma rflts_mono:
 
       
   330   shows "sum_list (map rsize (rflts rs))\<le> sum_list (map rsize rs)"
 
       
   331   apply(induct rs)
 
       
   332   apply simp
 
       
   333   apply(case_tac "a = RZERO")
 
       
   334    apply simp
 
       
   335   apply(case_tac "\<exists>rs1. a = RALTS rs1")
 
       
   336   apply(erule exE)
 
       
   337    apply simp
 
       
   338   apply(subgoal_tac "rflts (a # rs) = a # (rflts rs)")
 
       
   339   prefer 2
 
       
   340   using rflts_def_idiot apply blast
 
       
   341   apply simp
 
       
   342   done
 
       
   343 
       
   344 lemma rdistinct_smaller: shows "sum_list (map rsize (rdistinct rs ss)) \<le>
 
       
   345 sum_list (map rsize rs )"
 
       
   346   apply (induct rs arbitrary: ss)
 
       
   347    apply simp
 
       
   348   by (simp add: trans_le_add2)
 
       
   349 
       
   350 lemma rdistinct_phi_smaller: "sum_list (map rsize (rdistinct rs {})) \<le> sum_list (map rsize rs)"
 
       
   351   by (simp add: rdistinct_smaller)
 
       
   352 
       
   353 
       
   354 lemma rsimp_alts_mono :
 
       
   355   shows "\<And>x. (\<And>xa. xa \<in> set x \<Longrightarrow> rsize (rsimp xa) \<le> rsize xa)  \<Longrightarrow>
 
       
   356 rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {})) \<le> Suc (sum_list (map rsize x))"
 
       
   357   apply(subgoal_tac "rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {} )) 
       
   358                     \<le> rsize (RALTS (rdistinct (rflts (map rsimp x)) {} ))")
 
       
   359   prefer 2
 
       
   360   using rsimp_aalts_smaller apply auto[1]
 
       
   361   apply(subgoal_tac "rsize (RALTS (rdistinct (rflts (map rsimp x)) {})) \<le>Suc( sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})))")
 
       
   362   prefer 2
 
       
   363   using ralts_cap_mono apply blast
 
       
   364   apply(subgoal_tac "sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})) \<le>
 
       
   365                      sum_list (map rsize ( (rflts (map rsimp x))))")
 
       
   366   prefer 2
 
       
   367   using rdistinct_smaller apply presburger
 
       
   368   apply(subgoal_tac "sum_list (map rsize (rflts (map rsimp x))) \<le> 
       
   369                      sum_list (map rsize (map rsimp x))")
 
       
   370   prefer 2
 
       
   371   using rflts_mono apply blast
 
       
   372   apply(subgoal_tac "sum_list (map rsize (map rsimp x)) \<le> sum_list (map rsize x)")
 
       
   373   prefer 2
 
       
   374   
       
   375   apply (simp add: sum_list_mono)
 
       
   376   by linarith
 
       
   377 
       
   378 
       
   379 
       
   380 
       
   381 
   270 lemma rsimp_mono:
 
   382 lemma rsimp_mono:
 
   271   shows "rsize (rsimp r) \<le> rsize r"
 
   383   shows "rsize (rsimp r) \<le> rsize r"
 
       
   384 
   272   apply(induct r)
 
   385   apply(induct r)
 
   273        apply simp_all
 
   386              apply simp_all
 
       
   387 
   274   apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))")
 
   388   apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))")
 
   275   
   389   
   276     apply force
 
   390     apply force
 
   277   using rSEQ_mono
 
   391   using rSEQ_mono
 
   278   apply presburger
 
   392    apply presburger
 
   279   sorry
 
   393   using rsimp_alts_mono by auto
 
   280 
   394 
   281 lemma idiot:
 
   395 lemma idiot:
 
   282   shows "rsimp_SEQ RONE r = r"
 
   396   shows "rsimp_SEQ RONE r = r"
 
   283   apply(case_tac r)
 
   397   apply(case_tac r)
 
   284        apply simp_all
 
   398        apply simp_all
 
   285   done
 
   399   done
 
   286 
   400 
   287 lemma no_dup_after_simp:
 
   401 lemma no_alt_short_list_after_simp:
 
   288   shows "RALTS rs = rsimp r \<Longrightarrow> distinct rs"
 
   402   shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
 
   289   sorry
 
   403   sorry
 
   290 
   404 
   291 lemma no_further_dB_after_simp:
 
   405 lemma no_further_dB_after_simp:
 
   292   shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"
 
   406   shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"
 
   293   sorry
 
   407 
   294 
   408   sorry
 
   295 lemma longlist_withstands_rsimp_alts:
 
   409 
   296   shows "length rs \<ge> 2 \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
 
       
   297   sorry
 
       
   298 
       
   299 lemma no_alt_short_list_after_simp:
 
       
   300   shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
 
       
   301   sorry
 
       
   302 
   410 
   303 lemma idiot2:
 
   411 lemma idiot2:
 
   304   shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk>
 
   412   shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk>
 
   305     \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2"
 
   413     \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2"
 
   306   apply(case_tac r1)
 
   414   apply(case_tac r1)
 
   549 
   657 
   550 lemma cond_list_head_last:
 
   658 lemma cond_list_head_last:
 
   551   shows "rnullable (rders r1 s) \<Longrightarrow> 
   659   shows "rnullable (rders r1 s) \<Longrightarrow> 
   552         RALTS (r # (cond_list r1 r2 (s @ [c]))) = RALTS (r # ((rder c r2) # (map (rder c) (cond_list r1 r2 s))))"
 
   660         RALTS (r # (cond_list r1 r2 (s @ [c]))) = RALTS (r # ((rder c r2) # (map (rder c) (cond_list r1 r2 s))))"
 
   553   using suffix_plus1charn by blast
 
   661   using suffix_plus1charn by blast
 
       
   662 
       
   663 lemma simp_flatten2:
 
       
   664   shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"
 
       
   665   sorry
 
   554 
   666 
   555 
   667 
   556 lemma simp_flatten:
 
   668 lemma simp_flatten:
 
   557   shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))"
 
   669   shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))"
 
   558 
   670 
   829                           (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s))
 
   941                           (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s))
 
   830                          ) 
   942                          ) 
   831         )"
 
   943         )"
 
   832   sorry
 
   944   sorry
 
   833 
   945 
   834 lemma hand_made_def_rlist_size:
 
   946 
   835   shows "rlist_size rs = sum_list (map rsize rs)"
 
       
   836 proof (induct rs)
 
       
   837   case Nil show ?case by simp
 
       
   838 next
 
       
   839   case (Cons a rs) thus ?case
 
       
   840     by simp
 
       
   841 qed
 
       
   842 
   947 
   843 (*this section deals with the property of distinctBy: creates a list without duplicates*)
 
   948 (*this section deals with the property of distinctBy: creates a list without duplicates*)
 
   844 lemma distinct_mono:
 
   949 lemma distinct_mono:
 
   845   shows "rlist_size (rdistinct (a # s) {}) \<le> rlist_size (a # (rdistinct s {}) )"
 
   950   shows "rlist_size (rdistinct (a # s) {}) \<le> rlist_size (a # (rdistinct s {}) )"
 
   846   sorry
 
   951   sorry
 
  1015 
  1120 
  1016 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list => char list list" where
 
  1121 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list => char list list" where
 
  1017 "star_update c r [] = []"
 
  1122 "star_update c r [] = []"
 
  1018 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) 
  1123 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) 
  1019                                 then (s@[c]) # [c] # (star_update c r Ss) 
  1124                                 then (s@[c]) # [c] # (star_update c r Ss) 
  1020                                else   s # (star_update c r Ss) )"
 
  1125                                else   (s@[c]) # (star_update c r Ss) )"
 
  1021 
  1126 
  1022 lemma star_update_case1:
 
  1127 lemma star_update_case1:
 
  1023   shows "rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # [c] # (star_update c r Ss)"
 
  1128   shows "rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # [c] # (star_update c r Ss)"
 
  1024   
  1129   
  1025   by force
 
  1130   by force
 
  1026 
  1131 
  1027 lemma star_update_case2:
 
  1132 lemma star_update_case2:
 
  1028   shows "\<not>rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = s # (star_update c r Ss)"
 
  1133   shows "\<not>rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # (star_update c r Ss)"
 
       
  1134   by simp
 
       
  1135 
       
  1136 lemma bubble_break: shows "rflts [r, RZERO] = rflts [r]"
 
       
  1137   apply(case_tac r)
 
       
  1138        apply simp+
 
       
  1139   done
 
       
  1140 
       
  1141 lemma rsimp_alts_idem_aux1:
 
       
  1142   shows "rsimp_ALTs (rdistinct (rflts [rsimp a]) {}) = rsimp (RALTS [a])"
 
       
  1143   by force
 
       
  1144 
       
  1145 
       
  1146 
       
  1147 lemma rsimp_alts_idem_aux2:
 
       
  1148   shows "rsimp a = rsimp (RALTS [a])"
 
       
  1149   apply(simp)
 
       
  1150   apply(case_tac "rsimp a")
 
       
  1151        apply simp+
 
       
  1152   apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
 
  1029   by simp
 
  1153   by simp
 
  1030 
  1154 
  1031 lemma rsimp_alts_idem:
 
  1155 lemma rsimp_alts_idem:
 
  1032   shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs (a # [(rsimp (rsimp_ALTs as))] ))"
 
  1156   shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs (a # [(rsimp (rsimp_ALTs as))] ))"
 
  1033   sorry
 
  1157   apply(induct as)
 
       
  1158    apply(subgoal_tac "rsimp (rsimp_ALTs [a, rsimp (rsimp_ALTs [])]) = rsimp (rsimp_ALTs [a, RZERO])")
 
       
  1159   prefer 2
 
       
  1160     apply simp
 
       
  1161   using bubble_break rsimp_alts_idem_aux2 apply auto[1]
 
       
  1162   apply(case_tac as)
 
       
  1163    apply(subgoal_tac "rsimp_ALTs( aa # as) = aa")
 
       
  1164   prefer 2
 
       
  1165     apply simp
 
       
  1166   using head_one_more_simp apply fastforce
 
       
  1167   apply(subgoal_tac "rsimp_ALTs (aa # as) = RALTS (aa # as)")
 
       
  1168   prefer 2
 
       
  1169   
       
  1170   using rsimp_ALTs.simps(3) apply presburger
 
       
  1171   
       
  1172   apply(simp only:)
 
       
  1173   apply(subgoal_tac "rsimp_ALTs (a # aa # aaa # list) = RALTS (a # aa # aaa # list)")
 
       
  1174   prefer 2
 
       
  1175   using rsimp_ALTs.simps(3) apply presburger
 
       
  1176   apply(simp only:)
 
       
  1177   apply(subgoal_tac "rsimp_ALTs [a, rsimp (RALTS (aa # aaa # list))] = RALTS (a # [rsimp (RALTS (aa # aaa # list))])")
 
       
  1178   prefer 2
 
       
  1179   
       
  1180   using rsimp_ALTs.simps(3) apply presburger
 
       
  1181   apply(simp only:)
 
       
  1182   using simp_flatten2
 
       
  1183   apply(subgoal_tac " rsimp (RALT a (rsimp (RALTS (aa # aaa # list))))  =  rsimp (RALT a ((RALTS (aa # aaa # list)))) ")
 
       
  1184   prefer 2
 
       
  1185 
       
  1186   apply (metis head_one_more_simp list.simps(9) rsimp.simps(2))
 
       
  1187   apply (simp only:)
 
       
  1188   done
 
       
  1189 
  1034 
  1190 
  1035 lemma rsimp_alts_idem2:
 
  1191 lemma rsimp_alts_idem2:
 
  1036   shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs ((rsimp a) # [(rsimp (rsimp_ALTs as))] ))"
 
  1192   shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs ((rsimp a) # [(rsimp (rsimp_ALTs as))] ))"
 
  1037   sorry
 
  1193   using head_one_more_simp rsimp_alts_idem by auto
 
       
  1194 
  1038 
  1195 
  1039 lemma evolution_step1:
 
  1196 lemma evolution_step1:
 
  1040   shows "rsimp
 
  1197   shows "rsimp
 
  1041         (rsimp_ALTs
 
  1198         (rsimp_ALTs
 
  1042           (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) =
 
  1199           (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) =
 
  1054                  rsimp 
  1211                  rsimp 
  1055         (rsimp_ALTs
 
  1212         (rsimp_ALTs
 
  1056           (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)))]))  "
 
  1213           (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)))]))  "
 
  1057   by (simp add: assms rsimp_alts_idem)
 
  1214   by (simp add: assms rsimp_alts_idem)
 
  1058 
  1215 
       
  1216 lemma rsimp_seq_aux1:
 
       
  1217   shows "r = RONE \<and> r2 = RSTAR r0 \<Longrightarrow> rsimp_SEQ r r2 = r2"
 
       
  1218   apply simp
 
       
  1219   done
 
       
  1220 
       
  1221 lemma multiple_alts_simp_flatten:
 
       
  1222   shows "rsimp (RALT (RALT r1 r2) (rsimp_ALTs rs)) = rsimp (RALTS (r1 # r2 # rs))"
 
       
  1223   by (metis Cons_eq_appendI append_self_conv2 rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem simp_flatten)
 
       
  1224 
       
  1225 
       
  1226 lemma evo3_main_aux1:
 
       
  1227   shows "rsimp
 
       
  1228             (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r)))
 
       
  1229               (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) =
 
       
  1230            rsimp
 
       
  1231             (RALTS
 
       
  1232               (RSEQ (rders_simp r (a @ [x])) (RSTAR r) #
 
       
  1233                RSEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))"
 
       
  1234   apply(subgoal_tac "rsimp
 
       
  1235             (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r)))
 
       
  1236               (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) =
 
       
  1237 rsimp
 
       
  1238             (RALT (RALT (RSEQ ( (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r)))
 
       
  1239               (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) ")
 
       
  1240   prefer 2
 
       
  1241    apply (simp add: rsimp_idem)
 
       
  1242   apply (simp only:)
 
       
  1243   apply(subst multiple_alts_simp_flatten)
 
       
  1244   by simp
 
       
  1245 
       
  1246 
       
  1247 lemma evo3_main_nullable:
 
       
  1248   shows "
 
       
  1249 \<And>a Ss.
 
       
  1250        \<lbrakk>rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) =
 
       
  1251         rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)));
 
       
  1252         rders_simp r a \<noteq> RONE; rders_simp r a \<noteq> RZERO; rnullable (rders_simp r a)\<rbrakk>
 
       
  1253        \<Longrightarrow> rsimp
 
       
  1254             (rsimp_ALTs
 
       
  1255               [rder x (RSEQ (rders_simp r a) (RSTAR r)),
 
       
  1256                rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) =
 
       
  1257            rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))"
 
       
  1258   apply(subgoal_tac "rder x (RSEQ (rders_simp r a) (RSTAR r)) 
       
  1259                    = RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r))")
 
       
  1260   prefer 2
 
       
  1261    apply simp
 
       
  1262   apply(simp only:)
 
       
  1263   apply(subgoal_tac "star_update x r (a # Ss) = (a @ [x]) # [x] # (star_update x r Ss)")
 
       
  1264    prefer 2
 
       
  1265   using star_update_case1 apply presburger
 
       
  1266   apply(simp only:)
 
       
  1267   apply(subst List.list.map(2))+
 
       
  1268   apply(subgoal_tac "rsimp
 
       
  1269             (rsimp_ALTs
 
       
  1270               [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)),
 
       
  1271                rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = 
       
  1272 rsimp
 
       
  1273             (RALTS
 
       
  1274               [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)),
 
       
  1275                rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])")
 
       
  1276   prefer 2
 
       
  1277   using rsimp_ALTs.simps(3) apply presburger
 
       
  1278   apply(simp only:)
 
       
  1279   apply(subgoal_tac " rsimp
 
       
  1280             (rsimp_ALTs
 
       
  1281               (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) #
 
       
  1282                rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) 
       
  1283 = 
       
  1284  rsimp
 
       
  1285             (RALTS
 
       
  1286               (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) #
 
       
  1287                rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))")
 
       
  1288 
       
  1289   prefer 2
 
       
  1290   using rsimp_ALTs.simps(3) apply presburger
 
       
  1291   apply (simp only:)
 
       
  1292   apply(subgoal_tac " rsimp
 
       
  1293             (RALT (RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ ( (rder x r)) (RSTAR r)))
 
       
  1294               (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = 
       
  1295              rsimp
 
       
  1296             (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r)))
 
       
  1297               (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))")
 
       
  1298   prefer 2
 
       
  1299    apply (simp add: rsimp_idem)
 
       
  1300   apply(simp only:)
 
       
  1301   apply(subgoal_tac "             rsimp
 
       
  1302             (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r)))
 
       
  1303               (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = 
       
  1304              rsimp
 
       
  1305             (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r)))
 
       
  1306               (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))")
 
       
  1307    prefer 2
 
       
  1308   using rders_simp_append rders_simp_one_char rsimp_idem apply presburger
 
       
  1309   apply(simp only:)
 
       
  1310   apply(subgoal_tac " rsimp
 
       
  1311             (RALTS
 
       
  1312               (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) #
 
       
  1313                rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) = 
       
  1314  rsimp
 
       
  1315             (RALTS
 
       
  1316               (RSEQ (rders_simp r (a @ [x])) (RSTAR r) #
 
       
  1317                RSEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))")
 
       
  1318   prefer 2
 
       
  1319   apply (smt (z3) idiot2 list.simps(9) rrexp.distinct(9) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_idem)
 
       
  1320   apply(simp only:)
 
       
  1321   apply(subgoal_tac "      rsimp
 
       
  1322             (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r)))
 
       
  1323               (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) =
 
       
  1324      rsimp
 
       
  1325             (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r)))
 
       
  1326               ( (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))  ")
 
       
  1327   prefer 2
 
       
  1328   using rsimp_idem apply force
 
       
  1329   apply(simp only:)
 
       
  1330   using evo3_main_aux1 by blast
 
       
  1331   
       
  1332 
       
  1333 lemma evo3_main_not1:
 
       
  1334   shows " \<not>rnullable (rders_simp r a) \<Longrightarrow> rder x (RSEQ (rders_simp r a) (RSTAR r)) = RSEQ (rder x (rders_simp r a)) (RSTAR r)"
 
       
  1335   by fastforce
 
       
  1336 
       
  1337 
       
  1338 lemma evo3_main_not2:
 
       
  1339   shows "\<not>rnullable (rders_simp r a) \<Longrightarrow>  rsimp
 
       
  1340             (rsimp_ALTs
 
       
  1341               (rder x (RSEQ (rders_simp r a) (RSTAR r)) # rs)) = rsimp
 
       
  1342             (rsimp_ALTs
 
       
  1343               ((RSEQ (rders_simp r (a @ [x])) (RSTAR r)) # rs))"
 
       
  1344   by (simp add: rders_simp_append rsimp_alts_idem2 rsimp_idem)
 
       
  1345 
       
  1346 lemma evo3_main_not3:
 
       
  1347   shows "rsimp
 
       
  1348             (rsimp_ALTs
 
       
  1349               (rsimp_SEQ r1 (RSTAR r) # rs)) = 
       
  1350          rsimp (rsimp_ALTs
 
       
  1351               (RSEQ r1 (RSTAR r) # rs))"
 
       
  1352   by (metis idiot2 rrexp.distinct(9) rsimp.simps(1) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2)
 
       
  1353 
       
  1354 
       
  1355 lemma evo3_main_notnullable:
 
       
  1356   shows "\<And>a Ss.
 
       
  1357        \<lbrakk>rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) =
 
       
  1358         rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)));
 
       
  1359         rders_simp r a \<noteq> RONE; rders_simp r a \<noteq> RZERO; \<not>rnullable (rders_simp r a)\<rbrakk>
 
       
  1360        \<Longrightarrow> rsimp
 
       
  1361             (rsimp_ALTs
 
       
  1362               [rder x (RSEQ (rders_simp r a) (RSTAR r)),
 
       
  1363                rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) =
 
       
  1364            rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))"
 
       
  1365   apply(subst star_update_case2)
 
       
  1366    apply simp
 
       
  1367   apply(subst List.list.map(2))
 
       
  1368   apply(subst evo3_main_not2)
 
       
  1369    apply simp
 
       
  1370   apply(subst evo3_main_not3)
 
       
  1371   using rsimp_alts_idem by presburger
 
       
  1372 
       
  1373 
       
  1374 lemma evo3_aux2:
 
       
  1375   shows "rders_simp r a = RONE \<Longrightarrow> rsimp_SEQ (rders_simp (rders_simp r a) [x]) (RSTAR r) = RZERO"
 
       
  1376   by simp
 
       
  1377 lemma evo3_aux3:
 
       
  1378   shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"
 
       
  1379   by (metis list.simps(8) list.simps(9) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem)
 
       
  1380 
       
  1381 lemma evo3_aux4:
 
       
  1382   shows " rsimp
 
       
  1383             (rsimp_ALTs
 
       
  1384               [RSEQ (rder x r) (RSTAR r),
 
       
  1385                rsimp (rsimp_ALTs rs)]) =
 
       
  1386            rsimp
 
       
  1387             (rsimp_ALTs
 
       
  1388               (rsimp_SEQ (rders_simp r [x]) (RSTAR r) # rs))"
 
       
  1389   by (metis rders_simp_one_char rsimp.simps(1) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2)
 
       
  1390 
       
  1391 lemma evo3_aux5:
 
       
  1392   shows "rders_simp r a \<noteq> RONE \<and> rders_simp r a \<noteq> RZERO \<Longrightarrow> rsimp_SEQ (rders_simp r a) (RSTAR r) = RSEQ (rders_simp r a) (RSTAR r)"
 
       
  1393   using idiot2 by blast
 
       
  1394 
       
  1395 
       
  1396 lemma evolution_step3:
 
       
  1397   shows" \<And>a Ss.
 
       
  1398        rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) =
 
       
  1399        rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) \<Longrightarrow>
 
       
  1400        rsimp
 
       
  1401         (rsimp_ALTs
 
       
  1402           [rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)),
 
       
  1403            rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) =
 
       
  1404        rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))"
 
       
  1405   apply(case_tac "rders_simp r a = RONE")
 
       
  1406    apply(subst rsimp_seq_aux1)
 
       
  1407     apply simp
 
       
  1408   apply(subst rder.simps(6))
 
       
  1409    apply(subgoal_tac "rnullable (rders_simp r a)")
 
       
  1410     prefer 2
 
       
  1411   using rnullable.simps(2) apply presburger
 
       
  1412    apply(subst star_update_case1)
 
       
  1413     apply simp
 
       
  1414 
       
  1415    apply(subst List.list.map)+
 
       
  1416   apply(subst rders_simp_append)
 
       
  1417    apply(subst evo3_aux2)
 
       
  1418     apply simp
 
       
  1419    apply(subst evo3_aux3)
 
       
  1420    apply(subst evo3_aux4)
 
       
  1421    apply simp
 
       
  1422   apply(case_tac "rders_simp r a = RZERO")
 
       
  1423 
       
  1424    apply (simp add: rsimp_alts_idem2)
 
       
  1425    apply(subgoal_tac "rders_simp r (a @ [x]) = RZERO")
 
       
  1426   prefer 2
 
       
  1427   using rder.simps(1) rders_simp_append rders_simp_one_char rsimp.simps(3) apply presburger
 
       
  1428   using rflts.simps(2) rsimp.simps(3) rsimp_SEQ.simps(1) apply presburger
 
       
  1429   apply(subst evo3_aux5)
 
       
  1430    apply simp
 
       
  1431   apply(case_tac "rnullable (rders_simp r a) ")
 
       
  1432   using evo3_main_nullable apply blast
 
       
  1433   using evo3_main_notnullable apply blast
 
       
  1434   done
 
  1059 
  1435 
  1060 (*
 
  1436 (*
 
  1061 proof (prove)
 
  1437 proof (prove)
 
  1062 goal (1 subgoal):
 
  1438 goal (1 subgoal):
 
  1063  1. map f (a # s) = f a # map f s 
  1439  1. map f (a # s) = f a # map f s 
  1073   apply(induct Ss)
 
  1449   apply(induct Ss)
 
  1074    apply simp
 
  1450    apply simp
 
  1075   apply(subst List.list.map(2))
 
  1451   apply(subst List.list.map(2))
 
  1076   apply(subst evolution_step2)
 
  1452   apply(subst evolution_step2)
 
  1077    apply simp
 
  1453    apply simp
 
  1078   apply(case_tac "rnullable (rders_simp r a)")
 
  1454 
  1079    apply(subst star_update_case1)
 
  1455 
  1080     apply simp
 
       
  1081    apply(subst List.list.map)+
 
       
  1082   sledgehammer
 
       
  1083   sorry
 
  1456   sorry
 
  1084 
  1457 
  1085 
  1458 
  1086 lemma star_seqs_produce_star_seqs:
 
  1459 lemma star_seqs_produce_star_seqs:
 
  1087   shows "rsimp (rsimp_ALTs (map (rder x \<circ> (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))
 
  1460   shows "rsimp (rsimp_ALTs (map (rder x \<circ> (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))
 
  1092   shows "map (rder x) (map (\<lambda>s. f s) Ss) = map (\<lambda>s. (rder x (f s))) Ss"
 
  1465   shows "map (rder x) (map (\<lambda>s. f s) Ss) = map (\<lambda>s. (rder x (f s))) Ss"
 
  1093   by force
 
  1466   by force
 
  1094 
  1467 
  1095 lemma ralts_vs_rsimpalts:
 
  1468 lemma ralts_vs_rsimpalts:
 
  1096   shows "rsimp (RALTS rs) = rsimp (rsimp_ALTs rs)"
 
  1469   shows "rsimp (RALTS rs) = rsimp (rsimp_ALTs rs)"
 
  1097   sorry
 
  1470   by (metis evo3_aux3 rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) simp_flatten2)
 
       
  1471   
  1098 
  1472 
  1099 lemma linearity_of_list_of_star_or_starseqs: 
  1473 lemma linearity_of_list_of_star_or_starseqs: 
  1100   fixes r::rrexp and Ss::"char list list" and x::char
 
  1474   fixes r::rrexp and Ss::"char list list" and x::char
 
  1101   shows "\<exists>Ssa. rsimp (rder x (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) =
 
  1475   shows "\<exists>Ssa. rsimp (rder x (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) =
 
  1102                  rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)))"
 
  1476                  rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)))"
 
  1154           rsimp (RALTS (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))")
 
  1528           rsimp (RALTS (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))")
 
  1155   prefer 2
 
  1529   prefer 2
 
  1156   using star_list_push_der apply presburger
 
  1530   using star_list_push_der apply presburger
 
  1157 
  1531 
  1158 
  1532 
  1159   sorry
 
  1533   by (metis ralts_vs_rsimpalts starseq_list_evolution)
 
       
  1534 
       
  1535 
       
  1536 lemma starder_is_a_list:
 
       
  1537   shows " \<exists>Ss. rders_simp (RSTAR r) s = rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) \<or> rders_simp (RSTAR r) s = RSTAR r"
 
       
  1538   apply(case_tac s)
 
       
  1539   prefer 2
 
       
  1540   apply (metis neq_Nil_conv starder_is_a_list_of_stars_or_starseqs)
 
       
  1541   apply simp
 
       
  1542   done
 
       
  1543 
       
  1544 
       
  1545 (** start about bounds here**)
 
       
  1546 
       
  1547 
       
  1548 lemma list_simp_size:
 
       
  1549   shows "rlist_size (map rsimp rs) \<le> rlist_size rs"
 
       
  1550   apply(induct rs)
 
       
  1551    apply simp
 
       
  1552   apply simp
 
       
  1553   apply (subgoal_tac "rsize (rsimp a) \<le> rsize a")
 
       
  1554   prefer 2
 
       
  1555   using rsimp_mono apply fastforce
 
       
  1556   using add_le_mono by presburger
 
       
  1557 
       
  1558 lemma inside_list_simp_inside_list:
 
       
  1559   shows "r \<in> set rs \<Longrightarrow> rsimp r \<in> set (map rsimp rs)"
 
       
  1560   apply (induct rs)
 
       
  1561    apply simp
 
       
  1562   apply auto
 
       
  1563   done
 
       
  1564 
       
  1565 
       
  1566 lemma rsize_star_seq_list:
 
       
  1567   shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) \<Longrightarrow>  \<exists>N3.\<forall>Ss.  
       
  1568 rlist_size (rdistinct (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss) {}) < N3"
 
       
  1569   sorry
 
       
  1570 
       
  1571 
       
  1572 lemma rdistinct_bound_by_no_simp:
 
       
  1573   shows "
 
       
  1574 
       
  1575    rlist_size (rdistinct  (map rsimp rs) (set (map rsimp ss)))
 
       
  1576  \<le> (rlist_size (rdistinct rs (set ss)))
 
       
  1577 "
 
       
  1578   apply(induct rs arbitrary: ss)
 
       
  1579    apply simp
 
       
  1580   apply(case_tac "a \<in> set ss")
 
       
  1581    apply(subgoal_tac "rsimp a \<in> set (map rsimp ss)")
 
       
  1582   prefer 2
 
       
  1583   using inside_list_simp_inside_list apply blast
 
       
  1584 
       
  1585    apply simp
 
       
  1586   apply simp
 
       
  1587   by (metis List.set_insert add_le_mono image_insert insert_absorb rsimp_mono trans_le_add2)
 
       
  1588 
       
  1589 
       
  1590 lemma starder_closed_form_bound_aux1:
 
       
  1591   shows 
       
  1592 "\<forall>Ss. rsize (rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) \<le>
 
       
  1593   Suc (rlist_size ( (rdistinct ( ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss))) {}))) "
 
       
  1594   
       
  1595   sorry
 
       
  1596 
       
  1597 lemma starder_closed_form_bound:
 
       
  1598   shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) \<Longrightarrow> \<exists>N3.\<forall>Ss.  
       
  1599 rsize(rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3"
 
       
  1600   apply(subgoal_tac " \<exists>N3.\<forall>Ss.  
       
  1601 rlist_size (rdistinct (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss) {}) < N3")
 
       
  1602   prefer 2
 
       
  1603   
       
  1604   using rsize_star_seq_list apply auto[1]
 
       
  1605   apply(erule exE)
 
       
  1606   apply(rule_tac x = "Suc N3" in exI)
 
       
  1607   apply(subgoal_tac "\<forall>Ss. rsize (rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) \<le>
 
       
  1608  Suc (rlist_size ( (rdistinct ( ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss))) {})))")
 
       
  1609   prefer 2
 
       
  1610   using starder_closed_form_bound_aux1 apply blast
 
       
  1611   by (meson less_trans_Suc linorder_not_le not_less_eq)
 
       
  1612 
       
  1613   
       
  1614 thm starder_closed_form_bound_aux1
 
       
  1615 
       
  1616 (*
 
       
  1617  "ralts_vs_rsimpalts", , and "starder_closed_form_bound_aux1", which could be due to a bug in Sledgehammer or to inconsistent axioms (including "sorry"s) 
       
  1618 *)
 
       
  1619 
       
  1620 lemma starder_size_bound:
 
       
  1621   shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) \<Longrightarrow> \<exists>N3.\<forall>Ss.  
       
  1622 rsize(rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3 \<and>
 
       
  1623 rsize (RSTAR r0) < N3"
 
       
  1624   apply(subgoal_tac " \<exists>N3.\<forall>Ss.  
       
  1625 rsize(rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3")
 
       
  1626   prefer 2
 
       
  1627   using starder_closed_form_bound apply blast
 
       
  1628   apply(erule exE)
 
       
  1629   apply(rule_tac x = "max N3 (Suc (rsize (RSTAR r0)))" in exI)
 
       
  1630   using less_max_iff_disj by blast
 
       
  1631 
       
  1632 
  1160 
  1633 
  1161 
  1634 
  1162 lemma finite_star:
 
  1635 lemma finite_star:
 
  1163   shows "(\<forall>s. rsize (rders_simp r0 s) < N0 )
 
  1636   shows "(\<forall>s. rsize (rders_simp r0 s) < N0 )
 
  1164            \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3"
 
  1637            \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3"
 
  1165 
  1638   apply(subgoal_tac  " \<exists>N3. \<forall>Ss. 
  1166   sorry
 
  1639 rsize(rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3 \<and>
 
       
  1640 rsize (RSTAR r0) < N3")
 
       
  1641   prefer 2
 
       
  1642   using starder_size_bound apply blast
 
       
  1643   apply(erule exE)
 
       
  1644   apply(rule_tac x = N3 in exI)
 
       
  1645   by (metis starder_is_a_list)
 
  1167 
  1646 
  1168 
  1647 
  1169 lemma rderssimp_zero:
 
  1648 lemma rderssimp_zero:
 
  1170   shows"rders_simp RZERO s = RZERO"
 
  1649   shows"rders_simp RZERO s = RZERO"
 
  1171   apply(induction s)
 
  1650   apply(induction s)
lexing