Quelle DP_Library.thy Sprache: Isabelle

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

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.