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" text‹Already existing for @{term "inj"}:› 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" by(induct n) (auto simp: add.assoc) 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)" by (simp add: atLeast_upt sum_list_distinct_conv_sum_set) 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