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 \
(\<exists>x \<in> set xs. \<exists>y \<in> set xs. P x y) = (\<exists>(x, y) \<in> set (alluopairs xs). P x y)"
by (blast intro!: alluopairs_bex)
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
