diff -r 370dae790b30 -r 2b5b3f83e2b6 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Wed Apr 13 22:20:08 2022 +0100
+++ b/thys2/ClosedForms.thy	Fri Apr 15 19:35:29 2022 +0100
@@ -2,6 +2,81 @@
 "BasicIdentities"
 begin
 
+lemma flts_middle0:
+  shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
+  apply(induct rsa)
+  apply simp
+  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma simp_flatten3:
+  shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
+  apply(induct rsa)
+  
+  using simp_flatten apply force
+
+  sorry
+
+inductive 
+  hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<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))"
+(*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)"
+
+inductive 
+  hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<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"
+  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"
+  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"
+  by (meson hr_in_rstar hreal_trans)
+
+lemma hrewrites_seq_context:
+  shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<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"
+  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")
+  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"
+  by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
+
+
+
 lemma map_concat_cons:
   shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
   by simp
@@ -19,11 +94,6 @@
 
 
 
-lemma flts_middle0:
-  shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
-  apply(induct rsa)
-  apply simp
-  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
 lemma flts_middle01:
   shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)"
@@ -331,17 +401,6 @@
 
 
 
-lemma grewrite_equal_rsimp:
-  shows "\<lbrakk>rs1 \<leadsto>g rs2; rsimp_ALTs (rdistinct (rflts (map rsimp rs1)) (rset \<union> \<Union>(alt_set ` rset))) =
-          rsimp_ALTs (rdistinct (rflts (map rsimp rs2)) (rset \<union> \<Union>(alt_set ` rset)))\<rbrakk>
-       \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs1))  (rset \<union> \<Union>(alt_set ` rset))) =
-           rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs2))  (rset \<union> \<Union>(alt_set ` rset)))"
-  apply(induct rs1 rs2 arbitrary:rset rule: grewrite.induct)
-     apply simp
-  apply (metis append_Cons append_Nil flts_middle0)
-    apply(case_tac "rsimp r \<in> rset")
-     apply simp
-  oops
 
 lemma grewrite_cases_middle:
   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 
@@ -1188,13 +1247,6 @@
   apply (metis idiot idiot2 rrexp.distinct(5))
   by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
 
-lemma basic_rsimp_SEQ_property1:
-  shows "rsimp_SEQ RONE r = r"
-  by (simp add: idiot)
-
-lemma basic_rsimp_SEQ_property3:
-  shows "rsimp_SEQ r RZERO = RZERO"  
-  using rsimp_SEQ.elims by blast
 
 thm rsimp_SEQ.elims
 
@@ -1270,87 +1322,6 @@
   using der_simp_nullability by presburger
   
 
-inductive 
-  hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<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))"
-(*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)"
-
-inductive 
-  hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<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"
-  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"
-  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"
-  by (meson hr_in_rstar hreal_trans)
-
-lemma hrewrites_seq_context:
-  shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<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"
-  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")
-  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"
-  by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
-
-lemma hrewrite_simpeq:
-  shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
-  apply(induct rule: hrewrite.induct)
-            apply simp+
-  apply (simp add: basic_rsimp_SEQ_property3)
-  apply (simp add: basic_rsimp_SEQ_property1)
-  using rsimp.simps(1) apply presburger
-        apply simp+
-  using flts_middle0 apply force
-  using simp_flatten3 apply presburger
-  apply simp+
-  apply (simp add: idem_after_simp1)
-  using grewrite.intros(4) grewrite_equal_rsimp by presburger
-
-lemma hrewrites_simpeq:
-  shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
-  apply(induct rule: hrewrites.induct)
-   apply simp
-  apply(subgoal_tac "rsimp r2 = rsimp r3")
-   apply auto[1]
-  using hrewrite_simpeq by presburger
-  
 
 lemma grewrite_ralts:
   shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
@@ -1457,7 +1428,31 @@
 (*  apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")*)
 
   
-
+lemma hrewrite_simpeq:
+  shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+  apply(induct rule: hrewrite.induct)
+            apply simp+
+  apply (simp add: basic_rsimp_SEQ_property3)
+  apply (simp add: basic_rsimp_SEQ_property1)
+  using rsimp.simps(1) apply presburger
+        apply simp+
+  using flts_middle0 apply force
+
+  
+  using simp_flatten3 apply presburger
+
+  apply simp+
+  apply (simp add: idem_after_simp1)
+  using grewrite.intros(4) grewrite_equal_rsimp by presburger
+
+lemma hrewrites_simpeq:
+  shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+  apply(induct rule: hrewrites.induct)
+   apply simp
+  apply(subgoal_tac "rsimp r2 = rsimp r3")
+   apply auto[1]
+  using hrewrite_simpeq by presburger
+  
 
 
 lemma simp_hrewrites:
@@ -2275,4 +2270,5 @@
 
 
 
+
 end
\ No newline at end of file