thys3/src/ClosedFormsBounds.thy
changeset 563 c92a41d9c4da
parent 496 f493a20feeb3
equal deleted inserted replaced
562:57e33978e55d 563:c92a41d9c4da
   139   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)) = 
   140                      insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
   140                      insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
   141              apply(simp only:)
   141              apply(simp only:)
   142   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)))
   143                    \<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)))")
   144   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))
   145   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)
   146             apply fastforce
   146             apply fastforce
   147            apply fastforce
   147            apply fastforce
   148   apply (metis Un_iff insert_absorb)
   148   apply (metis Un_iff insert_absorb)
   149          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))
   150         apply (meson UnCI rdistinct.simps(2))
   150         apply (meson UnCI rdistinct.simps(2))
   151   using rflts.simps(4) apply presburger
   151   using rflts.simps(4) apply presburger
   152       apply simp
   152       apply simp
   153       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")
   154   apply(simp only:)
   154         apply(simp only:)
   155   apply (metis Un_insert_left insertE rrexp.distinct(15))
   155   apply (metis Un_insert_left insertE rrexp.distinct(17))
   156       apply fastforce
   156       apply fastforce
   157      apply(case_tac "a \<in> noalts_set")
   157      apply(case_tac "a \<in> noalts_set")
   158       apply simp
   158       apply simp
   159   apply(subgoal_tac "a \<notin> alts_set")
   159   apply(subgoal_tac "a \<notin> alts_set")
   160       prefer 2
   160       prefer 2
   172   apply fastforce
   172   apply fastforce
   173        apply simp
   173        apply simp
   174   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")
   175         apply(simp only:)
   175         apply(simp only:)
   176         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")
   177   apply(simp only:)
   177           apply(simp only:)
   178   apply (metis insertE rrexp.distinct(21))
   178   apply (metis insertE nonalt.simps(1) nonalt.simps(4))
   179         apply blast
   179         apply blast
   180   
   180   
   181   apply fastforce
   181   apply fastforce
   182   apply force
   182   apply force
   183      apply simp
   183       apply simp
   184      apply (metis Un_insert_left insert_iff rrexp.distinct(21))
   184   apply (metis Un_insert_left insertE nonalt.simps(1) nonalt.simps(4))
   185     apply(case_tac "a \<in> noalts_set")
   185     apply(case_tac "a \<in> noalts_set")
   186      apply simp
   186      apply simp
   187   apply(subgoal_tac "a \<notin> alts_set")
   187   apply(subgoal_tac "a \<notin> alts_set")
   188       prefer 2
   188       prefer 2
   189       apply blast
   189       apply blast
   202   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")
   203         apply(simp only:)
   203         apply(simp only:)
   204         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")
   205   apply(simp only:)
   205   apply(simp only:)
   206 
   206 
   207 
   207          apply (metis insertE rrexp.distinct(31))
   208   apply (metis insertE rrexp.distinct(25))
       
   209   apply blast
   208   apply blast
   210   apply fastforce
   209   apply fastforce
   211   apply force
   210   apply force
   212      apply simp
   211      apply simp
   213   
   212   
   214     apply (metis Un_insert_left insertE rrexp.distinct(25))
   213     apply (metis Un_insert_left insertE rrexp.distinct(31))
   215 
   214 
   216   using Suc_le_mono flts_size_reduction_alts apply presburger
   215   using Suc_le_mono flts_size_reduction_alts apply presburger
   217      apply(case_tac "a \<in> noalts_set")
   216      apply(case_tac "a \<in> noalts_set")
   218       apply simp
   217       apply simp
   219   apply(subgoal_tac "a \<notin> alts_set")
   218   apply(subgoal_tac "a \<notin> alts_set")
   232   apply fastforce
   231   apply fastforce
   233        apply simp
   232        apply simp
   234   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")
   235         apply(simp only:)
   234         apply(simp only:)
   236         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")
   237   apply(simp only:)
   236        apply(simp only:)
   238   apply (metis insertE rrexp.distinct(29))
   237   apply (metis insertE rrexp.distinct(37))
   239 
   238 
   240         apply blast
   239         apply blast
   241   
   240   
   242   apply fastforce
   241   apply fastforce
   243   apply force
   242   apply force
   244      apply simp
   243      apply simp
   245   apply (metis Un_insert_left insert_iff rrexp.distinct(29))
   244    apply (metis Un_insert_left insert_iff rrexp.distinct(37))
   246   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))
   247 
   272 
   248 
   273 
   249 lemma flts_vs_nflts:
   274 lemma flts_vs_nflts:
   250   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"
   251   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)"
   375     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)
   376   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))"
   377     by simp    
   402     by simp    
   378   finally show ?thesis by simp  
   403   finally show ?thesis by simp  
   379 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 
   380 
   619 
   381 
   620 
   382 lemma seq_estimate_bounded: 
   621 lemma seq_estimate_bounded: 
   383   assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" 
   622   assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" 
   384       and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
   623       and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
   423   ultimately show "rsize (rders_simp (RSEQ r1 r2) s)
   662   ultimately show "rsize (rders_simp (RSEQ r1 r2) s)
   424        \<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))"
   425     by auto 
   664     by auto 
   426 qed
   665 qed
   427 
   666 
   428 
       
   429 lemma rders_simp_bounded: 
   667 lemma rders_simp_bounded: 
   430   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"
   431   apply(induct r)
   669   apply(induct r)
   432   apply(rule_tac x = "Suc 0 " in exI)
   670   apply(rule_tac x = "Suc 0 " in exI)
   433   using three_easy_cases0 apply force
   671   using three_easy_cases0 apply force
   438   apply(rule allI)
   676   apply(rule allI)
   439   apply(rule seq_closed_form_bounded2)
   677   apply(rule seq_closed_form_bounded2)
   440   apply(assumption)
   678   apply(assumption)
   441   apply(assumption)
   679   apply(assumption)
   442   apply (metis alts_closed_form_bounded size_list_estimation')
   680   apply (metis alts_closed_form_bounded size_list_estimation')
   443   using star_closed_form_bounded by blast
   681   using star_closed_form_bounded apply blast
   444 
   682   using ntimes_closed_form_boundedA by blast
   445 
   683   
       
   684   
   446 unused_thms
   685 unused_thms
       
   686 export_code rders_simp rsimp rder in Scala module_name Example
       
   687 
   447 
   688 
   448 end
   689 end