# HG changeset patch
# User Chengsong
# Date 1650047729 -3600
# Node ID 2b5b3f83e2b60e3767d6becfa2a91c5ac3fa9fdd
# Parent  370dae790b3032fbc0913ca2e5abd7070f76e581
1sorry left

diff -r 370dae790b30 -r 2b5b3f83e2b6 thys2/BasicIdentities.thy
--- a/thys2/BasicIdentities.thy	Wed Apr 13 22:20:08 2022 +0100
+++ b/thys2/BasicIdentities.thy	Fri Apr 15 19:35:29 2022 +0100
@@ -341,13 +341,8 @@
        apply simp_all
   done
 
-lemma no_alt_short_list_after_simp:
-  shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
-  sorry
 
-lemma no_further_dB_after_simp:
-  shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"
-  sorry
+
 
 
 lemma idiot2:
@@ -403,35 +398,454 @@
   apply auto
   done
 
-lemma rsimp_idem:
-  shows "rsimp (rsimp r) = rsimp r"
-  sorry
+
+
+fun nonalt :: "rrexp \<Rightarrow> bool"
+  where
+  "nonalt (RALTS  rs) = False"
+| "nonalt r = True"
+
+
+fun good :: "rrexp \<Rightarrow> bool" where
+  "good RZERO = False"
+| "good (RONE) = True" 
+| "good (RCHAR c) = True"
+| "good (RALTS []) = False"
+| "good (RALTS [r]) = False"
+| "good (RALTS (r1 # r2 # rs)) = ((distinct ( (r1 # r2 # rs))) \<and>(\<forall>r' \<in> set (r1 # r2 # rs). good r' \<and> nonalt r'))"
+| "good (RSEQ RZERO _) = False"
+| "good (RSEQ RONE _) = False"
+| "good (RSEQ  _ RZERO) = False"
+| "good (RSEQ r1 r2) = (good r1 \<and> good r2)"
+| "good (RSTAR r) = True"
+
+
+lemma  k0a:
+  shows "rflts [RALTS rs] =   rs"
+  apply(simp)
+  done
+
+lemma bbbbs:
+  assumes "good r" "r = RALTS rs"
+  shows "rsimp_ALTs  (rflts [r]) = RALTS rs"
+  using  assms
+  by (metis good.simps(4) good.simps(5) k0a rsimp_ALTs.elims)
+
+lemma bbbbs1:
+  shows "nonalt r \<or> (\<exists> rs. r  = RALTS  rs)"
+  by (meson nonalt.elims(3))
+
+
+
+lemma good0:
+  assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r" "distinct rs"
+  shows "good (rsimp_ALTs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
+  using  assms
+  apply(induct  rs rule: rsimp_ALTs.induct)
+  apply(auto)
+  done
 
-corollary rsimp_inner_idem1:
-  shows "rsimp r = RSEQ r1 r2 \<Longrightarrow> rsimp r1 = r1 \<and> rsimp r2 = r2"
+lemma good0a:
+  assumes "rflts (map rsimp rs) \<noteq> Nil" "\<forall>r \<in> set (rflts (map rsimp rs)). nonalt r"
+  shows "good (rsimp (RALTS rs)) \<longleftrightarrow> (\<forall>r \<in> set (rflts (map rsimp rs)). good r)"
+  using  assms
+  apply(simp)
+  apply(auto)
+   apply(subst (asm) good0)
   
-  sorry
+  apply (metis rdistinct_set_equality set_empty)
+   apply(simp)
+    apply(auto)
+     apply (metis rdistinct_set_equality)
+  using rdistinct_does_the_job apply blast
+  apply (metis rdistinct_set_equality)
+  by (metis good0 rdistinct_does_the_job rdistinct_set_equality set_empty)
+
+
+lemma flts0:
+  assumes "r \<noteq> RZERO" "nonalt r"
+  shows "rflts [r] \<noteq> []"
+  using  assms
+  apply(induct r)
+       apply(simp_all)
+  done
+
+lemma flts1:
+  assumes "good r" 
+  shows "rflts [r] \<noteq> []"
+  using  assms
+  apply(induct r)
+       apply(simp_all)
+  using good.simps(4) by blast
+
+lemma flts2:
+  assumes "good r" 
+  shows "\<forall>r' \<in> set (rflts [r]). good r' \<and> nonalt r'"
+  using  assms
+  apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 2
+    apply(simp)
+    apply(auto)[1]
+  
+     apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
+    apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
+   apply fastforce
+  apply(simp)
+  done  
+
 
