theory ClosedForms imports
"BasicIdentities"
begin


lemma idem_after_simp1:
  shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
  apply(case_tac "rsimp aa")
  apply simp+
  apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
  by simp


lemma distinct_removes_last:
  shows "\<lbrakk>a \<in> set as\<rbrakk>
    \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
  apply(induct as arbitrary: rset ab rset1 a)
     apply simp
    apply simp
  apply(case_tac "aa \<in> rset")
   apply(case_tac "a = aa")
  apply (metis append_Cons)
    apply simp
   apply(case_tac "a \<in> set as")
  apply (metis append_Cons rdistinct.simps(2) set_ConsD)
   apply(case_tac "a = aa")
    prefer 2
    apply simp
   apply (metis append_Cons)
  apply(case_tac "ab \<in> rset1")
  prefer 2
   apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = 
               ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")
  prefer 2
  apply force
  apply(simp only:)
     apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")
    apply(simp only:)
    apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")
     apply blast
    apply(case_tac "a \<in> insert ab rset1")
     apply simp
     apply (metis insertI1)
    apply simp
    apply (meson insertI1)
   apply simp
  apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")
   apply simp
  by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))


lemma distinct_removes_middle:
  shows  "\<lbrakk>a \<in> set as\<rbrakk>
    \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
   apply(induct as arbitrary: rset rset1 ab as2 as3 a)
     apply simp
    apply simp
   apply(case_tac "a \<in> rset")
    apply simp
    apply metis
   apply simp
   apply (metis insertI1)
  apply(case_tac "a = ab")
   apply simp
   apply(case_tac "ab \<in> rset")
    apply simp
    apply presburger
   apply (meson insertI1)
  apply(case_tac "a \<in> rset")
  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
  apply(case_tac "ab \<in> rset")
  apply simp
   apply (meson insert_iff)
  apply simp
  by (metis insertI1)


lemma distinct_removes_middle3:
  shows  "\<lbrakk>a \<in> set as\<rbrakk>
    \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
  using distinct_removes_middle(1) by fastforce

lemma distinct_removes_last2:
  shows "\<lbrakk>a \<in> set as\<rbrakk>
    \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
  by (simp add: distinct_removes_last(1))

lemma distinct_removes_middle2:
  shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}"
  by (metis distinct_removes_middle(1))

lemma distinct_removes_list:
  shows "\<lbrakk>a \<in> set as; \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
  apply(induct rs)
   apply simp+
  apply(subgoal_tac "rdistinct (as @ aa # rs) {} = rdistinct (as @ rs) {}")
   prefer 2
  apply (metis append_Cons append_Nil distinct_removes_middle(1))
  by presburger



lemma simp_rdistinct_f: shows 
"f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = 
                      rsimp (rsimp_ALTs (rdistinct (map f rs) frset))  "
  apply(induct rs arbitrary: rset)
   apply simp
   apply(case_tac "a \<in> rset")
  apply(case_tac " f a \<in> frset")
   apply simp
   apply blast
  apply(subgoal_tac "f a \<notin> frset")
   apply(simp)
   apply(subgoal_tac "f ` (insert a rset) = insert (f a) frset")
  prefer 2
  apply (meson image_insert)
  
  oops

lemma spawn_simp_rsimpalts:
  shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"
  apply(cases rs)
   apply simp
  apply(case_tac list)
   apply simp
   apply(subst rsimp_idem[symmetric])
   apply simp
  apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")
   apply(simp only:)
   apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")
    apply(simp only:)
  prefer 2
  apply simp
   prefer 2
  using rsimp_ALTs.simps(3) apply presburger
  apply auto
  apply(subst rsimp_idem)+
  by (metis comp_apply rsimp_idem)

lemma spawn_simp_distinct:
  shows "rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) = rsimp (rsimp_ALTs (rsa @ rs))
