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/ClosedForms.thy
changeset 489 2b5b3f83e2b6
parent 488 370dae790b30
child 490 64183736777a
equal deleted inserted replaced
488:370dae790b30 489:2b5b3f83e2b6 
     1 theory ClosedForms imports
 
     1 theory ClosedForms imports
 
     2 "BasicIdentities"
 
     2 "BasicIdentities"
 
     3 begin
 
     3 begin
 
     4 
     4 
       
     5 lemma flts_middle0:
 
       
     6   shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
 
       
     7   apply(induct rsa)
 
       
     8   apply simp
 
       
     9   by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
    10 
       
    11 lemma simp_flatten3:
 
       
    12   shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
 
       
    13   apply(induct rsa)
 
       
    14   
       
    15   using simp_flatten apply force
 
       
    16 
       
    17   sorry
 
       
    18 
       
    19 inductive 
       
    20   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
 
       
    21 where
 
       
    22   "RSEQ  RZERO r2 \<leadsto> RZERO"
 
       
    23 | "RSEQ  r1 RZERO \<leadsto> RZERO"
 
       
    24 | "RSEQ  RONE r \<leadsto>  r"
 
       
    25 | "r1 \<leadsto> r2 \<Longrightarrow> RSEQ  r1 r3 \<leadsto> RSEQ r2 r3"
 
       
    26 | "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4"
 
       
    27 | "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS  (rs1 @ [r'] @ rs2))"
 
       
    28 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
 
       
    29 | "RALTS  (rsa @ [RZERO] @ rsb) \<leadsto> RALTS  (rsa @ rsb)"
 
       
    30 | "RALTS  (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)"
 
       
    31 | "RALTS  [] \<leadsto> RZERO"
 
       
    32 | "RALTS  [r] \<leadsto> r"
 
       
    33 | "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
 
       
    34 
       
    35 inductive 
       
    36   hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
 
       
    37 where 
       
    38   rs1[intro, simp]:"r \<leadsto>* r"
 
       
    39 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
       
    40 
       
    41 
       
    42 lemma hr_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
 
       
    43   using hrewrites.intros(1) hrewrites.intros(2) by blast
 
       
    44  
       
    45 lemma hreal_trans[trans]: 
       
    46   assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
 
       
    47   shows "r1 \<leadsto>* r3"
 
       
    48   using a2 a1
 
       
    49   apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct) 
       
    50   apply(auto)
 
       
    51   done
 
       
    52 
       
    53 lemma  hmany_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
       
    54   by (meson hr_in_rstar hreal_trans)
 
       
    55 
       
    56 lemma hrewrites_seq_context:
 
       
    57   shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r3"
 
       
    58   apply(induct r1 r2 rule: hrewrites.induct)
 
       
    59    apply simp
 
       
    60   using hrewrite.intros(4) by blast
 
       
    61 
       
    62 lemma hrewrites_seq_context2:
 
       
    63   shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 \<leadsto>* RSEQ r0 r2"
 
       
    64   apply(induct r1 r2 rule: hrewrites.induct)
 
       
    65    apply simp
 
       
    66   using hrewrite.intros(5) by blast
 
       
    67 
       
    68 lemma hrewrites_seq_context0:
 
       
    69   shows "r1 \<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RZERO"
 
       
    70   apply(subgoal_tac "RSEQ r1 r3 \<leadsto>* RSEQ RZERO r3")
 
       
    71   using hrewrite.intros(1) apply blast
 
       
    72   by (simp add: hrewrites_seq_context)
 
       
    73 
       
    74 lemma hrewrites_seq_contexts:
 
       
    75   shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4"
 
       
    76   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
       
    77 
       
    78 
       
    79 
     5 lemma map_concat_cons:
 
    80 lemma map_concat_cons:
 
     6   shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
 
    81   shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
 
     7   by simp
 
    82   by simp
 
     8 
    83 
     9 lemma neg_removal_element_of:
 
    84 lemma neg_removal_element_of:
 
    17 
    92 
    18 
    93 
    19 
    94 
    20 
    95 
    21 
    96 
    22 lemma flts_middle0:
 
       
    23   shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
 
       
    24   apply(induct rsa)
 
       
    25   apply simp
 
       
    26   by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
       
    27 
    97 
    28 lemma flts_middle01:
 
    98 lemma flts_middle01:
 
    29   shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)"
 
    99   shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)"
 
    30   by (simp add: flts_middle0)
 
   100   by (simp add: flts_middle0)
 
    31 
   101 
   329   using in_mono by fastforce
 
   399   using in_mono by fastforce
 
   330 
   400 
   331 
   401 
   332 
   402 
   333 
   403 
   334 lemma grewrite_equal_rsimp:
 
       
   335   shows "\<lbrakk>rs1 \<leadsto>g rs2; rsimp_ALTs (rdistinct (rflts (map rsimp rs1)) (rset \<union> \<Union>(alt_set ` rset))) =
 
       
   336           rsimp_ALTs (rdistinct (rflts (map rsimp rs2)) (rset \<union> \<Union>(alt_set ` rset)))\<rbrakk>
 
       
   337        \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs1))  (rset \<union> \<Union>(alt_set ` rset))) =
 
       
   338            rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs2))  (rset \<union> \<Union>(alt_set ` rset)))"
 
       
   339   apply(induct rs1 rs2 arbitrary:rset rule: grewrite.induct)
 
       
   340      apply simp
 
       
   341   apply (metis append_Cons append_Nil flts_middle0)
 
       
   342     apply(case_tac "rsimp r \<in> rset")
 
       
   343      apply simp
 
       
   344   oops
 
       
   345 
   404 
   346 lemma grewrite_cases_middle:
 
   405 lemma grewrite_cases_middle:
 
   347   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 
   406   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 
   348 (\<exists>rsa rsb rsc. rs1 =  (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or>
 
   407 (\<exists>rsa rsb rsc. rs1 =  (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or>
 
   349 (\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc) \<or>
 
   408 (\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc) \<or>
 
  1186   apply(induct r rule: rsimp.induct)
 
  1245   apply(induct r rule: rsimp.induct)
 
  1187   apply(auto)
 
  1246   apply(auto)
 
  1188   apply (metis idiot idiot2 rrexp.distinct(5))
 
  1247   apply (metis idiot idiot2 rrexp.distinct(5))
 
  1189   by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
 
  1248   by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
 
  1190 
  1249 
  1191 lemma basic_rsimp_SEQ_property1:
 
       
  1192   shows "rsimp_SEQ RONE r = r"
 
       
  1193   by (simp add: idiot)
 
       
  1194 
       
  1195 lemma basic_rsimp_SEQ_property3:
 
       
  1196   shows "rsimp_SEQ r RZERO = RZERO"  
       
  1197   using rsimp_SEQ.elims by blast
 
       
  1198 
  1250 
  1199 thm rsimp_SEQ.elims
 
  1251 thm rsimp_SEQ.elims
 
  1200 
  1252 
  1201 
  1253 
  1202 lemma basic_rsimp_SEQ_property2:
 
  1254 lemma basic_rsimp_SEQ_property2:
 
  1268    apply simp
 
  1320    apply simp
 
  1269   using rsimp_idem apply presburger
 
  1321   using rsimp_idem apply presburger
 
  1270   using der_simp_nullability by presburger
 
  1322   using der_simp_nullability by presburger
 
  1271   
  1323   
  1272 
  1324 
       
  1325 
       
  1326 lemma grewrite_ralts:
 
       
  1327   shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
 
       
  1328   by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
 
       
  1329 
       
  1330 lemma grewrites_ralts:
 
       
  1331   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
 
       
  1332   apply(induct rule: grewrites.induct)
 
       
  1333   apply simp
 
       
  1334   using grewrite_ralts hreal_trans by blast
 
       
  1335   
       
  1336 
       
  1337 lemma distinct_grewrites_subgoal1:
 
       
  1338   shows "  
       
  1339        \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3"
 
       
  1340   apply(subgoal_tac "RALTS rs1 \<leadsto>* RALTS rs3")
 
       
  1341   apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
       
  1342   apply(subgoal_tac "rs1 \<leadsto>g* rs3")
 
       
  1343   using grewrites_ralts apply blast
 
       
  1344   using grewrites.intros(2) by presburger
 
       
  1345 
       
  1346 
       
  1347 
       
  1348 
       
  1349 
       
  1350 
       
  1351 lemma grewrites_ralts_rsimpalts:
 
       
  1352   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* rsimp_ALTs rs' "
 
       
  1353   apply(induct rs rs' rule: grewrites.induct)
 
       
  1354    apply(case_tac rs)
 
       
  1355   using hrewrite.intros(9) apply force
 
       
  1356    apply(case_tac list)
 
       
  1357   apply simp
 
       
  1358   using hr_in_rstar hrewrite.intros(10) rsimp_ALTs.simps(2) apply presburger
 
       
  1359    apply simp
 
       
  1360   apply(case_tac rs2)
 
       
  1361    apply simp
 
       
  1362    apply (metis grewrite.intros(3) grewrite_singleton rsimp_ALTs.simps(1))
 
       
  1363   apply(case_tac list)
 
       
  1364    apply(simp)
 
       
  1365   using distinct_grewrites_subgoal1 apply blast
 
       
  1366   apply simp
 
       
  1367   apply(case_tac rs3)
 
       
  1368    apply simp
 
       
  1369   using grewrites_ralts hrewrite.intros(9) apply blast
 
       
  1370   by (metis (no_types, opaque_lifting) grewrite_ralts hr_in_rstar hreal_trans hrewrite.intros(10) neq_Nil_conv rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
       
  1371 
       
  1372 lemma hrewrites_alts:
 
       
  1373   shows " r \<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto>* (RALTS  (rs1 @ [r'] @ rs2))"
 
       
  1374   apply(induct r r' rule: hrewrites.induct)
 
       
  1375   apply simp
 
       
  1376   using hrewrite.intros(6) by blast
 
       
  1377 
  1273 inductive 
  1378 inductive 
  1274   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
 
  1379   srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)
 
  1275 where
 
  1380 where
 
  1276   "RSEQ  RZERO r2 \<leadsto> RZERO"
 
  1381   ss1: "[] scf\<leadsto>* []"
 
  1277 | "RSEQ  r1 RZERO \<leadsto> RZERO"
 
  1382 | ss2: "\<lbrakk>r \<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
 
  1278 | "RSEQ  RONE r \<leadsto>  r"
 
  1383 
  1279 | "r1 \<leadsto> r2 \<Longrightarrow> RSEQ  r1 r3 \<leadsto> RSEQ r2 r3"
 
  1384 
  1280 | "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4"
 
  1385 lemma hrewrites_alts_cons:
 
  1281 | "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS  (rs1 @ [r'] @ rs2))"
 
  1386   shows " RALTS rs \<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) \<leadsto>* RALTS (r # rs')"
 
  1282 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
 
  1387 
  1283 | "RALTS  (rsa @ [RZERO] @ rsb) \<leadsto> RALTS  (rsa @ rsb)"
 
  1388 
  1284 | "RALTS  (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)"
 
  1389   oops
 
  1285 | "RALTS  [] \<leadsto> RZERO"
 
  1390 
  1286 | "RALTS  [r] \<leadsto> r"
 
  1391 
  1287 | "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
 
  1392 lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) \<leadsto>* (RALTS (rs@rs2))"
 
  1288 
  1393 
  1289 inductive 
  1394   apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)
 
  1290   hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
 
  1395    apply(rule rs1)
 
  1291 where 
  1396   apply(drule_tac x = "rsa@[r']" in meta_spec)
 
  1292   rs1[intro, simp]:"r \<leadsto>* r"
 
  1397   apply simp
 
  1293 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
  1398   apply(rule hreal_trans)
 
  1294 
  1399    prefer 2
 
  1295 
  1400    apply(assumption)
 
  1296 lemma hr_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
 
  1401   apply(drule hrewrites_alts)
 
  1297   using hrewrites.intros(1) hrewrites.intros(2) by blast
 
  1402   by auto
 
  1298  
  1403 
  1299 lemma hreal_trans[trans]: 
  1404 
  1300   assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
 
  1405 corollary srewritescf_alt1: 
  1301   shows "r1 \<leadsto>* r3"
 
  1406   assumes "rs1 scf\<leadsto>* rs2"
 
  1302   using a2 a1
 
  1407   shows "RALTS rs1 \<leadsto>* RALTS rs2"
 
  1303   apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct) 
  1408   using assms
 
  1304   apply(auto)
 
  1409   by (metis append_Nil srewritescf_alt)
 
  1305   done
 
  1410 
  1306 
  1411 
  1307 lemma  hmany_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
  1412 
  1308   by (meson hr_in_rstar hreal_trans)
 
  1413 
  1309 
  1414 lemma trivialrsimp_srewrites: 
  1310 lemma hrewrites_seq_context:
 
  1415   "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
 
  1311   shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r3"
 
  1416 
  1312   apply(induct r1 r2 rule: hrewrites.induct)
 
  1417   apply(induction rs)
 
  1313    apply simp
 
  1418    apply simp
 
  1314   using hrewrite.intros(4) by blast
 
  1419    apply(rule ss1)
 
  1315 
  1420   by (metis insert_iff list.simps(15) list.simps(9) srewritescf.simps)
 
  1316 lemma hrewrites_seq_context2:
 
  1421 
  1317   shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 \<leadsto>* RSEQ r0 r2"
 
  1422 lemma hrewrites_list: 
  1318   apply(induct r1 r2 rule: hrewrites.induct)
 
  1423   shows
 
  1319    apply simp
 
  1424 " (\<And>xa. xa \<in> set x \<Longrightarrow> xa \<leadsto>* rsimp xa) \<Longrightarrow> RALTS x \<leadsto>* RALTS (map rsimp x)"
 
  1320   using hrewrite.intros(5) by blast
 
  1425   apply(induct x)
 
  1321 
  1426    apply(simp)+
 
  1322 lemma hrewrites_seq_context0:
 
  1427   by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)
 
  1323   shows "r1 \<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RZERO"
 
  1428 (*  apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")*)
 
  1324   apply(subgoal_tac "RSEQ r1 r3 \<leadsto>* RSEQ RZERO r3")
 
  1429 
  1325   using hrewrite.intros(1) apply blast
 
  1430   
  1326   by (simp add: hrewrites_seq_context)
 
       
  1327 
       
  1328 lemma hrewrites_seq_contexts:
 
       
  1329   shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4"
 
       
  1330   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
       
  1331 
       
  1332 lemma hrewrite_simpeq:
 
  1431 lemma hrewrite_simpeq:
 
  1333   shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
 
  1432   shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
 
  1334   apply(induct rule: hrewrite.induct)
 
  1433   apply(induct rule: hrewrite.induct)
 
  1335             apply simp+
 
  1434             apply simp+
 
  1336   apply (simp add: basic_rsimp_SEQ_property3)
 
  1435   apply (simp add: basic_rsimp_SEQ_property3)
 
  1337   apply (simp add: basic_rsimp_SEQ_property1)
 
  1436   apply (simp add: basic_rsimp_SEQ_property1)
 
  1338   using rsimp.simps(1) apply presburger
 
  1437   using rsimp.simps(1) apply presburger
 
  1339         apply simp+
 
  1438         apply simp+
 
  1340   using flts_middle0 apply force
 
  1439   using flts_middle0 apply force
 
       
  1440 
       
  1441   
  1341   using simp_flatten3 apply presburger
 
  1442   using simp_flatten3 apply presburger
 
       
  1443 
  1342   apply simp+
 
  1444   apply simp+
 
  1343   apply (simp add: idem_after_simp1)
 
  1445   apply (simp add: idem_after_simp1)
 
  1344   using grewrite.intros(4) grewrite_equal_rsimp by presburger
 
  1446   using grewrite.intros(4) grewrite_equal_rsimp by presburger
 
  1345 
  1447 
  1346 lemma hrewrites_simpeq:
 
  1448 lemma hrewrites_simpeq:
 
  1349    apply simp
 
  1451    apply simp
 
  1350   apply(subgoal_tac "rsimp r2 = rsimp r3")
 
  1452   apply(subgoal_tac "rsimp r2 = rsimp r3")
 
  1351    apply auto[1]
 
  1453    apply auto[1]
 
  1352   using hrewrite_simpeq by presburger
 
  1454   using hrewrite_simpeq by presburger
 
  1353   
  1455   
  1354 
       
  1355 lemma grewrite_ralts:
 
       
  1356   shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
 
       
  1357   by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
 
       
  1358 
       
  1359 lemma grewrites_ralts:
 
       
  1360   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
 
       
  1361   apply(induct rule: grewrites.induct)
 
       
  1362   apply simp
 
       
  1363   using grewrite_ralts hreal_trans by blast
 
       
  1364   
       
  1365 
       
  1366 lemma distinct_grewrites_subgoal1:
 
       
  1367   shows "  
       
  1368        \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3"
 
       
  1369   apply(subgoal_tac "RALTS rs1 \<leadsto>* RALTS rs3")
 
       
  1370   apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
       
  1371   apply(subgoal_tac "rs1 \<leadsto>g* rs3")
 
       
  1372   using grewrites_ralts apply blast
 
       
  1373   using grewrites.intros(2) by presburger
 
       
  1374 
       
  1375 
       
  1376 
       
  1377 
       
  1378 
       
  1379 
       
  1380 lemma grewrites_ralts_rsimpalts:
 
       
  1381   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* rsimp_ALTs rs' "
 
       
  1382   apply(induct rs rs' rule: grewrites.induct)
 
       
  1383    apply(case_tac rs)
 
       
  1384   using hrewrite.intros(9) apply force
 
       
  1385    apply(case_tac list)
 
       
  1386   apply simp
 
       
  1387   using hr_in_rstar hrewrite.intros(10) rsimp_ALTs.simps(2) apply presburger
 
       
  1388    apply simp
 
       
  1389   apply(case_tac rs2)
 
       
  1390    apply simp
 
       
  1391    apply (metis grewrite.intros(3) grewrite_singleton rsimp_ALTs.simps(1))
 
       
  1392   apply(case_tac list)
 
       
  1393    apply(simp)
 
       
  1394   using distinct_grewrites_subgoal1 apply blast
 
       
  1395   apply simp
 
       
  1396   apply(case_tac rs3)
 
       
  1397    apply simp
 
       
  1398   using grewrites_ralts hrewrite.intros(9) apply blast
 
       
  1399   by (metis (no_types, opaque_lifting) grewrite_ralts hr_in_rstar hreal_trans hrewrite.intros(10) neq_Nil_conv rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
       
  1400 
       
  1401 lemma hrewrites_alts:
 
       
  1402   shows " r \<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto>* (RALTS  (rs1 @ [r'] @ rs2))"
 
       
  1403   apply(induct r r' rule: hrewrites.induct)
 
       
  1404   apply simp
 
       
  1405   using hrewrite.intros(6) by blast
 
       
  1406 
       
  1407 inductive 
       
  1408   srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)
 
       
  1409 where
 
       
  1410   ss1: "[] scf\<leadsto>* []"
 
       
  1411 | ss2: "\<lbrakk>r \<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
 
       
  1412 
       
  1413 
       
  1414 lemma hrewrites_alts_cons:
 
       
  1415   shows " RALTS rs \<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) \<leadsto>* RALTS (r # rs')"
 
       
  1416 
       
  1417 
       
  1418   oops
 
       
  1419 
       
  1420 
       
  1421 lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) \<leadsto>* (RALTS (rs@rs2))"
 
       
  1422 
       
  1423   apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)
 
       
  1424    apply(rule rs1)
 
       
  1425   apply(drule_tac x = "rsa@[r']" in meta_spec)
 
       
  1426   apply simp
 
       
  1427   apply(rule hreal_trans)
 
       
  1428    prefer 2
 
       
  1429    apply(assumption)
 
       
  1430   apply(drule hrewrites_alts)
 
       
  1431   by auto
 
       
  1432 
       
  1433 
       
  1434 corollary srewritescf_alt1: 
       
  1435   assumes "rs1 scf\<leadsto>* rs2"
 
       
  1436   shows "RALTS rs1 \<leadsto>* RALTS rs2"
 
       
  1437   using assms
 
       
  1438   by (metis append_Nil srewritescf_alt)
 
       
  1439 
       
  1440 
       
  1441 
       
  1442 
       
  1443 lemma trivialrsimp_srewrites: 
       
  1444   "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
 
       
  1445 
       
  1446   apply(induction rs)
 
       
  1447    apply simp
 
       
  1448    apply(rule ss1)
 
       
  1449   by (metis insert_iff list.simps(15) list.simps(9) srewritescf.simps)
 
       
  1450 
       
  1451 lemma hrewrites_list: 
       
  1452   shows
 
       
  1453 " (\<And>xa. xa \<in> set x \<Longrightarrow> xa \<leadsto>* rsimp xa) \<Longrightarrow> RALTS x \<leadsto>* RALTS (map rsimp x)"
 
       
  1454   apply(induct x)
 
       
  1455    apply(simp)+
 
       
  1456   by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)
 
       
  1457 (*  apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")*)
 
       
  1458 
       
  1459   
       
  1460 
       
  1461 
  1456 
  1462 
  1457 
  1463 lemma simp_hrewrites:
 
  1458 lemma simp_hrewrites:
 
  1464   shows "r1 \<leadsto>* rsimp r1"
 
  1459   shows "r1 \<leadsto>* rsimp r1"
 
  1465   apply(induct r1)
 
  1460   apply(induct r1)
 
  2273    apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem)
 
  2268    apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem)
 
  2274   using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger
 
  2269   using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger
 
  2275 
  2270 
  2276 
  2271 
  2277 
  2272 
       
  2273 
  2278 end
 
  2274 end
lexing