Theory Util

(* Victor B. F. Gomes, University of Cambridge
   Martin Kleppmann, University of Cambridge
   Dominic P. Mulligan, University of Cambridge
   Alastair R. Beresford, University of Cambridge
*)

section‹Technical Lemmas›

text‹This section contains a list of helper definitions and lemmas about sets, lists and
     the option monad.›

theory
  Util
imports
  Main
  "HOL-Library.Monad_Syntax"
begin

subsection‹Kleisli arrow composition›

definition kleisli :: "('b ⇒ 'b option) ⇒ ('b ⇒ 'b option) ⇒ ('b ⇒ 'b option)" (infixr "⊳" 65) where
  "f ⊳ g ≡ λx. (f x ⤜ (λy. g y))"

lemma kleisli_comm_cong:
  assumes "x ⊳ y = y ⊳ x"
  shows   "z ⊳ x ⊳ y = z ⊳ y ⊳ x"
  using assms by(clarsimp simp add: kleisli_def)

lemma kleisli_assoc:
  shows "(z ⊳ x) ⊳ y = z ⊳ (x ⊳ y)"
  by(auto simp add: kleisli_def)

subsection‹Lemmas about sets›

lemma distinct_set_notin [dest]:
  assumes "distinct (x#xs)"
  shows   "x ∉ set xs"
  using assms by(induction xs, auto)

lemma set_membership_equality_technicalD [dest]:
  assumes "{x} ∪ (set xs) = {y} ∪ (set ys)"
  shows "x = y ∨ y ∈ set xs"
  using assms by(induction xs, auto)

lemma set_equality_technical:
  assumes "{x} ∪ (set xs) = {y} ∪ (set ys)"
      and "x ∉ set xs"
      and "y ∉ set ys"
      and "y ∈ set xs"
    shows "{x} ∪ (set xs - {y}) = set ys"
  using assms by (induction xs) auto
    
lemma set_elem_nth:
  assumes "x ∈ set xs"
  shows   "∃m. m < length xs ∧ xs ! m = x"
  using assms by(induction xs, simp) (meson in_set_conv_nth)
    
subsection‹Lemmas about list›

lemma list_nil_or_snoc:
  shows "xs = [] ∨ (∃y ys. xs = ys@[y])"
  by (induction xs, auto)

lemma suffix_eq_distinct_list:
  assumes "distinct xs"
      and "ys@suf1 = xs"
      and "ys@suf2 = xs"
    shows "suf1 = suf2"
  using assms by(induction xs arbitrary: suf1 suf2 rule: rev_induct, simp) (metis append_eq_append_conv)

lemma pre_suf_eq_distinct_list:
  assumes "distinct xs"
      and "ys ≠ []"
      and "pre1@ys@suf1 = xs"
      and "pre2@ys@suf2 = xs"
    shows "pre1 = pre2 ∧ suf1 = suf2"
using assms
  apply(induction xs arbitrary: pre1 pre2 ys, simp)
  apply(case_tac "pre1"; case_tac "pre2"; clarify)
   apply(metis suffix_eq_distinct_list append_Nil)
  apply(metis Un_iff append_eq_Cons_conv distinct.simps(2) list.set_intros(1) set_append suffix_eq_distinct_list)
  apply(metis Un_iff append_eq_Cons_conv distinct.simps(2) list.set_intros(1) set_append suffix_eq_distinct_list)
  apply(metis distinct.simps(2) hd_append2 list.sel(1) list.sel(3) list.simps(3) tl_append2)
  done

lemma list_head_unaffected:
  assumes "hd (x @ [y, z]) = v"
    shows "hd (x @ [y   ]) = v"
  using assms by (metis hd_append list.sel(1))

lemma list_head_butlast:
  assumes "hd xs = v"
  and "length xs > 1"
  shows "hd (butlast xs) = v"
  using assms by (metis hd_conv_nth length_butlast length_greater_0_conv less_trans nth_butlast zero_less_diff zero_less_one)

lemma list_head_length_one:
  assumes "hd xs = x"
    and "length xs = 1"
  shows "xs = [x]"
  using assms by(metis One_nat_def Suc_length_conv hd_Cons_tl length_0_conv list.sel(3))

lemma list_two_at_end:
  assumes "length xs > 1"
  shows "∃xs' x y. xs = xs' @ [x, y]"
  using assms
  apply(induction xs rule: rev_induct, simp)
  apply(case_tac "length xs = 1", simp)
   apply(metis append_self_conv2 length_0_conv length_Suc_conv)
  apply(rule_tac x="butlast xs" in exI, rule_tac x="last xs" in exI, simp)
  done

lemma list_nth_split_technical:
  assumes "m < length cs"
      and "cs ≠ []"
    shows "∃xs ys. cs = xs@(cs!m)#ys"
  using assms
  apply(induction m arbitrary: cs)
   apply(meson in_set_conv_decomp nth_mem)
  apply(metis in_set_conv_decomp length_list_update set_swap set_update_memI)
  done

lemma list_nth_split:
  assumes "m < length cs"
      and "n < m"
      and "1 < length cs"
    shows "∃xs ys zs. cs = xs@(cs!n)#ys@(cs!m)#zs"
using assms proof(induction n arbitrary: cs m)
  case 0 thus ?case
    apply(case_tac cs; clarsimp)
    apply(rule_tac x="[]" in exI, clarsimp)
    apply(rule list_nth_split_technical, simp, force)
    done
next
  case (Suc n)
  thus ?case
  proof (cases cs)
    case Nil
    then show ?thesis
      using Suc.prems by auto
  next
    case (Cons a as)
    hence "m-1 < length as" "n < m-1"
      using Suc by force+
    then obtain xs ys zs where "as = xs @ as ! n # ys @ as ! (m-1) # zs"
      using Suc by force
    thus ?thesis
      apply(rule_tac x="a#xs" in exI) 
      using Suc Cons apply force
      done
   qed
qed

lemma list_split_two_elems:
  assumes "distinct cs"
      and "x ∈ set cs"
      and "y ∈ set cs"
      and "x ≠ y"
    shows "∃pre mid suf. cs = pre @ x # mid @ y # suf ∨ cs = pre @ y # mid @ x # suf"
proof -
  obtain xi yi where *: "xi < length cs ∧ x = cs ! xi" "yi < length cs ∧ y = cs ! yi" "xi ≠ yi"
    using set_elem_nth linorder_neqE_nat assms by metis
  thus ?thesis
    by (metis list_nth_split One_nat_def less_Suc_eq linorder_neqE_nat not_less_zero)
qed

lemma split_list_unique_prefix:
  assumes "x ∈ set xs"
  shows "∃pre suf. xs = pre @ x # suf ∧ (∀y ∈ set pre. x ≠ y)"
using assms proof(induction xs)
  case Nil thus ?case by clarsimp
next
  case (Cons y ys)
  then show ?case
    proof (cases "y=x")
      case True
      then show ?thesis by force
    next
      case False
      then obtain pre suf where "ys = pre @ x # suf ∧ (∀y∈set pre. x ≠ y)"
        using assms Cons by auto
      thus ?thesis
        using split_list_first by force
    qed
qed

lemma map_filter_append:
  shows "List.map_filter P (xs @ ys) = List.map_filter P xs @ List.map_filter P ys"
  by(auto simp add: List.map_filter_def)

end