\<and> (a1 \<in> set rsa1 \<longrightarrow> rsimp (rsimp_ALTs (rsa1 @ rs)) = rsimp (rsimp_ALTs (rsa1 @ a1 # rs)))
\<and> rsimp  (rsimp_ALTs (rsc @ rs)) = rsimp (rsimp_ALTs (rsc @ (rdistinct rs (set rsc))))"
  apply(induct rs arbitrary: rsa rsa1 a1 rsc)
   apply simp
   apply(subgoal_tac "rsimp (rsimp_ALTs (rsa1 @ [a1])) = rsimp (rsimp_ALTs (rsa1 @ (rdistinct [a1] (set rsa1))))")
  prefer 2
  



  oops

lemma inv_one_derx:
  shows " RONE = rder xa r2 \<Longrightarrow> r2 = RCHAR xa"
  apply(case_tac r2)
       apply simp+
  using rrexp.distinct(1) apply presburger
    apply (metis rder.simps(5) rrexp.distinct(13) rrexp.simps(20))
   apply simp+
  done

lemma shape_of_derseq:
  shows "rder x (RSEQ r1 r2) = RSEQ (rder x r1) r2 \<or> rder x (RSEQ r1 r2) = (RALT (RSEQ (rder x r1) r2) (rder x r2))"
  using rder.simps(5) by presburger
lemma shape_of_derseq2:
  shows "rder x (RSEQ r11 r12) = RSEQ x41 x42 \<Longrightarrow> x41 = rder x r11"
  by (metis rrexp.distinct(25) rrexp.inject(2) shape_of_derseq)

lemma alts_preimage_case1:
  shows "rder x r = RALTS [r] \<Longrightarrow> \<exists>ra. r = RALTS [ra]"
  apply(case_tac r)
       apply simp+
  apply (metis rrexp.simps(12) rrexp.simps(20))
  apply (metis rrexp.inject(3) rrexp.simps(30) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) shape_of_derseq)
   apply auto[1]
  by auto

lemma alts_preimage_case2:
  shows "rder x r = RALT r1 r2 \<Longrightarrow> \<exists>ra rb. (r = RSEQ ra rb \<or> r = RALT ra rb)"
  apply(case_tac r)
       apply simp+
  apply (metis rrexp.distinct(15) rrexp.distinct(7))
    apply simp
  apply auto[1]
  by auto

lemma alts_preimage_case2_2:
  shows "rder x r = RALT r1 r2 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd. r = RALT rc rd)"
  using alts_preimage_case2 by blast

lemma alts_preimage_case3:
  shows "rder x r = RALT r1 r2 \<Longrightarrow>  (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rcs rc rd. r = RALTS rcs \<and> rcs = [rc, rd])"
  using alts_preimage_case2 by blast

lemma star_seq:
  shows "rder x (RSEQ (RSTAR a) b) = RALT (RSEQ (RSEQ (rder x a) (RSTAR a)) b) (rder x b)"
  using rder.simps(5) rder.simps(6) rnullable.simps(6) by presburger

lemma language_equality_id1:
  shows "\<not>rnullable a \<Longrightarrow> rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)"
  apply (subst star_seq)
  apply simp
  done



lemma distinct_der_set:
  shows "(rder x) ` rset = dset \<Longrightarrow>
rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))"
  apply(induct rs arbitrary: rset dset)
   apply simp
  apply(case_tac "a \<in> rset")
   apply(subgoal_tac "rder x a \<in> dset")
  prefer 2
    apply blast
   apply simp
  apply(case_tac "rder x a \<notin> dset")
   prefer 2
   apply simp
 
  oops

lemma map_concat_cons:
  shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
  by simp

lemma neg_removal_element_of:
  shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"
  by simp

lemma simp_more_flts:
  shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts rs) {}))"

  oops

lemma simp_more_distinct1:
  shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (rdistinct rs {}))"
  apply(induct rs)
   apply simp
  apply simp
  oops


(*
\<and>
  rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = 
  rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))
*)
lemma simp_removes_duplicate2:
  shows "a "

  oops

lemma flts_removes0:
  shows "  rflts (rs @ [RZERO])  =
           rflts rs"
  apply(induct rs)
   apply simp
  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
  
lemma flts_keeps1:
  shows " rflts (rs @ [RONE]) = 
          rflts  rs @ [RONE] "
  apply (induct rs)
   apply simp
  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)

lemma flts_keeps_others:
  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]"
  apply(induct rs)
   apply simp
  apply (simp add: rflts_def_idiot)
  apply(case_tac a)
       apply simp
  using flts_keeps1 apply blast
     apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
  apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
  apply blast
  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)


lemma rflts_def_idiot2:
  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"
  apply(induct rs)
   apply simp
  by (metis append.assoc in_set_conv_decomp insert_iff list.simps(15) rflts.simps(2) rflts.simps(3) rflts_def_idiot)

lemma rflts_spills_last:
  shows "a = RALTS rs \<Longrightarrow> rflts (rs1 @ [a]) = rflts rs1 @ rs"
  apply (induct rs1)
  apply simp
  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)


