(* 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