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.
thys/PDerivs.thy
changeset 329 a730a5a0bab9
parent 313 3b8e3a156200
child 359 fedc16924b76
equal deleted inserted replaced
328:e50c470bcfeb 329:a730a5a0bab9 
     1    
     1    
     2 theory PDerivs
 
     2 theory PDerivs
 
     3   imports Spec
 
     3   imports Spec 
     4 begin
 
     4 begin
 
       
     5 
       
     6 
     5 
     7 
     6 abbreviation
 
     8 abbreviation
 
     7   "SEQs rs r \<equiv> (\<Union>r' \<in> rs. {SEQ r' r})"
 
     9   "SEQs rs r \<equiv> (\<Union>r' \<in> rs. {SEQ r' r})"
 
     8 
    10 
     9 lemma SEQs_eq_image:
 
    11 lemma SEQs_eq_image:
 
   342   finally show "card (pders_Set A r) \<le> awidth r + 1" by simp
 
   344   finally show "card (pders_Set A r) \<le> awidth r + 1" by simp
 
   343 qed
 
   345 qed
 
   344 
   346 
   345 (* other result by antimirov *)
 
   347 (* other result by antimirov *)
 
   346 
   348 
       
   349 lemma card_pders_awidth: 
       
   350   shows "card (pders s r) \<le> awidth r + 1"
 
       
   351 proof -
 
       
   352   have "pders s r \<subseteq> pders_Set UNIV r"
 
       
   353     using pders_Set_def by auto
 
       
   354   then have "card (pders s r) \<le> card (pders_Set UNIV r)"
 
       
   355     by (simp add: card_mono finite_pders_set)
 
       
   356   then show "card (pders s r) \<le> awidth r + 1"
 
       
   357     using card_pders_set_le_awidth order_trans by blast
 
       
   358 qed
 
       
   359     
       
   360   
       
   361   
       
   362 
       
   363 
   347 fun subs :: "rexp \<Rightarrow> rexp set" where
 
   364 fun subs :: "rexp \<Rightarrow> rexp set" where
 
   348 "subs ZERO = {ZERO}" |
 
   365 "subs ZERO = {ZERO}" |
 
   349 "subs ONE = {ONE}" |
 
   366 "subs ONE = {ONE}" |
 
   350 "subs (CHAR a) = {CHAR a, ONE}" |
 
   367 "subs (CHAR a) = {CHAR a, ONE}" |
 
   351 "subs (ALT r1 r2) = (subs r1 \<union> subs r2 \<union> {ALT r1 r2})" |
 
   368 "subs (ALT r1 r2) = (subs r1 \<union> subs r2 \<union> {ALT r1 r2})" |
 
   352 "subs (SEQ r1 r2) = (subs r1 \<union> subs r2 \<union> {SEQ r1 r2} \<union>  SEQs (subs r1) r2)" |
 
   369 "subs (SEQ r1 r2) = (subs r1 \<union> subs r2 \<union> {SEQ r1 r2} \<union>  SEQs (subs r1) r2)" |
 
   353 "subs (STAR r1) = (subs r1 \<union> {STAR r1} \<union> SEQs (subs r1) (STAR r1))"
 
   370 "subs (STAR r1) = (subs r1 \<union> {STAR r1} \<union> SEQs (subs r1) (STAR r1))"
 
       
   371 
       
   372 lemma subs_finite:
 
       
   373   shows "finite (subs r)"
 
       
   374   apply(induct r) 
       
   375   apply(simp_all)
 
       
   376   done
 
       
   377 
       
   378 
   354 
   379 
   355 lemma pders_subs:
 
   380 lemma pders_subs:
 
   356   shows "pders s r \<subseteq> subs r"
 
   381   shows "pders s r \<subseteq> subs r"
 
   357   apply(induct r arbitrary: s)
 
   382   apply(induct r arbitrary: s)
 
   358        apply(simp)
 
   383        apply(simp)
 
   398   apply(induct r)
 
   423   apply(induct r)
 
   399   apply(simp)
 
   424   apply(simp)
 
   400   apply(simp_all)
 
   425   apply(simp_all)
 
   401   done
 
   426   done
 
   402 
   427 
   403 lemma
 
   428 lemma subs_card:
 
       
   429   shows "card (subs r) \<le> Suc (size2 r + size2 r)"
 
       
   430   apply(induct r)
 
       
   431        apply(auto)
 
       
   432     apply(subst card_insert)
 
       
   433      apply(simp add: subs_finite)
 
       
   434     apply(simp add: subs_finite)
 
       
   435   oops
 
       
   436 
       
   437 lemma subs_size2:
 
   404   shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)"
 
   438   shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)"
 
   405   apply(induct r)
 
   439   apply(induct r)
 
   406        apply(simp)
 
   440        apply(simp)
 
   407       apply(simp)
 
   441       apply(simp)
 
   408      apply(simp)
 
   442      apply(simp)
 
   425    apply(assumption)
 
   459    apply(assumption)
 
   426   apply(simp)
 
   460   apply(simp)
 
   427   using size_rexp
 
   461   using size_rexp
 
   428   apply(simp)
 
   462   apply(simp)
 
   429   done
 
   463   done
 
       
   464 
       
   465 lemma awidth_size:
 
       
   466   shows "awidth r \<le> size2 r"
 
       
   467   apply(induct r)
 
       
   468        apply(simp_all)
 
       
   469   done
 
       
   470 
       
   471 lemma Sum1:
 
       
   472   fixes A B :: "nat set"
 
       
   473   assumes "A \<subseteq> B" "finite A" "finite B"
 
       
   474   shows "\<Sum>A \<le> \<Sum>B"
 
       
   475   using  assms
 
       
   476   by (simp add: sum_mono2)
 
       
   477 
       
   478 lemma Sum2:
 
       
   479   fixes A :: "rexp set"  
       
   480   and   f g :: "rexp \<Rightarrow> nat" 
       
   481   assumes "finite A" "\<forall>x \<in> A. f x \<le> g x"
 
       
   482   shows "sum f A \<le> sum g A"
 
       
   483   using  assms
 
       
   484   apply(induct A)
 
       
   485    apply(auto)
 
       
   486   done
 
       
   487 
       
   488 
       
   489 
       
   490 
       
   491 
       
   492 lemma pders_max_size:
 
       
   493   shows "(sum size2 (pders s r)) \<le> (Suc (size2 r)) ^ 3"
 
       
   494 proof -
 
       
   495   have "(sum size2 (pders s r)) \<le> sum (\<lambda>_. Suc (size2 r  * size2 r)) (pders s r)" 
       
   496     apply(rule_tac Sum2)
 
       
   497      apply (meson pders_subs rev_finite_subset subs_finite)
 
       
   498     using pders_subs subs_size2 by blast
 
       
   499   also have "... \<le> (Suc (size2 r  * size2 r)) * (sum (\<lambda>_. 1) (pders s r))"
 
       
   500     by simp
 
       
   501   also have "... \<le> (Suc (size2 r  * size2 r)) * card (pders s r)"
 
       
   502     by simp
 
       
   503   also have "... \<le> (Suc (size2 r  * size2 r)) * (Suc (awidth r))"
 
       
   504     using Suc_eq_plus1 card_pders_awidth mult_le_mono2 by presburger
 
       
   505   also have "... \<le> (Suc (size2 r  * size2 r)) * (Suc (size2 r))"
 
       
   506     using Suc_le_mono awidth_size mult_le_mono2 by presburger
 
       
   507   also have "... \<le> (Suc (size2 r)) ^ 3"
 
       
   508     by (smt One_nat_def Suc_1 Suc_mult_le_cancel1 Suc_n_not_le_n antisym_conv le_Suc_eq mult.commute nat_le_linear numeral_3_eq_3 power2_eq_square power2_le_imp_le power_Suc size_rexp)    
       
   509   finally show ?thesis  .
 
       
   510 qed
 
   430   
   511   
       
   512 lemma pders_Set_max_size:
 
       
   513   shows "(sum size2 (pders_Set A r)) \<le> (Suc (size2 r)) ^ 3"
 
       
   514 proof -
 
       
   515   have "(sum size2 (pders_Set A r)) \<le> sum (\<lambda>_. Suc (size2 r  * size2 r)) (pders_Set A r)" 
       
   516     apply(rule_tac Sum2)
 
       
   517      apply (simp add: finite_pders_set)
 
       
   518     by (meson pders_Set_subsetI pders_subs subs_size2 subsetD)
 
       
   519   also have "... \<le> (Suc (size2 r  * size2 r)) * (sum (\<lambda>_. 1) (pders_Set A r))"
 
       
   520     by simp
 
       
   521   also have "... \<le> (Suc (size2 r  * size2 r)) * card (pders_Set A r)"
 
       
   522     by simp
 
       
   523   also have "... \<le> (Suc (size2 r  * size2 r)) * (Suc (awidth r))"
 
       
   524     using Suc_eq_plus1 card_pders_set_le_awidth mult_le_mono2 by presburger
 
       
   525   also have "... \<le> (Suc (size2 r  * size2 r)) * (Suc (size2 r))"
 
       
   526     using Suc_le_mono awidth_size mult_le_mono2 by presburger
 
       
   527   also have "... \<le> (Suc (size2 r)) ^ 3"
 
       
   528     by (smt One_nat_def Suc_1 Suc_mult_le_cancel1 Suc_n_not_le_n antisym_conv le_Suc_eq mult.commute nat_le_linear numeral_3_eq_3 power2_eq_square power2_le_imp_le power_Suc size_rexp)    
       
   529   finally show ?thesis  .
 
       
   530 qed    
       
   531 
   431 fun height :: "rexp \<Rightarrow> nat" where
 
   532 fun height :: "rexp \<Rightarrow> nat" where
 
   432   "height ZERO = 1" |
 
   533   "height ZERO = 1" |
 
   433   "height ONE = 1" |
 
   534   "height ONE = 1" |
 
   434   "height (CHAR c) = 1" |
 
   535   "height (CHAR c) = 1" |
 
   435   "height (ALT r1 r2) = Suc (max (height r1) (height r2))" |
 
   536   "height (ALT r1 r2) = Suc (max (height r1) (height r2))" |
 
   436   "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" |
 
   537   "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" |
 
   437   "height (STAR r1) = Suc (height r1)" 
   538   "height (STAR r1) = Suc (height r1)" 
   438 
   539 
       
   540 lemma height_size2:
 
       
   541   shows "height r \<le> size2 r"
 
       
   542   apply(induct r)
 
       
   543   apply(simp_all)
 
       
   544   done
 
       
   545 
   439 lemma height_rexp:
 
   546 lemma height_rexp:
 
   440   fixes r :: rexp
 
   547   fixes r :: rexp
 
   441   shows "1 \<le> height r"
 
   548   shows "1 \<le> height r"
 
   442   apply(induct r)
 
   549   apply(induct r)
 
   443   apply(simp_all)
 
   550   apply(simp_all)
 
   444   done
 
   551   done
 
   445 
   552 
   446 lemma 
   553 lemma subs_height:
 
   447   shows "\<forall>r1 \<in> subs r. height r1 \<le> Suc (height r)"
 
   554   shows "\<forall>r1 \<in> subs r. height r1 \<le> Suc (height r)"
 
   448   apply(induct r)
 
   555   apply(induct r)
 
   449   apply(auto)+
 
   556   apply(auto)+
 
   450   done  
   557   done  
   451   
   558   
   452 
       
   453 
       
   454 (* tests *)
 
       
   455 
       
   456   
   559   
   457 
   560 
   458 end
 
   561 end
lexing