theory ClosedForms imports

"BasicIdentities"

begin

lemma add0_isomorphic:

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

  sorry

lemma distinct_removes_last:

  shows "\<lbrakk>(a::rrexp) \<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_last2:

  shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk>

    \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"

  using distinct_removes_last(1) by presburger

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

(*  apply (smt (z3) append.right_neutral empty_iff list.distinct(1) list.inject no_alt_short_list_after_simp no_further_dB_after_simp rdistinct.elims rflts.elims rflts.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2)))*)

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

  shows "rsimp  (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) \<and>

  rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = 

  rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))"

  apply(induct rs arbitrary: rsa rsb)

   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::rrexp) \<in> set as\<rbrakk>

    \<Longrightarrow> rdistinct as {} = rdistinct (as @ [a]) {}"

  using distinct_removes_last2 by blast

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)) {})"

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 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))) {}))")