Theory List_Product_More

section‹List Product Helpers›
theory List_Product_More
imports Main
begin

(*TODO: this definition could also go to Main*)
lemma List_product_concat_map: "List.product xs ys = concat (map (λx. map (λy. (x,y)) ys) xs)"
  by(induction xs) (simp)+


definition all_pairs :: "'a list ⇒ ('a × 'a) list" where
  "all_pairs xs ≡ concat (map (λx. map (λy. (x,y)) xs) xs)"

lemma all_pairs_list_product: "all_pairs xs = List.product xs xs"
  by(simp add: all_pairs_def List_product_concat_map)
  
lemma all_pairs: "∀ (x,y) ∈ (set xs × set xs). (x,y) ∈ set (all_pairs xs)"
  by(simp add: all_pairs_list_product)

lemma all_pairs_set: "set (all_pairs xs) = set xs × set xs"
  by(simp add: all_pairs_list_product)

end