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