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 \ ('a \ '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) \ {(x,y). x\ set xs \ y\ set xs}" wenzelm@49519 11 by (induct xs) auto nipkow@41849 12 nipkow@41849 13 lemma alluopairs_set: nipkow@41849 14 "\x\ set xs ; y \ set xs\ \ (x,y) \ set (alluopairs xs) \ (y,x) \ set (alluopairs xs) " wenzelm@49519 15 by (induct xs) auto nipkow@41849 16 nipkow@41849 17 lemma alluopairs_bex: nipkow@41849 18 assumes Pc: "\ x \ set xs. \y\ set xs. P x y = P y x" nipkow@41849 19 shows "(\ x \ set xs. \ y \ set xs. P x y) = (\ (x,y) \ set (alluopairs xs). P x y)" nipkow@41849 20 proof nipkow@41849 21 assume "\x\set xs. \y\set xs. P x y" wenzelm@49519 22 then obtain x y where x: "x \ set xs" and y:"y \ 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"\(x, y)\set (alluopairs xs). P x y" nipkow@41849 25 by auto nipkow@41849 26 next nipkow@41849 27 assume "\(x, y)\set (alluopairs xs). P x y" wenzelm@49519 28 then obtain "x" and "y" where xy: "(x,y) \ set (alluopairs xs)" and P: "P x y" wenzelm@49519 29 by blast+ nipkow@41849 30 from xy have "x \ set xs \ y\ set xs" using alluopairs_set1 by blast nipkow@41849 31 with P show "\x\set xs. \y\set xs. P x y" by blast nipkow@41849 32 qed nipkow@41849 33 nipkow@41849 34 lemma alluopairs_ex: wenzelm@49519 35 "\x y. P x y = P y x \ wenzelm@49519 36 (\x \ set xs. \ y \ set xs. P x y) = (\(x,y) \ set (alluopairs xs). P x y)" wenzelm@49519 37 by (blast intro!: alluopairs_bex) nipkow@41849 38 nipkow@41849 39 end