# Theory DP_Library

theory DP_Library
imports Main
```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
```