Theory DP_Library

theory DP_Library
imports Main
begin

primrec alluopairs:: "'a list ⇒ ('a × 'a) list"
where
  "alluopairs [] = []"
| "alluopairs (x # xs) = map (Pair x) (x # xs) @ alluopairs xs"

lemma alluopairs_set1: "set (alluopairs xs) ≤ {(x, y). x∈ set xs ∧ y∈ set xs}"
  by (induct xs) auto

lemma alluopairs_set:
  "x∈ set xs ⟹ y ∈ set xs ⟹ (x, y) ∈ set (alluopairs xs) ∨ (y, x) ∈ set (alluopairs xs)"
  by (induct xs) auto

lemma alluopairs_bex:
  assumes Pc: "∀x ∈ set xs. ∀y ∈ set xs. P x y = P y x"
  shows "(∃x ∈ set xs. ∃y ∈ set xs. P x y) ⟷ (∃(x, y) ∈ set (alluopairs xs). P x y)"
proof
  assume "∃x ∈ set xs. ∃y ∈ set xs. P x y"
  then obtain x y where x: "x ∈ set xs" and y: "y ∈ set xs" and P: "P x y"
    by blast
  from alluopairs_set[OF x y] P Pc x y show "∃(x, y) ∈ set (alluopairs xs). P x y" 
    by auto
next
  assume "∃(x, y) ∈ set (alluopairs xs). P x y"
  then obtain x and y where xy: "(x, y) ∈ set (alluopairs xs)" and P: "P x y"
    by blast+
  from xy have "x ∈ set xs ∧ y ∈ set xs"
    using alluopairs_set1 by blast
  with P show "∃x∈set xs. ∃y∈set xs. P x y" by blast
qed

lemma alluopairs_ex:
  "∀x y. P x y = P y x ⟹
    (∃x ∈ set xs. ∃y ∈ set xs. P x y) = (∃(x, y) ∈ set (alluopairs xs). P x y)"
  by (blast intro!: alluopairs_bex)

end