theory RfltsRdistinctProps imports "Rsimp"

begin

lemma all_that_same_elem:

  shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>

       \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset"

  apply(induct rs)

   apply simp

  apply(subgoal_tac "aa = a")

   apply simp

  by (metis empty_iff insert_iff list.discI rdistinct.simps(2))

lemma rdistinct1:

  assumes "a \<in> acc"

  shows "a \<notin> set (rdistinct rs acc)"

  using assms

  apply(induct rs arbitrary: acc a)

   apply(auto)

  done

lemma rdistinct_does_the_job:

  shows "distinct (rdistinct rs s)"

  apply(induct rs s rule: rdistinct.induct)

  apply(auto simp add: rdistinct1)

  done

lemma rdistinct_concat:

  assumes "set rs \<subseteq> rset"

  shows "rdistinct (rs @ rsa) rset = rdistinct rsa rset"

  using assms

  apply(induct rs)

  apply simp+

  done

lemma distinct_not_exist:

  assumes "a \<notin> set rs"

  shows "rdistinct rs rset = rdistinct rs (insert a rset)"

  using assms

  apply(induct rs arbitrary: rset)

  apply(auto)

  done

lemma rdistinct_on_distinct:

  shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs"

  apply(induct rs)

  apply simp

  using distinct_not_exist by fastforce

lemma distinct_rdistinct_append:

  assumes "distinct rs1" "\<forall>r \<in> set rs1. r \<notin> acc"

  shows "rdistinct (rs1 @ rsa) acc = rs1 @ (rdistinct rsa (acc \<union> set rs1))"

  using assms

  apply(induct rs1 arbitrary: rsa acc)

   apply(auto)[1]

  apply(auto)[1]

  apply(drule_tac x="rsa" in meta_spec)

  apply(drule_tac x="{a} \<union> acc" in meta_spec)

  apply(simp)

  apply(drule meta_mp)

   apply(auto)[1]

  apply(simp)

  done

lemma rdistinct_set_equality1:

  shows "set (rdistinct rs acc) = set rs - acc"

  apply(induct rs acc rule: rdistinct.induct)

  apply(auto)

  done

lemma rdistinct_set_equality:

  shows "set (rdistinct rs {}) = set rs"

  by (simp add: rdistinct_set_equality1)

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

  assumes "nonalt r" "r \<noteq> RZERO"

  shows "rflts [r] = [r]"

  using assms

  apply(case_tac  r)

       apply(simp_all)

  done

lemma rflts_def_idiot:

  shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow> rflts (a # rs) = a # rflts rs"

  apply(case_tac a)

  apply simp_all

  done

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

  shows "rflts (rs1 @ [RALTS rs]) = rflts rs1 @ rs"

  apply (induct rs1 rule: rflts.induct)

  apply(auto)

  done

lemma flts_keeps1:

  shows "rflts (rs @ [RONE]) = rflts rs @ [RONE]"

  apply (induct rs rule: rflts.induct)

  apply(auto)

  done

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 rule: rflts.induct)

  apply(auto)

  by (meson k0b nonalt.elims(3))

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 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 rule: rflts.induct)

  apply(auto)

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

  shows "\<lbrakk> \<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 @ a # rs) {} = rdistinct (as @ rs) {}")

   prefer 2

  apply (metis append_Cons append_Nil distinct_removes_middle(1))

  by presburger

lemma last_elem_out:

  shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"

  apply(induct xs arbitrary: rset)

  apply simp+

  done

lemma rdistinct_concat_general:

  shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"

  apply(induct rs1 arbitrary: rs2 rule: rev_induct)

   apply simp

  apply(drule_tac x = "x # rs2" in meta_spec)

  apply simp

  apply(case_tac "x \<in> set xs")

   apply simp

   apply (simp add: distinct_removes_middle3 insert_absorb)

  apply simp

  by (simp add: last_elem_out)

lemma distinct_once_enough:

  shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"

  apply(subgoal_tac "distinct (rdistinct rs {})")

   apply(subgoal_tac 

" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")

  apply(simp only:)

  using rdistinct_concat_general apply blast

  apply (simp add: distinct_rdistinct_append rdistinct_set_equality1)

  by (simp add: rdistinct_does_the_job)

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_last(1) 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_last(1) rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))

    apply (metis distinct_removes_last(1) flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))

   prefer 2

   apply (metis distinct_removes_last(1) 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(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")

    prefer 2

  apply (metis (mono_tags, lifting) image_iff image_set spilled_alts_contained)

  apply (metis rflts_spills_last)

  by (metis distinct_removes_list spilled_alts_contained)

lemma distinct_early_app1:

  shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"

  apply(induct rs arbitrary: rset rset1)

   apply simp

  apply simp

  apply(case_tac "a \<in> rset1")

   apply simp

   apply(case_tac "a \<in> rset")

    apply simp+

   apply blast

  apply(case_tac "a \<in> rset1")

   apply simp+

  apply(case_tac "a \<in> rset")

   apply simp

   apply (metis insert_subsetI)

  apply simp

  by (meson insert_mono)

lemma distinct_early_app:

  shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"

  apply(induct rsb)

   apply simp

  using distinct_early_app1 apply blast

  by (metis distinct_early_app1 distinct_once_enough empty_subsetI)

lemma distinct_eq_interesting1:

  shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"

  apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")

   apply(simp only:)

  using distinct_early_app apply blast 

  by (metis append_Cons distinct_early_app rdistinct.simps(2))

end