lemma spilled_alts_contained:
  shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)"
  apply(induct rs1)
   apply simp 
  apply(case_tac "a = aa")
   apply simp
  apply(subgoal_tac " a \<in> set rs1")
  prefer 2
   apply (meson set_ConsD)
  apply(case_tac aa)
  using rflts.simps(2) apply presburger
      apply fastforce
  apply fastforce
  apply fastforce
  apply fastforce
  by fastforce

lemma distinct_removes_duplicate_flts:
  shows " a \<in> set rsa
       \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
           rdistinct (rflts (map rsimp rsa)) {}"
  apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
  prefer 2
  apply simp
  apply(induct "rsimp a")
       apply simp
  using flts_removes0 apply presburger
      apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =  
                          rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
      apply (simp only:)
       apply(subst flts_keeps1)
  apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6))
      apply presburger
        apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a]))    {} =  
                            rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
      apply (simp only:)
      prefer 2
      apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3))
  apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))

    apply (metis distinct_removes_last2 flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
   prefer 2
   apply (metis distinct_removes_last2 flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29))
  apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x")
  prefer 2
  apply (simp add: rflts_spills_last)
  apply(simp only:)
  apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")
  prefer 2
  using spilled_alts_contained apply presburger
  by (metis append_self_conv distinct_removes_list in_set_conv_decomp rev_exhaust)

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)"
  by (simp add: flts_middle0)

lemma flts_append1:
  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk>  \<Longrightarrow>
         rflts (rsa @ [a] @ rsb) = rflts rsa @ [a] @ (rflts rsb)"
  apply(induct rsa arbitrary: rsb)
   apply simp
  using rflts_def_idiot apply presburger
  apply(case_tac aa)  
       apply simp+
  done

lemma flts_append:
  shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
  apply(induct rs1)
   apply simp
  apply(case_tac a)
       apply simp+
  done

lemma simp_removes_duplicate1:
  shows  " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) =  rsimp (RALTS (rsa))"
and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
  apply(induct rsa arbitrary: a1)
     apply simp
    apply simp
  prefer 2
  apply(case_tac "a = aa")
     apply simp
    apply simp
  apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2))
  apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9))
  by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2))
  
lemma simp_removes_duplicate2:
  shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))"
  apply(induct rsb arbitrary: rsa)
   apply simp
  using distinct_removes_duplicate_flts apply auto[1]
  by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1))

lemma simp_removes_duplicate3:
  shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
  using simp_removes_duplicate2 by auto

lemma distinct_removes_middle4:
  shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"
  using distinct_removes_middle(1) by fastforce

lemma distinct_removes_middle_list:
  shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"
  apply(induct x)
   apply simp
  by (simp add: distinct_removes_middle3)


lemma distinct_removes_duplicate_flts2:
  shows " a \<in> set rsa
       \<Longrightarrow> rdistinct (rflts (rsa @ [a] @ rsb)) {} =
           rdistinct (rflts (rsa @ rsb)) {}"
  apply(induct a arbitrary: rsb)
  using flts_middle01 apply presburger
      apply(subgoal_tac "rflts (rsa @ [RONE] @ rsb) = rflts rsa @ [RONE] @ rflts rsb")
  prefer 2
  using flts_append1 apply blast
      apply simp
      apply(subgoal_tac "RONE \<in> set (rflts rsa)")
  prefer 2
  using rflts_def_idiot2 apply blast
      apply(subst distinct_removes_middle3)
       apply simp
  using flts_append apply presburger
     apply simp
  apply (metis distinct_removes_middle3 flts_append in_set_conv_decomp rflts.simps(5))
  apply (metis distinct_removes_middle(1) flts_append flts_append1 rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
   apply(subgoal_tac "rflts (rsa @ [RALTS x] @ rsb) = rflts rsa @ x @ rflts rsb")
    prefer 2
  apply (simp add: flts_append)
   apply (simp only:)

   apply(subgoal_tac "\<forall>r1 \<in> set x. r1 \<in> set (rflts rsa)")
    prefer 2
  using spilled_alts_contained apply blast
  apply(subst flts_append)
  using distinct_removes_middle_list apply blast
  using distinct_removes_middle2 flts_append rflts_def_idiot2 by fastforce


lemma simp_removes_duplicate:
  shows "a \<in> set rsa \<Longrightarrow> rsimp (rsimp_ALTs (rsa @ a # rs)) =  rsimp (rsimp_ALTs (rsa @ rs))"
  apply(subgoal_tac "rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (RALTS (rsa @ a # rs))")
   prefer 2
  apply (smt (verit, best) Cons_eq_append_conv append_is_Nil_conv empty_set equals0D list.distinct(1) rsimp_ALTs.elims)
  apply(simp only:)
  apply simp
  apply(subgoal_tac "(rdistinct (rflts (map rsimp rsa @ rsimp a # map rsimp rs)) {}) = (rdistinct (rflts (map rsimp rsa @  map rsimp rs)) {})")
   apply(simp only:)
  prefer 2
   apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
    prefer 2
  apply simp
  using distinct_removes_duplicate_flts2 apply force
  apply(case_tac rsa)
   apply simp
  apply(case_tac rs)
   apply simp
   apply(case_tac list)
    apply simp
  using idem_after_simp1 apply presburger
   apply simp+
  apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)")
   apply simp
  using rsimpalts_conscons by presburger
  
