author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 55814 aefa1db74d9d
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
     1 theory DP_Library
     2 imports Main
     3 begin
     5 primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list"
     6 where
     7   "alluopairs [] = []"
     8 | "alluopairs (x # xs) = map (Pair x) (x # xs) @ alluopairs xs"
    10 lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x, y). x\<in> set xs \<and> y\<in> set xs}"
    11   by (induct xs) auto
    13 lemma alluopairs_set:
    14   "x\<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> (x, y) \<in> set (alluopairs xs) \<or> (y, x) \<in> set (alluopairs xs)"
    15   by (induct xs) auto
    17 lemma alluopairs_bex:
    18   assumes Pc: "\<forall>x \<in> set xs. \<forall>y \<in> set xs. P x y = P y x"
    19   shows "(\<exists>x \<in> set xs. \<exists>y \<in> set xs. P x y) \<longleftrightarrow> (\<exists>(x, y) \<in> set (alluopairs xs). P x y)"
    20 proof
    21   assume "\<exists>x \<in> set xs. \<exists>y \<in> set xs. P x y"
    22   then obtain x y where x: "x \<in> set xs" and y: "y \<in> set xs" and P: "P x y"
    23     by blast
    24   from alluopairs_set[OF x y] P Pc x y show "\<exists>(x, y) \<in> set (alluopairs xs). P x y" 
    25     by auto
    26 next
    27   assume "\<exists>(x, y) \<in> set (alluopairs xs). P x y"
    28   then obtain x and y where xy: "(x, y) \<in> set (alluopairs xs)" and P: "P x y"
    29     by blast+
    30   from xy have "x \<in> set xs \<and> y \<in> set xs"
    31     using alluopairs_set1 by blast
    32   with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
    33 qed
    35 lemma alluopairs_ex:
    36   "\<forall>x y. P x y = P y x \<Longrightarrow>
    37     (\<exists>x \<in> set xs. \<exists>y \<in> set xs. P x y) = (\<exists>(x, y) \<in> set (alluopairs xs). P x y)"
    38   by (blast intro!: alluopairs_bex)
    40 end