equal
deleted
inserted
replaced
1077 shows "breakHead [rder x (RSEQ r1 r2)] = RSEQ (rder x r1) r2 # map (rders r2) (vsuf [x] r1)" |
1077 shows "breakHead [rder x (RSEQ r1 r2)] = RSEQ (rder x r1) r2 # map (rders r2) (vsuf [x] r1)" |
1078 by simp |
1078 by simp |
1079 |
1079 |
1080 |
1080 |
1081 lemma vsuf_compose2: |
1081 lemma vsuf_compose2: |
1082 shows "(map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1)) = map (rders r2) (vsuf (xs @ [x]) r1)" |
1082 shows "(map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1)) = |
|
1083 map (rders r2) (vsuf (xs @ [x]) r1)" |
1083 proof(induct xs arbitrary: r1) |
1084 proof(induct xs arbitrary: r1) |
1084 case Nil |
1085 case Nil |
1085 then show ?case |
1086 then show ?case |
1086 by simp |
1087 by simp |
1087 next |
1088 next |
1242 "created_by_star (RSEQ ra (RSTAR rb))" |
1243 "created_by_star (RSEQ ra (RSTAR rb))" |
1243 | "\<lbrakk>created_by_star r1; created_by_star r2\<rbrakk> \<Longrightarrow> created_by_star (RALT r1 r2)" |
1244 | "\<lbrakk>created_by_star r1; created_by_star r2\<rbrakk> \<Longrightarrow> created_by_star (RALT r1 r2)" |
1244 |
1245 |
1245 |
1246 |
1246 |
1247 |
|
1248 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where |
|
1249 "star_update c r [] = []" |
|
1250 |"star_update c r (s # Ss) = (if (rnullable (rders r s)) |
|
1251 then (s@[c]) # [c] # (star_update c r Ss) |
|
1252 else (s@[c]) # (star_update c r Ss) )" |
|
1253 |
|
1254 |
|
1255 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" |
|
1256 where |
|
1257 "star_updates [] r Ss = Ss" |
|
1258 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" |
|
1259 |
|
1260 |
1247 |
1261 |
1248 lemma cbs_ders_cbs: |
1262 lemma cbs_ders_cbs: |
1249 shows "created_by_star r \<Longrightarrow> created_by_star (rder c r)" |
1263 shows "created_by_star r \<Longrightarrow> created_by_star (rder c r)" |
1250 apply(induct r rule: created_by_star.induct) |
1264 apply(induct r rule: created_by_star.induct) |
1251 apply simp |
1265 apply simp |
1259 apply (simp add: created_by_star.intros(1)) |
1273 apply (simp add: created_by_star.intros(1)) |
1260 apply(subst rders_append) |
1274 apply(subst rders_append) |
1261 apply simp |
1275 apply simp |
1262 using cbs_ders_cbs by auto |
1276 using cbs_ders_cbs by auto |
1263 |
1277 |
1264 (* |
1278 |
1265 lemma created_by_star_cases: |
|
1266 shows "created_by_star r \<Longrightarrow> \<exists>ra rb. (r = RALT ra rb \<and> created_by_star ra \<and> created_by_star rb) \<or> r = RSEQ ra rb " |
|
1267 by (meson created_by_star.cases) |
|
1268 *) |
|
1269 |
1279 |
1270 |
1280 |
1271 lemma hfau_pushin: |
1281 lemma hfau_pushin: |
1272 shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))" |
1282 shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))" |
1273 |
|
1274 proof(induct r rule: created_by_star.induct) |
1283 proof(induct r rule: created_by_star.induct) |
1275 case (1 ra rb) |
1284 case (1 ra rb) |
1276 then show ?case by simp |
1285 then show ?case by simp |
1277 next |
1286 next |
1278 case (2 r1 r2) |
1287 case (2 r1 r2) |
1285 qed |
1294 qed |
1286 |
1295 |
1287 (*AALTS [a\x . b.c, b\x .c, c \x]*) |
1296 (*AALTS [a\x . b.c, b\x .c, c \x]*) |
1288 (*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*) |
1297 (*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*) |
1289 |
1298 |
1290 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where |
|
1291 "star_update c r [] = []" |
|
1292 |"star_update c r (s # Ss) = (if (rnullable (rders r s)) |
|
1293 then (s@[c]) # [c] # (star_update c r Ss) |
|
1294 else (s@[c]) # (star_update c r Ss) )" |
|
1295 |
|
1296 |
|
1297 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" |
|
1298 where |
|
1299 "star_updates [] r Ss = Ss" |
|
1300 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" |
|
1301 |
|
1302 |
|
1303 lemma stupdates_append: shows |
1299 lemma stupdates_append: shows |
1304 "star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)" |
1300 "star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)" |
1305 apply(induct s arbitrary: Ss) |
1301 apply(induct s arbitrary: Ss) |
1306 apply simp |
1302 apply simp |
1307 apply simp |
1303 apply simp |
1319 by (simp add: rders_append) |
1315 by (simp add: rders_append) |
1320 |
1316 |
1321 |
1317 |
1322 |
1318 |
1323 lemma stupdates_join_general: |
1319 lemma stupdates_join_general: |
1324 shows "concat (map hflat_aux (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))) = |
1320 shows "concat |
1325 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)" |
1321 (map hflat_aux (map (rder x) |
|
1322 (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss))) |
|
1323 ) = |
|
1324 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)" |
1326 apply(induct xs arbitrary: Ss) |
1325 apply(induct xs arbitrary: Ss) |
1327 apply (simp) |
1326 apply (simp) |
1328 prefer 2 |
1327 prefer 2 |
1329 apply auto[1] |
1328 apply auto[1] |
1330 using stupdate_induct1 by blast |
1329 using stupdate_induct1 by blast |
1384 apply(induct rule: created_by_star.induct) |
1383 apply(induct rule: created_by_star.induct) |
1385 apply simp |
1384 apply simp |
1386 apply (metis rsimp.simps(6) rsimp_seq_equal1) |
1385 apply (metis rsimp.simps(6) rsimp_seq_equal1) |
1387 using cbs_hfau_rsimpeq1 hflat_aux.simps(1) by presburger |
1386 using cbs_hfau_rsimpeq1 hflat_aux.simps(1) by presburger |
1388 |
1387 |
1389 |
|
1390 (* |
|
1391 lemma hfau_rsimpeq2_oldproof: shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
|
1392 apply(induct r) |
|
1393 apply simp+ |
|
1394 apply (metis rsimp_seq_equal1) |
|
1395 prefer 2 |
|
1396 apply simp |
|
1397 apply(case_tac x) |
|
1398 apply simp |
|
1399 apply(case_tac "list") |
|
1400 apply simp |
|
1401 apply (metis idem_after_simp1) |
|
1402 apply(case_tac "lista") |
|
1403 prefer 2 |
|
1404 apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2)) |
|
1405 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))") |
|
1406 apply simp |
|
1407 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))") |
|
1408 using hflat_aux.simps(1) apply presburger |
|
1409 apply simp |
|
1410 using cbs_hfau_rsimpeq1 by fastforce |
|
1411 *) |
|
1412 |
|
1413 lemma star_closed_form1: |
1388 lemma star_closed_form1: |
1414 shows "rsimp (rders (RSTAR r0) (c#s)) = |
1389 shows "rsimp (rders (RSTAR r0) (c#s)) = |
1415 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
1390 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
1416 using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger |
1391 using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger |
1417 |
1392 |