diff -r 48ce16d61e03 -r 61eff2abb0b6 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Sat Apr 16 09:52:57 2022 +0100
+++ b/thys2/ClosedForms.thy	Tue Apr 19 09:08:01 2022 +0100
@@ -25,62 +25,62 @@
   
 
 inductive 
-  hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
+  hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
 where
-  "RSEQ  RZERO r2 \<leadsto> RZERO"
-| "RSEQ  r1 RZERO \<leadsto> RZERO"
-| "RSEQ  RONE r \<leadsto>  r"
-| "r1 \<leadsto> r2 \<Longrightarrow> RSEQ  r1 r3 \<leadsto> RSEQ r2 r3"
-| "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4"
-| "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS  (rs1 @ [r'] @ rs2))"
+  "RSEQ  RZERO r2 h\<leadsto> RZERO"
+| "RSEQ  r1 RZERO h\<leadsto> RZERO"
+| "RSEQ  RONE r h\<leadsto>  r"
+| "r1 h\<leadsto> r2 \<Longrightarrow> RSEQ  r1 r3 h\<leadsto> RSEQ r2 r3"
+| "r3 h\<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 h\<leadsto> RSEQ r1 r4"
+| "r h\<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto> (RALTS  (rs1 @ [r'] @ rs2))"
 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
-| "RALTS  (rsa @ [RZERO] @ rsb) \<leadsto> RALTS  (rsa @ rsb)"
-| "RALTS  (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)"
-| "RALTS  [] \<leadsto> RZERO"
-| "RALTS  [r] \<leadsto> r"
-| "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
+| "RALTS  (rsa @ [RZERO] @ rsb) h\<leadsto> RALTS  (rsa @ rsb)"
+| "RALTS  (rsa @ [RALTS rs1] @ rsb) h\<leadsto> RALTS (rsa @ rs1 @ rsb)"
+| "RALTS  [] h\<leadsto> RZERO"
+| "RALTS  [r] h\<leadsto> r"
+| "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) h\<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
 
 inductive 
-  hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
+  hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto>* _" [100, 100] 100)
 where 
-  rs1[intro, simp]:"r \<leadsto>* r"
-| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
-
-
-lemma hr_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
+  rs1[intro, simp]:"r h\<leadsto>* r"
+| rs2[intro]: "\<lbrakk>r1 h\<leadsto>* r2; r2 h\<leadsto> r3\<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"
+
+
+lemma hr_in_rstar : "r1 h\<leadsto> r2 \<Longrightarrow> r1 h\<leadsto>* r2"
   using hrewrites.intros(1) hrewrites.intros(2) by blast
  
 lemma hreal_trans[trans]: 
-  assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
-  shows "r1 \<leadsto>* r3"
+  assumes a1: "r1 h\<leadsto>* r2"  and a2: "r2 h\<leadsto>* r3"
+  shows "r1 h\<leadsto>* r3"
   using a2 a1
   apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct) 
   apply(auto)
   done
 
-lemma  hmany_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
+lemma  hmany_steps_later: "\<lbrakk>r1 h\<leadsto> r2; r2 h\<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"
   by (meson hr_in_rstar hreal_trans)
 
 lemma hrewrites_seq_context:
-  shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r3"
+  shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r3"
   apply(induct r1 r2 rule: hrewrites.induct)
    apply simp
   using hrewrite.intros(4) by blast
 
 lemma hrewrites_seq_context2:
-  shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 \<leadsto>* RSEQ r0 r2"
+  shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 h\<leadsto>* RSEQ r0 r2"
   apply(induct r1 r2 rule: hrewrites.induct)
    apply simp
   using hrewrite.intros(5) by blast
 
 lemma hrewrites_seq_context0:
-  shows "r1 \<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RZERO"
-  apply(subgoal_tac "RSEQ r1 r3 \<leadsto>* RSEQ RZERO r3")
+  shows "r1 h\<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RZERO"
+  apply(subgoal_tac "RSEQ r1 r3 h\<leadsto>* RSEQ RZERO r3")
   using hrewrite.intros(1) apply blast
   by (simp add: hrewrites_seq_context)
 
 lemma hrewrites_seq_contexts:
