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
```     1 theory DP_Library
```
```     2 imports Main
```
```     3 begin
```
```     4
```
```     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)"
```
```     9
```
```    10 lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
```
```    11   by (induct xs) auto
```
```    12
```
```    13 lemma alluopairs_set:
```
```    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) "
```
```    15   by (induct xs) auto
```
```    16
```
```    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) = (\<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" using alluopairs_set1 by blast
```
```    31   with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
```
```    32 qed
```
```    33
```
```    34 lemma alluopairs_ex:
```
```    35   "\<forall>x y. P x y = P y x \<Longrightarrow>
```
```    36     (\<exists>x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists>(x,y) \<in> set (alluopairs xs). P x y)"
```
```    37   by (blast intro!: alluopairs_bex)
```
```    38
```
```    39 end
```