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