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/SizeBound4.thy
changeset 397 e1b74d618f1b
parent 396 cc8e231529fb
child 398 dac6d27c99c6
equal deleted inserted replaced
396:cc8e231529fb 397:e1b74d618f1b 
   130   shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
 
   130   shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
 
   131   apply(induct r)
 
   131   apply(induct r)
 
   132   apply(auto)
 
   132   apply(auto)
 
   133   done
 
   133   done
 
   134 
   134 
   135 lemma fuse_Nil:
 
       
   136   shows "fuse [] r = r"
 
       
   137   by (induct r)(simp_all)
 
       
   138 
       
   139 (*
 
       
   140 lemma map_fuse_Nil:
 
       
   141   shows "map (fuse []) rs = rs"
 
       
   142   by (induct rs)(simp_all add: fuse_Nil)
 
       
   143 *)
 
       
   144 
   135 
   145 fun intern :: "rexp \<Rightarrow> arexp" where
 
   136 fun intern :: "rexp \<Rightarrow> arexp" where
 
   146   "intern ZERO = AZERO"
 
   137   "intern ZERO = AZERO"
 
   147 | "intern ONE = AONE []"
 
   138 | "intern ONE = AONE []"
 
   148 | "intern (CH c) = ACHAR [] c"
 
   139 | "intern (CH c) = ACHAR [] c"
 
   278 lemma retrieve_fuse2:
 
   269 lemma retrieve_fuse2:
 
   279   assumes "\<Turnstile> v : (erase r)"
 
   270   assumes "\<Turnstile> v : (erase r)"
 
   280   shows "retrieve (fuse bs r) v = bs @ retrieve r v"
 
   271   shows "retrieve (fuse bs r) v = bs @ retrieve r v"
 
   281   using assms
 
   272   using assms
 
   282   apply(induct r arbitrary: v bs)
 
   273   apply(induct r arbitrary: v bs)
 
   283          apply(auto elim: Prf_elims)[4]
 
   274   apply(auto elim: Prf_elims)[4]
 
   284    defer
 
   275   apply(case_tac x2a)
 
       
   276   apply(simp)
 
       
   277   using Prf_elims(1) apply blast
 
       
   278   apply(case_tac x2a)
 
       
   279   apply(simp)
 
       
   280   apply(simp)
 
       
   281   apply(case_tac list)
 
       
   282   apply(simp)
 
       
   283   apply(simp)
 
       
   284   apply (smt (verit, best) Prf_elims(3) append_assoc retrieve.simps(4) retrieve.simps(5))
 
       
   285   apply(simp)
 
   285   using retrieve_encode_STARS
 
   286   using retrieve_encode_STARS
 
   286    apply(auto elim!: Prf_elims)[1]
 
       
   287    apply(case_tac vs)
 
       
   288     apply(simp)
 
       
   289    apply(simp)
 
       
   290   (* AALTs  case *)
 
       
   291   apply(simp)
 
       
   292   apply(case_tac x2a)
 
       
   293    apply(simp)
 
       
   294    apply(auto elim!: Prf_elims)[1]
 
       
   295   apply(simp)
 
       
   296    apply(case_tac list)
 
       
   297    apply(simp)
 
       
   298   apply(auto)
 
       
   299   apply(auto elim!: Prf_elims)[1]
 
   287   apply(auto elim!: Prf_elims)[1]
 
       
   288   apply(case_tac vs)
 
       
   289   apply(simp)
 
       
   290   apply(simp)
 
   300   done
 
   291   done
 
   301 
   292 
   302 lemma retrieve_fuse:
 
   293 lemma retrieve_fuse:
 
   303   assumes "\<Turnstile> v : r"
 
   294   assumes "\<Turnstile> v : r"
 
   304   shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"
 
   295   shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"
 
   312   using assms
 
   303   using assms
 
   313   apply(induct v r )
 
   304   apply(induct v r )
 
   314   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
 
   305   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
 
   315   done
 
   306   done
 
   316 
   307 
   317 (*
 
   308 
   318 lemma bnullable_Hdbmkeps_Hd:
 
   309 lemma retrieve_AALTs_bnullable1:
 
   319   assumes "bnullable a" 
   310   assumes "bnullable r"
 
   320   shows  "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"
 
   311   shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
 
   321   using assms by simp
 
   312          = bs @ retrieve r (mkeps (erase r))"
 
   322 *)
 
   313   using assms
 
   323 
   314   apply(case_tac rs)
 
   324 
   315   apply(auto simp add: bnullable_correctness)
 
   325 lemma r2:
 
   316   done
 
   326   assumes "x \<in> set rs" "bnullable x"
 
   317 
   327   shows "bnullable (AALTs bs rs)"
 
   318 lemma retrieve_AALTs_bnullable2:
 
   328   using assms
 
   319   assumes "\<not>bnullable r" "bnullables rs"
 
   329   apply(induct rs)
 
   320   shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
 
   330    apply(auto)
 
   321          = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
 
   331   done
 
       
   332 
       
   333 lemma  r3:
 
       
   334   assumes "\<not> bnullable r" 
       
   335           "bnullables rs"
 
       
   336   shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) =
 
       
   337          retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))"
 
       
   338   using assms
 
   322   using assms
 
   339   apply(induct rs arbitrary: r bs)
 
   323   apply(induct rs arbitrary: r bs)
 
   340    apply(auto)[1]
 
       
   341   apply(auto)
 
   324   apply(auto)
 
   342   using bnullable_correctness apply blast
 
   325   using bnullable_correctness apply blast
 
   343     apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)
 
       
   344    apply(subst retrieve_fuse2[symmetric])
 
       
   345   apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable)
 
       
   346    apply(simp)
 
       
   347   apply(case_tac "bnullable a")
 
       
   348   apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2)
 
       
   349   apply(drule_tac x="a" in meta_spec)
 
       
   350   apply(drule_tac x="bs" in meta_spec)
 
       
   351   apply(drule meta_mp)
 
       
   352    apply(simp)
 
       
   353   apply(drule meta_mp)
 
       
   354    apply(auto)
 
       
   355   apply(subst retrieve_fuse2[symmetric])
 
       
   356   apply(case_tac rs)
 
   326   apply(case_tac rs)
 
   357     apply(simp)
 
   327   apply(auto)
 
   358    apply(auto)[1]
 
   328   using bnullable_correctness apply blast
 
   359       apply (simp add: bnullable_correctness)
 
   329   apply(case_tac rs)
 
   360   
   330   apply(auto)
 
   361   apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2)
 
   331   done
 
   362     apply (simp add: bnullable_correctness)
 
   332 
   363   apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2)
 
   333 lemma bmkeps_retrieve_AALTs: 
   364   apply(simp)
 
       
   365   done
 
       
   366 
       
   367 lemma t: 
       
   368   assumes "\<forall>r \<in> set rs. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" 
   334   assumes "\<forall>r \<in> set rs. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" 
   369           "bnullables rs"
 
   335           "bnullables rs"
 
   370   shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
 
   336   shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
 
   371  using assms
 
   337  using assms
 
   372   apply(induct rs arbitrary: bs)
 
   338   apply(induct rs arbitrary: bs)
 
   373   apply(auto)
 
   339   apply(auto)
 
   374   apply (metis (no_types, opaque_lifting) bmkepss.cases bnullable_correctness erase.simps(5) erase.simps(6) mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
 
   340   using retrieve_AALTs_bnullable1 apply presburger
 
   375   apply (metis r3)
 
   341   apply (metis retrieve_AALTs_bnullable2)
 
   376   apply (metis (no_types, lifting) bmkepss.cases bnullable_correctness empty_iff erase.simps(6) list.set(1) mkeps.simps(3) retrieve.simps(4))
 
   342   apply (simp add: retrieve_AALTs_bnullable1)
 
   377   apply (metis r3)
 
   343   by (metis retrieve_AALTs_bnullable2)
 
   378   done
 
   344 
   379       
   345     
   380 lemma bmkeps_retrieve:
 
   346 lemma bmkeps_retrieve:
 
   381   assumes "bnullable r"
 
   347   assumes "bnullable r"
 
   382   shows "bmkeps r = retrieve r (mkeps (erase r))"
 
   348   shows "bmkeps r = retrieve r (mkeps (erase r))"
 
   383   using assms
 
   349   using assms
 
   384   apply(induct r)
 
   350   apply(induct r)
 
   385   apply(auto)
 
   351   apply(auto)  
   386   using t by auto
 
   352   using bmkeps_retrieve_AALTs by auto
 
   387 
   353 
   388 lemma bder_retrieve:
 
   354 lemma bder_retrieve:
 
   389   assumes "\<Turnstile> v : der c (erase r)"
 
   355   assumes "\<Turnstile> v : der c (erase r)"
 
   390   shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
 
   356   shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
 
   391   using assms  
   357   using assms  
   392   apply(induct r arbitrary: v rule: erase.induct)
 
   358   apply(induct r arbitrary: v rule: erase.induct)
 
   393          apply(simp)
 
   359   using Prf_elims(1) apply auto[1]
 
   394          apply(erule Prf_elims)
 
   360   using Prf_elims(1) apply auto[1]
 
   395         apply(simp)
 
   361   apply(auto)[1]
 
   396         apply(erule Prf_elims) 
   362   apply (metis Prf_elims(4) injval.simps(1) retrieve.simps(1) retrieve.simps(2))
 
   397         apply(simp)
 
   363   using Prf_elims(1) apply blast
 
   398       apply(case_tac "c = ca")
 
   364   (* AALTs case *)
 
   399        apply(simp)
 
   365   apply(simp)
 
   400        apply(erule Prf_elims)
 
   366   apply(erule Prf_elims)
 
   401        apply(simp)
 
   367   apply(simp)
 
   402       apply(simp)
 
   368   apply(simp)
 
   403        apply(erule Prf_elims)
 
       
   404   apply(simp)
 
       
   405       apply(erule Prf_elims)
 
       
   406      apply(simp)
 
       
   407     apply(simp)
 
       
   408   apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
 
   369   apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
 
   409     apply(erule Prf_elims)
 
       
   410      apply(simp)
 
       
   411     apply(simp)
 
       
   412     apply(case_tac rs)
 
       
   413      apply(simp)
 
       
   414     apply(simp)
 
       
   415   apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
 
       
   416    apply(simp)
 
       
   417    apply(case_tac "nullable (erase r1)")
 
       
   418     apply(simp)
 
       
   419   apply(erule Prf_elims)
 
   370   apply(erule Prf_elims)
 
   420      apply(subgoal_tac "bnullable r1")
 
   371   apply(simp)
 
   421   prefer 2
 
   372   apply(simp)
 
   422   using bnullable_correctness apply blast
 
   373   apply(case_tac rs)
 
   423     apply(simp)
 
   374   apply(simp)
 
   424      apply(erule Prf_elims)
 
   375   apply(simp)
 
   425      apply(simp)
 
   376   using Prf_elims(3) apply fastforce
 
   426    apply(subgoal_tac "bnullable r1")
 
   377   (* ASEQ case *) 
   427   prefer 2
 
   378   apply(simp)
 
   428   using bnullable_correctness apply blast
 
   379   apply(case_tac "nullable (erase r1)")
 
   429     apply(simp)
 
   380   apply(simp)
 
   430     apply(simp add: retrieve_fuse2)
 
   381   apply(erule Prf_elims)
 
   431     apply(simp add: bmkeps_retrieve)
 
   382   using Prf_elims(2) bnullable_correctness apply force
 
   432    apply(simp)
 
   383   apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
 
   433    apply(erule Prf_elims)
 
   384   apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
 
   434    apply(simp)
 
   385   using Prf_elims(2) apply force
 
   435   using bnullable_correctness apply blast
 
   386   (* ASTAR case *)  
   436   apply(rename_tac bs r v)
 
   387   apply(rename_tac bs r v)
 
   437   apply(simp)
 
   388   apply(simp)  
   438   apply(erule Prf_elims)
 
       
   439      apply(clarify)
 
       
   440   apply(erule Prf_elims)
 
   389   apply(erule Prf_elims)
 
   441   apply(clarify)
 
   390   apply(clarify)
 
   442   apply(subst injval.simps)
 
   391   apply(erule Prf_elims)
 
   443   apply(simp del: retrieve.simps)
 
   392   apply(clarify)
 
   444   apply(subst retrieve.simps)
 
   393   by (simp add: retrieve_fuse2)
 
   445   apply(subst retrieve.simps)
 
       
   446   apply(simp)
 
       
   447   apply(simp add: retrieve_fuse2)
 
       
   448   done
 
       
   449   
       
   450 
   394 
   451 
   395 
   452 lemma MAIN_decode:
 
   396 lemma MAIN_decode:
 
   453   assumes "\<Turnstile> v : ders s r"
 
   397   assumes "\<Turnstile> v : ders s r"
 
   454   shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
 
   398   shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
 
   579   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
 
   523   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
 
   580   apply(induct s1 arbitrary: r s2)
 
   524   apply(induct s1 arbitrary: r s2)
 
   581   apply(simp_all)
 
   525   apply(simp_all)
 
   582   done
 
   526   done
 
   583 
   527 
   584 lemma L_bsimp_ASEQ:
 
       
   585   "L (erase (ASEQ bs r1 r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
 
       
   586   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
 
       
   587   apply(simp_all)
 
       
   588   by (metis erase_fuse fuse.simps(4))
 
       
   589 
       
   590 lemma L_bsimp_AALTs:
 
       
   591   "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"
 
       
   592   apply(induct bs rs rule: bsimp_AALTs.induct)
 
       
   593   apply(simp_all add: erase_fuse)
 
       
   594   done
 
       
   595 
       
   596 lemma L_erase_AALTs:
 
       
   597   shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"
 
       
   598   apply(induct rs)
 
       
   599    apply(simp)
 
       
   600   apply(simp)
 
       
   601   apply(case_tac rs)
 
       
   602    apply(simp)
 
       
   603   apply(simp)
 
       
   604   done
 
       
   605 
       
   606 lemma L_erase_flts:
 
       
   607   shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"
 
       
   608   apply(induct rs rule: flts.induct)
 
       
   609   apply(simp_all)
 
       
   610   apply(auto)
 
       
   611   using L_erase_AALTs erase_fuse apply auto[1]
 
       
   612   by (simp add: L_erase_AALTs erase_fuse)
 
       
   613 
       
   614 lemma L_erase_dB_acc:
 
       
   615   shows "(\<Union> (L ` acc) \<union> (\<Union> (L ` erase ` (set (distinctBy rs erase acc))))) 
       
   616             = \<Union> (L ` acc) \<union>  \<Union> (L ` erase ` (set rs))"
 
       
   617   apply(induction rs arbitrary: acc)
 
       
   618   apply simp_all
 
       
   619   by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute)
 
       
   620 
       
   621 
       
   622 lemma L_erase_dB:
 
       
   623   shows "(\<Union> (L ` erase ` (set (distinctBy rs erase {})))) = \<Union> (L ` erase ` (set rs))"
 
       
   624   by (metis L_erase_dB_acc Un_commute Union_image_empty)
 
       
   625 
       
   626 lemma L_bsimp_erase:
 
       
   627   shows "L (erase r) = L (erase (bsimp r))"
 
       
   628   apply(induct r)
 
       
   629   apply(simp)
 
       
   630   apply(simp)
 
       
   631   apply(simp)
 
       
   632   apply(auto simp add: Sequ_def)[1]
 
       
   633   apply(subst L_bsimp_ASEQ[symmetric])
 
       
   634   apply(auto simp add: Sequ_def)[1]
 
       
   635   apply(subst (asm)  L_bsimp_ASEQ[symmetric])
 
       
   636   apply(auto simp add: Sequ_def)[1]
 
       
   637   apply(simp)
 
       
   638   apply(subst L_bsimp_AALTs[symmetric])
 
       
   639   defer
 
       
   640   apply(simp)
 
       
   641   apply(subst (2)L_erase_AALTs)  
       
   642   apply(subst L_erase_dB)
 
       
   643   apply(subst L_erase_flts)
 
       
   644   apply (simp add: L_erase_AALTs)
 
       
   645   done
 
       
   646 
       
   647 lemma L_bders_simp:
 
       
   648   shows "L (erase (bders_simp r s)) = L (erase (bders r s))"
 
       
   649   apply(induct s arbitrary: r rule: rev_induct)
 
       
   650   apply(simp)
 
       
   651   apply(simp)
 
       
   652   apply(simp add: ders_append)
 
       
   653   apply(simp add: bders_simp_append)
 
       
   654   apply(simp add: L_bsimp_erase[symmetric])
 
       
   655   by (simp add: der_correctness)
 
       
   656 
       
   657 
   528 
   658 lemma bmkeps_fuse:
 
   529 lemma bmkeps_fuse:
 
   659   assumes "bnullable r"
 
   530   assumes "bnullable r"
 
   660   shows "bmkeps (fuse bs r) = bs @ bmkeps r"
 
   531   shows "bmkeps (fuse bs r) = bs @ bmkeps r"
 
   661   by (metis assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
 
   532   by (metis assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
 
   665   shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"
 
   536   shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"
 
   666   using assms
 
   537   using assms
 
   667   apply(induct rs arbitrary: bs)
 
   538   apply(induct rs arbitrary: bs)
 
   668   apply(auto simp add: bmkeps_fuse bnullable_fuse)
 
   539   apply(auto simp add: bmkeps_fuse bnullable_fuse)
 
   669   done
 
   540   done
 
   670 
       
   671 
       
   672 lemma b4:
 
       
   673   shows "bnullable (bders_simp r s) = bnullable (bders r s)"
 
       
   674 proof -
 
       
   675   have "L (erase (bders_simp r s)) = L (erase (bders r s))"
 
       
   676     using L_bders_simp by force
 
       
   677   then show "bnullable (bders_simp r s) = bnullable (bders r s)"
 
       
   678     using bnullable_correctness nullable_correctness by blast
 
       
   679 qed
 
       
   680 
       
   681 
   541 
   682 lemma bder_fuse:
 
   542 lemma bder_fuse:
 
   683   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
 
   543   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
 
   684   apply(induct a arbitrary: bs c)
 
   544   apply(induct a arbitrary: bs c)
 
   685        apply(simp_all)
 
   545        apply(simp_all)
 
   858     apply(simp)
 
   718     apply(simp)
 
   859     apply(rule srewrites_single)
 
   719     apply(rule srewrites_single)
 
   860     apply(rule rrewrite_srewrite.ss6[simplified])
 
   720     apply(rule rrewrite_srewrite.ss6[simplified])
 
   861     apply(simp add: erase_fuse)
 
   721     apply(simp add: erase_fuse)
 
   862     done
 
   722     done
 
   863  qed (auto intro: rrewrite_srewrite.intros)
 
   723 qed (auto intro: rrewrite_srewrite.intros)
 
   864 
   724 
   865 
   725 
   866 lemma rewrites_fuse:  
   726 lemma rewrites_fuse:  
   867   assumes "r1 \<leadsto>* r2"
 
   727   assumes "r1 \<leadsto>* r2"
 
   868   shows "fuse bs r1 \<leadsto>* fuse bs r2"
 
   728   shows "fuse bs r1 \<leadsto>* fuse bs r2"
 
  1171 
  1031 
  1172 
  1032 
  1173 theorem main_blexer_simp: 
  1033 theorem main_blexer_simp: 
  1174   shows "blexer r s = blexer_simp r s"
 
  1034   shows "blexer r s = blexer_simp r s"
 
  1175   unfolding blexer_def blexer_simp_def
 
  1035   unfolding blexer_def blexer_simp_def
 
  1176   using b4 main_aux by simp
 
  1036   by (metis central main_aux rewrites_bnullable_eq)
 
  1177 
  1037 
  1178 
  1038 
  1179 theorem blexersimp_correctness: 
  1039 theorem blexersimp_correctness: 
  1180   shows "lexer r s = blexer_simp r s"
 
  1040   shows "lexer r s = blexer_simp r s"
 
  1181   using blexer_correctness main_blexer_simp by simp
 
  1041   using blexer_correctness main_blexer_simp by simp
lexing