Theory Remdups_Rev

section‹Reverse Remdups›
theory Remdups_Rev
imports Main
begin

definition remdups_rev :: "'a list ⇒ 'a list" where
  "remdups_rev rs ≡ rev (remdups (rev rs))"

lemma remdups_append: "remdups (rs @ rs2) = remdups [r←rs . r ∉ set rs2] @ remdups rs2"
  by(induction rs arbitrary: rs2) (simp_all)

lemma remdups_rev_append: "remdups_rev (rs @ rs2) = remdups_rev rs @ remdups_rev [r←rs2 . r ∉ set rs]"
  proof(induction rs arbitrary: rs2)
  case Cons thus ?case by(simp add: remdups_append rev_filter remdups_rev_def)
  qed(simp add: remdups_rev_def)

lemma remdups_rev_fst:
  "remdups_rev (r#rs) = (if r ∈ set rs then r#remdups_rev (removeAll r rs) else r#remdups_rev rs)"
proof -
  have 1: "r ∉ set rs ⟹ remdups_rev (r # rs) = r # remdups_rev rs"
    unfolding remdups_rev_def
    proof(induction rs)
    case (Cons r rs)
      { fix rs and rs2::"'a list"
        have "set rs ∩ set rs2 = {} ⟹ remdups (rs @ rs2) = remdups rs @ remdups rs2"
          by(induction rs arbitrary: rs2) (simp_all)
      } note h=this
      { fix r and rs::"'a list"
        from h[of "rev rs" "[r]"] have "r ∉ set rs ⟹ remdups (rev rs @ [r]) = remdups (rev rs) @ [r]" by simp
      }
      with Cons show ?case by fastforce  
    qed(simp)

  have 2: "r ∈ set rs ⟹ remdups_rev (r # rs) = r # remdups_rev (rev (removeAll r (rev rs)))"
    unfolding remdups_rev_def
    proof(induction rs)
    case Cons thus ?case
      apply(simp add: removeAll_filter_not_eq remdups_append)
      apply(safe)
        apply(simp_all)
       apply metis
      apply metis
      done
    qed(simp)

  have "rev (removeAll r (rev rs)) = removeAll r rs" by (simp add: removeAll_filter_not_eq rev_filter)
  with 1 2 show ?thesis by simp
qed

lemma remdups_rev_set: "set (remdups_rev rs) = set rs" by (simp add: remdups_rev_def) 

lemma remdups_rev_removeAll: "remdups_rev (removeAll r rs) = removeAll r (remdups_rev rs)"
  by (simp add: remdups_filter remdups_rev_def removeAll_filter_not_eq rev_filter)

text‹Faster code equations›
fun remdups_rev_code :: "'a list ⇒ 'a list ⇒ 'a list" where
  "remdups_rev_code _ [] = []" |
  "remdups_rev_code ps (r#rs) = (if r ∈ set ps then remdups_rev_code ps rs else r#remdups_rev_code (r#ps) rs)"

lemma remdups_rev_code[code_unfold]: "remdups_rev rs = remdups_rev_code [] rs"
proof -
  { fix ps1 ps2 p and rs::"'a list"
    have "set ps1 = set ps2 ⟹ remdups_rev_code ps1 rs = remdups_rev_code ps2 rs"
      proof(induction rs arbitrary: ps1 ps2)
      case Nil thus ?case by simp
      next
      case (Cons r rs) show ?case
        apply(subst remdups_rev_code.simps)+ (*simplifier loops*)
        apply(case_tac "r ∈ set ps1")
         using Cons apply metis
        using Cons apply(simp)
        done
      qed
  } note remdups_rev_code_ps_seteq=this
  { fix ps1 ps2 p and rs::"'a list"
    have "remdups_rev_code (ps1@ps2) rs = remdups_rev_code ps2 (filter (λr. r ∉ set ps1) rs)"
      proof(induction rs arbitrary: ps1 ps2)
      case (Cons r rs)
        have "remdups_rev_code (r # ps1 @ ps2) rs = remdups_rev_code (ps1 @ r # ps2) rs"
          by(rule remdups_rev_code_ps_seteq) simp
        with Cons.IH have "remdups_rev_code (r # ps1 @ ps2) rs = remdups_rev_code (r#ps2) [r←rs . r ∉ set ps1]" by simp
        from this show ?case by(simp add: Cons)
      qed(simp add: remdups_rev_def)
   } note remdups_rev_code_ps_append=this
  { fix ps p and rs::"'a list"
    have "remdups_rev_code (p # ps) rs = remdups_rev_code ps (removeAll p rs)"
      by(simp add: remdups_rev_code_ps_append[of "[p]" "ps" rs, simplified] removeAll_filter_not_eq) metis
  } note remdups_rev_code_ps_fst=this
  { fix ps p and rs::"'a list"
    have "remdups_rev_code ps (removeAll p rs) = removeAll p (remdups_rev_code ps rs)"
      apply(induction rs arbitrary: ps)
       apply(simp_all)
      apply(safe)
       apply(simp_all)
      apply(simp add: remdups_rev_code_ps_fst removeAll_filter_not_eq)
      done
  } note remdups_rev_code_removeAll=this
  {fix ps
    have "∀p ∈ set ps. p ∉ set rs ⟹ remdups_rev rs = remdups_rev_code ps rs"
      apply(induction rs arbitrary: ps)
       apply(simp add: remdups_rev_def)
      apply(simp add: remdups_rev_fst remdups_rev_removeAll)
      apply safe
        apply(simp_all)
       apply(simp add: remdups_rev_code_ps_fst remdups_rev_code_removeAll)
       apply metis
      by blast
  }
  thus ?thesis by simp
qed
  

end