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"

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