theory ClosedForms imports
"BasicIdentities"
begin

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: )
  sorry

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 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))))"
  sorry

end