-  shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4"
+  shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4"
   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
 
@@ -1215,7 +1215,7 @@
 
 
 
-(*a more refined notion of \<leadsto>* is needed,
+(*a more refined notion of h\<leadsto>* is needed,
 this lemma fails when rs1 contains some RALTS rs where elements
 of rs appear in later parts of rs1, which will be picked up by rs2
 and deduplicated*)
@@ -1546,11 +1546,11 @@
 
 
 lemma grewrite_ralts:
-  shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
+  shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
   by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
 
 lemma grewrites_ralts:
-  shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
+  shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
   apply(induct rule: grewrites.induct)
   apply simp
   using grewrite_ralts hreal_trans by blast
@@ -1558,8 +1558,8 @@
 
 lemma distinct_grewrites_subgoal1:
   shows "  
-       \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3"
-  apply(subgoal_tac "RALTS rs1 \<leadsto>* RALTS rs3")
+       \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 h\<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 h\<leadsto>* rsimp_ALTs rs3"
+  apply(subgoal_tac "RALTS rs1 h\<leadsto>* RALTS rs3")
   apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
   apply(subgoal_tac "rs1 \<leadsto>g* rs3")
   using grewrites_ralts apply blast
@@ -1571,7 +1571,7 @@
 
 
 lemma grewrites_ralts_rsimpalts:
-  shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* rsimp_ALTs rs' "
+  shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* rsimp_ALTs rs' "
   apply(induct rs rs' rule: grewrites.induct)
    apply(case_tac rs)
   using hrewrite.intros(9) apply force
@@ -1592,7 +1592,7 @@
   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))
 
 lemma hrewrites_alts:
-  shows " r \<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto>* (RALTS  (rs1 @ [r'] @ rs2))"
+  shows " r h\<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto>* (RALTS  (rs1 @ [r'] @ rs2))"
   apply(induct r r' rule: hrewrites.induct)
   apply simp
   using hrewrite.intros(6) by blast
@@ -1601,17 +1601,17 @@
   srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)
 where
   ss1: "[] scf\<leadsto>* []"
-| ss2: "\<lbrakk>r \<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
+| ss2: "\<lbrakk>r h\<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
 
 
 lemma hrewrites_alts_cons:
-  shows " RALTS rs \<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) \<leadsto>* RALTS (r # rs')"
+  shows " RALTS rs h\<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) h\<leadsto>* RALTS (r # rs')"
 
 
   oops
 
 
-lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) \<leadsto>* (RALTS (rs@rs2))"
+lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) h\<leadsto>* (RALTS (rs@rs2))"
 
   apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)
    apply(rule rs1)
@@ -1626,7 +1626,7 @@
 
 corollary srewritescf_alt1: 
   assumes "rs1 scf\<leadsto>* rs2"
-  shows "RALTS rs1 \<leadsto>* RALTS rs2"
+  shows "RALTS rs1 h\<leadsto>* RALTS rs2"
   using assms
   by (metis append_Nil srewritescf_alt)
 
@@ -1634,7 +1634,7 @@
 
 
 lemma trivialrsimp_srewrites: 
-  "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
+  "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x h\<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
 
   apply(induction rs)
    apply simp
@@ -1643,15 +1643,15 @@
 
 lemma hrewrites_list: 
   shows
-" (\<And>xa. xa \<in> set x \<Longrightarrow> xa \<leadsto>* rsimp xa) \<Longrightarrow> RALTS x \<leadsto>* RALTS (map rsimp x)"
+" (\<And>xa. xa \<in> set x \<Longrightarrow> xa h\<leadsto>* rsimp xa) \<Longrightarrow> RALTS x h\<leadsto>* RALTS (map rsimp x)"
   apply(induct x)
    apply(simp)+
   by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)
