theory ClosedForms imports
"BasicIdentities"
begin



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)
  

  
  sorry


lemma distinct_der:
  shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))"

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

  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