thys3/src/BlexerSimp.thy
changeset 563 c92a41d9c4da
parent 496 f493a20feeb3
child 569 5af61c89f51e
equal deleted inserted replaced
562:57e33978e55d 563:c92a41d9c4da
    16 | "(ACHAR bs1 c) ~1 (ACHAR bs2 d) = (if c = d then True else False)"
    16 | "(ACHAR bs1 c) ~1 (ACHAR bs2 d) = (if c = d then True else False)"
    17 | "(ASEQ bs1 ra1 ra2) ~1 (ASEQ bs2 rb1 rb2) = (ra1 ~1 rb1 \<and> ra2 ~1 rb2)"
    17 | "(ASEQ bs1 ra1 ra2) ~1 (ASEQ bs2 rb1 rb2) = (ra1 ~1 rb1 \<and> ra2 ~1 rb2)"
    18 | "(AALTs bs1 []) ~1 (AALTs bs2 []) = True"
    18 | "(AALTs bs1 []) ~1 (AALTs bs2 []) = True"
    19 | "(AALTs bs1 (r1 # rs1)) ~1 (AALTs bs2 (r2 # rs2)) = (r1 ~1 r2 \<and> (AALTs bs1 rs1) ~1 (AALTs bs2 rs2))"
    19 | "(AALTs bs1 (r1 # rs1)) ~1 (AALTs bs2 (r2 # rs2)) = (r1 ~1 r2 \<and> (AALTs bs1 rs1) ~1 (AALTs bs2 rs2))"
    20 | "(ASTAR bs1 r1) ~1 (ASTAR bs2 r2) = r1 ~1 r2"
    20 | "(ASTAR bs1 r1) ~1 (ASTAR bs2 r2) = r1 ~1 r2"
       
    21 | "(ANTIMES bs1 r1 n1) ~1 (ANTIMES bs2 r2 n2) = (r1 ~1 r2 \<and> n1 = n2)"
    21 | "_ ~1 _ = False"
    22 | "_ ~1 _ = False"
    22 
    23 
    23 
    24 
    24 
    25 
    25 lemma eq1_L:
    26 lemma eq1_L:
   100 
   101 
   101 lemma bmkeps_fuse:
   102 lemma bmkeps_fuse:
   102   assumes "bnullable r"
   103   assumes "bnullable r"
   103   shows "bmkeps (fuse bs r) = bs @ bmkeps r"
   104   shows "bmkeps (fuse bs r) = bs @ bmkeps r"
   104   using assms
   105   using assms
   105   by (induct r rule: bnullable.induct) (auto)
   106   apply(induct r rule: bnullable.induct) 
       
   107         apply(auto)
       
   108   apply (metis append.assoc bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4))  
       
   109    apply(case_tac n)
       
   110   apply(auto)
       
   111   done
   106 
   112 
   107 lemma bmkepss_fuse: 
   113 lemma bmkepss_fuse: 
   108   assumes "bnullables rs"
   114   assumes "bnullables rs"
   109   shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"
   115   shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"
   110   using assms
   116   using assms
   361   apply(auto intro: rrewrite_srewrite.intros)
   367   apply(auto intro: rrewrite_srewrite.intros)
   362   apply (meson srewrites.simps srewrites1 ss5)
   368   apply (meson srewrites.simps srewrites1 ss5)
   363   using rs1 srewrites7 apply presburger
   369   using rs1 srewrites7 apply presburger
   364   using srewrites7 apply force
   370   using srewrites7 apply force
   365   apply (simp add: srewrites7)
   371   apply (simp add: srewrites7)
       
   372    apply(simp add: srewrites7)
   366   by (simp add: srewrites7)
   373   by (simp add: srewrites7)
       
   374   
   367 
   375 
   368 lemma bnullable0:
   376 lemma bnullable0:
   369 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" 
   377 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" 
   370   and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" 
   378   and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" 
   371   apply(induct rule: rrewrite_srewrite.inducts)
   379   apply(induct rule: rrewrite_srewrite.inducts)
   396   then show ?case
   404   then show ?case
   397     using bmkepss.simps bnullable0(1) by presburger
   405     using bmkepss.simps bnullable0(1) by presburger
   398 next
   406 next
   399   case (ss5 bs1 rs1 rsb)
   407   case (ss5 bs1 rs1 rsb)
   400   then show ?case
   408   then show ?case
   401     by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
   409     apply (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
       
   410     apply(case_tac rs1)
       
   411      apply(auto simp add: bnullable_fuse)
       
   412     apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4))
       
   413     apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4))
       
   414     apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4))
       
   415     by (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4))    
   402 next
   416 next
   403   case (ss6 a1 a2 rsa rsb rsc)
   417   case (ss6 a1 a2 rsa rsb rsc)
   404   then show ?case
   418   then show ?case
   405     by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD)
   419     by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD)
       
   420 next
       
   421   case (bs10 rs1 rs2 bs)
       
   422   then show ?case
       
   423     by (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) 
   406 qed (auto)
   424 qed (auto)
   407 
   425 
   408 lemma rewrites_bmkeps: 
   426 lemma rewrites_bmkeps: 
   409   assumes "r1 \<leadsto>* r2" "bnullable r1" 
   427   assumes "r1 \<leadsto>* r2" "bnullable r1" 
   410   shows "bmkeps r1 = bmkeps r2"
   428   shows "bmkeps r1 = bmkeps r2"