src/HOL/Decision_Procs/DP_Library.thy
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51474 1e9e68247ad1
parent 49519 4d2c93e1d9c8
child 55814 aefa1db74d9d
permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
nipkow@41849
     1
theory DP_Library
nipkow@41849
     2
imports Main
nipkow@41849
     3
begin
nipkow@41849
     4
wenzelm@49519
     5
primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list"
wenzelm@49519
     6
where
nipkow@41849
     7
  "alluopairs [] = []"
nipkow@41849
     8
| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
nipkow@41849
     9
nipkow@41849
    10
lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
wenzelm@49519
    11
  by (induct xs) auto
nipkow@41849
    12
nipkow@41849
    13
lemma alluopairs_set:
nipkow@41849
    14
  "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
wenzelm@49519
    15
  by (induct xs) auto
nipkow@41849
    16
nipkow@41849
    17
lemma alluopairs_bex:
nipkow@41849
    18
  assumes Pc: "\<forall> x \<in> set xs. \<forall>y\<in> set xs. P x y = P y x"
nipkow@41849
    19
  shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
nipkow@41849
    20
proof
nipkow@41849
    21
  assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
wenzelm@49519
    22
  then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y"
wenzelm@49519
    23
    by blast
nipkow@41849
    24
  from alluopairs_set[OF x y] P Pc x y show"\<exists>(x, y)\<in>set (alluopairs xs). P x y" 
nipkow@41849
    25
    by auto
nipkow@41849
    26
next
nipkow@41849
    27
  assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
wenzelm@49519
    28
  then obtain "x" and "y" where xy: "(x,y) \<in> set (alluopairs xs)" and P: "P x y"
wenzelm@49519
    29
    by blast+
nipkow@41849
    30
  from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
nipkow@41849
    31
  with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
nipkow@41849
    32
qed
nipkow@41849
    33
nipkow@41849
    34
lemma alluopairs_ex:
wenzelm@49519
    35
  "\<forall>x y. P x y = P y x \<Longrightarrow>
wenzelm@49519
    36
    (\<exists>x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists>(x,y) \<in> set (alluopairs xs). P x y)"
wenzelm@49519
    37
  by (blast intro!: alluopairs_bex)
nipkow@41849
    38
nipkow@41849
    39
end