lemma simp_der_pierce_flts:
  shows " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
           rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))"
  oops



lemma simp_more_distinct:
  shows "rsimp  (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) "
and  "a1 \<in> set rsb \<Longrightarrow> rsimp (rsimp_ALTs (rsb @ a1 # rs)) =  rsimp (rsimp_ALTs (rsb @ rs))"
  apply(induct rs arbitrary: rsa rsb a1)
     apply simp
  apply simp
  apply(case_tac " a \<in> set rsa")
   apply simp
   prefer 2
   apply simp
   apply(drule_tac x = "rsa @ [a]" in meta_spec)
   apply simp


  sorry

lemma non_empty_list:
  shows "a \<in> set as \<Longrightarrow> as \<noteq> []"
  by (metis empty_iff empty_set)

lemma distinct_comp:
  shows "rdistinct (rs1@rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
  apply(induct rs2 arbitrary: rs1)
   apply simp
  apply(subgoal_tac "rs1 @ a # rs2 = (rs1 @ [a]) @ rs2")
   apply(simp only:)
   apply(case_tac "a \<in> set rs1")
    apply simp
  oops

lemma instantiate1:
  shows "\<lbrakk>\<And>ab rset1.  rdistinct (ab # as) rset1 = rdistinct (ab # as @ [ab]) rset1\<rbrakk> \<Longrightarrow>  
rdistinct (aa # as) rset = rdistinct (aa # as @ [aa]) rset"
  apply(drule_tac x = "aa" in meta_spec)
  apply(drule_tac x = "rset" in meta_spec)
  apply simp
  done
  

lemma not_head_elem:
  shows " \<lbrakk>aa \<in> set (a # as); aa \<notin> (set as)\<rbrakk> \<Longrightarrow> a = aa"
  
  by fastforce

(*
  apply simp
  apply (metis append_Cons)
  apply(case_tac "ab \<in> rset1")
  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
  apply(subgoal_tac "rdistinct (ab # (aa # as) @ [ab]) rset1 = 
               ab # (rdistinct ((aa # as) @ [ab]) (insert ab rset1))")
   apply(simp only:)
   apply(subgoal_tac "rdistinct (ab # aa # as) rset1 = ab # (rdistinct (aa # as) (insert ab rset1))")
  apply(simp only:)
    apply(subgoal_tac "rdistinct ((aa # as) @ [ab]) (insert ab rset1) = rdistinct (aa # as) (insert ab rset1)")
  apply blast
*)
  

lemma flts_identity1:
  shows  "rflts (rs @ [RONE]) = rflts rs @ [RONE] "
  apply(induct rs)
   apply simp+
  apply(case_tac a)
       apply simp
      apply simp+
  done

lemma flts_identity10:
  shows " rflts (rs @ [RCHAR c]) = rflts rs @ [RCHAR c]"
  apply(induct rs)
   apply simp+
  apply(case_tac a)
       apply simp+
  done

lemma flts_identity11:
  shows " rflts (rs @ [RSEQ r1 r2]) = rflts rs @ [RSEQ r1 r2]"
  apply(induct rs)
   apply simp+
  apply(case_tac a)
       apply simp+
  done

lemma flts_identity12:
  shows " rflts (rs @ [RSTAR r0]) = rflts rs @ [RSTAR r0]"
  apply(induct rs)
   apply simp+
  apply(case_tac a)
       apply simp+
  done

lemma flts_identity2:
  shows "a \<noteq> RZERO \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow>  rflts (rs @ [a]) = rflts rs @ [a]"
  apply(case_tac a)
       apply simp
  using flts_identity1 apply auto[1]
  using flts_identity10 apply blast
  using flts_identity11 apply auto[1]
   apply blast
  using flts_identity12 by presburger

lemma flts_identity3:
  shows "a = RZERO  \<Longrightarrow> rflts (rs @ [a]) = rflts rs"
  apply simp
  apply(induct rs)
   apply simp+
  apply(case_tac aa)
       apply simp+
  done

lemma distinct_removes_last3:
  shows "\<lbrakk>a \<in> set as\<rbrakk>
    \<Longrightarrow> rdistinct as {} = rdistinct (as @ [a]) {}"
  by (simp add: distinct_removes_last2)

lemma set_inclusion_with_flts1:
  shows " \<lbrakk>RONE \<in> set rs\<rbrakk> \<Longrightarrow> RONE  \<in> set (rflts rs)"
  apply(induct rs)
   apply simp
  apply(case_tac " RONE \<in> set rs")
   apply simp
  apply (metis Un_upper2 insert_absorb insert_subset list.set_intros(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append)
  apply(case_tac "RONE = a")
   apply simp
  apply simp
  done

lemma set_inclusion_with_flts10:
  shows " \<lbrakk>RCHAR x \<in> set rs\<rbrakk> \<Longrightarrow> RCHAR x  \<in> set (rflts rs)"
  apply(induct rs)
   apply simp
  apply(case_tac " RCHAR x \<in> set rs")
   apply simp
  apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
  apply(case_tac "RCHAR x = a")
   apply simp
  apply fastforce
  apply simp
  done

lemma set_inclusion_with_flts11:
  shows " \<lbrakk>RSEQ r1 r2 \<in> set rs\<rbrakk> \<Longrightarrow> RSEQ r1 r2  \<in> set (rflts rs)"
  apply(induct rs)
   apply simp
  apply(case_tac " RSEQ r1 r2 \<in> set rs")
   apply simp
  apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
  apply(case_tac "RSEQ r1 r2 = a")
   apply simp
  apply fastforce
  apply simp
  done


lemma set_inclusion_with_flts:
  shows " \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RONE\<rbrakk> \<Longrightarrow> rsimp a \<in> set (rflts (map rsimp as))"
  by (simp add: set_inclusion_with_flts1)
  
lemma "\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk>
          \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) = 
rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})"

  sorry


