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 492 61eff2abb0b6
parent 491 48ce16d61e03
equal deleted inserted replaced
491:48ce16d61e03 492:61eff2abb0b6 
    23 
    23 
    24 
    24 
    25   
    25   
    26 
    26 
    27 inductive 
    27 inductive 
    28   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
 
    28   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
 
    29 where
 
    29 where
 
    30   "RSEQ  RZERO r2 \<leadsto> RZERO"
 
    30   "RSEQ  RZERO r2 h\<leadsto> RZERO"
 
    31 | "RSEQ  r1 RZERO \<leadsto> RZERO"
 
    31 | "RSEQ  r1 RZERO h\<leadsto> RZERO"
 
    32 | "RSEQ  RONE r \<leadsto>  r"
 
    32 | "RSEQ  RONE r h\<leadsto>  r"
 
    33 | "r1 \<leadsto> r2 \<Longrightarrow> RSEQ  r1 r3 \<leadsto> RSEQ r2 r3"
 
    33 | "r1 h\<leadsto> r2 \<Longrightarrow> RSEQ  r1 r3 h\<leadsto> RSEQ r2 r3"
 
    34 | "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4"
 
    34 | "r3 h\<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 h\<leadsto> RSEQ r1 r4"
 
    35 | "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS  (rs1 @ [r'] @ rs2))"
 
    35 | "r h\<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto> (RALTS  (rs1 @ [r'] @ rs2))"
 
    36 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
 
    36 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
 
    37 | "RALTS  (rsa @ [RZERO] @ rsb) \<leadsto> RALTS  (rsa @ rsb)"
 
    37 | "RALTS  (rsa @ [RZERO] @ rsb) h\<leadsto> RALTS  (rsa @ rsb)"
 
    38 | "RALTS  (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)"
 
    38 | "RALTS  (rsa @ [RALTS rs1] @ rsb) h\<leadsto> RALTS (rsa @ rs1 @ rsb)"
 
    39 | "RALTS  [] \<leadsto> RZERO"
 
    39 | "RALTS  [] h\<leadsto> RZERO"
 
    40 | "RALTS  [r] \<leadsto> r"
 
    40 | "RALTS  [r] h\<leadsto> r"
 
    41 | "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
 
    41 | "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) h\<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
 
    42 
    42 
    43 inductive 
    43 inductive 
    44   hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
 
    44   hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto>* _" [100, 100] 100)
 
    45 where 
    45 where 
    46   rs1[intro, simp]:"r \<leadsto>* r"
 
    46   rs1[intro, simp]:"r h\<leadsto>* r"
 
    47 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
    47 | rs2[intro]: "\<lbrakk>r1 h\<leadsto>* r2; r2 h\<leadsto> r3\<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"
 
    48 
    48 
    49 
    49 
    50 lemma hr_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
 
    50 lemma hr_in_rstar : "r1 h\<leadsto> r2 \<Longrightarrow> r1 h\<leadsto>* r2"
 
    51   using hrewrites.intros(1) hrewrites.intros(2) by blast
 
    51   using hrewrites.intros(1) hrewrites.intros(2) by blast
 
    52  
    52  
    53 lemma hreal_trans[trans]: 
    53 lemma hreal_trans[trans]: 
    54   assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
 
    54   assumes a1: "r1 h\<leadsto>* r2"  and a2: "r2 h\<leadsto>* r3"
 
    55   shows "r1 \<leadsto>* r3"
 
    55   shows "r1 h\<leadsto>* r3"
 
    56   using a2 a1
 
    56   using a2 a1
 
    57   apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct) 
    57   apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct) 
    58   apply(auto)
 
    58   apply(auto)
 
    59   done
 
    59   done
 
    60 
    60 
    61 lemma  hmany_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
    61 lemma  hmany_steps_later: "\<lbrakk>r1 h\<leadsto> r2; r2 h\<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"
 
    62   by (meson hr_in_rstar hreal_trans)
 
    62   by (meson hr_in_rstar hreal_trans)
 
    63 
    63 
    64 lemma hrewrites_seq_context:
 
    64 lemma hrewrites_seq_context:
 
    65   shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r3"
 
    65   shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r3"
 
    66   apply(induct r1 r2 rule: hrewrites.induct)
 
    66   apply(induct r1 r2 rule: hrewrites.induct)
 
    67    apply simp
 
    67    apply simp
 
    68   using hrewrite.intros(4) by blast
 
    68   using hrewrite.intros(4) by blast
 
    69 
    69 
    70 lemma hrewrites_seq_context2:
 
    70 lemma hrewrites_seq_context2:
 
    71   shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 \<leadsto>* RSEQ r0 r2"
 
    71   shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 h\<leadsto>* RSEQ r0 r2"
 
    72   apply(induct r1 r2 rule: hrewrites.induct)
 
    72   apply(induct r1 r2 rule: hrewrites.induct)
 
    73    apply simp
 
    73    apply simp
 
    74   using hrewrite.intros(5) by blast
 
    74   using hrewrite.intros(5) by blast
 
    75 
    75 
    76 lemma hrewrites_seq_context0:
 
    76 lemma hrewrites_seq_context0:
 
    77   shows "r1 \<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RZERO"
 
    77   shows "r1 h\<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RZERO"
 
    78   apply(subgoal_tac "RSEQ r1 r3 \<leadsto>* RSEQ RZERO r3")
 
    78   apply(subgoal_tac "RSEQ r1 r3 h\<leadsto>* RSEQ RZERO r3")
 
    79   using hrewrite.intros(1) apply blast
 
    79   using hrewrite.intros(1) apply blast
 
    80   by (simp add: hrewrites_seq_context)
 
    80   by (simp add: hrewrites_seq_context)
 
    81 
    81 
    82 lemma hrewrites_seq_contexts:
 
    82 lemma hrewrites_seq_contexts:
 
    83   shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4"
 
    83   shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4"
 
    84   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
    84   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
    85 
    85 
    86 
    86 
    87 
    87 
    88 lemma map_concat_cons:
 
    88 lemma map_concat_cons:
 
  1213   by (metis append_self_conv2 frewrite_rd_grewrites list.set(1))
 
  1213   by (metis append_self_conv2 frewrite_rd_grewrites list.set(1))
 
  1214 
  1214 
  1215 
  1215 
  1216 
  1216 
  1217 
  1217 
  1218 (*a more refined notion of \<leadsto>* is needed,
 
  1218 (*a more refined notion of h\<leadsto>* is needed,
 
  1219 this lemma fails when rs1 contains some RALTS rs where elements
 
  1219 this lemma fails when rs1 contains some RALTS rs where elements
 
  1220 of rs appear in later parts of rs1, which will be picked up by rs2
 
  1220 of rs appear in later parts of rs1, which will be picked up by rs2
 
  1221 and deduplicated*)
 
  1221 and deduplicated*)
 
  1222 lemma frewrites_simpeq:
 
  1222 lemma frewrites_simpeq:
 
  1223   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
 
  1223   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
 
  1544   using der_simp_nullability by presburger
 
  1544   using der_simp_nullability by presburger
 
  1545   
  1545   
  1546 
  1546 
  1547 
  1547 
  1548 lemma grewrite_ralts:
 
  1548 lemma grewrite_ralts:
 
  1549   shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
 
  1549   shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
 
  1550   by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
 
  1550   by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
 
  1551 
  1551 
  1552 lemma grewrites_ralts:
 
  1552 lemma grewrites_ralts:
 
  1553   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
 
  1553   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
 
  1554   apply(induct rule: grewrites.induct)
 
  1554   apply(induct rule: grewrites.induct)
 
  1555   apply simp
 
  1555   apply simp
 
  1556   using grewrite_ralts hreal_trans by blast
 
  1556   using grewrite_ralts hreal_trans by blast
 
  1557   
  1557   
  1558 
  1558 
  1559 lemma distinct_grewrites_subgoal1:
 
  1559 lemma distinct_grewrites_subgoal1:
 
  1560   shows "  
  1560   shows "  
  1561        \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3"
 
  1561        \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 h\<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 h\<leadsto>* rsimp_ALTs rs3"
 
  1562   apply(subgoal_tac "RALTS rs1 \<leadsto>* RALTS rs3")
 
  1562   apply(subgoal_tac "RALTS rs1 h\<leadsto>* RALTS rs3")
 
  1563   apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
  1563   apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
  1564   apply(subgoal_tac "rs1 \<leadsto>g* rs3")
 
  1564   apply(subgoal_tac "rs1 \<leadsto>g* rs3")
 
  1565   using grewrites_ralts apply blast
 
  1565   using grewrites_ralts apply blast
 
  1566   using grewrites.intros(2) by presburger
 
  1566   using grewrites.intros(2) by presburger
 
  1567 
  1567 
  1569 
  1569 
  1570 
  1570 
  1571 
  1571 
  1572 
  1572 
  1573 lemma grewrites_ralts_rsimpalts:
 
  1573 lemma grewrites_ralts_rsimpalts:
 
  1574   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* rsimp_ALTs rs' "
 
  1574   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* rsimp_ALTs rs' "
 
  1575   apply(induct rs rs' rule: grewrites.induct)
 
  1575   apply(induct rs rs' rule: grewrites.induct)
 
  1576    apply(case_tac rs)
 
  1576    apply(case_tac rs)
 
  1577   using hrewrite.intros(9) apply force
 
  1577   using hrewrite.intros(9) apply force
 
  1578    apply(case_tac list)
 
  1578    apply(case_tac list)
 
  1579   apply simp
 
  1579   apply simp
 
  1590    apply simp
 
  1590    apply simp
 
  1591   using grewrites_ralts hrewrite.intros(9) apply blast
 
  1591   using grewrites_ralts hrewrite.intros(9) apply blast
 
  1592   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))
 
  1592   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))
 
  1593 
  1593 
  1594 lemma hrewrites_alts:
 
  1594 lemma hrewrites_alts:
 
  1595   shows " r \<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto>* (RALTS  (rs1 @ [r'] @ rs2))"
 
  1595   shows " r h\<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto>* (RALTS  (rs1 @ [r'] @ rs2))"
 
  1596   apply(induct r r' rule: hrewrites.induct)
 
  1596   apply(induct r r' rule: hrewrites.induct)
 
  1597   apply simp
 
  1597   apply simp
 
  1598   using hrewrite.intros(6) by blast
 
  1598   using hrewrite.intros(6) by blast
 
  1599 
  1599 
  1600 inductive 
  1600 inductive 
  1601   srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)
 
  1601   srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)
 
  1602 where
 
  1602 where
 
  1603   ss1: "[] scf\<leadsto>* []"
 
  1603   ss1: "[] scf\<leadsto>* []"
 
  1604 | ss2: "\<lbrakk>r \<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
 
  1604 | ss2: "\<lbrakk>r h\<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
 
  1605 
  1605 
  1606 
  1606 
  1607 lemma hrewrites_alts_cons:
 
  1607 lemma hrewrites_alts_cons:
 
  1608   shows " RALTS rs \<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) \<leadsto>* RALTS (r # rs')"
 
  1608   shows " RALTS rs h\<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) h\<leadsto>* RALTS (r # rs')"
 
  1609 
  1609 
  1610 
  1610 
  1611   oops
 
  1611   oops
 
  1612 
  1612 
  1613 
  1613 
  1614 lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) \<leadsto>* (RALTS (rs@rs2))"
 
  1614 lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) h\<leadsto>* (RALTS (rs@rs2))"
 
  1615 
  1615 
  1616   apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)
 
  1616   apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)
 
  1617    apply(rule rs1)
 
  1617    apply(rule rs1)
 
  1618   apply(drule_tac x = "rsa@[r']" in meta_spec)
 
  1618   apply(drule_tac x = "rsa@[r']" in meta_spec)
 
  1619   apply simp
 
  1619   apply simp
 
  1624   by auto
 
  1624   by auto
 
  1625 
  1625 
  1626 
  1626 
  1627 corollary srewritescf_alt1: 
  1627 corollary srewritescf_alt1: 
  1628   assumes "rs1 scf\<leadsto>* rs2"
 
  1628   assumes "rs1 scf\<leadsto>* rs2"
 
  1629   shows "RALTS rs1 \<leadsto>* RALTS rs2"
 
  1629   shows "RALTS rs1 h\<leadsto>* RALTS rs2"
 
  1630   using assms
 
  1630   using assms
 
  1631   by (metis append_Nil srewritescf_alt)
 
  1631   by (metis append_Nil srewritescf_alt)
 
  1632 
  1632 
  1633 
  1633 
  1634 
  1634 
  1635 
  1635 
  1636 lemma trivialrsimp_srewrites: 
  1636 lemma trivialrsimp_srewrites: 
  1637   "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
 
  1637   "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x h\<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
 
  1638 
  1638 
  1639   apply(induction rs)
 
  1639   apply(induction rs)
 
  1640    apply simp
 
  1640    apply simp
 
  1641    apply(rule ss1)
 
  1641    apply(rule ss1)
 
  1642   by (metis insert_iff list.simps(15) list.simps(9) srewritescf.simps)
 
  1642   by (metis insert_iff list.simps(15) list.simps(9) srewritescf.simps)
 
  1643 
  1643 
  1644 lemma hrewrites_list: 
  1644 lemma hrewrites_list: 
  1645   shows
 
  1645   shows
 
  1646 " (\<And>xa. xa \<in> set x \<Longrightarrow> xa \<leadsto>* rsimp xa) \<Longrightarrow> RALTS x \<leadsto>* RALTS (map rsimp x)"
 
  1646 " (\<And>xa. xa \<in> set x \<Longrightarrow> xa h\<leadsto>* rsimp xa) \<Longrightarrow> RALTS x h\<leadsto>* RALTS (map rsimp x)"
 
  1647   apply(induct x)
 
  1647   apply(induct x)
 
  1648    apply(simp)+
 
  1648    apply(simp)+
 
  1649   by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)
 
  1649   by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)
 
  1650 (*  apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")*)
 
  1650 (*  apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")*)
 
  1651 
  1651 
  1652   
  1652   
  1653 lemma hrewrite_simpeq:
 
  1653 lemma hrewrite_simpeq:
 
  1654   shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
 
  1654   shows "r1 h\<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
 
  1655   apply(induct rule: hrewrite.induct)
 
  1655   apply(induct rule: hrewrite.induct)
 
  1656             apply simp+
 
  1656             apply simp+
 
  1657   apply (simp add: basic_rsimp_SEQ_property3)
 
  1657   apply (simp add: basic_rsimp_SEQ_property3)
 
  1658   apply (simp add: basic_rsimp_SEQ_property1)
 
  1658   apply (simp add: basic_rsimp_SEQ_property1)
 
  1659   using rsimp.simps(1) apply presburger
 
  1659   using rsimp.simps(1) apply presburger
 
  1666   apply simp+
 
  1666   apply simp+
 
  1667   apply (simp add: idem_after_simp1)
 
  1667   apply (simp add: idem_after_simp1)
 
  1668   using grewrite.intros(4) grewrite_equal_rsimp by presburger
 
  1668   using grewrite.intros(4) grewrite_equal_rsimp by presburger
 
  1669 
  1669 
  1670 lemma hrewrites_simpeq:
 
  1670 lemma hrewrites_simpeq:
 
  1671   shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
 
  1671   shows "r1 h\<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
 
  1672   apply(induct rule: hrewrites.induct)
 
  1672   apply(induct rule: hrewrites.induct)
 
  1673    apply simp
 
  1673    apply simp
 
  1674   apply(subgoal_tac "rsimp r2 = rsimp r3")
 
  1674   apply(subgoal_tac "rsimp r2 = rsimp r3")
 
  1675    apply auto[1]
 
  1675    apply auto[1]
 
  1676   using hrewrite_simpeq by presburger
 
  1676   using hrewrite_simpeq by presburger
 
  1677   
  1677   
  1678 
  1678 
  1679 
  1679 
  1680 lemma simp_hrewrites:
 
  1680 lemma simp_hrewrites:
 
  1681   shows "r1 \<leadsto>* rsimp r1"
 
  1681   shows "r1 h\<leadsto>* rsimp r1"
 
  1682   apply(induct r1)
 
  1682   apply(induct r1)
 
  1683        apply simp+
 
  1683        apply simp+
 
  1684     apply(case_tac "rsimp r11 = RONE")
 
  1684     apply(case_tac "rsimp r11 = RONE")
 
  1685      apply simp
 
  1685      apply simp
 
  1686      apply(subst basic_rsimp_SEQ_property1)
 
  1686      apply(subst basic_rsimp_SEQ_property1)
 
  1687   apply(subgoal_tac "RSEQ r11 r12 \<leadsto>* RSEQ RONE r12")
 
  1687   apply(subgoal_tac "RSEQ r11 r12 h\<leadsto>* RSEQ RONE r12")
 
  1688   using hreal_trans hrewrite.intros(3) apply blast
 
  1688   using hreal_trans hrewrite.intros(3) apply blast
 
  1689   using hrewrites_seq_context apply presburger
 
  1689   using hrewrites_seq_context apply presburger
 
  1690     apply(case_tac "rsimp r11 = RZERO")
 
  1690     apply(case_tac "rsimp r11 = RZERO")
 
  1691      apply simp
 
  1691      apply simp
 
  1692   using hrewrite.intros(1) hrewrites_seq_context apply blast
 
  1692   using hrewrite.intros(1) hrewrites_seq_context apply blast
 
  1696   apply (meson hrewrite.intros(2) hrewrites.simps hrewrites_seq_context2)
 
  1696   apply (meson hrewrite.intros(2) hrewrites.simps hrewrites_seq_context2)
 
  1697     apply(subst basic_rsimp_SEQ_property2)
 
  1697     apply(subst basic_rsimp_SEQ_property2)
 
  1698        apply simp+
 
  1698        apply simp+
 
  1699   using hrewrites_seq_contexts apply presburger
 
  1699   using hrewrites_seq_contexts apply presburger
 
  1700    apply simp
 
  1700    apply simp
 
  1701    apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")
 
  1701    apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")
 
  1702   apply(subgoal_tac "RALTS (map rsimp x) \<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")
 
  1702   apply(subgoal_tac "RALTS (map rsimp x) h\<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")
 
  1703   using hreal_trans apply blast
 
  1703   using hreal_trans apply blast
 
  1704     apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)
 
  1704     apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)
 
  1705 
  1705 
  1706    apply (simp add: grewrites_ralts hrewrites_list)
 
  1706    apply (simp add: grewrites_ralts hrewrites_list)
 
  1707   by simp
 
  1707   by simp
 
  1708 
  1708 
  1709 lemma interleave_aux1:
 
  1709 lemma interleave_aux1:
 
  1710   shows " RALT (RSEQ RZERO r1) r \<leadsto>*  r"
 
  1710   shows " RALT (RSEQ RZERO r1) r h\<leadsto>*  r"
 
  1711   apply(subgoal_tac "RSEQ RZERO r1 \<leadsto>* RZERO")
 
  1711   apply(subgoal_tac "RSEQ RZERO r1 h\<leadsto>* RZERO")
 
  1712   apply(subgoal_tac "RALT (RSEQ RZERO r1) r \<leadsto>* RALT RZERO r")
 
  1712   apply(subgoal_tac "RALT (RSEQ RZERO r1) r h\<leadsto>* RALT RZERO r")
 
  1713   apply (meson grewrite.intros(1) grewrite_ralts hreal_trans hrewrite.intros(10) hrewrites.simps)
 
  1713   apply (meson grewrite.intros(1) grewrite_ralts hreal_trans hrewrite.intros(10) hrewrites.simps)
 
  1714   using rs1 srewritescf_alt1 ss1 ss2 apply presburger
 
  1714   using rs1 srewritescf_alt1 ss1 ss2 apply presburger
 
  1715   by (simp add: hr_in_rstar hrewrite.intros(1))
 
  1715   by (simp add: hr_in_rstar hrewrite.intros(1))
 
  1716 
  1716 
  1717 
  1717 
  1718 
  1718 
  1719 lemma rnullable_hrewrite:
 
  1719 lemma rnullable_hrewrite:
 
  1720   shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
 
  1720   shows "r1 h\<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
 
  1721   apply(induct rule: hrewrite.induct)
 
  1721   apply(induct rule: hrewrite.induct)
 
  1722             apply simp+
 
  1722             apply simp+
 
  1723      apply blast
 
  1723      apply blast
 
  1724     apply simp+
 
  1724     apply simp+
 
  1725   done
 
  1725   done
 
  1726 
  1726 
  1727 
  1727 
  1728 lemma interleave1:
 
  1728 lemma interleave1:
 
  1729   shows "r \<leadsto> r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
 
  1729   shows "r h\<leadsto> r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
 
  1730   apply(induct r r' rule: hrewrite.induct)
 
  1730   apply(induct r r' rule: hrewrite.induct)
 
  1731             apply (simp add: hr_in_rstar hrewrite.intros(1))
 
  1731             apply (simp add: hr_in_rstar hrewrite.intros(1))
 
  1732   apply (metis (no_types, lifting) basic_rsimp_SEQ_property3 list.simps(8) list.simps(9) rder.simps(1) rder.simps(5) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) simp_hrewrites)
 
  1732   apply (metis (no_types, lifting) basic_rsimp_SEQ_property3 list.simps(8) list.simps(9) rder.simps(1) rder.simps(5) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) simp_hrewrites)
 
  1733           apply simp
 
  1733           apply simp
 
  1734           apply(subst interleave_aux1)
 
  1734           apply(subst interleave_aux1)
 
  1756    apply (simp add: hr_in_rstar hrewrite.intros(10))
 
  1756    apply (simp add: hr_in_rstar hrewrite.intros(10))
 
  1757   apply simp
 
  1757   apply simp
 
  1758   using hrewrite.intros(11) by auto
 
  1758   using hrewrite.intros(11) by auto
 
  1759 
  1759 
  1760 lemma interleave_star1:
 
  1760 lemma interleave_star1:
 
  1761   shows "r \<leadsto>* r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
 
  1761   shows "r h\<leadsto>* r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
 
  1762   apply(induct rule : hrewrites.induct)
 
  1762   apply(induct rule : hrewrites.induct)
 
  1763    apply simp
 
  1763    apply simp
 
  1764   by (meson hreal_trans interleave1)
 
  1764   by (meson hreal_trans interleave1)
 
  1765 
  1765 
  1766 
  1766 
  1773      apply simp
 
  1773      apply simp
 
  1774   
  1774   
  1775   using inside_simp_seq_nullable apply blast
 
  1775   using inside_simp_seq_nullable apply blast
 
  1776     apply simp
 
  1776     apply simp
 
  1777   apply (smt (verit, del_insts) basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem)
 
  1777   apply (smt (verit, del_insts) basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem)
 
  1778    apply(subgoal_tac "rder x (RALTS xa) \<leadsto>* rder x (rsimp (RALTS xa))")
 
  1778    apply(subgoal_tac "rder x (RALTS xa) h\<leadsto>* rder x (rsimp (RALTS xa))")
 
  1779   using hrewrites_simpeq apply presburger
 
  1779   using hrewrites_simpeq apply presburger
 
  1780   using interleave_star1 simp_hrewrites apply presburger
 
  1780   using interleave_star1 simp_hrewrites apply presburger
 
  1781   by simp
 
  1781   by simp
 
  1782   
  1782   
  1783 
  1783
lexing