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.
thys4/posix/FBound.thy
changeset 590 988e92a70704
parent 589 86e0203db2da
child 591 b2d0de6aee18
equal deleted inserted replaced
589:86e0203db2da 590:988e92a70704 
   239 inductive leq1 ("_ \<le>1 _" [80, 80] 80) where  
   239 inductive leq1 ("_ \<le>1 _" [80, 80] 80) where  
   240   "r1 \<le>1 r1"
 
   240   "r1 \<le>1 r1"
 
   241 | "AZERO \<le>1 ASEQ bs AZERO r" 
   241 | "AZERO \<le>1 ASEQ bs AZERO r" 
   242 | "AZERO \<le>1 ASEQ bs r AZERO"
 
   242 | "AZERO \<le>1 ASEQ bs r AZERO"
 
   243 | "fuse (bs @ bs1) r2 \<le>1 ASEQ bs (AONE bs1) r2"
 
   243 | "fuse (bs @ bs1) r2 \<le>1 ASEQ bs (AONE bs1) r2"
 
   244 | " AALTs bs (rs1 @ rs) \<le>1 AALTs bs (rs1 @( AZERO # rs))"
 
   244 | "AALTs bs (rs1 @ rs) \<le>1 AALTs bs (rs1 @( AZERO # rs))"
 
   245 | "AALTs bs1 (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs1 (rsa @ (AALTs bs1 rs1) # rsb)"
 
   245 | "AALTs bs (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs (rsa @ (AALTs bs1 rs1) # rsb)"
 
   246 | "rerase a1 = rerase a2 \<Longrightarrow> AALTs bs (rsa @ [a1] @ rsb @ rsc) \<le>1 AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc) "
 
   246 | "rerase a1 = rerase a2 \<Longrightarrow> AALTs bs (rsa @ [a1] @ rsb @ rsc) \<le>1 AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc) "
 
   247 | "r1 \<le>1 r2 \<Longrightarrow> r1  \<le>1 ASEQ bs (AONE bs1) r2"
 
   247 | "r1 \<le>1 r2 \<Longrightarrow> r1  \<le>1 ASEQ bs (AONE bs1) r2"
 
   248 | "r2 \<le>1 r1 \<Longrightarrow> AALTs bs (rs1 @ r2 # rs) \<le>1 AALTs bs (rs1 @ r1 # rs)"
 
   248 | "r2 \<le>1 r1 \<Longrightarrow> AALTs bs (rs1 @ r2 # rs) \<le>1 AALTs bs (rs1 @ r1 # rs)"
 
   249 | "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r  r2 \<le>1 ASEQ bs r r1"
 
   249 | "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r  r2 \<le>1 ASEQ bs r r1"
 
   250 | "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r2 r  \<le>1 ASEQ bs r1 r"
 
   250 | "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r2 r  \<le>1 ASEQ bs r1 r"
 
   251 | "r \<le>1 r' \<Longrightarrow> ASTAR bs r \<le>1 ASTAR bs r'"
 
   251 | "r \<le>1 r' \<Longrightarrow> ASTAR bs r \<le>1 ASTAR bs r'"
 
   252 | "AZERO \<le>1 AALTs bs []"
 
   252 | "AZERO \<le>1 AALTs bs []"
 
   253 | "fuse bs r \<le>1 AALTs bs [r]"
 
   253 | "fuse bs r \<le>1 AALTs bs [r]"
 
   254 | "\<lbrakk>r1' \<le>1 r1;  r2' \<le>1 r2\<rbrakk> \<Longrightarrow> bsimp_ASEQ bs1 r1' r2' \<le>1 ASEQ bs1 r1 r2"
 
   254 | "\<lbrakk>r1' \<le>1 r1;  r2' \<le>1 r2\<rbrakk> \<Longrightarrow> bsimp_ASEQ bs1 r1' r2' \<le>1 ASEQ bs1 r1 r2"
 
       
   255 | "\<lbrakk>AALTs bs rs1 \<le>1 AALTs bs rs2; r1 \<le>1 r2 \<rbrakk> \<Longrightarrow> AALTs bs (r1 # rs1) \<le>1 AALTs bs (r2 # rs2)"
 
       
   256 | "\<lbrakk>r1 \<le>1 r2; r2 \<le>1 r3 \<rbrakk> \<Longrightarrow> r1 \<le>1 r3"
 
       
   257 
       
   258 
       
   259 lemma leq1_6_variant1:
 
       
   260   shows "AALTs bs ( (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs ((AALTs bs1 rs1) # rsb)"
 
       
   261   by (metis leq1.intros(6) self_append_conv2)
 
       
   262 
       
   263 
       
   264 
       
   265 lemma flts_leq1:
 
       
   266   shows "AALTs bs (flts rs) \<le>1 AALTs bs rs"
 
       
   267   apply(induct rule: flts.induct)
 
       
   268          apply (simp add: leq1.intros(1))
 
       
   269         apply simp
 
       
   270   apply (metis append_Nil leq1.intros(17) leq1.intros(5))
 
       
   271        apply simp
 
       
   272        apply(subgoal_tac "AALTs bs (map (fuse bsa) rs1 @ flts rs) \<le>1 AALTs bs (AALTs bsa rs1 # flts rs)")
 
       
   273         apply (meson leq1.intros(1) leq1.intros(16) leq1.intros(17))
 
       
   274   using leq1_6_variant1 apply presburger
 
       
   275   apply (simp add: leq1.intros(1) leq1.intros(16))
 
       
   276   using leq1.intros(1) leq1.intros(16) apply auto[1]
 
       
   277   using leq1.intros(1) leq1.intros(16) apply force
 
       
   278    apply (simp add: leq1.intros(1) leq1.intros(16))
 
       
   279   using leq1.intros(1) leq1.intros(16) by force
 
       
   280 
       
   281 lemma dB_leq12:
 
       
   282   shows "AALTs bs (distinctWith rs1 eq1 (set rs2)) \<le>1 AALTs bs (rs1 @ rs2)"
 
       
   283   sorry
 
       
   284 
       
   285 
       
   286 lemma dB_leq1:
 
       
   287   shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs"
 
       
   288   by (metis append.right_neutral dB_leq12 list.set(1))
 
       
   289 
       
   290 
   255 
   291 
   256 lemma stupid_leq1_1:
 
   292 lemma stupid_leq1_1:
 
   257   shows " rerase  r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))"
 
   293   shows " rerase  r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))"
 
   258   apply(induct r2)
 
   294   apply(induct r2)
 
   259         apply simp+
 
   295         apply simp+
 
   274    apply simp
 
   310    apply simp
 
   275   apply(case_tac "\<exists>bs1. r1' = AONE bs1")
 
   311   apply(case_tac "\<exists>bs1. r1' = AONE bs1")
 
   276    apply(erule exE)
 
   312    apply(erule exE)
 
   277    apply simp
 
   313    apply simp
 
   278   apply (metis asize_rsize le_SucI rerase_fuse trans_le_add2)
 
   314   apply (metis asize_rsize le_SucI rerase_fuse trans_le_add2)
 
   279   by (smt (verit, best) Suc_eq_plus1 ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral add_cancel_right_right add_mono_thms_linordered_semiring(1) asize.simps(5) asize_rsize nat_add_left_cancel_le order.trans order_trans plus_1_eq_Suc rSEQ_mono rerase_bsimp_ASEQ rsize.simps(5))
 
   315   apply (smt (verit, best) Suc_eq_plus1 ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral add_cancel_right_right add_mono_thms_linordered_semiring(1) asize.simps(5) asize_rsize nat_add_left_cancel_le order.trans order_trans plus_1_eq_Suc rSEQ_mono rerase_bsimp_ASEQ rsize.simps(5))
 
       
   316   sorry
 
   280 
   317 
   281 
   318 
   282 
   319 
   283 lemma size_deciding_equality:
 
   320 lemma size_deciding_equality:
 
   284   shows "asize r1 \<noteq> asize r2 \<Longrightarrow> r1 \<noteq> r2 "
 
   321   shows "asize r1 \<noteq> asize r2 \<Longrightarrow> r1 \<noteq> r2 "
 
   314   apply(subgoal_tac "rsize (rerase (fuse bs ra)) \<noteq> rsize (RSEQ r (RALTS [rerase ra]))")
 
   351   apply(subgoal_tac "rsize (rerase (fuse bs ra)) \<noteq> rsize (RSEQ r (RALTS [rerase ra]))")
 
   315   
   352   
   316   apply force
 
   353   apply force
 
   317   apply simp
 
   354   apply simp
 
   318   apply(simp add: asize_rsize)
 
   355   apply(simp add: asize_rsize)
 
   319   by (simp add: rerase_fuse size_deciding_equality4)
 
   356   apply (simp add: rerase_fuse size_deciding_equality4)
 
   320 
   357   apply (metis Suc_n_not_le_n asize_rsize leq1.intros(15) leq1_size rsize.simps(5) trans_le_add2)
 
   321   
   358   sorry
 
   322 
   359 
   323   
   360   
   324 
   361 
   325 lemma leq1_less_or_equal: shows
 
   362 lemma leq1_less_or_equal: shows
 
   326 "r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"
 
   363 "r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"
 
   342        apply simp
 
   379        apply simp
 
   343       apply simp
 
   380       apply simp
 
   344      apply simp
 
   381      apply simp
 
   345     apply simp
 
   382     apply simp
 
   346    apply simp
 
   383    apply simp
 
   347   apply simp
 
   384    apply simp
 
   348   using r_finite1 rerase_fuse by auto
 
   385 
   349 
   386   using r_finite1 rerase_fuse apply auto[1]
 
       
   387   apply (smt (verit, best) BlexerSimp.bsimp_ASEQ0 BlexerSimp.bsimp_ASEQ2 bsimp_ASEQ.simps(1) bsimp_ASEQ1 leq1_trans1 rerase.simps(5) rerase_bsimp_ASEQ rerase_fuse rrexp.inject(2) rsimp_SEQ.simps(22))
 
       
   388   sorry
 
   350 
   389 
   351 
   390 
   352 
   391 
   353 
   392 
   354 
   393 
   417 
   456 
   418 lemma bsimp_reduces:
 
   457 lemma bsimp_reduces:
 
   419   shows "bsimp r \<le>1 r"
 
   458   shows "bsimp r \<le>1 r"
 
   420   apply(induct rule: bsimp.induct)
 
   459   apply(induct rule: bsimp.induct)
 
   421         apply simp
 
   460         apply simp
 
   422   
   461         apply (simp add: leq1.intros(15))
 
       
   462        apply simp
 
       
   463   apply(case_tac rs)
 
       
   464         apply simp
 
       
   465   
       
   466   apply (simp add: leq1.intros(13))
 
       
   467        apply(case_tac list)
 
       
   468         apply simp
 
       
   469   
       
   470 
   423   sorry
 
   471   sorry
 
   424 
   472 
   425 
   473 
   426 
   474 
   427 lemma bitcodes_unchanging:
 
   475 lemma bitcodes_unchanging:
lexing