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/ClosedFormsBounds.thy
changeset 451 7a016eeb118d
parent 450 dabd25e8e4e9
child 452 4aded96b3923
equal deleted inserted replaced
450:dabd25e8e4e9 451:7a016eeb118d 
     1 
     1 (**)
 
     2 theory ClosedFormsBounds
 
     2 theory ClosedFormsBounds
 
     3   imports "GeneralRegexBound" "ClosedForms"
 
     3   imports "GeneralRegexBound" "ClosedForms"
 
     4 begin
 
     4 begin
 
     5 
       
     6 lemma alts_ders_lambda_shape_ders:
 
     5 lemma alts_ders_lambda_shape_ders:
 
     7   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"
 
     8   by (simp add: image_iff)
 
     7   by (simp add: image_iff)
 
     9 
       
    10 
       
    11 
     8 
    12 lemma rlist_bound:
 
     9 lemma rlist_bound:
 
    13   shows "\<forall>r \<in> set rs. rsize r \<le> N \<Longrightarrow> sum_list (map rsize rs) \<le> N * (length rs)"
 
    10   shows "\<forall>r \<in> set rs. rsize r \<le> N \<Longrightarrow> sum_list (map rsize rs) \<le> N * (length rs)"
 
    14   apply(induct rs)
 
    11   apply(induct rs)
 
    15   apply simp
 
    12   apply simp
 
    44 
    41 
    45 lemma alts_simp_ineq_unfold:
 
    42 lemma alts_simp_ineq_unfold:
 
    46   shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))"
 
    43   shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))"
 
    47   using rsimp_aalts_smaller by auto
 
    44   using rsimp_aalts_smaller by auto
 
    48 
    45 
       
    46 lemma no_elem_distinct :
 
       
    47   shows "a \<notin> set rs \<Longrightarrow> rdistinct rs rset = rdistinct rs (insert a rset)"
 
       
    48   apply(induct rs arbitrary: rset)
 
       
    49    apply simp
 
       
    50   by force
 
       
    51   
       
    52 
       
    53 
       
    54 
       
    55 inductive good :: "rrexp \<Rightarrow> bool"
 
       
    56   where
 
       
    57 "RZERO \<notin> set rs \<Longrightarrow> good (RALTS rs)"
 
       
    58 |"good RZERO"
 
       
    59 |"good RONE"
 
       
    60 |"good (RCHAR c)"
 
       
    61 |"good (RSEQ r1 r2)"
 
       
    62 |"good (RSTAR r0)"
 
       
    63 
       
    64 
       
    65 lemma after_flts_no0:
 
       
    66   shows "\<forall>r \<in> set rs. good r \<Longrightarrow> RZERO \<notin> set (rflts rs)"
 
       
    67   apply(induct rs)
 
       
    68    apply simp
 
       
    69   apply(case_tac a)
 
       
    70        apply simp
 
       
    71   apply simp
 
       
    72   apply simp
 
       
    73     apply simp
 
       
    74   apply simp
 
       
    75   using good.simps apply blast
 
       
    76   apply simp
 
       
    77   done
 
       
    78 
    49 lemma flts_has_no_zero:
 
    79 lemma flts_has_no_zero:
 
    50   shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)"
 
    80   shows "\<forall>r \<in> set rs. good r \<Longrightarrow> rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)"
 
    51 
    81   apply(subgoal_tac "RZERO \<notin> set (rflts rs)")  
    52   sorry
 
    82    apply (meson no_elem_distinct)
 
       
    83   apply(insert after_flts_no0)
 
       
    84   by blast
 
       
    85 
       
    86 lemma shape_of_alts:
 
       
    87   shows "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs) \<Longrightarrow> RZERO \<notin> alts_set \<and> RONE \<notin> alts_set"
 
       
    88   by fastforce
 
       
    89 
       
    90 lemma quantified2_implies1:
 
       
    91   shows "\<forall>r. P \<and> Q \<Longrightarrow> \<forall>r. P"
 
       
    92   by auto
 
       
    93 
       
    94 lemma quantified_quantifiedAB_A:
 
       
    95   shows " (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) \<Longrightarrow> \<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs"
 
       
    96   by fastforce
 
       
    97 
       
    98 
       
    99 
       
   100 
       
   101 lemma list_distinct_removal:
 
       
   102   shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rs1) rset = rdistinct rs1 rset"
 
       
   103   apply(induct rs arbitrary: rset)
 
       
   104    apply simp
 
       
   105   by simp
 
       
   106 
       
   107 
       
   108 lemma rdistinct_mono_list:
 
       
   109   shows " sum_list (map rsize (rdistinct (x5 @ rs) rset )) \<le>
 
       
   110         ( sum_list (map rsize x5)) + (sum_list (map rsize (rdistinct  rs ((set x5 ) \<union> rset))))"
 
       
   111   apply(induct x5 arbitrary: rs rset)
 
       
   112    apply simp
 
       
   113   apply(case_tac "a \<in> rset")
 
       
   114    apply simp
 
       
   115    apply (simp add: add.assoc insert_absorb trans_le_add2)
 
       
   116   apply simp
 
       
   117   by (metis Un_insert_right)
 
       
   118 
       
   119 
       
   120 lemma flts_size_reduction_alts:
 
       
   121   shows " \<And>a rs noalts_set alts_set corr_set x5.
 
       
   122        \<lbrakk>\<And>noalts_set alts_set corr_set.
 
       
   123            (\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs) \<and>
 
       
   124            (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) \<Longrightarrow>
 
       
   125            Suc (sum_list (map rsize (rdistinct (rflts rs) (noalts_set \<union> corr_set))))
 
       
   126            \<le> Suc (sum_list (map rsize (rdistinct rs (insert RZERO (noalts_set \<union> alts_set)))));
 
       
   127         (\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs) \<and>
 
       
   128         (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set);
 
       
   129         a = RALTS x5\<rbrakk>
 
       
   130        \<Longrightarrow> Suc (sum_list (map rsize (rdistinct (rflts (a # rs)) (noalts_set \<union> corr_set))))
 
       
   131            \<le> Suc (sum_list
 
       
   132                     (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))))"
 
       
   133   apply(case_tac "a \<in> alts_set")
 
       
   134    apply simp
 
       
   135    apply(subgoal_tac "set x5 \<subseteq> corr_set")
 
       
   136   apply(subst list_distinct_removal)
 
       
   137   apply auto[1]
 
       
   138     apply presburger
 
       
   139    apply fastforce
 
       
   140   apply (subgoal_tac "a \<notin> noalts_set")
 
       
   141   prefer 2
 
       
   142   apply blast
 
       
   143   apply simp
 
       
   144   apply(subgoal_tac "sum_list (map rsize (rdistinct (x5 @ rflts rs) (noalts_set \<union> corr_set))) 
       
   145                    \<le> sum_list (map rsize x5 ) + sum_list (map rsize (rdistinct (rflts rs) ((set x5) \<union> (noalts_set \<union> corr_set))))")
 
       
   146   prefer 2
 
       
   147   using rdistinct_mono_list apply presburger
 
       
   148   apply(subgoal_tac "insert (RALTS x5) (noalts_set \<union> alts_set) = noalts_set \<union> (insert (RALTS x5) alts_set)")
 
       
   149    apply(simp only:)
 
       
   150   apply(subgoal_tac "sum_list (map rsize x5) + 
       
   151 sum_list (map rsize (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> (set x5))))) \<le>
 
       
   152 Suc (sum_list (map rsize x5) +
 
       
   153                    sum_list
 
       
   154                     (map rsize
 
       
   155                       (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set)))))")
 
       
   156   
       
   157   apply (simp add: Un_left_commute inf_sup_aci(5))
 
       
   158    apply(subgoal_tac "sum_list (map rsize (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> set x5))))
 
       
   159 \<le> sum_list
 
       
   160                     (map rsize
 
       
   161                       (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set))))")
 
       
   162     apply linarith
 
       
   163    apply(subgoal_tac "\<forall>r \<in>  insert (RALTS x5) alts_set. \<exists>xs1.( r = RALTS xs1 \<and> set xs1 \<subseteq> corr_set \<union> set x5)")
 
       
   164     apply presburger
 
       
   165    apply (meson insert_iff sup.cobounded2 sup.coboundedI1)
 
       
   166   by blast
 
       
   167 
       
   168 
       
   169 
       
   170 
       
   171 lemma flts_vs_nflts1:
 
       
   172   shows "(\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs)
 
       
   173  \<and> (\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set))  
       
   174 \<Longrightarrow>  (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set)  )))
 
       
   175          \<le>  (sum_list (map rsize (rdistinct rs (insert RZERO (noalts_set \<union> alts_set) ))))"
 
       
   176     apply(induct rs arbitrary: noalts_set alts_set corr_set)
 
       
   177    apply simp
 
       
   178   apply(case_tac a)
 
       
   179        apply(case_tac "RZERO \<in> noalts_set")
 
       
   180         apply simp
 
       
   181        apply(subgoal_tac "RZERO \<notin> alts_set")
 
       
   182         apply simp
 
       
   183        apply fastforce
 
       
   184       apply(case_tac "RONE \<in> noalts_set")
 
       
   185        apply simp
 
       
   186       apply(subgoal_tac "RONE \<notin> alts_set")
 
       
   187   prefer 2
 
       
   188   apply fastforce
 
       
   189       apply(case_tac "RONE \<in> corr_set")
 
       
   190        apply(subgoal_tac "rflts (a # rs) = RONE # rflts rs")
 
       
   191         apply(simp only:)
 
       
   192         apply(subgoal_tac "rdistinct (RONE # rflts rs) (noalts_set \<union> corr_set) = 
       
   193                            rdistinct (rflts rs) (noalts_set \<union> corr_set)")
 
       
   194          apply(simp only:)
 
       
   195   apply(subgoal_tac "rdistinct (RONE # rs) (insert RZERO (noalts_set \<union> alts_set)) =
 
       
   196                      RONE # (rdistinct rs (insert RONE (insert RZERO (noalts_set \<union> alts_set)))) ")
 
       
   197           apply(simp only:)
 
       
   198   apply(subgoal_tac "rdistinct (rflts rs) (noalts_set \<union> corr_set) = 
       
   199                      rdistinct (rflts rs) (insert RONE (noalts_set \<union> corr_set))")
 
       
   200   apply (simp only:)
 
       
   201   apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
 
       
   202             apply(simp only:)
 
       
   203   apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) = 
       
   204                      insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
 
       
   205              apply(simp only:)
 
       
   206   apply(subgoal_tac "  (sum_list
 
       
   207                     (map rsize ( rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))
 
       
   208                    \<le>  (sum_list
 
       
   209                     (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))")
 
       
   210   apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
 
       
   211   apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
 
       
   212             apply fastforce
 
       
   213            apply fastforce
 
       
   214   apply (metis Un_iff insert_absorb)
 
       
   215          apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1))
 
       
   216         apply (meson UnCI rdistinct.simps(2))
 
       
   217   using rflts.simps(4) apply presburger
 
       
   218       apply simp
 
       
   219       apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
 
       
   220   apply(simp only:)
 
       
   221   apply (metis Un_insert_left insertE rrexp.distinct(15))
 
       
   222       apply fastforce
 
       
   223      apply(case_tac "a \<in> noalts_set")
 
       
   224       apply simp
 
       
   225   apply(subgoal_tac "a \<notin> alts_set")
 
       
   226       prefer 2
 
       
   227       apply blast
 
       
   228   apply(case_tac "a \<in> corr_set")
 
       
   229       apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
 
       
   230   prefer 2
 
       
   231   apply fastforce
 
       
   232       apply(simp only:)
 
       
   233       apply(subgoal_tac "  sum_list
 
       
   234                (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))
 
       
   235 \<le>
 
       
   236                 sum_list
 
       
   237                (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set))))")
 
       
   238 
       
   239        apply(subgoal_tac 
       
   240 "sum_list (map rsize (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)))
 
       
   241 \<le>
 
       
   242  sum_list (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))")
 
       
   243   apply fastforce
 
       
   244        apply simp
 
       
   245   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
       
   246         apply(simp only:)
 
       
   247         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
       
   248   apply(simp only:)
 
       
   249   apply (metis insertE rrexp.distinct(21))
 
       
   250         apply blast
 
       
   251   
       
   252   apply fastforce
 
       
   253   apply force
 
       
   254      apply simp
 
       
   255      apply (metis Un_insert_left insert_iff rrexp.distinct(21))
 
       
   256     apply(case_tac "a \<in> noalts_set")
 
       
   257      apply simp
 
       
   258   apply(subgoal_tac "a \<notin> alts_set")
 
       
   259       prefer 2
 
       
   260       apply blast
 
       
   261   apply(case_tac "a \<in> corr_set")
 
       
   262       apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
 
       
   263   prefer 2
 
       
   264   apply fastforce
 
       
   265       apply(simp only:)
 
       
   266       apply(subgoal_tac "  sum_list
 
       
   267                (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))
 
       
   268 \<le>
 
       
   269                 sum_list
 
       
   270                (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set))))")
 
       
   271 
       
   272        apply(subgoal_tac 
       
   273 "sum_list (map rsize (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)))
 
       
   274 \<le>
 
       
   275  sum_list (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))")
 
       
   276   apply fastforce
 
       
   277        apply simp
 
       
   278   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
       
   279         apply(simp only:)
 
       
   280         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
       
   281   apply(simp only:)
 
       
   282 
       
   283 
       
   284   apply (metis insertE rrexp.distinct(25))
 
       
   285   apply blast
 
       
   286   apply fastforce
 
       
   287   apply force
 
       
   288      apply simp
 
       
   289   
       
   290     apply (metis Un_insert_left insertE rrexp.distinct(25))
 
       
   291 
       
   292   using Suc_le_mono flts_size_reduction_alts apply presburger
 
       
   293      apply(case_tac "a \<in> noalts_set")
 
       
   294       apply simp
 
       
   295   apply(subgoal_tac "a \<notin> alts_set")
 
       
   296       prefer 2
 
       
   297       apply blast
 
       
   298   apply(case_tac "a \<in> corr_set")
 
       
   299       apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
 
       
   300   prefer 2
 
       
   301   apply fastforce
 
       
   302       apply(simp only:)
 
       
   303       apply(subgoal_tac "  sum_list
 
       
   304                (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))
 
       
   305 \<le>
 
       
   306                 sum_list
 
       
   307                (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set))))")
 
       
   308 
       
   309        apply(subgoal_tac 
       
   310 "sum_list (map rsize (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)))
 
       
   311 \<le>
 
       
   312  sum_list (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))")
 
       
   313   apply fastforce
 
       
   314        apply simp
 
       
   315   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
 
       
   316         apply(simp only:)
 
       
   317         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
 
       
   318   apply(simp only:)
 
       
   319   apply (metis insertE rrexp.distinct(29))
 
       
   320 
       
   321         apply blast
 
       
   322   
       
   323   apply fastforce
 
       
   324   apply force
 
       
   325      apply simp
 
       
   326   apply (metis Un_insert_left insert_iff rrexp.distinct(29))
 
       
   327   done
 
       
   328 
       
   329 
       
   330 
       
   331 
    53 
   332 
    54 lemma flts_vs_nflts:
 
   333 lemma flts_vs_nflts:
 
    55   shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs
 
   334   shows "(\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs)
 
    56  \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)  
   335  \<and> (\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set))  
    57 \<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set)  )))
 
   336 \<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set)  )))
 
    58          \<le> Suc (sum_list (map rsize (rdistinct rs (noalts_set \<union> alts_set) )))"
 
   337          \<le> Suc (sum_list (map rsize (rdistinct rs (insert RZERO (noalts_set \<union> alts_set) ))))"
 
    59   apply(induct rs arbitrary: noalts_set)
 
   338   apply(induct rs arbitrary: noalts_set alts_set corr_set)
 
    60    apply simp
 
   339    apply simp
 
    61 
   340   apply(case_tac a)
 
    62   sorry
 
   341        apply(case_tac "RZERO \<in> noalts_set")
 
       
   342         apply simp
 
       
   343        apply(subgoal_tac "RZERO \<notin> alts_set")
 
       
   344         apply simp
 
       
   345        apply fastforce
 
       
   346       apply(case_tac "RONE \<in> noalts_set")
 
       
   347        apply simp
 
       
   348       apply(subgoal_tac "RONE \<notin> alts_set")
 
       
   349   prefer 2
 
       
   350   apply fastforce
 
       
   351       apply(case_tac "RONE \<in> corr_set")
 
       
   352        apply(subgoal_tac "rflts (a # rs) = RONE # rflts rs")
 
       
   353         apply(simp only:)
 
       
   354         apply(subgoal_tac "rdistinct (RONE # rflts rs) (noalts_set \<union> corr_set) = 
       
   355                            rdistinct (rflts rs) (noalts_set \<union> corr_set)")
 
       
   356          apply(simp only:)
 
       
   357   apply(subgoal_tac "rdistinct (RONE # rs) (insert RZERO (noalts_set \<union> alts_set)) =
 
       
   358                      RONE # (rdistinct rs (insert RONE (insert RZERO (noalts_set \<union> alts_set)))) ")
 
       
   359           apply(simp only:)
 
       
   360   apply(subgoal_tac "rdistinct (rflts rs) (noalts_set \<union> corr_set) = 
       
   361                      rdistinct (rflts rs) (insert RONE (noalts_set \<union> corr_set))")
 
       
   362   apply (simp only:)
 
       
   363   apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
 
       
   364             apply(simp only:)
 
       
   365   apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) = 
       
   366                      insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
 
       
   367              apply(simp only:)
 
       
   368   apply(subgoal_tac " Suc (sum_list
 
       
   369                     (map rsize ( rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))
 
       
   370                    \<le> Suc (sum_list
 
       
   371                     (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))")
 
       
   372   apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
 
       
   373   apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
 
       
   374             apply fastforce
 
       
   375            apply fastforce
 
       
   376   apply (metis Un_iff insert_absorb)
 
       
   377          apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1))
 
       
   378         apply (meson UnCI rdistinct.simps(2))
 
       
   379   using rflts.simps(4) apply presburger
 
       
   380       apply simp
 
       
   381       apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
 
       
   382   apply(simp only:)
 
       
   383   apply (metis Un_insert_left insertE rrexp.distinct(15))
 
       
   384       apply fastforce
 
       
   385      apply(case_tac "a \<in> noalts_set")
 
       
   386       apply simp
 
       
   387   apply(subgoal_tac "a \<notin> alts_set")
 
       
   388       prefer 2
 
       
   389       apply blast
 
       
   390   apply(case_tac "a \<in> corr_set")
 
       
   391       apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
 
       
   392   prefer 2
 
       
   393   apply fastforce
 
       
   394       apply(simp only:)
 
       
   395   apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
 
       
   396   apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
 
       
   397      apply(case_tac "a \<in> noalts_set")
 
       
   398       apply simp
 
       
   399   apply(subgoal_tac "a \<notin> alts_set")
 
       
   400       prefer 2
 
       
   401       apply blast
 
       
   402   apply(case_tac "a \<in> corr_set")
 
       
   403       apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
 
       
   404   prefer 2
 
       
   405   apply fastforce
 
       
   406       apply(simp only:)
 
       
   407   apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
 
       
   408   apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
 
       
   409    prefer 2
 
       
   410      apply(case_tac "a \<in> noalts_set")
 
       
   411       apply simp
 
       
   412   apply(subgoal_tac "a \<notin> alts_set")
 
       
   413       prefer 2
 
       
   414       apply blast
 
       
   415   apply(case_tac "a \<in> corr_set")
 
       
   416       apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
 
       
   417   prefer 2
 
       
   418   apply fastforce
 
       
   419       apply(simp only:)
 
       
   420   apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
 
       
   421   apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
 
       
   422   using flts_size_reduction_alts apply presburger
 
       
   423   done
 
       
   424 
       
   425 
       
   426 
       
   427 
       
   428 
       
   429 (*  apply(rutac x = "\<lambda>a rs noalts_set alts_set corr_set. set xs ")*)
 
       
   430   
    63 
   431 
    64 lemma distinct_simp_ineq_general:
 
   432 lemma distinct_simp_ineq_general:
 
    65   shows "rsimp ` no_simp = has_simp \<and> finite no_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
 
   433   shows "rsimp ` no_simp = has_simp \<and> finite no_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
 
    66     \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))"
 
   434     \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))"
 
    67   apply(induct rs arbitrary: no_simp has_simp)
 
   435   apply(induct rs arbitrary: no_simp has_simp)
 
    71     apply auto[1]
 
   439     apply auto[1]
 
    72   apply blast
 
   440   apply blast
 
    73   apply(case_tac "rsimp a \<in> no_simp")
 
   441   apply(case_tac "rsimp a \<in> no_simp")
 
    74    apply(subgoal_tac "rsimp a \<in> has_simp")
 
   442    apply(subgoal_tac "rsimp a \<in> has_simp")
 
    75   prefer 2
 
   443   prefer 2
 
    76   apply (simp add: rev_image_eqI rsimp_idem)
 
   444     apply (simp add: rev_image_eqI rsimp_idem)
 
    77   sledgehammer[timeout = 100]
 
   445   apply simp
 
    78 
   446    apply (metis finite_insert image_insert insert_absorb trans_le_add2)
 
    79   sorry
 
   447   apply(case_tac "rsimp a \<notin> has_simp")
 
       
   448   apply simp
 
       
   449    apply (metis add_mono_thms_linordered_semiring(1) finite.insertI image_insert rsimp_mono)
 
       
   450   apply simp
 
       
   451   by (metis finite.insertI image_insert insert_absorb trans_le_add2)
 
    80 
   452 
    81 
   453 
    82 lemma not_mentioned_elem_distinct_strong:
 
   454 lemma not_mentioned_elem_distinct_strong:
 
    83   shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs rset)) = (r \<in> set (rdistinct rs (insert a rset)))"
 
   455   shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs rset)) = (r \<in> set (rdistinct rs (insert a rset)))"
 
    84   apply(induct rs arbitrary: rset)
 
   456   apply(induct rs arbitrary: rset)
 
    90   by (metis not_mentioned_elem_distinct_strong)
 
   462   by (metis not_mentioned_elem_distinct_strong)
 
    91 
   463 
    92 
   464 
    93 
   465 
    94 
   466 
    95 
   467 lemma larger_acc_smaller_distinct_res0:
 
       
   468   shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))"
 
       
   469   apply(induct rs arbitrary: ss SS)
 
       
   470   apply simp
 
       
   471   apply(case_tac "a \<in> ss")
 
       
   472    apply(subgoal_tac "a \<in> SS")
 
       
   473     apply simp
 
       
   474    apply blast
 
       
   475   apply(case_tac "a \<in> SS")
 
       
   476    apply simp
 
       
   477    apply(subgoal_tac "insert a ss \<subseteq> SS")
 
       
   478     apply simp
 
       
   479   apply (simp add: trans_le_add2)
 
       
   480   apply blast
 
       
   481   apply(simp)
 
       
   482   apply(subgoal_tac "insert a ss \<subseteq> insert a SS")
 
       
   483    apply blast
 
       
   484   by blast
 
    96 
   485 
    97 
   486 
    98 lemma without_flts_ineq:
 
   487 lemma without_flts_ineq:
 
    99   shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> 
   488   shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> 
   100          Suc (sum_list (map rsize (rdistinct (    rs  ) {}  )))"
 
   489          Suc (sum_list (map rsize (rdistinct (    rs  ) {}  )))"
 
   101   by (metis empty_iff flts_vs_nflts sup_bot_left)
 
   490 proof -
 
       
   491   have " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le>  
       
   492          Suc (sum_list (map rsize (rdistinct rs (insert RZERO {}))))"
 
       
   493     by (metis empty_iff flts_vs_nflts sup_bot_left)
 
       
   494   also have "... \<le>  Suc (sum_list (map rsize (rdistinct rs {})))" 
       
   495     by (simp add: larger_acc_smaller_distinct_res0)
 
       
   496   finally show ?thesis sledgehammer
 
       
   497     by blast
 
       
   498 qed
 
       
   499 
       
   500 
   102 
   501 
   103 
   502 
   104 
   503 
   105 
   504 
   106 lemma distinct_simp_ineq:
 
   505 lemma distinct_simp_ineq:
 
   129 
   528 
   130 lemma rdistinct_equality1:
 
   529 lemma rdistinct_equality1:
 
   131   shows "a \<notin> ss \<Longrightarrow> rdistinct (a  # rs) ss = a # rdistinct rs (insert a ss) "
 
   530   shows "a \<notin> ss \<Longrightarrow> rdistinct (a  # rs) ss = a # rdistinct rs (insert a ss) "
 
   132   by auto
 
   531   by auto
 
   133 
   532 
   134 lemma larger_acc_smaller_distinct_res0:
 
   533 
   135   shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))"
 
       
   136   apply(induct rs arbitrary: ss SS)
 
       
   137   apply simp
 
       
   138   apply(case_tac "a \<in> ss")
 
       
   139    apply(subgoal_tac "a \<in> SS")
 
       
   140     apply simp
 
       
   141    apply blast
 
       
   142   apply(case_tac "a \<in> SS")
 
       
   143    apply simp
 
       
   144    apply(subgoal_tac "insert a ss \<subseteq> SS")
 
       
   145     apply simp
 
       
   146   apply (simp add: trans_le_add2)
 
       
   147   apply blast
 
       
   148   apply(simp)
 
       
   149   apply(subgoal_tac "insert a ss \<subseteq> insert a SS")
 
       
   150    apply blast
 
       
   151   by blast
 
       
   152 
   534 
   153 
   535 
   154 lemma larger_acc_smaller_distinct_res:
 
   536 lemma larger_acc_smaller_distinct_res:
 
   155   shows " (sum_list (map rsize (rdistinct rs ss))) \<ge> (sum_list (map rsize (rdistinct rs (insert a ss))))"
 
   537   shows " (sum_list (map rsize (rdistinct rs ss))) \<ge> (sum_list (map rsize (rdistinct rs (insert a ss))))"
 
   156   apply(subgoal_tac "ss \<subseteq> (insert a ss)")
 
   538   apply(subgoal_tac "ss \<subseteq> (insert a ss)")
 
   391   apply (metis alts_closed_form_bounded size_list_estimation')
 
   773   apply (metis alts_closed_form_bounded size_list_estimation')
 
   392   using star_closed_form_bounded by blast
 
   774   using star_closed_form_bounded by blast
 
   393 
   775 
   394 
   776 
   395 
   777 
   396 
   778 unused_thms
 
   397 
   779 
   398 
   780 
   399 
   781 
   400 
   782 
   401 
   783
lexing