thys/BitCoded.thy
changeset 317 db0ff630bbb7
parent 316 0eaa1851a5b6
child 318 43e070803c1c
equal deleted inserted replaced
316:0eaa1851a5b6 317:db0ff630bbb7
    95 | AALTs "bit list" "arexp list"
    95 | AALTs "bit list" "arexp list"
    96 | ASTAR "bit list" arexp
    96 | ASTAR "bit list" arexp
    97 
    97 
    98 abbreviation
    98 abbreviation
    99   "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"
    99   "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"
       
   100 
       
   101 fun asize :: "arexp \<Rightarrow> nat" where
       
   102   "asize AZERO = 1"
       
   103 | "asize (AONE cs) = 1" 
       
   104 | "asize (ACHAR cs c) = 1"
       
   105 | "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
       
   106 | "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
       
   107 | "asize (ASTAR cs r) = Suc (asize r)"
       
   108 
   100 
   109 
   101 
   110 
   102 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
   111 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
   103   "fuse bs AZERO = AZERO"
   112   "fuse bs AZERO = AZERO"
   104 | "fuse bs (AONE cs) = AONE (bs @ cs)" 
   113 | "fuse bs (AONE cs) = AONE (bs @ cs)" 
   470   "flts [] = []"
   479   "flts [] = []"
   471 | "flts (AZERO # rs) = flts rs"
   480 | "flts (AZERO # rs) = flts rs"
   472 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
   481 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
   473 | "flts (r1 # rs) = r1 # flts rs"
   482 | "flts (r1 # rs) = r1 # flts rs"
   474 
   483 
   475 (*
       
   476 lemma flts_map:
       
   477   assumes "\<forall>r \<in> set rs. f r = r"
       
   478   shows "map f (flts rs) = flts (map f rs)"
       
   479   using assms
       
   480   apply(induct rs rule: flts.induct)
       
   481         apply(simp_all)
       
   482        apply(case_tac rs)
       
   483   apply(simp)
       
   484 *)
       
   485 
       
   486 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
   484 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
   487   where
   485   where
   488   "bsimp_ASEQ _ AZERO _ = AZERO"
   486   "bsimp_ASEQ _ AZERO _ = AZERO"
   489 | "bsimp_ASEQ _ _ AZERO = AZERO"
   487 | "bsimp_ASEQ _ _ AZERO = AZERO"
   490 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
   488 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
   513 definition blexer_simp where
   511 definition blexer_simp where
   514  "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 
   512  "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 
   515                 decode (bmkeps (bders_simp (intern r) s)) r else None"
   513                 decode (bmkeps (bders_simp (intern r) s)) r else None"
   516 
   514 
   517 
   515 
       
   516 lemma asize0:
       
   517   shows "0 < asize r"
       
   518   apply(induct  r)
       
   519        apply(auto)
       
   520   done
       
   521 
       
   522 
   518 lemma bders_simp_append:
   523 lemma bders_simp_append:
   519   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
   524   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
   520   apply(induct s1 arbitrary: r s2)
   525   apply(induct s1 arbitrary: r s2)
   521    apply(simp)
   526    apply(simp)
   522   apply(simp)
   527   apply(simp)
   523   done
   528   done
   524 
   529 
   525 
   530 lemma bsimp_ASEQ_size:
       
   531   shows "asize (bsimp_ASEQ bs r1 r2) \<le> Suc (asize r1 + asize r2)"
       
   532   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
       
   533   apply(auto)
       
   534   done
       
   535 
       
   536 lemma fuse_size:
       
   537   shows "asize (fuse bs r) = asize r"
       
   538   apply(induct r)
       
   539   apply(auto)
       
   540   done
       
   541 
       
   542 lemma flts_size:
       
   543   shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
       
   544   apply(induct rs rule: flts.induct)
       
   545         apply(simp_all)
       
   546   by (metis (mono_tags, lifting) add_mono_thms_linordered_semiring(1) comp_apply fuse_size le_SucI order_refl sum_list_cong)
       
   547   
       
   548 
       
   549 lemma bsimp_AALTs_size:
       
   550   shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"
       
   551   apply(induct rs rule: bsimp_AALTs.induct)
       
   552   apply(auto simp add: fuse_size)
       
   553   done
       
   554   
       
   555 lemma bsimp_size:
       
   556   shows "asize (bsimp r) \<le> asize r"
       
   557   apply(induct r)
       
   558        apply(simp_all)
       
   559    apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)
       
   560   apply(rule le_trans)
       
   561    apply(rule bsimp_AALTs_size)
       
   562   apply(simp)
       
   563    apply(rule le_trans)
       
   564    apply(rule flts_size)
       
   565   by (simp add: sum_list_mono)
       
   566 
       
   567 fun nonalt :: "arexp \<Rightarrow> bool"
       
   568   where
       
   569   "nonalt (AALTs bs2 rs) = False"
       
   570 | "nonalt r = True"
       
   571 
       
   572 
       
   573 
       
   574 
       
   575 lemma bsimp_AALTs_size2:
       
   576   assumes "\<forall>r \<in> set  rs. nonalt r"
       
   577   shows "asize (bsimp_AALTs bs rs) \<ge> sum_list (map asize rs)"
       
   578   using assms
       
   579   apply(induct rs rule: bsimp_AALTs.induct)
       
   580     apply(simp_all add: fuse_size)
       
   581   done
       
   582 
       
   583 lemma qq:
       
   584   shows "map (asize \<circ> fuse bs) rs = map asize rs"
       
   585   apply(induct rs)
       
   586    apply(auto simp add: fuse_size)
       
   587   done
       
   588 
       
   589 lemma flts_size2:
       
   590   assumes "\<exists>bs rs'. AALTs bs  rs' \<in> set rs"
       
   591   shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)"
       
   592   using assms
       
   593   apply(induct rs)
       
   594    apply(auto simp add: qq)
       
   595    apply (simp add: flts_size less_Suc_eq_le)
       
   596   apply(case_tac a)
       
   597        apply(auto simp add: qq)
       
   598    prefer 2
       
   599    apply (simp add: flts_size le_imp_less_Suc)
       
   600   using less_Suc_eq by auto
       
   601   
   526 lemma L_bsimp_ASEQ:
   602 lemma L_bsimp_ASEQ:
   527   "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
   603   "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
   528   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
   604   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
   529   apply(simp_all)
   605   apply(simp_all)
   530   by (metis erase_fuse fuse.simps(4))
   606   by (metis erase_fuse fuse.simps(4))
   573   apply(subst L_erase_flts)
   649   apply(subst L_erase_flts)
   574   apply(auto)
   650   apply(auto)
   575    apply (simp add: L_erase_AALTs)
   651    apply (simp add: L_erase_AALTs)
   576   using L_erase_AALTs by blast
   652   using L_erase_AALTs by blast
   577 
   653 
       
   654 lemma bsimp_ASEQ0:
       
   655   shows "bsimp_ASEQ bs r1 AZERO = AZERO"
       
   656   apply(induct r1)
       
   657   apply(auto)
       
   658   done
       
   659 
       
   660 
   578 
   661 
   579 lemma bsimp_ASEQ1:
   662 lemma bsimp_ASEQ1:
   580   assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
   663   assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
   581   shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
   664   shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
   582   using assms
   665   using assms
   618 
   701 
   619 
   702 
   620 lemma b4:
   703 lemma b4:
   621   shows "bnullable (bders_simp r s) = bnullable (bders r s)"
   704   shows "bnullable (bders_simp r s) = bnullable (bders r s)"
   622   by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
   705   by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
   623   
       
   624 
   706 
   625 lemma q1:
   707 lemma q1:
   626   assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"
   708   assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"
   627   shows "map (\<lambda>r. bmkeps(bsimp r)) rs = map bmkeps rs"
   709   shows "map (\<lambda>r. bmkeps(bsimp r)) rs = map bmkeps rs"
   628   using assms
   710   using assms
   664   shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
   746   shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
   665   apply(induct rs arbitrary: bs)
   747   apply(induct rs arbitrary: bs)
   666   apply(simp)
   748   apply(simp)
   667   apply(simp)
   749   apply(simp)
   668   done
   750   done
       
   751 
       
   752 lemma fuse_empty:
       
   753   shows "fuse [] r = r"
       
   754   apply(induct r)
       
   755        apply(auto)
       
   756   done
       
   757 
       
   758 lemma flts_fuse:
       
   759   shows "map (fuse bs) (flts rs) = flts (map (fuse bs) rs)"
       
   760   apply(induct rs arbitrary: bs rule: flts.induct)
       
   761         apply(auto simp add: fuse_append)
       
   762   done
       
   763 
       
   764 lemma bsimp_ASEQ_fuse:
       
   765   shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"
       
   766   apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)
       
   767   apply(auto)
       
   768   done
       
   769 
       
   770 lemma bsimp_AALTs_fuse:
       
   771   assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"
       
   772   shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"
       
   773   using assms
       
   774   apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)
       
   775   apply(auto)
       
   776   done
       
   777 
       
   778 
       
   779 
       
   780 lemma bsimp_fuse:
       
   781   shows "fuse bs (bsimp r) = bsimp (fuse bs r)"
       
   782 apply(induct r arbitrary: bs)
       
   783        apply(simp)
       
   784       apply(simp)
       
   785      apply(simp)
       
   786     prefer 3
       
   787     apply(simp)
       
   788    apply(simp)
       
   789    apply (simp add: bsimp_ASEQ_fuse)
       
   790   apply(simp)
       
   791   by (simp add: bsimp_AALTs_fuse fuse_append)
       
   792 
       
   793 lemma bsimp_fuse_AALTs:
       
   794   shows "fuse bs (bsimp (AALTs [] rs)) = bsimp (AALTs bs rs)"
       
   795   apply(subst bsimp_fuse) 
       
   796   apply(simp)
       
   797   done
       
   798 
       
   799 lemma bsimp_fuse_AALTs2:
       
   800   shows "fuse bs (bsimp_AALTs [] rs) = bsimp_AALTs bs rs"
       
   801   using bsimp_AALTs_fuse fuse_append by auto
       
   802   
       
   803 
       
   804 lemma bsimp_ASEQ_idem:
       
   805   assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"
       
   806   shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"
       
   807   using assms
       
   808   apply(case_tac "bsimp r1 = AZERO")
       
   809     apply(simp)
       
   810  apply(case_tac "bsimp r2 = AZERO")
       
   811     apply(simp)
       
   812   apply (metis bnullable.elims(2) bnullable.elims(3) bsimp.simps(3) bsimp_ASEQ.simps(2) bsimp_ASEQ.simps(3) bsimp_ASEQ.simps(4) bsimp_ASEQ.simps(5) bsimp_ASEQ.simps(6))  
       
   813   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
       
   814     apply(auto)[1]
       
   815     apply(subst bsimp_ASEQ2)
       
   816    apply(subst bsimp_ASEQ2)
       
   817   apply (metis assms(2) bsimp_fuse)
       
   818       apply(subst bsimp_ASEQ1)
       
   819       apply(auto)
       
   820   done
       
   821 
       
   822 
       
   823 fun nonnested :: "arexp \<Rightarrow> bool"
       
   824   where
       
   825   "nonnested (AALTs bs2 []) = True"
       
   826 | "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
       
   827 | "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
       
   828 | "nonnested r = True"
       
   829 
       
   830 
       
   831 lemma  k0:
       
   832   shows "flts (r # rs1) = flts [r] @ flts rs1"
       
   833   apply(induct r arbitrary: rs1)
       
   834    apply(auto)
       
   835   done
       
   836 
       
   837 lemma  k00:
       
   838   shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
       
   839   apply(induct rs1 arbitrary: rs2)
       
   840    apply(auto)
       
   841   by (metis append.assoc k0)
       
   842 
       
   843 lemma  k0a:
       
   844   shows "flts [AALTs bs rs] = map (fuse bs)  rs"
       
   845   apply(simp)
       
   846   done
       
   847 
       
   848 fun spill where
       
   849  "spill (AALTs bs rs) =  map (fuse bs) rs"
       
   850 
       
   851 lemma  k0a2:
       
   852   assumes "\<not> nonalt r"  
       
   853   shows "flts [r] = spill r"
       
   854   using  assms
       
   855   apply(case_tac r)
       
   856   apply(simp_all)
       
   857   done
       
   858 
       
   859 lemma  k0b:
       
   860   assumes "nonalt r" "r \<noteq> AZERO"
       
   861   shows "flts [r] = [r]"
       
   862   using assms
       
   863   apply(case_tac  r)
       
   864   apply(simp_all)
       
   865   done
       
   866 
       
   867 lemma nn1:
       
   868   assumes "nonnested (AALTs bs rs)"
       
   869   shows "\<nexists>bs1 rs1. flts rs = [AALTs bs1 rs1]"
       
   870   using assms
       
   871   apply(induct rs rule: flts.induct)
       
   872   apply(auto)
       
   873   done
       
   874 
       
   875 lemma nn1q:
       
   876   assumes "nonnested (AALTs bs rs)"
       
   877   shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set (flts rs)"
       
   878   using assms
       
   879   apply(induct rs rule: flts.induct)
       
   880   apply(auto)
       
   881   done
       
   882 
       
   883 lemma nn1qq:
       
   884   assumes "nonnested (AALTs bs rs)"
       
   885   shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs"
       
   886   using assms
       
   887   apply(induct rs rule: flts.induct)
       
   888   apply(auto)
       
   889   done
       
   890 
       
   891 lemma nn10:
       
   892   assumes "nonnested (AALTs cs rs)" 
       
   893   shows "nonnested (AALTs (bs @ cs) rs)"
       
   894   using assms
       
   895   apply(induct rs arbitrary: cs bs)
       
   896    apply(simp_all)
       
   897   apply(case_tac a)
       
   898        apply(simp_all)
       
   899   done
       
   900 
       
   901 lemma nn11a:
       
   902   assumes "nonalt r"
       
   903   shows "nonalt (fuse bs r)"
       
   904   using assms
       
   905   apply(induct r)
       
   906        apply(auto)
       
   907   done
       
   908 
       
   909 
       
   910 lemma nn1a:
       
   911   assumes "nonnested r"
       
   912   shows "nonnested (fuse bs r)"
       
   913   using assms
       
   914   apply(induct bs r arbitrary: rule: fuse.induct)
       
   915        apply(simp_all add: nn10)
       
   916   done  
       
   917 
       
   918 lemma n0:
       
   919   shows "nonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
       
   920   apply(induct rs  arbitrary: bs)
       
   921    apply(auto)
       
   922     apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
       
   923    apply (metis list.set_intros(2) nn1qq nonalt.elims(3))
       
   924   by (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))
       
   925 
       
   926   
       
   927   
       
   928 
       
   929 lemma nn1c:
       
   930   assumes "\<forall>r \<in> set rs. nonnested r"
       
   931   shows "\<forall>r \<in> set (flts rs). nonalt r"
       
   932   using assms
       
   933   apply(induct rs rule: flts.induct)
       
   934         apply(auto)
       
   935   apply(rule nn11a)
       
   936   by (metis nn1qq nonalt.elims(3))
       
   937 
       
   938 lemma nn1bb:
       
   939   assumes "\<forall>r \<in> set rs. nonalt r"
       
   940   shows "nonnested (bsimp_AALTs bs rs)"
       
   941   using assms
       
   942   apply(induct bs rs rule: bsimp_AALTs.induct)
       
   943     apply(auto)
       
   944    apply (metis nn11a nonalt.simps(1) nonnested.elims(3))
       
   945   using n0 by auto
       
   946     
       
   947 lemma nn1b:
       
   948   shows "nonnested (bsimp r)"
       
   949   apply(induct r)
       
   950        apply(simp_all)
       
   951   apply(case_tac "bsimp r1 = AZERO")
       
   952     apply(simp)
       
   953  apply(case_tac "bsimp r2 = AZERO")
       
   954    apply(simp)
       
   955     apply(subst bsimp_ASEQ0)
       
   956   apply(simp)
       
   957   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
       
   958     apply(auto)[1]
       
   959     apply(subst bsimp_ASEQ2)
       
   960   apply (simp add: nn1a)    
       
   961    apply(subst bsimp_ASEQ1)
       
   962       apply(auto)
       
   963   apply(rule nn1bb)
       
   964   apply(auto)
       
   965   by (metis (mono_tags, hide_lams) imageE nn1c set_map)
       
   966 
       
   967 lemma rt:
       
   968   shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
       
   969   apply(induct rs)
       
   970    apply(simp)
       
   971   apply(simp)
       
   972   apply(subst  k0)
       
   973   apply(simp)
       
   974   by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1)
       
   975 
       
   976 lemma flts_idem:
       
   977   assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r"
       
   978   shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)"
       
   979   using assms
       
   980   apply(induct rs)
       
   981    apply(simp)
       
   982   apply(simp)
       
   983   apply(subst k0)
       
   984   apply(subst (2) k0) 
       
   985   apply(case_tac "bsimp a = AZERO")
       
   986    apply(simp)
       
   987   apply(case_tac "nonalt (bsimp a)")
       
   988   thm k0 k0a k0b
       
   989   apply(subst k0b)
       
   990      apply(simp)
       
   991     apply(simp)
       
   992    apply(simp)
       
   993   apply(subst k0b)
       
   994      apply(simp)
       
   995     apply(simp)
       
   996    apply(simp)
       
   997   apply(subst k0)
       
   998   apply(subst k0b)
       
   999      apply(simp)
       
  1000     apply(simp)
       
  1001    apply(simp)
       
  1002   apply(simp)
       
  1003   apply(simp add: k00)
       
  1004   apply(subst k0a2)
       
  1005    apply(simp)
       
  1006   apply(subst k0a2)
       
  1007    apply(simp)
       
  1008   apply(case_tac a)
       
  1009   apply(simp_all)
       
  1010   sorry
       
  1011 
       
  1012 lemma bsimp_AALTs_idem:
       
  1013   (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r \<and> nonalt (bsimp r)" *)
       
  1014   (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" *)
       
  1015   shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
       
  1016   apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
       
  1017   apply(case_tac x)
       
  1018   apply(simp)
       
  1019   apply(simp)
       
  1020   apply(case_tac "\<exists>bs'  rs'. a = AALTs bs' rs'")
       
  1021    apply(clarify)
       
  1022   apply(case_tac list)
       
  1023         apply(simp)
       
  1024        apply(simp) 
       
  1025 
       
  1026   apply(drule_tac x="flts (rs' @ list)" in spec)
       
  1027   apply(erule impE)
       
  1028   prefer 2
       
  1029   apply(case_tac a)
       
  1030        apply(simp)
       
  1031        apply(case_tac list)
       
  1032         apply(simp)
       
  1033        apply(simp) 
       
  1034    apply(case_tac list)
       
  1035         apply(simp)
       
  1036       apply(simp) 
       
  1037    apply(case_tac list)
       
  1038         apply(simp)
       
  1039      apply(simp) 
       
  1040   prefer 3
       
  1041    apply(case_tac list)
       
  1042         apply(simp)
       
  1043        apply(simp) 
       
  1044    apply(case_tac list)
       
  1045     apply(simp)
       
  1046       
       
  1047 
       
  1048        apply(simp) 
       
  1049 
       
  1050       apply(case_tac "flts (map bsimp list)")
       
  1051        apply(simp)
       
  1052       apply(simp)
       
  1053   
       
  1054   
       
  1055 
       
  1056    prefer 2
       
  1057    apply(simp)
       
  1058   
       
  1059    apply(subst k0)
       
  1060    apply(subst (2) k0)
       
  1061   
       
  1062   apply(case_tac a)
       
  1063        apply(simp_all)
       
  1064   
       
  1065   prefer 2
       
  1066    apply(simp)
       
  1067   apply(case_tac r)
       
  1068        apply(auto)
       
  1069    apply(case_tac "bsimp x42 = AZERO")
       
  1070     apply(simp)
       
  1071  apply(case_tac "bsimp x43 = AZERO")
       
  1072    apply(simp)
       
  1073    apply(subst bsimp_ASEQ0)
       
  1074    apply(subst bsimp_ASEQ0)
       
  1075   apply(simp)
       
  1076   apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
       
  1077     apply(auto)[1]
       
  1078     apply(subst bsimp_ASEQ2)
       
  1079    apply(subst bsimp_ASEQ2)
       
  1080   prefer 2
       
  1081       apply(subst bsimp_ASEQ1)
       
  1082       apply(auto)
       
  1083   apply(subst bsimp_ASEQ1)
       
  1084       apply(auto)
       
  1085   apply(subst (asm) bsimp_ASEQ2)
       
  1086    apply(subst (asm) bsimp_ASEQ2)
       
  1087   using flts_fuse bsimp_fuse bsimp_fuse_AALTs bsimp_fuse_AALTs2 bsimp_AALTs.simps flts.simps
       
  1088     
       
  1089    apply(case_tac x43)
       
  1090         apply(simp_all)
       
  1091     prefer 3
       
  1092   oops
       
  1093 
       
  1094 lemma bsimp_idem:
       
  1095   shows "bsimp (bsimp r) = bsimp r"
       
  1096 apply(induct r taking: "asize" rule: measure_induct)
       
  1097   apply(case_tac x)
       
  1098   apply(simp)
       
  1099       apply(simp)
       
  1100      apply(simp)
       
  1101     prefer 3
       
  1102     apply(simp)
       
  1103    apply(simp)
       
  1104    apply (simp add: bsimp_ASEQ_idem)
       
  1105   apply(clarify)
       
  1106   apply(case_tac x52)
       
  1107   apply(simp)
       
  1108   apply(simp)
       
  1109   apply(subst k0)
       
  1110   apply(subst (2) k0)
       
  1111   apply(case_tac "bsimp a = AZERO")
       
  1112    apply(simp)
       
  1113    apply(frule_tac x="AALTs x51 (flts (map bsimp list))" in spec)
       
  1114    apply(drule mp)
       
  1115     apply(simp)
       
  1116   apply (meson add_le_cancel_right asize0 le_trans not_le rt trans_le_add2)
       
  1117   apply(simp)
       
  1118     apply(subst (asm) flts_idem)
       
  1119      apply(auto)[1]
       
  1120      apply(drule_tac  x="r" in spec)
       
  1121   apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
       
  1122   apply(simp)
       
  1123   apply(subst flts_idem)
       
  1124    apply(auto)[1]
       
  1125      apply(drule_tac  x="r" in spec)
       
  1126   apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
       
  1127    apply(simp)
       
  1128   apply(case_tac "nonalt (bsimp a)")
       
  1129   apply(subst k0b)
       
  1130      apply(simp)
       
  1131     apply(simp)
       
  1132   apply(subst k0b)
       
  1133      apply(simp)
       
  1134     apply(simp)
       
  1135    apply(auto)[1]
       
  1136   apply(frule_tac x="AALTs x51 (bsimp a # flts (map bsimp list))" in spec)
       
  1137    apply(drule mp)
       
  1138     apply(simp)
       
  1139     prefer 2
       
  1140     apply(simp)
       
  1141   apply(subst (asm) k0)
       
  1142   apply(subst (asm) flts_idem)
       
  1143      apply(auto)[1]
       
  1144   apply (simp add: sum_list_map_remove1)
       
  1145   apply(subst (asm) k0b)
       
  1146      apply(simp)
       
  1147     apply(simp)
       
  1148     apply(simp)
       
  1149    apply(subst k0)
       
  1150   apply(subst flts_idem)
       
  1151      apply(auto)[1]
       
  1152      apply (simp add: sum_list_map_remove1)
       
  1153   apply(subst k0b)
       
  1154      apply(simp)
       
  1155     apply(simp)
       
  1156   apply(simp)
       
  1157 lemma XX_bder:
       
  1158   shows "bsimp (bder c (bsimp r)) = (bsimp \<circ> bder c) r"
       
  1159   apply(induct r)
       
  1160        apply(simp)
       
  1161       apply(simp)
       
  1162      apply(simp)
       
  1163     prefer 3
       
  1164     apply(simp)
       
  1165   prefer 2
       
  1166    apply(simp)
       
  1167    apply(case_tac x2a)
       
  1168     apply(simp)
       
  1169   apply(simp)
       
  1170   apply(auto)[1]
       
  1171 
   669 
  1172 
   670 lemma q3a:
  1173 lemma q3a:
   671   assumes "\<exists>r \<in> set rs. bnullable r"
  1174   assumes "\<exists>r \<in> set rs. bnullable r"
   672   shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
  1175   shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
   673   using assms
  1176   using assms
   756    apply(simp)
  1259    apply(simp)
   757    apply (simp add: r0)
  1260    apply (simp add: r0)
   758   apply(simp)
  1261   apply(simp)
   759   using qq4 r1 r2 by auto
  1262   using qq4 r1 r2 by auto
   760 
  1263 
   761 lemma  k0:
  1264 
   762   shows "flts (r # rs1) = flts [r] @ flts rs1"
       
   763   apply(induct r arbitrary: rs1)
       
   764    apply(auto)
       
   765   done
       
   766 
  1265 
   767 lemma k1:
  1266 lemma k1:
   768   assumes "\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; bnullable x2aa\<rbrakk> \<Longrightarrow> bmkeps x2aa = bmkeps (bsimp x2aa)"
  1267   assumes "\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; bnullable x2aa\<rbrakk> \<Longrightarrow> bmkeps x2aa = bmkeps (bsimp x2aa)"
   769           "\<exists>x\<in>set x2a. bnullable x"
  1268           "\<exists>x\<in>set x2a. bnullable x"
   770         shows "bmkeps (AALTs x1 (flts x2a)) = bmkeps (AALTs x1 (flts (map bsimp x2a)))"
  1269         shows "bmkeps (AALTs x1 (flts x2a)) = bmkeps (AALTs x1 (flts (map bsimp x2a)))"
   834   apply(case_tac  rs)
  1333   apply(case_tac  rs)
   835    apply(simp_all)
  1334    apply(simp_all)
   836   done
  1335   done
   837 
  1336 
   838 
  1337 
       
  1338 fun extr :: "arexp  \<Rightarrow> (bit list) set" where
       
  1339   "extr (AONE bs) = {bs}"
       
  1340 | "extr (ACHAR bs c) = {bs}"
       
  1341 | "extr (AALTs bs (r#rs)) = 
       
  1342      {bs @ bs' | bs'.  bs' \<in> extr r} \<union>
       
  1343      {bs @ bs' | bs'.  bs' \<in> extr (AALTs [] rs)}"
       
  1344 | "extr (ASEQ bs r1 r2) = 
       
  1345      {bs @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r1 \<and> bs2 \<in> extr r2}"
       
  1346 | "extr (ASTAR bs r) = {bs @ [S]} \<union>
       
  1347      {bs @ [Z] @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r \<and> bs2 \<in> extr (ASTAR  [] r)}"
   839 
  1348 
   840 
  1349 
   841 lemma MAIN_decode:
  1350 lemma MAIN_decode:
   842   assumes "\<Turnstile> v : ders s r"
  1351   assumes "\<Turnstile> v : ders s r"
   843   shows "Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r"
  1352   shows "Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r"
   957    apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
  1466    apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
   958      apply(clarify)
  1467      apply(clarify)
   959      apply(simp)
  1468      apply(simp)
   960      apply(subst bsimp_ASEQ2)
  1469      apply(subst bsimp_ASEQ2)
   961      apply(subst bsimp_ASEQ2)
  1470      apply(subst bsimp_ASEQ2)
   962   apply(simp add: erase_fuse)
  1471      apply(simp add: erase_fuse)
       
  1472      apply(case_tac r1)
       
  1473           apply(simp_all)
       
  1474   using Prf_elims(4) apply fastforce
       
  1475       apply(erule Prf_elims)
       
  1476       apply(simp)
       
  1477   
       
  1478       apply(simp)
       
  1479   
       
  1480   
   963      defer
  1481      defer
   964      apply(subst bsimp_ASEQ1)
  1482      apply(subst bsimp_ASEQ1)
   965   using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
  1483   using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
   966   using L_bsimp_erase L_
  1484   using L_bsimp_erase L_
   967 
  1485