-corollary rsimp_inner_idem2:
-  shows "rsimp r = RALTS rs \<Longrightarrow> \<forall>r' \<in> (set rs). rsimp r' = r'"
-  sorry
+
+lemma flts3:
+  assumes "\<forall>r \<in> set rs. good r \<or> r = RZERO" 
+  shows "\<forall>r \<in> set (rflts rs). good r"
+  using  assms
+  apply(induct rs arbitrary: rule: rflts.induct)
+        apply(simp_all)
+  by (metis UnE flts2 k0a)
+
+lemma flts3b:
+  assumes "\<exists>r\<in>set rs. good r"
+  shows "rflts rs \<noteq> []"
+  using  assms
+  apply(induct rs arbitrary: rule: rflts.induct)
+        apply(simp)
+       apply(simp)
+      apply(simp)
+      apply(auto)
+  done
+
+lemma flts4:
+  assumes "rsimp_ALTs (rflts rs) = RZERO"
+  shows "\<forall>r \<in> set rs. \<not> good r"
+  using assms
+  apply(induct rs  rule: rflts.induct)
+        apply(auto)
+        defer
+  apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 rsimp_ALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))
+  using rsimp_ALTs.elims apply auto[1]
+  using rsimp_ALTs.elims apply auto[1]
+  using rsimp_ALTs.elims apply auto[1]
+  using rsimp_ALTs.elims apply auto[1]
+  using rsimp_ALTs.elims apply auto[1]
+  by (smt (verit, del_insts) append_Cons append_is_Nil_conv bbbbs k0a list.inject rrexp.distinct(7) rsimp_ALTs.elims)
+
+
+lemma  k0:
+  shows "rflts (r # rs1) = rflts [r] @ rflts rs1"
+  apply(induct r arbitrary: rs1)
+   apply(auto)
+  done
 
