# Theory Common_Lemmas

```section"Injectivity for two argument functions"

theory Common_Lemmas
imports
"HOL.List"
"HOL-Library.Tree"
begin

text ‹This section introduces @{term "inj2_on"} which generalizes @{term "inj_on"} on curried
functions with two arguments and contains subsequent theorems about such functions.›

text"
We could use curried function directly with for example ‹case_prod›,
but this way the proofs become simpler and easier to read."
definition inj2_on :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a set ⇒ 'b set ⇒ bool" where
"inj2_on f A B ⟷ (∀x1∈A. ∀x2∈A. ∀y1∈B. ∀y2∈B. f x1 y1 = f x2 y2 ⟶ x1 = x2 ∧ y1 = y2)"

abbreviation inj2 :: "('a ⇒ 'b ⇒ 'c) ⇒ bool" where
"inj2 f ≡ inj2_on f UNIV UNIV"

subsection ‹Correspondence between @{term "inj2_on"} and @{term "inj_on"}›

lemma inj2_curried: "inj2_on (curry f) A B ⟷ inj_on f (A×B)"
unfolding inj2_on_def inj_on_def by auto

lemma inj2_on_all: "inj2 f ⟹ inj2_on f A B"
unfolding inj2_on_def by simp

lemma inj2_inj_first: "inj2 f ⟹ inj f"
unfolding inj2_on_def inj_on_def by simp

lemma inj2_inj_second: "inj2 f ⟹ inj (f x)"
unfolding inj2_on_def inj_on_def by simp

lemma inj2_inj_second_flipped: "inj2 f ⟹ inj (λx. f x y)"
unfolding inj2_on_def inj_on_def by simp

subsection"Proofs with inj2"

thm distinct_map

lemma inj2_on_distinct_map:
assumes "inj2_on f {x} (set xs)"
shows "distinct xs = distinct (map (f x) xs)"
using assms distinct_map by (auto simp: inj2_on_def inj_onI)

lemma inj2_distinct_map:
assumes "inj2 f"
shows "distinct xs = distinct (map (f x) xs)"
using assms inj2_on_distinct_map inj2_on_all by fast

lemma inj2_on_distinct_concat_map:
assumes "inj2_on f (set xs) (set ys)"
shows "⟦distinct ys; distinct xs⟧ ⟹ distinct [f x y. x ← xs, y ← ys]"
using assms proof(induct xs)
case Nil
then show ?case by simp
next
case (Cons x xs)
then have nin: "x ∉ set xs"
by simp

then have "inj2_on f {x} (set ys)"
using Cons unfolding inj2_on_def by simp
then have 1: "distinct (map (f x) ys)"
using Cons inj2_on_distinct_map by fastforce

have 2: "distinct (concat (map (λx. map (f x) ys) xs))"
using Cons unfolding inj2_on_def by simp

have 3: "⟦xa ∈ set xs; xb ∈ set ys; f x xb = f xa xc; xc ∈ set ys⟧ ⟹ False " for xa xb xc
using Cons(4) unfolding inj2_on_def
using nin by force

from 1 2 3 show ?case
by auto
qed

lemma inj2_distinct_concat_map:
assumes "inj2 f"
shows "⟦distinct ys; distinct xs⟧ ⟹ distinct [f x y. x ← xs, y ← ys]"
using assms inj2_on_all inj2_on_distinct_concat_map by blast

lemma inj2_distinct_concat_map_function:
assumes "inj2 f"
shows"⟦∀ x ∈ set xs. distinct (g x); distinct xs⟧ ⟹ distinct [f x y. x ← xs, y ← g x]"
proof(induct xs)
case Nil
then show ?case by simp
next
case (Cons x xs)
have 1: "distinct (map (f x) (g x))"
using Cons assms inj2_distinct_map by fastforce

have 2: "distinct (concat (map (λx. map (f x) (g x)) xs))"
using Cons by simp

have 3: "⋀xa xb xc. ⟦xa ∈ set xs; xb ∈ set (g x); f x xb = f xa xc; xc ∈ set (g xa)⟧
⟹ False"
using Cons assms unfolding inj2_on_def by auto

show ?case using 1 2 3
by auto
qed

lemma distinct_concat_Nil: "distinct (concat (map (λy. []) xs))"
by(induct xs) auto

lemma inj2_distinct_concat_map_function_filter:
assumes "inj2 f"
shows"⟦∀ x ∈ set xs. distinct (g x); distinct xs⟧ ⟹ distinct [f x y. x ← xs, y ← g x, h x]"
proof(induct xs)
case Nil
then show ?case by simp
next
case (Cons x xs)
have 1: "distinct (map (f x) (g x))"
using Cons assms inj2_distinct_map by fastforce

have 2: "distinct (concat (map (λx. concat (map (λy. if h x then [f x y] else []) (g x))) xs))"
using Cons by simp

have 3: "⋀xa xb xc.
⟦h x; xa ∈ set (g x); xb ∈ set xs; f x xa = f xb xc; xc ∈ set (g xb); xc ∈ (if h xb then UNIV else {})⟧ ⟹ False"
by (metis Cons.prems(2) assms distinct.simps(2) inj2_on_def iso_tuple_UNIV_I)

then have 4: "distinct (concat (map (λy. []) (g x)))"
using distinct_concat_Nil by auto

show ?case using 1 2 3 4 by auto
qed

subsection‹Specializations of @{term "inj2"}›

subsubsection"Cons"

lemma Cons_inj2: "inj2 (#)"
unfolding inj2_on_def by simp

lemma Cons_distinct_concat_map: "⟦distinct ys; distinct xs⟧ ⟹ distinct [x#y. x ← xs, y ← ys]"
using inj2_distinct_concat_map Cons_inj2 by auto

lemma Cons_distinct_concat_map_function:
"⟦∀ x ∈ set xs. distinct (g x) ; distinct xs⟧ ⟹ distinct [x # y. x ← xs, y ← g x]"
using inj2_distinct_concat_map_function Cons_inj2 by auto

lemma Cons_distinct_concat_map_function_distinct_on_all:
"⟦∀ x. distinct (g x) ; distinct xs⟧ ⟹ distinct [x # y. x ← xs, y ← g x]"
using Cons_distinct_concat_map_function by (metis (full_types))

subsubsection"Node right"

lemma Node_right_inj2: "inj2 (λl r. Node l e r)"
unfolding inj2_on_def by simp

lemma Node_right_distinct_concat_map:
"⟦distinct ys; distinct xs⟧ ⟹ distinct [Node x e y. x ← xs, y ← ys]"
using inj2_distinct_concat_map Node_right_inj2 by fast

subsubsection"Node left"

lemma Node_left_inj2: "inj2 (λr l. Node l e r)"
unfolding inj2_on_def by simp

lemma Node_left_distinct_map: "distinct xs = distinct (map (λl. ⟨l, (), r⟩) xs)"
using inj2_distinct_map Node_left_inj2 by fast

subsubsection"Cons Suc"

lemma Cons_Suc_inj2: "inj2 (λx ys. Suc x # ys)"
unfolding inj2_on_def by simp

lemma Cons_Suc_distinct_concat_map_function:
"⟦∀ x ∈ set xs. distinct (g x) ; distinct xs⟧ ⟹ distinct [Suc x # y. x ← xs, y ← g x]"
using inj2_distinct_concat_map_function Cons_Suc_inj2 by auto

section"Lemmas for cardinality proofs "

lemma length_concat_map: "length [f x r . x ← xs, r ← ys] = length ys * length xs"
by(induct xs arbitrary: ys) auto

text"An useful extension to ‹length_concat›"
thm length_concat
lemma length_concat_map_function_sum_list:
assumes "⋀ x. x ∈ set xs ⟹ length (g x) = h x"
shows "length [f x r . x ← xs, r ← g x] = sum_list (map h xs)"
using assms by(induct xs) auto

lemma sum_list_extract_last: "(∑x←[0..<Suc n]. f x) = (∑x←[0..<n]. f x) + f n"

lemma leq_sum_to_sum_list: "(∑x ≤ n. f x) = (∑x←[0..<Suc n]. f x)"
by (metis atMost_upto sum_set_upt_conv_sum_list_nat)

lemma less_sum_to_sum_list: "(∑x < n. f x) = (∑x←[0..< n]. f x)"

section"Miscellaneous"

text‹Similar to @{thm [source] "length_remove1"}:›
lemma Suc_length_remove1: "x ∈ set xs ⟹ Suc (length (remove1 x xs)) = length xs"
by(induct xs) auto

subsection"‹count_list› and replicate"
text"HOL.List doesn't have many lemmas about ‹count_list› (when not using multisets)"

lemma count_list_replicate: "count_list (replicate x y) y = x"
by (induct x) auto

lemma count_list_full_elem: "count_list xs y = length xs ⟷ (∀x ∈ set xs. x = y)"
proof(induct xs)
case Nil
then show ?case by simp
next
case (Cons z xs)
have "⟦count_list xs y = Suc (length xs); x ∈ set xs⟧ ⟹ x = y" for x
by (metis Suc_n_not_le_n count_le_length)
then show ?case
using Cons by auto
qed

text‹The following lemma verifies the reverse of @{thm [source] "count_notin"}:›
thm count_notin
lemma count_list_zero_not_elem: "count_list xs x = 0 ⟷ x ∉ set xs"
by(induct xs) auto

lemma count_list_length_replicate: "count_list xs y = length xs ⟷ xs = replicate (length xs) y"
by (metis count_list_full_elem count_list_replicate replicate_length_same)

lemma count_list_True_False: "count_list xs True + count_list xs False = length xs"
by(induct xs) auto

end```