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/ClosedFormsBounds.thy
changeset 642 6c13f76c070b
parent 558 671a83abccf3
equal deleted inserted replaced
641:cf7a5c863831 642:6c13f76c070b 
     1 
     1 
     2 theory ClosedFormsBounds
 
     2 theory ClosedFormsBounds
 
     3   imports "GeneralRegexBound" "ClosedForms"
 
     3   imports "GeneralRegexBound" "ClosedForms"
 
     4 begin
 
     4 begin
 
     5 
       
     6 
       
     7 lemma alts_ders_lambda_shape_ders:
 
     5 lemma alts_ders_lambda_shape_ders:
 
     8   shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s"
 
     6   shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s"
 
     9   by (simp add: image_iff)
 
     7   by (simp add: image_iff)
 
    10 
     8 
    11 lemma rlist_bound:
 
     9 lemma rlist_bound:
 
    13   shows "rsizes rs \<le> N * (length rs)"
 
    11   shows "rsizes rs \<le> N * (length rs)"
 
    14   using assms
 
    12   using assms
 
    15   apply(induct rs)
 
    13   apply(induct rs)
 
    16   apply simp
 
    14   apply simp
 
    17   by simp
 
    15   by simp
 
    18 
       
    19 lemma distinct_list_size_len_bounded:
 
       
    20   assumes "\<forall>r \<in> set rs. rsize r \<le> N" "length rs \<le> lrs"
 
       
    21   shows "rsizes rs \<le> lrs * N "
 
       
    22   using assms
 
       
    23   by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1)
 
       
    24 
    16 
    25 lemma alts_closed_form_bounded: 
    17 lemma alts_closed_form_bounded: 
    26   assumes "\<forall>r \<in> set rs. \<forall>s. rsize (rders_simp r s) \<le> N"
 
    18   assumes "\<forall>r \<in> set rs. \<forall>s. rsize (rders_simp r s) \<le> N"
 
    27   shows "rsize (rders_simp (RALTS rs) s) \<le> max (Suc (N * (length rs))) (rsize (RALTS rs))"
 
    19   shows "rsize (rders_simp (RALTS rs) s) \<le> max (Suc (N * (length rs))) (rsize (RALTS rs))"
 
    28 proof (cases s)
 
    20 proof (cases s)
 
   147   apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) = 
   139   apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) = 
   148                      insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
 
   140                      insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
 
   149              apply(simp only:)
 
   141              apply(simp only:)
 
   150   apply(subgoal_tac "rsizes (rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))
 
   142   apply(subgoal_tac "rsizes (rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))
 
   151                    \<le>  rsizes (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))")
 
   143                    \<le>  rsizes (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))")
 
   152   apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
 
   144   apply (smt (verit, ccfv_threshold) dual_order.trans insertE rrexp.distinct(17))
 
   153   apply (metis (no_types, opaque_lifting)  le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
 
   145   apply (metis (no_types, opaque_lifting)  le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
 
   154             apply fastforce
 
   146             apply fastforce
 
   155            apply fastforce
 
   147            apply fastforce
 
   156   apply (metis Un_iff insert_absorb)
 
   148   apply (metis Un_iff insert_absorb)
 
   157          apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1))
 
   149          apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1))
 
   158         apply (meson UnCI rdistinct.simps(2))
 
   150         apply (meson UnCI rdistinct.simps(2))
 
   159   using rflts.simps(4) apply presburger
 
   151   using rflts.simps(4) apply presburger
 
   160       apply simp
 
   152       apply simp
 
   161       apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
 
   153       apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
 
   162   apply(simp only:)
 
   154         apply(simp only:)
 
   163   apply (metis Un_insert_left insertE rrexp.distinct(15))
 
   155   apply (metis Un_insert_left insertE rrexp.distinct(17))
 
   164       apply fastforce
 
   156       apply fastforce
 
   165      apply(case_tac "a \<in> noalts_set")
 
   157      apply(case_tac "a \<in> noalts_set")
 
   166       apply simp
 
   158       apply simp
 
   167   apply(subgoal_tac "a \<notin> alts_set")
 
   159   apply(subgoal_tac "a \<notin> alts_set")
 
   168       prefer 2
 
   160       prefer 2
 
   180   apply fastforce
 
   172   apply fastforce
 
   181        apply simp
 
   173        apply simp
 
   182   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
   174   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
   183         apply(simp only:)
 
   175         apply(simp only:)
 
   184         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
   176         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
   185   apply(simp only:)
 
   177           apply(simp only:)
 
   186   apply (metis insertE rrexp.distinct(21))
 
   178   apply (metis insertE nonalt.simps(1) nonalt.simps(4))
 
   187         apply blast
 
   179         apply blast
 
   188   
   180   
   189   apply fastforce
 
   181   apply fastforce
 
   190   apply force
 
   182   apply force
 
   191      apply simp
 
   183       apply simp
 
   192      apply (metis Un_insert_left insert_iff rrexp.distinct(21))
 
   184   apply (metis Un_insert_left insertE nonalt.simps(1) nonalt.simps(4))
 
   193     apply(case_tac "a \<in> noalts_set")
 
   185     apply(case_tac "a \<in> noalts_set")
 
   194      apply simp
 
   186      apply simp
 
   195   apply(subgoal_tac "a \<notin> alts_set")
 
   187   apply(subgoal_tac "a \<notin> alts_set")
 
   196       prefer 2
 
   188       prefer 2
 
   197       apply blast
 
   189       apply blast
 
   210   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
   202   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
   211         apply(simp only:)
 
   203         apply(simp only:)
 
   212         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
   204         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
   213   apply(simp only:)
 
   205   apply(simp only:)
 
   214 
   206 
   215 
   207          apply (metis insertE rrexp.distinct(31))
 
   216   apply (metis insertE rrexp.distinct(25))
 
       
   217   apply blast
 
   208   apply blast
 
   218   apply fastforce
 
   209   apply fastforce
 
   219   apply force
 
   210   apply force
 
   220      apply simp
 
   211      apply simp
 
   221   
   212   
   222     apply (metis Un_insert_left insertE rrexp.distinct(25))
 
   213     apply (metis Un_insert_left insertE rrexp.distinct(31))
 
   223 
   214 
   224   using Suc_le_mono flts_size_reduction_alts apply presburger
 
   215   using Suc_le_mono flts_size_reduction_alts apply presburger
 
   225      apply(case_tac "a \<in> noalts_set")
 
   216      apply(case_tac "a \<in> noalts_set")
 
   226       apply simp
 
   217       apply simp
 
   227   apply(subgoal_tac "a \<notin> alts_set")
 
   218   apply(subgoal_tac "a \<notin> alts_set")
 
   240   apply fastforce
 
   231   apply fastforce
 
   241        apply simp
 
   232        apply simp
 
   242   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
   233   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
   243         apply(simp only:)
 
   234         apply(simp only:)
 
   244         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
   235         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
   245   apply(simp only:)
 
   236        apply(simp only:)
 
   246   apply (metis insertE rrexp.distinct(29))
 
   237   apply (metis insertE rrexp.distinct(37))
 
   247 
   238 
   248         apply blast
 
   239         apply blast
 
   249   
   240   
   250   apply fastforce
 
   241   apply fastforce
 
   251   apply force
 
   242   apply force
 
   252      apply simp
 
   243      apply simp
 
   253   apply (metis Un_insert_left insert_iff rrexp.distinct(29))
 
   244    apply (metis Un_insert_left insert_iff rrexp.distinct(37))
 
   254   done
 
   245   apply(case_tac "a \<in> noalts_set")
 
       
   246       apply simp
 
       
   247   apply(subgoal_tac "a \<notin> alts_set")
 
       
   248      prefer 2
 
       
   249       apply blast
 
       
   250   apply(case_tac "a \<in> corr_set")
 
       
   251       apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
 
       
   252   prefer 2
 
       
   253   apply fastforce
 
       
   254    apply(simp only:)
 
       
   255    apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le>
 
       
   256                rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))")
 
       
   257 
       
   258        apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le>
 
       
   259           rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))")
 
       
   260   apply fastforce
 
       
   261        apply simp
 
       
   262   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
       
   263         apply(simp only:)
 
       
   264         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
       
   265        apply(simp only:)
 
       
   266   apply (metis insertE nonalt.simps(1) nonalt.simps(7))
 
       
   267   apply blast
 
       
   268   apply blast
 
       
   269   apply force
 
       
   270   apply(auto)
 
       
   271   by (metis Un_insert_left insert_iff rrexp.distinct(39))
 
   255 
   272 
   256 
   273 
   257 lemma flts_vs_nflts:
 
   274 lemma flts_vs_nflts:
 
   258   assumes "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs"
 
   275   assumes "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs"
 
   259   and "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)"
 
   276   and "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)"
 
   316   apply(case_tac "a \<in> ss")
 
   333   apply(case_tac "a \<in> ss")
 
   317    apply simp
 
   334    apply simp
 
   318   by (simp add: larger_acc_smaller_distinct_res)
 
   335   by (simp add: larger_acc_smaller_distinct_res)
 
   319 
   336 
   320 
   337 
       
   338 lemma distinct_list_size_len_bounded:
 
       
   339   assumes "\<forall>r \<in> set rs. rsize r \<le> N" "length rs \<le> lrs"
 
       
   340   shows "rsizes rs \<le> lrs * N "
 
       
   341   using assms
 
       
   342   by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1)
 
   321 
   343 
   322 
   344 
   323 
   345 
   324 lemma rdistinct_same_set:
 
   346 lemma rdistinct_same_set:
 
   325   shows "r \<in> set rs \<longleftrightarrow> r \<in> set (rdistinct rs {})"
 
   347   shows "r \<in> set rs \<longleftrightarrow> r \<in> set (rdistinct rs {})"
 
   378     using star_control_bounded[OF assms] by (metis add_mono le_add1 mult_Suc plus_1_eq_Suc)
 
   400     using star_control_bounded[OF assms] by (metis add_mono le_add1 mult_Suc plus_1_eq_Suc)
 
   379   also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))"
 
   401   also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))"
 
   380     by simp    
   402     by simp    
   381   finally show ?thesis by simp  
   403   finally show ?thesis by simp  
   382 qed
 
   404 qed
 
       
   405 
       
   406 
       
   407 thm ntimes_closed_form
 
       
   408 
       
   409 thm rsize.simps
 
       
   410 
       
   411 lemma nupdates_snoc:
 
       
   412   shows " (nupdates (xs @ [x]) r optlist) = nupdate x r (nupdates xs r optlist)"
 
       
   413   by (simp add: nupdates_append)
 
       
   414 
       
   415 lemma nupdate_elems:
 
       
   416   shows "\<forall>opt \<in> set (nupdate c r optlist). opt = None \<or> (\<exists>s n. opt = Some (s, n))"
 
       
   417   using nonempty_string.cases by auto
 
       
   418 
       
   419 lemma nupdates_elems:
 
       
   420   shows "\<forall>opt \<in> set (nupdates s r optlist). opt = None \<or> (\<exists>s n. opt = Some (s, n))"
 
       
   421   by (meson nonempty_string.cases)
 
       
   422 
       
   423 
       
   424 lemma opterm_optlist_result_shape:
 
       
   425   shows "\<forall>r' \<in> set (map (optermsimp r) optlist). r' = RZERO \<or> (\<exists>s m. r' = RSEQ (rders_simp r s) (RNTIMES r m))"
 
       
   426   apply(induct optlist)
 
       
   427    apply simp
 
       
   428   apply(case_tac a)
 
       
   429   apply simp+
 
       
   430   by fastforce
 
       
   431 
       
   432 
       
   433 lemma opterm_optlist_result_shape2:
 
       
   434   shows "\<And>optlist. \<forall>r' \<in> set (map (optermsimp r) optlist). r' = RZERO \<or> (\<exists>s m. r' = RSEQ (rders_simp r s) (RNTIMES r m))"  
       
   435   using opterm_optlist_result_shape by presburger
 
       
   436 
       
   437 
       
   438 lemma nupdate_n_leq_n:
 
       
   439   shows "\<forall>r \<in> set (nupdate c' r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"
 
       
   440   apply(case_tac n)
 
       
   441    apply simp
 
       
   442   apply simp
 
       
   443   done
 
       
   444 (*
 
       
   445 lemma nupdate_induct_leqn:
 
       
   446   shows "\<lbrakk>\<forall>opt \<in> set optlist. opt = None \<or> (\<exists>s' m. opt = Some(s', m) \<and> m \<le> n) \<rbrakk> \<Longrightarrow> 
       
   447        \<forall>opt \<in> set (nupdate c' r optlist). opt = None \<or> (\<exists>s' m. opt = Some (s', m) \<and> m \<le> n)"
 
       
   448   apply (case_tac optlist)
 
       
   449    apply simp
 
       
   450   apply(case_tac a)
 
       
   451    apply simp
 
       
   452   sledgehammer
 
       
   453 *)
 
       
   454 
       
   455 
       
   456 lemma nupdates_n_leq_n:
 
       
   457   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)"
 
       
   458   apply(induct s rule: rev_induct)
 
       
   459    apply simp
 
       
   460   apply(subst nupdates_append)
 
       
   461   by (metis nupdates_elems_leqn nupdates_snoc)
 
       
   462   
       
   463 
       
   464 
       
   465 lemma ntimes_closed_form_list_elem_shape:
 
       
   466   shows "\<forall>r' \<in> set (map (optermsimp r) (nupdates s r [Some ([c], n)])). 
       
   467 r' = RZERO \<or> (\<exists>s' m. r' = RSEQ (rders_simp r s') (RNTIMES r m) \<and> m \<le> n)"
 
       
   468   apply(insert opterm_optlist_result_shape2)
 
       
   469   apply(case_tac s)
 
       
   470    apply(auto)
 
       
   471   apply (metis rders_simp_one_char)
 
       
   472   by (metis case_prod_conv nupdates.simps(2) nupdates_n_leq_n option.simps(4) option.simps(5))
 
       
   473 
       
   474 
       
   475 lemma ntimes_trivial1:
 
       
   476   shows "rsize RZERO \<le> N + rsize (RNTIMES r n)"
 
       
   477   by simp
 
       
   478 
       
   479 
       
   480 lemma ntimes_trivial20:
 
       
   481   shows "m \<le> n \<Longrightarrow> rsize (RNTIMES r m) \<le> rsize (RNTIMES r n)"
 
       
   482   by simp
 
       
   483 
       
   484 
       
   485 lemma ntimes_trivial2:
 
       
   486   assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
 
       
   487   shows "    r' = RSEQ (rders_simp r s1) (RNTIMES r m) \<and> m \<le> n
 
       
   488        \<Longrightarrow> rsize r' \<le> Suc (N + rsize (RNTIMES r n))"
 
       
   489   apply simp
 
       
   490   by (simp add: add_mono_thms_linordered_semiring(1) assms)
 
       
   491 
       
   492 lemma ntimes_closed_form_list_elem_bounded:
 
       
   493   assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
 
       
   494   shows "\<forall>r' \<in>  set  (map (optermsimp r) (nupdates s r [Some ([c], n)])). rsize r' \<le> Suc (N + rsize (RNTIMES r n))"
 
       
   495   apply(rule ballI)
 
       
   496   apply(subgoal_tac  "r' = RZERO \<or> (\<exists>s' m. r' = RSEQ (rders_simp r s') (RNTIMES r m) \<and> m \<le> n)")
 
       
   497   prefer 2
 
       
   498   using ntimes_closed_form_list_elem_shape apply blast
 
       
   499   apply(case_tac "r' = RZERO")
 
       
   500   using le_SucI ntimes_trivial1 apply presburger
 
       
   501   apply(subgoal_tac "\<exists>s1 m. r' = RSEQ (rders_simp r s1) (RNTIMES r m) \<and> m \<le> n")
 
       
   502   apply(erule exE)+
 
       
   503   using assms ntimes_trivial2 apply presburger
 
       
   504   by blast
 
       
   505 
       
   506 
       
   507 lemma P_holds_after_distinct:
 
       
   508   assumes "\<forall>r \<in> set rs. P r"
 
       
   509   shows "\<forall>r \<in> set (rdistinct rs rset). P r"
 
       
   510   by (simp add: assms rdistinct_set_equality1)
 
       
   511 
       
   512 lemma ntimes_control_bounded:
 
       
   513   assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
 
       
   514   shows "rsizes (rdistinct (map (optermsimp r) (nupdates s r [Some ([c], n)])) {}) 
       
   515      \<le> (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n)))"
 
       
   516   apply(subgoal_tac "\<forall>r' \<in> set (rdistinct (map (optermsimp r) (nupdates s r [Some ([c], n)])) {}).
 
       
   517           rsize r' \<le> Suc (N + rsize (RNTIMES r n))")
 
       
   518    apply (meson distinct_list_rexp_upto rdistinct_same_set)
 
       
   519   apply(subgoal_tac "\<forall>r' \<in> set (map (optermsimp r) (nupdates s r [Some ([c], n)])). rsize r' \<le> Suc (N + rsize (RNTIMES r n))")
 
       
   520    apply (simp add: rdistinct_set_equality)
 
       
   521   by (metis assms nat_le_linear not_less_eq_eq ntimes_closed_form_list_elem_bounded)
 
       
   522 
       
   523 
       
   524 
       
   525 lemma ntimes_closed_form_bounded0:
 
       
   526   assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
 
       
   527   shows " (rders_simp (RNTIMES r 0) s)  = RZERO \<or> (rders_simp (RNTIMES r 0) s)  = RNTIMES r 0
 
       
   528            "
 
       
   529   apply(induct s)
 
       
   530    apply simp
 
       
   531   by (metis always0 list.simps(3) rder.simps(7) rders.simps(2) rders_simp_same_simpders rsimp.simps(3))
 
       
   532 
       
   533 lemma ntimes_closed_form_bounded1:
 
       
   534   assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
 
       
   535   shows " rsize (rders_simp (RNTIMES r 0) s) \<le> max (rsize  RZERO) (rsize (RNTIMES r 0))"
 
       
   536   
       
   537   by (metis assms max.cobounded1 max.cobounded2 ntimes_closed_form_bounded0)
 
       
   538 
       
   539 lemma self_smaller_than_bound:
 
       
   540   shows "\<forall>s. rsize (rders_simp r s) \<le> N \<Longrightarrow> rsize r \<le> N"
 
       
   541   apply(drule_tac x = "[]" in spec)
 
       
   542   apply simp
 
       
   543   done
 
       
   544 
       
   545 lemma ntimes_closed_form_bounded_nil_aux:
 
       
   546   shows "max (rsize  RZERO) (rsize (RNTIMES r 0)) = 1 + rsize r"
 
       
   547   by auto
 
       
   548 
       
   549 lemma ntimes_closed_form_bounded_nil:
 
       
   550   assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
 
       
   551   shows " rsize (rders_simp (RNTIMES r 0) s) \<le> 1 + rsize r"
 
       
   552   using assms ntimes_closed_form_bounded1 by auto
 
       
   553 
       
   554 lemma ntimes_ineq1:
 
       
   555   shows "(rsize (RNTIMES r n)) \<ge> 1 + rsize r"
 
       
   556   by simp
 
       
   557 
       
   558 lemma ntimes_ineq2:
 
       
   559   shows "1 + rsize r \<le>  
       
   560 max ((Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n))))) (rsize (RNTIMES r n))"
 
       
   561   by (meson le_max_iff_disj ntimes_ineq1)
 
       
   562 
       
   563 lemma ntimes_closed_form_bounded:
 
       
   564   assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
 
       
   565   shows "rsize (rders_simp (RNTIMES r (Suc n)) s) \<le> 
       
   566            max ((Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n))))) (rsize (RNTIMES r n))"
 
       
   567 proof(cases s)
 
       
   568   case Nil
 
       
   569   then show "rsize (rders_simp (RNTIMES r (Suc n)) s)
 
       
   570     \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * Suc (N + rsize (RNTIMES r n))) (rsize (RNTIMES r n))" 
       
   571     by simp
 
       
   572 next
 
       
   573   case (Cons a list)
 
       
   574 
       
   575   then have "rsize (rders_simp (RNTIMES r (Suc n)) s) = 
       
   576              rsize (rsimp (RALTS ((map (optermsimp r)    (nupdates list r [Some ([a], n)])))))"
 
       
   577     using ntimes_closed_form by fastforce
 
       
   578   also have "... \<le> Suc (rsizes (rdistinct ((map (optermsimp r) (nupdates list r [Some ([a], n)]))) {}))"
 
       
   579     using alts_simp_control by blast 
       
   580   also have "... \<le> Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n)))" 
       
   581     using ntimes_control_bounded[OF assms]
 
       
   582     by (metis add_mono le_add1 mult_Suc plus_1_eq_Suc)
 
       
   583   also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * Suc (N + rsize (RNTIMES r n))) (rsize (RNTIMES r n))"
 
       
   584     by simp    
       
   585   finally show ?thesis by simp  
       
   586 qed
 
       
   587 
       
   588 
       
   589 lemma ntimes_closed_form_boundedA:
 
       
   590   assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
 
       
   591   shows "\<exists>N'. \<forall>s. rsize (rders_simp (RNTIMES r n) s) \<le> N'"
 
       
   592   apply(case_tac n)
 
       
   593   using assms ntimes_closed_form_bounded_nil apply blast
 
       
   594   using assms ntimes_closed_form_bounded by blast
 
       
   595 
       
   596 
       
   597 lemma star_closed_form_nonempty_bounded:
 
       
   598   assumes "\<forall>s. rsize (rders_simp r s) \<le> N" and "s \<noteq> []"
 
       
   599   shows "rsize (rders_simp (RSTAR r) s) \<le> 
       
   600             ((Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r))))) "
 
       
   601 proof(cases s)
 
       
   602   case Nil
 
       
   603   then show ?thesis 
       
   604     using local.Nil by fastforce
 
       
   605 next
 
       
   606   case (Cons a list)
 
       
   607   then have "rsize (rders_simp (RSTAR r) s) = 
       
   608     rsize (rsimp (RALTS ((map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])))))"
 
       
   609     using star_closed_form by fastforce
 
       
   610   also have "... \<le> Suc (rsizes (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])) {}))"
 
       
   611     using alts_simp_control by blast 
       
   612   also have "... \<le> Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r)))" 
       
   613     by (smt (z3) add_mono_thms_linordered_semiring(1) assms(1) le_add1 map_eq_conv mult_Suc plus_1_eq_Suc star_control_bounded)
 
       
   614   also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))"
 
       
   615     by simp    
       
   616   finally show ?thesis by simp  
       
   617 qed
 
       
   618 
   383 
   619 
   384 
   620 
   385 lemma seq_estimate_bounded: 
   621 lemma seq_estimate_bounded: 
   386   assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" 
   622   assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" 
   387       and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
 
   623       and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
 
   426   ultimately show "rsize (rders_simp (RSEQ r1 r2) s)
 
   662   ultimately show "rsize (rders_simp (RSEQ r1 r2) s)
 
   427        \<le> max (2 + N1 + (rsize r2) + N2 * card (sizeNregex N2)) (rsize (RSEQ r1 r2))"
 
   663        \<le> max (2 + N1 + (rsize r2) + N2 * card (sizeNregex N2)) (rsize (RSEQ r1 r2))"
 
   428     by auto 
   664     by auto 
   429 qed
 
   665 qed
 
   430 
   666 
   431 
       
   432 lemma rders_simp_bounded: 
   667 lemma rders_simp_bounded: 
   433   shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
 
   668   shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
 
   434   apply(induct r)
 
   669   apply(induct r)
 
   435   apply(rule_tac x = "Suc 0 " in exI)
 
   670   apply(rule_tac x = "Suc 0 " in exI)
 
   436   using three_easy_cases0 apply force
 
   671   using three_easy_cases0 apply force
 
   441   apply(rule allI)
 
   676   apply(rule allI)
 
   442   apply(rule seq_closed_form_bounded2)
 
   677   apply(rule seq_closed_form_bounded2)
 
   443   apply(assumption)
 
   678   apply(assumption)
 
   444   apply(assumption)
 
   679   apply(assumption)
 
   445   apply (metis alts_closed_form_bounded size_list_estimation')
 
   680   apply (metis alts_closed_form_bounded size_list_estimation')
 
   446   using star_closed_form_bounded by blast
 
   681   using star_closed_form_bounded apply blast
 
   447 
   682   using ntimes_closed_form_boundedA by blast
 
   448 
   683   
       
   684   
   449 unused_thms
 
   685 unused_thms
 
       
   686 export_code rders_simp rsimp rder in Scala module_name Example
 
       
   687 
   450 
   688 
   451 end
 
   689 end
lexing