-corollary rsimp_inner_idem3:
-  shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs"
-  by (meson map_idI rsimp_inner_idem2)
+lemma flts_nil2:
+  assumes "\<forall>y. rsize y < Suc (sum_list (map rsize rs)) \<longrightarrow>
+            good (rsimp y) \<or> rsimp y = RZERO"
+  and "rsimp_ALTs  (rflts (map rsimp rs)) = RZERO"
+  shows "rflts (map rsimp rs) = []"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(simp)
+  apply(subst (asm) k0)
+  apply(auto)
+  apply (metis rflts.simps(1) rflts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+  by (metis flts4 k0 less_add_Suc1 list.set_intros(1) rflts.simps(2))
+
 
-corollary rsimp_inner_idem4:
-  shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs"
-  sorry
+lemma good_SEQ:
+  assumes "r1 \<noteq> RZERO" "r2 \<noteq> RZERO" " r1 \<noteq> RONE"
+  shows "good (RSEQ r1 r2) = (good r1 \<and> good r2)"
+  using assms
+  apply(case_tac r1)
+       apply(simp_all)
+  apply(case_tac r2)
+          apply(simp_all)
+  apply(case_tac r2)
+         apply(simp_all)
+  apply(case_tac r2)
+        apply(simp_all)
+  apply(case_tac r2)
+       apply(simp_all)
+  done
+
+lemma rsize0:
+  shows "0 < rsize r"
+  apply(induct  r)
+       apply(auto)
+  done
+
+
+fun nonnested :: "rrexp \<Rightarrow> bool"
+  where
+  "nonnested (RALTS []) = True"
+| "nonnested (RALTS ((RALTS rs1) # rs2)) = False"
+| "nonnested (RALTS (r # rs2)) = nonnested (RALTS rs2)"
+| "nonnested r = True"
+
+
+
+lemma  k00:
+  shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
+  apply(induct rs1 arbitrary: rs2)
+   apply(auto)
+  by (metis append.assoc k0)
+
+
 
 
-lemma head_one_more_simp:
-  shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"
-  by (simp add: rsimp_idem)
+lemma k0b:
+  assumes "nonalt r" "r \<noteq> RZERO"
+  shows "rflts [r] = [r]"
+  using assms
+  apply(case_tac  r)
+  apply(simp_all)
+  done
+
+lemma nn1:
+  assumes "nonnested (RALTS rs)"
+  shows "\<nexists> rs1. rflts rs = [RALTS rs1]"
+  using assms
+  apply(induct rs rule: rflts.induct)
+  apply(auto)
+  done
+
+lemma nn1q:
+  assumes "nonnested (RALTS rs)"
+  shows "\<nexists>rs1. RALTS rs1 \<in> set (rflts rs)"
+  using assms
+  apply(induct rs rule: rflts.induct)
+  apply(auto)
+  done
+
+lemma nn1qq:
+  assumes "nonnested (RALTS rs)"
+  shows "\<nexists> rs1. RALTS rs1 \<in> set rs"
+  using assms
+  apply(induct rs rule: rflts.induct)
+  apply(auto)
+  done
+
+ 
+
+lemma n0:
+  shows "nonnested (RALTS rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
+  apply(induct rs )
+   apply(auto)
+    apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
+  apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))
+  using bbbbs1 apply fastforce
+  by (metis bbbbs1 list.set_intros(2) nn1qq)
+
+  
+  
+
+lemma nn1c:
+  assumes "\<forall>r \<in> set rs. nonnested r"
+  shows "\<forall>r \<in> set (rflts rs). nonalt r"
+  using assms
+  apply(induct rs rule: rflts.induct)
+        apply(auto)
+  using n0 by blast
+
+lemma nn1bb:
+  assumes "\<forall>r \<in> set rs. nonalt r"
+  shows "nonnested (rsimp_ALTs  rs)"
+  using assms
+  apply(induct  rs rule: rsimp_ALTs.induct)
+    apply(auto)
+  using nonalt.simps(1) nonnested.elims(3) apply blast
+  using n0 by auto
+
+lemma bsimp_ASEQ0:
+  shows "rsimp_SEQ  r1 RZERO = RZERO"
+  apply(induct r1)
+  apply(auto)
+  done
+
+lemma nn1b:
+  shows "nonnested (rsimp r)"
+  apply(induct r)
+       apply(simp_all)
+  apply(case_tac "rsimp r1 = RZERO")
+    apply(simp)
+ apply(case_tac "rsimp r2 = RZERO")
+   apply(simp)
+    apply(subst bsimp_ASEQ0)
+  apply(simp)
+  apply(case_tac "\<exists>bs. rsimp r1 = RONE")
+    apply(auto)[1]
+  using idiot apply fastforce
+  using idiot2 nonnested.simps(11) apply presburger
+  by (metis (mono_tags, lifting) image_iff list.set_map nn1bb nn1c rdistinct_set_equality)
+
+  
+lemma nn1d:
+  assumes "rsimp r = RALTS rs"
+  shows "\<forall>r1 \<in> set rs. \<forall>  bs. r1 \<noteq> RALTS  rs2"
+  using nn1b assms
+  by (metis nn1qq)
+
+lemma nn_flts:
+  assumes "nonnested (RALTS rs)"
+  shows "\<forall>r \<in>  set (rflts rs). nonalt r"
+  using assms
+  apply(induct rs rule: rflts.induct)
+        apply(auto)
+  done
+
+lemma nonalt_flts_rd:
+  shows "\<lbrakk>xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk>
+       \<Longrightarrow> nonalt xa"
+  by (metis ex_map_conv nn1b nn1c rdistinct_set_equality)
+
+lemma distinct_accLarge_empty:
+  shows "rset \<subseteq> rset' \<Longrightarrow> rdistinct rs rset = [] \<Longrightarrow> rdistinct rs rset' = []"
+  apply(induct rs arbitrary: rset rset')
+   apply simp+
+  by (metis list.distinct(1) subsetD)
+
+lemma rsimpalts_implies1:
+  shows " rsimp_ALTs (a # rdistinct rs {a}) = RZERO \<Longrightarrow> a = RZERO"
+  using rsimp_ALTs.elims by auto
+
+
+lemma rsimpalts_implies2:
+  shows "rsimp_ALTs (a # rdistinct rs rset) = RZERO \<Longrightarrow> rdistinct rs rset = []"
+  by (metis append_butlast_last_id rrexp.distinct(7) rsimpalts_conscons)
+
+lemma rsimpalts_implies21:
+  shows "rsimp_ALTs (a # rdistinct rs {a}) = RZERO \<Longrightarrow> rdistinct rs {a} = []"
+  using rsimpalts_implies2 by blast
+
 
-lemma head_one_more_dersimp:
-  shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)"
-  using head_one_more_simp rders_simp_append rders_simp_one_char by presburger
+lemma hollow_removemore_hollow:
+  shows "rsimp_ALTs (rdistinct rs {}) = RZERO \<Longrightarrow> 
+rsimp_ALTs (rdistinct rs rset) = RZERO "
+  apply(induct rs arbitrary: rset)
+   apply simp
+  apply simp
+  apply(case_tac " a \<in> rset")
+   apply simp
+   apply(drule_tac x = "rset" in meta_spec)
+  apply (smt (verit, best) Un_insert_left empty_iff rdistinct.elims rdistinct.simps(2) rrexp.distinct(7) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) singletonD sup_bot_left)
+  apply simp
+  apply(subgoal_tac "a = RZERO")
+  apply(subgoal_tac "rdistinct rs (insert a rset) = []")
+  using rsimp_ALTs.simps(2) apply presburger
+   apply(subgoal_tac "rdistinct rs {a} = []")
+  apply(subgoal_tac "{a} \<subseteq> insert a rset")
+  apply (meson distinct_accLarge_empty)
+    apply blast
+  using rsimpalts_implies21 apply blast
+  using rsimpalts_implies1 by blast
+
+lemma bsimp_ASEQ2:
+  shows "rsimp_SEQ RONE r2 =  r2"
+  apply(induct r2)
+  apply(auto)
+  done
+
+lemma elem_smaller_than_set:
+  shows "xa \<in> set  list \<Longrightarrow> rsize xa < Suc ( sum_list (map rsize list))"
+  apply(induct list)
+   apply simp
+  by (metis image_eqI le_imp_less_Suc list.set_map member_le_sum_list)
+
+
+lemma smaller_corresponding:
+  shows "xa \<in> set (map rsimp list) \<Longrightarrow> \<exists>xa' \<in> set list. rsize xa \<le> rsize xa'"
+  apply(induct list)
+   apply simp
+  by (metis list.set_intros(1) list.set_intros(2) list.simps(9) rsimp_mono set_ConsD)
+
+lemma simpelem_smaller_than_set:
+  shows "xa \<in> set (map rsimp list) \<Longrightarrow> rsize xa < Suc ( sum_list (map rsize ( list)))"
+  apply(subgoal_tac "\<exists>xa' \<in> set list. rsize xa \<le> rsize xa'")
+   
+  using elem_smaller_than_set order_le_less_trans apply blast
+  using smaller_corresponding by presburger
+
+
+lemma rsimp_list_mono:
+  shows "sum_list (map rsize (map rsimp rs)) \<le> sum_list (map rsize rs)"
+  apply(induct rs)
+   apply simp+
+  by (simp add: add_mono_thms_linordered_semiring(1) rsimp_mono)
+
+lemma good1_obvious_but_isabelle_needs_clarification:
+  shows "       \<lbrakk>\<forall>y. rsize y < Suc (rsize a + sum_list (map rsize list)) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;
+        rsimp_ALTs (rdistinct (rflts (map rsimp list)) {}) = RZERO; good (rsimp a);
+        xa \<in> set (rdistinct (rflts (rsimp a # map rsimp list)) {})\<rbrakk>
+       \<Longrightarrow> rsize xa < Suc (rsize a + sum_list (map rsize list))"
+  apply(subgoal_tac "rsize xa \<le> 
+          sum_list (map rsize (rdistinct (rflts (rsimp a # map rsimp list)) {}))")
+  apply(subgoal_tac "  sum_list (map rsize (rdistinct (rflts (rsimp a # map rsimp list)) {})) \<le>
+                       sum_list (map rsize ( (rflts (rsimp a # map rsimp list))))")
+  apply(subgoal_tac " sum_list (map rsize ( (rflts (rsimp a # map rsimp list)))) \<le>
+                      sum_list (map rsize  (rsimp a # map rsimp list))")
+  apply(subgoal_tac " sum_list (map rsize (rsimp a # map rsimp list)) \<le>
+                      sum_list (map rsize (a # list))")
+  apply simp
+  apply (metis Cons_eq_map_conv rsimp_list_mono)
+  using rflts_mono apply blast
+  using rdistinct_phi_smaller apply blast
+  using elem_smaller_than_set less_Suc_eq_le by blast
+
+(*says anything coming out of simp+flts+db will be good*)
+lemma good2_obv_simplified:
+  shows " \<lbrakk>\<forall>y. rsize y < Suc (sum_list (map rsize rs)) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;
+           xa \<in> set (rdistinct (rflts (map rsimp rs)) {}); good (rsimp xa) \<or> rsimp xa = RZERO\<rbrakk> \<Longrightarrow> good xa"
+  apply(subgoal_tac " \<forall>xa' \<in> set (map rsimp rs). good xa' \<or> xa' = RZERO")
+  prefer 2
+  apply (simp add: elem_smaller_than_set)
+  by (metis flts3 rdistinct_set_equality)
+
+  
+
+
+lemma good2_obvious_but_isabelle_needs_clarification:
+  shows "\<And>a list xa.
+       \<lbrakk>\<forall>y. rsize y < Suc (rsize a + sum_list (map rsize list)) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;
+        rsimp_ALTs (rdistinct (rflts (map rsimp list)) {}) = RZERO; good (rsimp a);
+        xa \<in> set (rdistinct (rflts (rsimp a # map rsimp list)) {}); good (rsimp xa) \<or> rsimp xa = RZERO\<rbrakk>
+       \<Longrightarrow> good xa"
+  by (metis good2_obv_simplified list.simps(9) sum_list.Cons)
+
+  
+
+lemma good1:
+  shows "good (rsimp a) \<or> rsimp a = RZERO"
+  apply(induct a taking: rsize rule: measure_induct)
+  apply(case_tac x)
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  prefer 3
+    apply(simp)
+   prefer 2
+   apply(simp only:)
+   apply simp
+  apply (smt (verit, ccfv_threshold) add_mono_thms_linordered_semiring(1) elem_smaller_than_set good0 good2_obv_simplified le_eq_less_or_eq nonalt_flts_rd order_less_trans plus_1_eq_Suc rdistinct_does_the_job rdistinct_phi_smaller rflts_mono rsimp_ALTs.simps(1) rsimp_list_mono)
+  apply simp
+  apply(subgoal_tac "good (rsimp x41) \<or> rsimp x41 = RZERO")
+   apply(subgoal_tac "good (rsimp x42) \<or> rsimp x42 = RZERO")
+    apply(case_tac "rsimp x41 = RZERO")
+     apply simp
+    apply(case_tac "rsimp x42 = RZERO")
+     apply simp
+  using bsimp_ASEQ0 apply blast
+    apply(subgoal_tac "good (rsimp x41)")
+     apply(subgoal_tac "good (rsimp x42)")
+      apply simp
+  apply (metis bsimp_ASEQ2 good_SEQ idiot2)
+  apply blast
+  apply fastforce
+  using less_add_Suc2 apply blast  
+  using less_iff_Suc_add by blast
 
 
 
@@ -507,6 +921,229 @@
   using RL_rder by force
   
 
+lemma good1a:
+  assumes "RL a \<noteq> {}"
+  shows "good (rsimp a)"
+  using good1 assms
+  by (metis RL.simps(1) RL_rsimp)
+
+
+
+lemma g1:
+  assumes "good (rsimp_ALTs  rs)"
+  shows "rsimp_ALTs  rs = RALTS rs \<or> (\<exists>r. rs = [r] \<and> rsimp_ALTs  [r] =  r)"
+using assms
+    apply(induct rs)
+  apply(simp)
+  apply(case_tac rs)
+  apply(simp only:)
+  apply(simp)
+  apply(case_tac  list)
+  apply(simp)
+  by simp
+
+lemma flts_0:
+  assumes "nonnested (RALTS   rs)"
+  shows "\<forall>r \<in> set (rflts rs). r \<noteq> RZERO"
+  using assms
+  apply(induct rs  rule: rflts.induct)
+        apply(simp) 
+       apply(simp) 
+      defer
+      apply(simp) 
+     apply(simp) 
+    apply(simp) 
+apply(simp) 
+  apply(rule ballI)
+  apply(simp)
+  done
+
+lemma flts_0a:
+  assumes "nonnested (RALTS   rs)"
+  shows "RZERO \<notin> set (rflts rs)"
+  using assms
+  using flts_0 by blast 
+  
+lemma qqq1:
+  shows "RZERO \<notin> set (rflts (map rsimp rs))"
+  by (metis ex_map_conv flts3 good.simps(1) good1)
+
+
+fun nonazero :: "rrexp \<Rightarrow> bool"
+  where
+  "nonazero RZERO = False"
+| "nonazero r = True"
+
+lemma flts_concat:
+  shows "rflts rs = concat (map (\<lambda>r. rflts [r]) rs)"
+  apply(induct rs)
+   apply(auto)
+  apply(subst k0)
+  apply(simp)
+  done
+
+lemma flts_single1:
+  assumes "nonalt r" "nonazero r"
+  shows "rflts [r] = [r]"
+  using assms
+  apply(induct r)
+  apply(auto)
+  done
+
+lemma flts_qq:
+  assumes "\<forall>y. rsize y < Suc (sum_list (map rsize rs)) \<longrightarrow> good y \<longrightarrow> rsimp y = y" 
+          "\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
+  shows "rflts (map rsimp rs) = rs"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(subgoal_tac "rflts [rsimp a] =  [a]")
+   prefer 2
+   apply(drule_tac x="a" in spec)
+   apply(drule mp)
+    apply(simp)
+   apply(auto)[1]
+  using good.simps(1) k0b apply blast
+  apply(auto)[1]  
+  done
+
+lemma sublist_distinct:
+  shows "distinct (rs1 @ rs2 ) \<Longrightarrow> distinct rs1 \<and> distinct rs2"
+  using distinct_append by blast
+
+lemma first2elem_distinct:
+  shows "distinct (a # b # rs) \<Longrightarrow> a \<noteq> b"
+  by force
+
+lemma rdistinct_does_not_remove:
+  shows "((\<forall>r \<in> rset. r \<notin> set rs) \<and> (distinct rs)) \<Longrightarrow> rdistinct rs rset = rs"
+  by (metis append.right_neutral distinct_rdistinct_append rdistinct.simps(1))
+
+lemma nonalt0_flts_keeps:
+  shows "(a \<noteq> RZERO) \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow> rflts (a # xs) = a # rflts xs"
+  apply(case_tac a)
+       apply simp+
+  done
+
+
+lemma nonalt0_fltseq:
+  shows "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r \<Longrightarrow> rflts rs = rs"
+  apply(induct rs)
+   apply simp
+  apply(case_tac "a = RZERO")
+   apply fastforce
+  apply(case_tac "\<exists>rs1. a = RALTS rs1")
+   apply(erule exE)
+   apply simp+
+  using nonalt0_flts_keeps by presburger
+
+  
+
+
+lemma goodalts_nonalt:
+  shows "good (RALTS rs) \<Longrightarrow> rflts rs = rs"
+  apply(induct x == "RALTS rs" arbitrary: rs rule: good.induct)
+    apply simp
+  
+  using good.simps(5) apply blast
+  apply simp
+  apply(case_tac "r1 = RZERO")
+  using good.simps(1) apply force
+  apply(case_tac "r2 = RZERO")
+  using good.simps(1) apply force
+  apply(subgoal_tac "rflts (r1 # r2 # rs) = r1 # r2 # rflts rs")
+  prefer 2
+   apply (metis nonalt.simps(1) rflts_def_idiot)
+  apply(subgoal_tac "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r")
+   apply(subgoal_tac "rflts rs = rs")
+    apply presburger
+  using nonalt0_fltseq apply presburger
+  using good.simps(1) by blast
+  
+
+  
+
+
+lemma test:
+  assumes "good r"
+  shows "rsimp r = r"
+
+  using assms
+  apply(induct rule: good.induct)
+                      apply simp
+                      apply simp
+                      apply simp
+                      apply simp
+                      apply simp
+                      apply(subgoal_tac "distinct (r1 # r2 # rs)")
+  prefer 2
+  using good.simps(6) apply blast
+  apply(subgoal_tac "rflts (r1 # r2 # rs ) = r1 # r2 # rs")
+  prefer 2
+  using goodalts_nonalt apply blast
+
+                      apply(subgoal_tac "r1 \<noteq> r2")
+  prefer 2
+                      apply (meson distinct_length_2_or_more)
+                      apply(subgoal_tac "r1 \<notin> set rs")
+                      apply(subgoal_tac "r2 \<notin> set rs")
+                      apply(subgoal_tac "\<forall>r \<in> set rs. rsimp r = r")
+                      apply(subgoal_tac "map rsimp rs = rs")
+  apply simp             
+                      apply(subgoal_tac "\<forall>r \<in>  {r1, r2}. r \<notin> set rs")
+  apply (metis distinct_not_exist rdistinct_on_distinct)
+  
+                      apply blast
+                      apply (meson map_idI)
+                      apply (metis good.simps(6) insert_iff list.simps(15))
+
+  apply (meson distinct.simps(2))
+                      apply (simp add: distinct.simps(2) distinct_length_2_or_more)
+                      apply simp+
+  done
+
+
+
+lemma rsimp_idem:
+  shows "rsimp (rsimp r) = rsimp r"
+  using test good1
+  by force
+
+
+
+
+
+corollary rsimp_inner_idem1:
+  shows "rsimp r = RSEQ r1 r2 \<Longrightarrow> rsimp r1 = r1 \<and> rsimp r2 = r2"
+  by (metis bsimp_ASEQ0 good.simps(7) good.simps(8) good1 good_SEQ rrexp.distinct(5) rsimp.simps(1) rsimp.simps(3) test)
+  
+
+corollary rsimp_inner_idem2:
+  shows "rsimp r = RALTS rs \<Longrightarrow> \<forall>r' \<in> (set rs). rsimp r' = r'"
+  by (metis flts2 good1 k0a rrexp.simps(12) test)
+  
+
+corollary rsimp_inner_idem3:
+  shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs"
+  by (meson map_idI rsimp_inner_idem2)
+
+corollary rsimp_inner_idem4:
+  shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs"
+  by (metis good1 goodalts_nonalt rrexp.simps(12))
+
+
+lemma head_one_more_simp:
+  shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"
+  by (simp add: rsimp_idem)
+
+lemma head_one_more_dersimp:
+  shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)"
+  using head_one_more_simp rders_simp_append rders_simp_one_char by presburger
+
+
+
 lemma der_simp_nullability:
   shows "rnullable r = rnullable (rsimp r)"
   using RL_rnullable RL_rsimp by auto
@@ -548,8 +1185,19 @@
 
 
 
+lemma no_alt_short_list_after_simp:
+  shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+  by (metis bbbbs good1 k0a rrexp.simps(12))
 
 
+lemma no_further_dB_after_simp:
+  shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"
+  apply(subgoal_tac "good (RALTS rs)")
+  apply(subgoal_tac "distinct rs")
+  using rdistinct_on_distinct apply blast
+  apply (metis distinct.simps(1) distinct.simps(2) empty_iff good.simps(6) list.exhaust set_empty2)
+  using good1 by fastforce
+
 
 lemma idem_after_simp1:
   shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
@@ -676,66 +1324,13 @@
 
 
 
-inductive good1 :: "rrexp \<Rightarrow> bool"
-  where
-"\<lbrakk>RZERO \<notin> set rs; \<nexists>rs1. RALTS rs1 \<in> set rs\<rbrakk> \<Longrightarrow> good1 (RALTS rs)"
-|"good1 RZERO"
-|"good1 RONE"
-|"good1 (RCHAR c)"
-|"good1 (RSEQ r1 r2)"
-|"good1 (RSTAR r0)"
 
-inductive goods :: "rrexp list \<Rightarrow> bool"
-  where
- "goods []"
-|"\<lbrakk>goods rs; r \<noteq> RZERO; \<nexists>rs1. RALTS rs1 = r\<rbrakk> \<Longrightarrow> goods (r # rs)"
-
-lemma goods_good1:
-  shows "goods rs = good1 (RALTS rs)"
-  apply(induct rs)
-  apply (simp add: good1.intros(1) goods.intros(1))
-  apply(case_tac "goods rs")
-   apply(case_tac a)
-        apply simp
-  using good1.simps goods.cases apply auto[1]
-  apply (simp add: good1.simps goods.intros(2))
-  apply (simp add: good1.simps goods.intros(2))
-     apply (simp add: good1.simps goods.intros(2))
-  using good1.simps goods.cases apply auto[1]
-  apply (metis good1.cases good1.intros(1) goods.intros(2) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.distinct(9) rrexp.inject(3) set_ConsD)
-  apply simp
-  by (metis good1.cases good1.intros(1) goods.cases list.distinct(1) list.inject list.set_intros(2) rrexp.distinct(15) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) rrexp.simps(26) rrexp.simps(30))
-
-lemma rsimp_good10:
-  shows "good1 (rsimp r)"
-  apply(induct r)
-       apply simp
-  
-       apply (simp add: good1.intros(2))
-      apply simp
-
-      apply (simp add: good1.intros(3))
-  
-  apply (simp add: good1.intros(4))
-  sledgehammer
-
-  sorry
-
-lemma rsimp_good1:
-  shows "rsimp r = r1 \<Longrightarrow> good1 r1"
-  using rsimp_good10 by blast
-
-  
 
 lemma rsimp_no_dup:
   shows "rsimp r = RALTS rs \<Longrightarrow> distinct rs"
-  sorry
+  by (metis no_further_dB_after_simp rdistinct_does_the_job)
 
 
-lemma rsimp_good1_2:
-  shows "map rsimp rsa = [RALTS rs] \<Longrightarrow> good1 (RALTS rs)"
-  by (metis Cons_eq_map_D rsimp_good1)
-  
 
 
 lemma simp_singlealt_flatten:
@@ -751,12 +1346,6 @@
   by (metis no_alt_short_list_after_simp) 
   
 
-lemma good1_flts:
-  shows "good1 (RALTS rs1) \<Longrightarrow> rflts rs1 = rs1"
-  apply(induct rs1)
-   apply simp 
-  by (metis good1.cases good1.intros(1) list.set_intros(1) rflts_def_idiot rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.inject(3) rsimp.simps(3) rsimp.simps(4) rsimp_inner_idem4 set_subset_Cons subsetD)
- 
 
 
 lemma good1_flatten:
@@ -766,11 +1355,9 @@
    apply simp+
   apply(subgoal_tac "rflts (rs1 @ map rsimp rsb) = rs1 @ rflts (map rsimp rsb)")
    apply simp
-  apply(subgoal_tac "good1 (RALTS rs1)")
-  prefer 2
-  using rsimp_good1 apply blast
-  using flts_append good1_flts by presburger
+  using flts_append rsimp_inner_idem4 by presburger
 
+  
 lemma flatten_rsimpalts:
   shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) = 
          rflts ( (rdistinct (rflts (map rsimp rsa)) {}) @ map rsimp rsb)"
@@ -781,59 +1368,43 @@
    apply(case_tac a)
         apply simp+
     apply(rename_tac rs1)
-    apply(subgoal_tac "good1 (RALTS rs1)")
-     apply(subgoal_tac "distinct rs1")
-  apply(subst rdistinct_on_distinct)
-  apply blast
-  apply(subst rdistinct_on_distinct)
-       apply blast
-  using good1_flatten apply blast
- 
-  using rsimp_no_dup apply force
+    apply (metis good1_flatten map_eq_Cons_D no_further_dB_after_simp)
+  
+  apply simp
   
-  using rsimp_good1_2 apply presburger
-
-   apply simp+
-  apply(case_tac "rflts (a # aa # lista)")
-   apply simp
-  by (smt (verit) append_Cons append_Nil empty_iff good1_flatten list.distinct(1) rdistinct.simps(2) rsimp.simps(2) rsimp_ALTs.elims rsimp_good1)
+  apply(subgoal_tac "\<forall>r \<in> set( rflts (map rsimp rsa)). good r")
+   apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}")
+    apply simp
+   apply(case_tac "listb")
+    apply simp+
+  apply (metis Cons_eq_appendI good1_flatten rflts.simps(3) rsimp.simps(2) rsimp_ALTs.simps(3))
+  by (metis (mono_tags, lifting) flts3 good1 image_iff list.set_map)
 
 
-lemma flts_good_good:
-  shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> good1 (RALTS (rflts rs ))"
-  apply(induct rs)
-   apply simp
-  using goods.intros(1) goods_good1 apply auto[1]
-  apply(case_tac  "a")
-  apply simp
-  apply (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(4) rrexp.distinct(1) rrexp.distinct(15))
-     apply simp
-  using goods.intros(2) goods_good1 apply blast
-  using goods.intros(2) goods_good1 apply auto[1]
-   apply(subgoal_tac "good1 a")
-  apply (metis Un_iff good1.cases good1.intros(1) list.set_intros(2) rflts.simps(3) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) set_append)
-  apply simp
-  by (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(7) rrexp.distinct(29) rrexp.distinct(9))
+lemma last_elem_out:
+  shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
+  apply(induct xs arbitrary: rset)
+  apply simp+
+  done
 
 
-lemma simp_flatten_aux1:
-  shows "\<forall>r \<in> set (map rsimp rsa). good1 r"
-  apply(induct rsa)
-   apply(simp add: goods.intros)
-  using rsimp_good1 by auto
-
-
-
-lemma simp_flatten_aux:
-  shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> rflts (rdistinct (rflts rs) {}) = (rdistinct (rflts rs) {})"
-  sorry
-
 
 
 lemma rdistinct_concat_general:
   shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+  apply(induct rs1 arbitrary: rs2 rule: rev_induct)
+   apply simp
+  apply(drule_tac x = "x # rs2" in meta_spec)
+  apply simp
+  apply(case_tac "x \<in> set xs")
+   apply simp
   
-  sorry
+   apply (simp add: distinct_removes_middle3 insert_absorb)
+  apply simp
+  by (simp add: last_elem_out)
+
+
+  
 
 lemma distinct_once_enough:
   shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
@@ -851,13 +1422,17 @@
   apply simp
   apply(subst flatten_rsimpalts)
   apply(simp add: flts_append)
-  apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good1 r")
-  apply (metis distinct_once_enough simp_flatten_aux)
-  using simp_flatten_aux1 by blast
+  by (metis distinct_once_enough nonalt0_fltseq nonalt_flts_rd qqq1 rdistinct_set_equality)
+
+lemma basic_rsimp_SEQ_property1:
+  shows "rsimp_SEQ RONE r = r"
+  by (simp add: idiot)
 
-lemma simp_flatten3:
-  shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
-  sorry
+
+
+lemma basic_rsimp_SEQ_property3:
+  shows "rsimp_SEQ r RZERO = RZERO"  
+  using rsimp_SEQ.elims by blast
 
 
 
diff -r 370dae790b30 -r 2b5b3f83e2b6 thys2/BitCoded.thy
--- a/thys2/BitCoded.thy	Wed Apr 13 22:20:08 2022 +0100
+++ b/thys2/BitCoded.thy	Fri Apr 15 19:35:29 2022 +0100
@@ -1,5 +1,5 @@
 
-theory BitCodedCT
+theory BitCoded
   imports "Lexer" 
 begin
 
@@ -29,7 +29,7 @@
 where
   "decode' ds ZERO = (Void, [])"
 | "decode' ds ONE = (Void, ds)"
-| "decode' ds (CHAR d) = (Char d, ds)"
+| "decode' ds (CH d) = (Char d, ds)"
 | "decode' [] (ALT r1 r2) = (Void, [])"
 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
@@ -111,7 +111,7 @@
 where
   "erase AZERO = ZERO"
 | "erase (AONE _) = ONE"
-| "erase (ACHAR _ c) = CHAR c"
+| "erase (ACHAR _ c) = CH c"
 | "erase (AALTs _ []) = ZERO"
 | "erase (AALTs _ [r]) = (erase r)"
 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
@@ -131,21 +131,6 @@
 | "nonalt r = True"
 
 
-fun good :: "arexp \<Rightarrow> bool" where
-  "good AZERO = False"
-| "good (AONE cs) = True" 
-| "good (ACHAR cs c) = True"
-| "good (AALTs cs []) = False"
-| "good (AALTs cs [r]) = False"
-| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
-| "good (ASEQ _ AZERO _) = False"
-| "good (ASEQ _ (AONE _) _) = False"
-| "good (ASEQ _ _ AZERO) = False"
-| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
-| "good (ASTAR cs r) = True"
-
-
-
 
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
   "fuse bs AZERO = AZERO"
@@ -165,7 +150,7 @@
 fun intern :: "rexp \<Rightarrow> arexp" where
   "intern ZERO = AZERO"
 | "intern ONE = AONE []"
-| "intern (CHAR c) = ACHAR [] c"
+| "intern (CH c) = ACHAR [] c"
 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
                                 (fuse [S]  (intern r2))"
 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
@@ -1118,6 +1103,25 @@
    apply(simp_all)
   done
 
+fun nonalt :: "arexp \<Rightarrow> bool"
+  where
+  "nonalt (AALTs bs2 rs) = False"
+| "nonalt r = True"
+
+
+fun good :: "arexp \<Rightarrow> bool" where
+  "good AZERO = False"
+| "good (AONE cs) = True" 
+| "good (ACHAR cs c) = True"
+| "good (AALTs cs []) = False"
+| "good (AALTs cs [r]) = False"
+| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
+| "good (ASEQ _ AZERO _) = False"
+| "good (ASEQ _ (AONE _) _) = False"
+| "good (ASEQ _ _ AZERO) = False"
+| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
+| "good (ASTAR cs r) = True"
+
 lemma bbbbs:
   assumes "good r" "r = AALTs bs1 rs"
   shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"
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