summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

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 "\<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

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

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)

39 end