lemma last_elem_dup1:
  shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))"
  apply simp
  apply(subgoal_tac "rsimp a \<in> set (map rsimp as)")
  prefer 2
   apply simp
  apply(case_tac "rsimp a")
       apply simp
  
  using flts_identity3 apply presburger
      apply(subst flts_identity2)
  using rrexp.distinct(1) rrexp.distinct(15) apply presburger
      apply(subst distinct_removes_last3[symmetric])
  using set_inclusion_with_flts apply blast
  apply simp
  apply (metis distinct_removes_last3 flts_identity10 set_inclusion_with_flts10)
  apply (metis distinct_removes_last3 flts_identity11 set_inclusion_with_flts11)
  sorry

lemma last_elem_dup:
  shows " a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs (as @ [a] )) = rsimp (rsimp_ALTs (as ))"
  apply(induct as rule: rev_induct)
   apply simp
  apply simp
  apply(subgoal_tac "xs \<noteq> []")
  prefer 2
  

  

  sorry

lemma appeared_before_remove_later:
  shows "a \<in>  set as \<Longrightarrow> rsimp (rsimp_ALTs ( as @ a # rs)) = rsimp (rsimp_ALTs (as @ rs))"
and "a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs as ) = rsimp (rsimp_ALTs (as @ [a]))"
  apply(induct rs arbitrary: as)
   apply simp
  

  sorry

