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/BitCoded.thy
changeset 322 22e34f93cd5d
parent 318 43e070803c1c
child 323 09ce1cdb70ab
equal deleted inserted replaced
321:72f54acfb976 322:22e34f93cd5d 
   104 | "asize (ACHAR cs c) = 1"
 
   104 | "asize (ACHAR cs c) = 1"
 
   105 | "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
 
   105 | "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
 
   106 | "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
 
   106 | "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
 
   107 | "asize (ASTAR cs r) = Suc (asize r)"
 
   107 | "asize (ASTAR cs r) = Suc (asize r)"
 
   108 
   108 
   109 
       
   110 
       
   111 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
 
       
   112   "fuse bs AZERO = AZERO"
 
       
   113 | "fuse bs (AONE cs) = AONE (bs @ cs)" 
       
   114 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
 
       
   115 | "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs"
 
       
   116 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
 
       
   117 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
 
       
   118 
       
   119 lemma fuse_append:
 
       
   120   shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
 
       
   121   apply(induct r)
 
       
   122   apply(auto)
 
       
   123   done
 
       
   124 
       
   125 
       
   126 fun intern :: "rexp \<Rightarrow> arexp" where
 
       
   127   "intern ZERO = AZERO"
 
       
   128 | "intern ONE = AONE []"
 
       
   129 | "intern (CHAR c) = ACHAR [] c"
 
       
   130 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
       
   131                                 (fuse [S]  (intern r2))"
 
       
   132 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
 
       
   133 | "intern (STAR r) = ASTAR [] (intern r)"
 
       
   134 
       
   135 
       
   136 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
 
       
   137   "retrieve (AONE bs) Void = bs"
 
       
   138 | "retrieve (ACHAR bs c) (Char d) = bs"
 
       
   139 | "retrieve (AALTs bs [r]) v = bs @ retrieve r v" 
       
   140 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
 
       
   141 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
 
       
   142 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
 
       
   143 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"
 
       
   144 | "retrieve (ASTAR bs r) (Stars (v#vs)) = 
       
   145      bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
 
       
   146 
       
   147 fun 
   109 fun 
   148   erase :: "arexp \<Rightarrow> rexp"
 
   110   erase :: "arexp \<Rightarrow> rexp"
 
   149 where
 
   111 where
 
   150   "erase AZERO = ZERO"
 
   112   "erase AZERO = ZERO"
 
   151 | "erase (AONE _) = ONE"
 
   113 | "erase (AONE _) = ONE"
 
   153 | "erase (AALTs _ []) = ZERO"
 
   115 | "erase (AALTs _ []) = ZERO"
 
   154 | "erase (AALTs _ [r]) = (erase r)"
 
   116 | "erase (AALTs _ [r]) = (erase r)"
 
   155 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
 
   117 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
 
   156 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
 
   118 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
 
   157 | "erase (ASTAR _ r) = STAR (erase r)"
 
   119 | "erase (ASTAR _ r) = STAR (erase r)"
 
       
   120 
       
   121 fun nonalt :: "arexp \<Rightarrow> bool"
 
       
   122   where
 
       
   123   "nonalt (AALTs bs2 rs) = False"
 
       
   124 | "nonalt r = True"
 
       
   125 
       
   126 
       
   127 fun good :: "arexp \<Rightarrow> bool" where
 
       
   128   "good AZERO = False"
 
       
   129 | "good (AONE cs) = True" 
       
   130 | "good (ACHAR cs c) = True"
 
       
   131 | "good (AALTs cs []) = False"
 
       
   132 | "good (AALTs cs (r#rs)) = (\<forall>r' \<in> set (r#rs). good r')"
 
       
   133 | "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
 
       
   134 | "good (ASTAR cs r) = True"
 
       
   135 
       
   136 
       
   137 
       
   138 
       
   139 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
 
       
   140   "fuse bs AZERO = AZERO"
 
       
   141 | "fuse bs (AONE cs) = AONE (bs @ cs)" 
       
   142 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
 
       
   143 | "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs"
 
       
   144 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
 
       
   145 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
 
       
   146 
       
   147 lemma fuse_append:
 
       
   148   shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
 
       
   149   apply(induct r)
 
       
   150   apply(auto)
 
       
   151   done
 
       
   152 
       
   153 
       
   154 fun intern :: "rexp \<Rightarrow> arexp" where
 
       
   155   "intern ZERO = AZERO"
 
       
   156 | "intern ONE = AONE []"
 
       
   157 | "intern (CHAR c) = ACHAR [] c"
 
       
   158 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
       
   159                                 (fuse [S]  (intern r2))"
 
       
   160 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
 
       
   161 | "intern (STAR r) = ASTAR [] (intern r)"
 
       
   162 
       
   163 
       
   164 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
 
       
   165   "retrieve (AONE bs) Void = bs"
 
       
   166 | "retrieve (ACHAR bs c) (Char d) = bs"
 
       
   167 | "retrieve (AALTs bs [r]) v = bs @ retrieve r v" 
       
   168 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
 
       
   169 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
 
       
   170 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
 
       
   171 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"
 
       
   172 | "retrieve (ASTAR bs r) (Stars (v#vs)) = 
       
   173      bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
 
       
   174 
       
   175 
   158 
   176 
   159 fun
 
   177 fun
 
   160  bnullable :: "arexp \<Rightarrow> bool"
 
   178  bnullable :: "arexp \<Rightarrow> bool"
 
   161 where
 
   179 where
 
   162   "bnullable (AZERO) = False"
 
   180   "bnullable (AZERO) = False"
 
   557   where
 
   575   where
 
   558   "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
 
   576   "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
 
   559 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
 
   577 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
 
   560 | "bsimp r = r"
 
   578 | "bsimp r = r"
 
   561 
   579 
       
   580 value "good (AALTs [] [AALTs [] [AONE []]])"
 
       
   581 value "bsimp (AALTs [] [AONE [], AALTs [] [AONE []]])"
 
       
   582 
       
   583 
   562 fun 
   584 fun 
   563   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 
   585   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 
   564 where
 
   586 where
 
   565   "bders_simp r [] = r"
 
   587   "bders_simp r [] = r"
 
   566 | "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"
 
   588 | "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"
 
   568 definition blexer_simp where
 
   590 definition blexer_simp where
 
   569  "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 
   591  "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 
   570                 decode (bmkeps (bders_simp (intern r) s)) r else None"
 
   592                 decode (bmkeps (bders_simp (intern r) s)) r else None"
 
   571 
   593 
   572 
   594 
   573 
       
   574 
       
   575 
       
   576 lemma asize0:
 
   595 lemma asize0:
 
   577   shows "0 < asize r"
 
   596   shows "0 < asize r"
 
   578   apply(induct  r)
 
   597   apply(induct  r)
 
   579        apply(auto)
 
   598        apply(auto)
 
   580   done
 
   599   done
 
   609 lemma bsimp_AALTs_size:
 
   628 lemma bsimp_AALTs_size:
 
   610   shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"
 
   629   shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"
 
   611   apply(induct rs rule: bsimp_AALTs.induct)
 
   630   apply(induct rs rule: bsimp_AALTs.induct)
 
   612   apply(auto simp add: fuse_size)
 
   631   apply(auto simp add: fuse_size)
 
   613   done
 
   632   done
 
   614   
   633 
       
   634 
   615 lemma bsimp_size:
 
   635 lemma bsimp_size:
 
   616   shows "asize (bsimp r) \<le> asize r"
 
   636   shows "asize (bsimp r) \<le> asize r"
 
   617   apply(induct r)
 
   637   apply(induct r)
 
   618        apply(simp_all)
 
   638        apply(simp_all)
 
   619    apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)
 
   639    apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)
 
   622   apply(simp)
 
   642   apply(simp)
 
   623    apply(rule le_trans)
 
   643    apply(rule le_trans)
 
   624    apply(rule flts_size)
 
   644    apply(rule flts_size)
 
   625   by (simp add: sum_list_mono)
 
   645   by (simp add: sum_list_mono)
 
   626 
   646 
   627 fun nonalt :: "arexp \<Rightarrow> bool"
 
   647 lemma bsimp_asize0:
 
   628   where
 
   648   shows "(\<Sum>x\<leftarrow>rs. asize (bsimp x)) \<le> sum_list (map asize rs)"
 
   629   "nonalt (AALTs bs2 rs) = False"
 
   649   apply(induct rs)
 
   630 | "nonalt r = True"
 
   650    apply(auto)
 
       
   651   by (simp add: add_mono bsimp_size)
 
       
   652   
       
   653 
   631 
   654 
   632 
   655 
   633 
   656 
   634 
   657 
   635 lemma bsimp_AALTs_size2:
 
   658 lemma bsimp_AALTs_size2:
 
  1055    apply(simp)
 
  1078    apply(simp)
 
  1056   apply(case_tac list)
 
  1079   apply(case_tac list)
 
  1057    apply(simp_all)
 
  1080    apply(simp_all)
 
  1058   done
 
  1081   done
 
  1059 
  1082 
       
  1083 lemma good_fuse:
 
       
  1084   shows "good (fuse bs r) = good r"
 
       
  1085   apply(induct r)
 
       
  1086        apply(auto)
 
       
  1087   apply (metis arexp.distinct(25) arexp.distinct(7) arexp.inject(4) good.elims(3) good.simps(4) good.simps(5))
 
       
  1088   by (metis good.simps(4) good.simps(5) neq_Nil_conv)
 
       
  1089 
       
  1090 lemma good0:
 
       
  1091   assumes "rs \<noteq> Nil"
 
       
  1092   shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
 
       
  1093   using  assms
 
       
  1094   apply(induct bs rs rule: bsimp_AALTs.induct)
 
       
  1095   apply(auto simp add: good_fuse)
 
       
  1096   done
 
       
  1097 
       
  1098 lemma good0a:
 
       
  1099   assumes "flts (map bsimp rs) \<noteq> Nil"
 
       
  1100   shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)"
 
       
  1101   using  assms
 
       
  1102   apply(simp)
 
       
  1103   apply(rule good0)
 
       
  1104   apply(simp)
 
       
  1105   done
 
       
  1106 
       
  1107 lemma flts0:
 
       
  1108   assumes "r \<noteq> AZERO" "nonalt r"
 
       
  1109   shows "flts [r] \<noteq> []"
 
       
  1110   using  assms
 
       
  1111   apply(induct r)
 
       
  1112        apply(simp_all)
 
       
  1113   done
 
       
  1114 
       
  1115 lemma flts1:
 
       
  1116   assumes "good r" 
       
  1117   shows "flts [r] \<noteq> []"
 
       
  1118   using  assms
 
       
  1119   apply(induct r)
 
       
  1120        apply(simp_all)
 
       
  1121   apply(case_tac x2a)
 
       
  1122    apply(simp)
 
       
  1123   apply(simp)
 
       
  1124   done
 
       
  1125 
       
  1126 lemma flts2:
 
       
  1127   assumes "good r" 
       
  1128   shows "\<forall>r' \<in> set (flts [r]). good r'"
 
       
  1129   using  assms
 
       
  1130   apply(induct r)
 
       
  1131        apply(simp)
 
       
  1132       apply(simp)
 
       
  1133      apply(simp)
 
       
  1134     prefer 2
 
       
  1135     apply(simp)
 
       
  1136     apply(auto)[1]
 
       
  1137   apply (metis good.simps(5) good_fuse in_set_insert insert_Nil list.exhaust)
 
       
  1138    prefer 2
 
       
  1139    apply(simp)
 
       
  1140   by fastforce
 
       
  1141 
       
  1142 lemma flts3a:
 
       
  1143   assumes "good r" 
       
  1144   shows "good (AALTs bs (flts [r]))"
 
       
  1145   using  assms
 
       
  1146   by (metis flts1 flts2 good.simps(5) neq_Nil_conv)
 
       
  1147 
       
  1148 
       
  1149 lemma flts3:
 
       
  1150   assumes "\<forall>r \<in> set rs. good r \<or> r = AZERO" 
       
  1151   shows "\<forall>r \<in> set (flts rs). good r"
 
       
  1152   using  assms
 
       
  1153   apply(induct rs arbitrary: rule: flts.induct)
 
       
  1154         apply(simp_all)
 
       
  1155   by (metis UnE flts2 k0a set_map)
 
       
  1156 
       
  1157 lemma flts3b:
 
       
  1158   assumes "\<exists>r\<in>set rs. good r"
 
       
  1159   shows "flts rs \<noteq> []"
 
       
  1160   using  assms
 
       
  1161   apply(induct rs arbitrary: rule: flts.induct)
 
       
  1162         apply(simp)
 
       
  1163        apply(simp)
 
       
  1164       apply(simp)
 
       
  1165       apply(auto)
 
       
  1166   done
 
       
  1167 
       
  1168 lemma flts4:
 
       
  1169   assumes "bsimp_AALTs bs (flts rs) = AZERO"
 
       
  1170   shows "\<forall>r \<in> set rs. \<not> good r"
 
       
  1171   using assms
 
       
  1172   apply(induct rs arbitrary: bs rule: flts.induct)
 
       
  1173         apply(auto)
 
       
  1174         defer
 
       
  1175   apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))
 
       
  1176   apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(2) good0 k0b list.distinct(1) list.inject nonalt.simps(3))
 
       
  1177   apply (metis arexp.distinct(3) arexp.distinct(7) bsimp_AALTs.elims fuse.simps(3) list.distinct(1) list.inject)
 
       
  1178   apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good.simps(6) good_fuse list.distinct(1) list.inject)
 
       
  1179   apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
 
       
  1180   apply (metis arexp.distinct(7) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) flts.simps(1) flts.simps(2) flts1 good.simps(7) good_fuse neq_Nil_conv)
 
       
  1181   by (metis (no_types, lifting) Nil_is_append_conv append_Nil2 arexp.distinct(7) bsimp_AALTs.elims butlast.simps(2) butlast_append flts1 flts2 good.simps(1) good0 k0a)
 
       
  1182 
       
  1183 lemma flts_nil:
 
       
  1184   assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
 
       
  1185             good (bsimp y) \<or> bsimp y = AZERO"
 
       
  1186   and "\<forall>r\<in>set rs. \<not> good (bsimp r)"
 
       
  1187   shows "flts (map bsimp rs) = []"
 
       
  1188   using assms
 
       
  1189   apply(induct rs)
 
       
  1190    apply(simp)
 
       
  1191   apply(simp)
 
       
  1192   apply(subst k0)
 
       
  1193   apply(simp)
 
       
  1194   by force
 
       
  1195   
       
  1196 
       
  1197 lemma good1:
 
       
  1198   shows "good (bsimp a) \<or> bsimp a = AZERO"
 
       
  1199   apply(induct a taking: asize rule: measure_induct)
 
       
  1200   apply(case_tac x)
 
       
  1201        apply(simp)
 
       
  1202       apply(simp)
 
       
  1203   apply(simp)
 
       
  1204   prefer 3
 
       
  1205     apply(simp)
 
       
  1206    prefer 2
 
       
  1207   apply(simp only:)
 
       
  1208    apply(case_tac "x52")
 
       
  1209     apply(simp)
 
       
  1210    apply(simp only: good0a)
 
       
  1211   apply(frule_tac x="a" in spec)
 
       
  1212    apply(drule mp)
 
       
  1213   apply(simp)
 
       
  1214     apply(erule disjE)
 
       
  1215      prefer 2
 
       
  1216      apply(simp)
 
       
  1217    apply(frule_tac x="AALTs x51 list" in spec)
 
       
  1218    apply(drule mp)
 
       
  1219   apply(simp add: asize0)
 
       
  1220     apply(auto)[1]
 
       
  1221   apply(frule_tac x="AALTs x51 list" in spec)
 
       
  1222    apply(drule mp)
 
       
  1223     apply(simp add: asize0)
 
       
  1224    apply(erule disjE)
 
       
  1225     apply(rule disjI1)
 
       
  1226   apply(simp add: good0)
 
       
  1227     apply(subst good0)
 
       
  1228      apply (metis Nil_is_append_conv flts1 k0)
 
       
  1229   apply(simp)
 
       
  1230     apply(subst k0)
 
       
  1231     apply(simp)
 
       
  1232     apply(auto)[1]
 
       
  1233   using flts2 apply blast
 
       
  1234     apply (metis good0 in_set_member member_rec(2))
 
       
  1235    apply(simp) 
       
  1236    apply(rule disjI1)
 
       
  1237    apply(drule flts4)
 
       
  1238    apply(subst k0)
 
       
  1239    apply(subst good0)
 
       
  1240     apply (metis append_is_Nil_conv flts1 k0)
 
       
  1241    apply(auto)[1]
 
       
  1242   using flts2 apply blast
 
       
  1243   apply (metis add.commute add_lessD1 flts_nil list.distinct(1) list.set_cases not_less_eq)
 
       
  1244   (* SEQ case *)
 
       
  1245   apply(simp)
 
       
  1246   apply(case_tac "bsimp x42 = AZERO")
 
       
  1247     apply(simp)
 
       
  1248  apply(case_tac "bsimp x43 = AZERO")
 
       
  1249    apply(simp)
 
       
  1250     apply(subst (2) bsimp_ASEQ0)
 
       
  1251   apply(simp)
 
       
  1252   apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
 
       
  1253     apply(auto)[1]
 
       
  1254    apply(subst bsimp_ASEQ2)
 
       
  1255   using good_fuse apply force
 
       
  1256    apply(subst bsimp_ASEQ1)
 
       
  1257      apply(auto)
 
       
  1258   using less_add_Suc1 apply blast
 
       
  1259   using less_add_Suc2 by blast
 
       
  1260 
       
  1261 lemma flts_append:
 
       
  1262   "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
 
       
  1263   apply(induct xs1  arbitrary: xs2  rule: rev_induct)
 
       
  1264    apply(auto)
 
       
  1265   apply(case_tac xs)
 
       
  1266    apply(auto)
 
       
  1267    apply(case_tac x)
 
       
  1268         apply(auto)
 
       
  1269   apply(case_tac x)
 
       
  1270         apply(auto)
 
       
  1271   done
 
       
  1272 
       
  1273 lemma g1:
 
       
  1274   assumes "good (bsimp_AALTs bs rs)"
 
       
  1275   shows "bsimp_AALTs bs rs = AALTs bs rs \<or> (\<exists>r. rs = [r] \<and> bsimp_AALTs bs [r] = fuse bs r)"
 
       
  1276 using assms
 
       
  1277     apply(induct rs arbitrary: bs)
 
       
  1278   apply(simp)
 
       
  1279   apply(case_tac rs)
 
       
  1280   apply(simp only:)
 
       
  1281   apply(simp)
 
       
  1282   apply(case_tac  list)
 
       
  1283   apply(simp)
 
       
  1284   by simp
 
       
  1285 
  1060 lemma flts_idem:
 
  1286 lemma flts_idem:
 
  1061   assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r"
 
  1287   assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
 
  1062   shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)"
 
  1288             bsimp (bsimp y) = bsimp y"
 
       
  1289   shows "map bsimp (flts (map bsimp rs)) = flts (map bsimp rs)"
 
  1063   using assms
 
  1290   using assms
 
  1064   apply(induct rs)
 
  1291   apply(induct rs)
 
  1065    apply(simp)
 
  1292    apply(simp)
 
  1066   apply(simp)
 
  1293   apply(simp)
 
  1067   apply(subst k0)
 
  1294   apply(subst k0)
 
  1068   apply(subst (2) k0) 
  1295   apply(subst (2) k0) 
       
  1296   apply(simp add: flts_append)
 
       
  1297   using good1
 
       
  1298   apply -
 
       
  1299   apply(drule_tac x="a" in meta_spec)
 
       
  1300   apply(erule disjE)
 
       
  1301   prefer 2
 
       
  1302    apply(simp)
 
       
  1303   using flts.simps
 
       
  1304   apply(case_tac a)
 
       
  1305        apply(simp_all)
 
       
  1306    defer
 
       
  1307    apply(drule g1)
 
       
  1308    apply(erule disjE)
 
       
  1309     apply(simp)
 
       
  1310     defer
 
       
  1311     apply(auto)[1]
 
       
  1312     
       
  1313 
       
  1314 
       
  1315 lemma flts_idem:
 
       
  1316   assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
 
       
  1317             bsimp (bsimp y) = bsimp y"
 
       
  1318   shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)"
 
       
  1319   using assms
 
       
  1320   apply(induct rs)
 
       
  1321    apply(simp)
 
       
  1322   apply(simp)
 
       
  1323   apply(subst k0)
 
       
  1324   apply(subst (2) k0) 
       
  1325   apply(simp add: flts_append)
 
       
  1326   using good1
 
       
  1327   apply -
 
       
  1328   apply(drule_tac x="a" in meta_spec)
 
       
  1329   apply(erule disjE)
 
       
  1330   prefer 2
 
       
  1331    apply(simp)
 
       
  1332   using flts.simps
 
       
  1333   apply(case_tac a)
 
       
  1334        apply(simp_all)
 
       
  1335    defer
 
       
  1336    apply(drule g1)
 
       
  1337    apply(erule disjE)
 
       
  1338     apply(simp)
 
       
  1339     defer
 
       
  1340     apply(auto)[1]
 
       
  1341   
       
  1342    apply(subst g1)
 
       
  1343     apply(simp)
 
       
  1344    apply(simp)
 
       
  1345   apply (me tis (full_types) arexp.inject(4) bsimp_AALTs.simps(2) flts3a fuse_empty g1 list.distinct(1))
 
       
  1346   
       
  1347   
       
  1348 
       
  1349 
  1069   apply(case_tac "bsimp a = AZERO")
 
  1350   apply(case_tac "bsimp a = AZERO")
 
  1070    apply(simp)
 
  1351    apply(simp)
 
  1071   apply(case_tac "nonalt (bsimp a)")
 
  1352   apply(case_tac "nonalt (bsimp a)")
 
  1072   thm k0 k0a k0b
 
  1353   thm k0 k0a k0b
 
  1073   apply(subst k0b)
 
  1354   apply(subst k0b)
 
  1091    apply(simp)
 
  1372    apply(simp)
 
  1092   apply(case_tac a)
 
  1373   apply(case_tac a)
 
  1093   apply(simp_all)
 
  1374   apply(simp_all)
 
  1094   oops
 
  1375   oops
 
  1095 
  1376 
  1096 lemma bsimp_AALTs_idem:
 
       
  1097   (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r \<and> nonalt (bsimp r)" *)
 
       
  1098   (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" *)
 
       
  1099   shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
 
       
  1100   apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
 
       
  1101   apply(case_tac x)
 
       
  1102   apply(simp)
 
       
  1103   apply(simp)
 
       
  1104   apply(case_tac "\<exists>bs'  rs'. a = AALTs bs' rs'")
 
       
  1105    apply(clarify)
 
       
  1106   apply(case_tac list)
 
       
  1107         apply(simp)
 
       
  1108        apply(simp) 
       
  1109 
       
  1110   apply(drule_tac x="flts (rs' @ list)" in spec)
 
       
  1111   apply(erule impE)
 
       
  1112   prefer 2
 
       
  1113   apply(case_tac a)
 
       
  1114        apply(simp)
 
       
  1115        apply(case_tac list)
 
       
  1116         apply(simp)
 
       
  1117        apply(simp) 
       
  1118    apply(case_tac list)
 
       
  1119         apply(simp)
 
       
  1120       apply(simp) 
       
  1121    apply(case_tac list)
 
       
  1122         apply(simp)
 
       
  1123      apply(simp) 
       
  1124   prefer 3
 
       
  1125    apply(case_tac list)
 
       
  1126         apply(simp)
 
       
  1127        apply(simp) 
       
  1128    apply(case_tac list)
 
       
  1129     apply(simp)
 
       
  1130       
       
  1131 
       
  1132        apply(simp) 
       
  1133 
       
  1134       apply(case_tac "flts (map bsimp list)")
 
       
  1135        apply(simp)
 
       
  1136       apply(simp)
 
       
  1137   
       
  1138   
       
  1139 
       
  1140    prefer 2
 
       
  1141    apply(simp)
 
       
  1142   
       
  1143    apply(subst k0)
 
       
  1144    apply(subst (2) k0)
 
       
  1145   
       
  1146   apply(case_tac a)
 
       
  1147        apply(simp_all)
 
       
  1148   
       
  1149   prefer 2
 
       
  1150    apply(simp)
 
       
  1151   apply(case_tac r)
 
       
  1152        apply(auto)
 
       
  1153    apply(case_tac "bsimp x42 = AZERO")
 
       
  1154     apply(simp)
 
       
  1155  apply(case_tac "bsimp x43 = AZERO")
 
       
  1156    apply(simp)
 
       
  1157    apply(subst bsimp_ASEQ0)
 
       
  1158    apply(subst bsimp_ASEQ0)
 
       
  1159   apply(simp)
 
       
  1160   apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
 
       
  1161     apply(auto)[1]
 
       
  1162     apply(subst bsimp_ASEQ2)
 
       
  1163    apply(subst bsimp_ASEQ2)
 
       
  1164   prefer 2
 
       
  1165       apply(subst bsimp_ASEQ1)
 
       
  1166       apply(auto)
 
       
  1167   apply(subst bsimp_ASEQ1)
 
       
  1168       apply(auto)
 
       
  1169   apply(subst (asm) bsimp_ASEQ2)
 
       
  1170    apply(subst (asm) bsimp_ASEQ2)
 
       
  1171   using flts_fuse bsimp_fuse bsimp_fuse_AALTs bsimp_fuse_AALTs2 bsimp_AALTs.simps flts.simps
 
       
  1172     
       
  1173    apply(case_tac x43)
 
       
  1174         apply(simp_all)
 
       
  1175     prefer 3
 
       
  1176   oops
 
       
  1177 
       
  1178 lemma ww:
 
       
  1179   shows "bsimp_AALTs bs [r] = fuse bs r"
 
       
  1180   by simp
 
       
  1181 
  1377 
  1182 lemma flts_0:
 
  1378 lemma flts_0:
 
  1183   assumes "nonnested (AALTs bs  rs)"
 
  1379   assumes "nonnested (AALTs bs  rs)"
 
  1184   shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
 
  1380   shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
 
  1185   using assms
 
  1381   using assms
 
  1192     apply(simp) 
  1388     apply(simp) 
  1193 apply(simp) 
  1389 apply(simp) 
  1194   apply(rule ballI)
 
  1390   apply(rule ballI)
 
  1195   apply(simp)
 
  1391   apply(simp)
 
  1196   done
 
  1392   done
 
  1197   
  1393 
  1198 lemma q1:
 
  1394 lemma flts_0a:
 
       
  1395   assumes "nonnested (AALTs bs  rs)"
 
       
  1396   shows "AZERO \<notin> set (flts rs)"
 
       
  1397   using assms
 
       
  1398   using flts_0 by blast 
       
  1399   
       
  1400 lemma qqq1:
 
  1199   shows "AZERO \<notin> set (flts (map bsimp rs))"
 
  1401   shows "AZERO \<notin> set (flts (map bsimp rs))"
 
  1200   apply(induct rs)
 
  1402   by (metis ex_map_conv flts3 good.simps(1) good1)
 
  1201    apply(simp)
 
  1403   
  1202   apply(simp)
 
       
  1203   apply(case_tac rs)
 
       
  1204   apply(simp)
 
       
  1205 
       
  1206 lemma cc:
 
  1404 lemma cc:
 
  1207   assumes "bsimp (fuse bs' r) = (AALTs bs rs)" 
  1405   assumes "bsimp (fuse bs' r) = (AALTs bs rs)" 
  1208   shows "\<forall>r \<in> set  rs. r \<noteq> AZERO"
 
  1406   shows "\<forall>r \<in> set  rs. r \<noteq> AZERO"
 
  1209   using assms
 
  1407   using assms
 
  1210  apply(induct r arbitrary: rs bs bs' rule: bsimp.induct)
 
  1408  apply(induct r arbitrary: rs bs bs' rule: bsimp.induct)
 
  1288      apply(auto)
 
  1486      apply(auto)
 
  1289   apply (simp add: bsimp_ASEQ0)
 
  1487   apply (simp add: bsimp_ASEQ0)
 
  1290   apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
 
  1488   apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
 
  1291     apply(auto)
 
  1489     apply(auto)
 
  1292     apply (simp add: bsimp_ASEQ2)
 
  1490     apply (simp add: bsimp_ASEQ2)
 
  1293   using bsimp_fuse apply fastforce
 
  1491   using bsimp_fuse apply fast force
 
  1294    apply (simp add: bsimp_ASEQ1)
 
  1492    apply (simp add: bsimp_ASEQ1)
 
  1295   
  1493   
  1296   
  1494   
  1297   
  1495   
  1298   apply(subst 
  1496   apply(subst 
  1338   apply(case_tac "length (flts (bsimp a # map bsimp list)) \<le> 1")
 
  1536   apply(case_tac "length (flts (bsimp a # map bsimp list)) \<le> 1")
 
  1339    prefer 2
 
  1537    prefer 2
 
  1340    apply(subst bsimp_AALTs_qq)
 
  1538    apply(subst bsimp_AALTs_qq)
 
  1341     apply(auto)[1]
 
  1539     apply(auto)[1]
 
  1342    apply(simp)
 
  1540    apply(simp)
 
       
  1541    apply(subst k0)
 
       
  1542    apply(simp)
 
       
  1543    apply(simp add: flts_append)
 
       
  1544    apply(subst (2) k0)
 
       
  1545   
       
  1546    apply(simp add: flts_append)
 
       
  1547 
  1343    prefer 2
 
  1548    prefer 2
 
  1344   apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or> 
  1549   apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or> 
  1345                      length (flts (bsimp a # map bsimp list)) = 1")
 
  1550                      length (flts (bsimp a # map bsimp list)) = 1")
 
  1346     prefer 2
 
  1551     prefer 2
 
  1347     apply(auto)[1]
 
  1552     apply(auto)[1]
 
  2298     apply(simp)
 
  2503     apply(simp)
 
  2299    apply(subst bnullable_correctness[symmetric])
 
  2504    apply(subst bnullable_correctness[symmetric])
 
  2300   apply(simp)
 
  2505   apply(simp)
 
  2301   oops
 
  2506   oops
 
  2302 
  2507 
  2303 lemma flts_append:
 
       
  2304   "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
 
       
  2305   apply(induct xs1  arbitrary: xs2  rule: rev_induct)
 
       
  2306    apply(auto)
 
       
  2307   apply(case_tac xs)
 
       
  2308    apply(auto)
 
       
  2309    apply(case_tac x)
 
       
  2310         apply(auto)
 
       
  2311   apply(case_tac x)
 
       
  2312         apply(auto)
 
       
  2313   done
 
       
  2314 
  2508 
  2315 lemma flts_bsimp:
 
  2509 lemma flts_bsimp:
 
  2316   "flts (map bsimp rs) = map bsimp (flts rs)"
 
  2510   "flts (map bsimp rs) = map bsimp (flts rs)"
 
  2317 apply(induct rs taking: size rule: measure_induct)
 
  2511 apply(induct rs taking: size rule: measure_induct)
 
  2318   apply(case_tac x)
 
  2512   apply(case_tac x)
lexing