-(*  apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")*)
+(*  apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")*)
 
   
 lemma hrewrite_simpeq:
-  shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+  shows "r1 h\<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
   apply(induct rule: hrewrite.induct)
             apply simp+
   apply (simp add: basic_rsimp_SEQ_property3)
@@ -1668,7 +1668,7 @@
   using grewrite.intros(4) grewrite_equal_rsimp by presburger
 
 lemma hrewrites_simpeq:
-  shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+  shows "r1 h\<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
   apply(induct rule: hrewrites.induct)
    apply simp
   apply(subgoal_tac "rsimp r2 = rsimp r3")
@@ -1678,13 +1678,13 @@
 
 
 lemma simp_hrewrites:
-  shows "r1 \<leadsto>* rsimp r1"
+  shows "r1 h\<leadsto>* rsimp r1"
   apply(induct r1)
        apply simp+
     apply(case_tac "rsimp r11 = RONE")
      apply simp
      apply(subst basic_rsimp_SEQ_property1)
-  apply(subgoal_tac "RSEQ r11 r12 \<leadsto>* RSEQ RONE r12")
+  apply(subgoal_tac "RSEQ r11 r12 h\<leadsto>* RSEQ RONE r12")
   using hreal_trans hrewrite.intros(3) apply blast
   using hrewrites_seq_context apply presburger
     apply(case_tac "rsimp r11 = RZERO")
@@ -1698,8 +1698,8 @@
        apply simp+
   using hrewrites_seq_contexts apply presburger
    apply simp
-   apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")
-  apply(subgoal_tac "RALTS (map rsimp x) \<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")
+   apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")
+  apply(subgoal_tac "RALTS (map rsimp x) h\<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")
   using hreal_trans apply blast
     apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)
 
@@ -1707,9 +1707,9 @@
   by simp
 
 lemma interleave_aux1:
-  shows " RALT (RSEQ RZERO r1) r \<leadsto>*  r"
-  apply(subgoal_tac "RSEQ RZERO r1 \<leadsto>* RZERO")
-  apply(subgoal_tac "RALT (RSEQ RZERO r1) r \<leadsto>* RALT RZERO r")
+  shows " RALT (RSEQ RZERO r1) r h\<leadsto>*  r"
+  apply(subgoal_tac "RSEQ RZERO r1 h\<leadsto>* RZERO")
+  apply(subgoal_tac "RALT (RSEQ RZERO r1) r h\<leadsto>* RALT RZERO r")
   apply (meson grewrite.intros(1) grewrite_ralts hreal_trans hrewrite.intros(10) hrewrites.simps)
   using rs1 srewritescf_alt1 ss1 ss2 apply presburger
   by (simp add: hr_in_rstar hrewrite.intros(1))
@@ -1717,7 +1717,7 @@
 
 
 lemma rnullable_hrewrite:
-  shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
+  shows "r1 h\<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
   apply(induct rule: hrewrite.induct)
             apply simp+
      apply blast
@@ -1726,7 +1726,7 @@
 
 
 lemma interleave1:
-  shows "r \<leadsto> r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
+  shows "r h\<leadsto> r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
   apply(induct r r' rule: hrewrite.induct)
             apply (simp add: hr_in_rstar hrewrite.intros(1))
   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)
@@ -1758,7 +1758,7 @@
   using hrewrite.intros(11) by auto
 
 lemma interleave_star1:
-  shows "r \<leadsto>* r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
+  shows "r h\<leadsto>* r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
   apply(induct rule : hrewrites.induct)
    apply simp
   by (meson hreal_trans interleave1)
@@ -1775,7 +1775,7 @@
   using inside_simp_seq_nullable apply blast
     apply simp
   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)
-   apply(subgoal_tac "rder x (RALTS xa) \<leadsto>* rder x (rsimp (RALTS xa))")
+   apply(subgoal_tac "rder x (RALTS xa) h\<leadsto>* rder x (rsimp (RALTS xa))")
   using hrewrites_simpeq apply presburger
   using interleave_star1 simp_hrewrites apply presburger
   by simp