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_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