lemma distinct_remove_later:
  shows "\<lbrakk>rder x a \<in> rder x ` set rsa\<rbrakk>
       \<Longrightarrow> rsimp (rsimp_ALTs (map (rder x) rsa @ rder x a # map (rder x) (rdistinct rs (insert a (set rsa))))) =
           rsimp (rsimp_ALTs (map (rder x) rsa @ map (rder x) (rdistinct rs (set rsa))))"
  
  sorry


lemma distinct_der_general:
  shows "rsimp (rsimp_ALTs (map (rder x) (rsa @ (rdistinct rs (set rsa))))) =
 rsimp ( rsimp_ALTs ((map (rder x) rsa)@(rdistinct (map (rder x) rs) (set (map (rder x) rsa)))) )"
  apply(induct rs arbitrary: rsa)
   apply simp
  apply(case_tac "a \<in> set rsa")
   apply(subgoal_tac "rder x a \<in> set (map (rder x) rsa)")
  apply simp
   apply simp
  apply(case_tac "rder x a \<notin> set (map (rder x) rsa)")
   apply(simp)
  apply(subst map_concat_cons)+
  apply(drule_tac x = "rsa @ [a]" in meta_spec)
   apply simp
  apply(drule neg_removal_element_of)
  apply simp
  apply(subst distinct_remove_later)
   apply simp
  apply(drule_tac x = "rsa" in meta_spec)
  by blast

  


lemma distinct_der:
  shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
  by (metis distinct_der_general list.simps(8) self_append_conv2 set_empty)

  


lemma rders_simp_lambda:
  shows " rsimp \<circ> rder x \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r (xs @ [x]))"
  using rders_simp_append by auto

lemma rders_simp_nonempty_simped:
  shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)"
  using rders_simp_same_simpders rsimp_idem by auto

lemma repeated_altssimp:
  shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =
           rsimp_ALTs (rdistinct (rflts rs) {})"
  by (metis map_idI rsimp.simps(2) rsimp_idem)


lemma add0_isomorphic:
  shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r"
  sorry


lemma distinct_append_simp:
  shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow>
           rsimp (rsimp_ALTs (f a # rs1)) =
           rsimp (rsimp_ALTs (f a # rs2))"
  apply(case_tac rs1)
   apply simp
   apply(case_tac rs2)
    apply simp
   apply simp
   prefer 2
   apply(case_tac list)
    apply(case_tac rs2)
     apply simp
  using add0_isomorphic apply blast 
    apply simp
  sorry

lemma alts_closed_form: shows 
"rsimp (rders_simp (RALTS rs) s) = 
rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
  apply(induct s rule: rev_induct)
   apply simp
  apply simp
  apply(subst rders_simp_append)
  apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) = 
 rsimp(rders_simp (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})) [x])")
   prefer 2
  apply (metis inside_simp_removal rders_simp_one_char)
  apply(simp only: )
  apply(subst rders_simp_one_char)
  apply(subst rsimp_idem)
  apply(subgoal_tac "rsimp (rder x (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {}))) =
                     rsimp ((rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))) ")
  prefer 2
  using rder_rsimp_ALTs_commute apply presburger
  apply(simp only:)
  apply(subgoal_tac "rsimp (rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))
= rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
   prefer 2
  
  using distinct_der apply presburger
  apply(simp only:)
  apply(subgoal_tac " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
                      rsimp (rsimp_ALTs (rdistinct ( (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)))) {}))")
   apply(simp only:)
  apply(subgoal_tac " rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) = 
                      rsimp (rsimp_ALTs (rdistinct (rflts ( (map (rsimp \<circ> (rder x) \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
    apply(simp only:)
  apply(subst rders_simp_lambda)
    apply(subst rders_simp_nonempty_simped)
     apply simp
    apply(subgoal_tac "\<forall>r \<in> set  (map (\<lambda>r. rders_simp r (xs @ [x])) rs). rsimp r = r")
  prefer 2
     apply (simp add: rders_simp_same_simpders rsimp_idem)
    apply(subst repeated_altssimp)
     apply simp
  apply fastforce
   apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem)
  sledgehammer
 (* by (metis inside_simp_removal rder_rsimp_ALTs_commute self_append_conv2 set_empty simp_more_distinct)

  *)

lemma alts_closed_form_variant: shows 
"s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = 
rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
  sorry



lemma star_closed_form:
  shows "rders_simp (RSTAR r0) (c#s) = 
rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
  apply(induct s)
   apply simp
  sorry



lemma seq_closed_form: shows 
"rsimp (rders_simp (RSEQ r1 r2) s) = 
rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # 
                (map (rders_simp r2) (vsuf s r1)) 
              )  
      )"
  apply(induct s)
  apply simp
  sorry


lemma seq_closed_form_variant: shows
"s \<noteq> [] \<Longrightarrow> (rders_simp (RSEQ r1 r2) s) = 
rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))"
  apply(induct s rule: rev_induct)
   apply simp
  apply(subst rders_simp_append)
  apply(subst rders_simp_one_char)
  apply(subst rsimp_idem[symmetric])
  apply(subst rders_simp_one_char[symmetric])
  apply(subst rders_simp_append[symmetric])
  apply(insert seq_closed_form)
  apply(subgoal_tac "rsimp (rders_simp (RSEQ r1 r2) (xs @ [x]))
 = rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1)))")
   apply force
  by presburger

end