src/HOL/Decision_Procs/DP_Library.thy
 author wenzelm Fri Mar 07 22:30:58 2014 +0100 (2014-03-07) changeset 55990 41c6b99c5fb7 parent 55814 aefa1db74d9d permissions -rw-r--r--
more antiquotations;
 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 [] = []" wenzelm@55814 8 | "alluopairs (x # xs) = map (Pair x) (x # xs) @ alluopairs xs" nipkow@41849 9 wenzelm@55814 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: wenzelm@55814 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: wenzelm@55814 18 assumes Pc: "\x \ set xs. \y \ set xs. P x y = P y x" wenzelm@55814 19 shows "(\x \ set xs. \y \ set xs. P x y) \ (\(x, y) \ set (alluopairs xs). P x y)" nipkow@41849 20 proof wenzelm@55814 21 assume "\x \ set xs. \y \ set xs. P x y" wenzelm@55814 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 wenzelm@55814 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 wenzelm@55814 27 assume "\(x, y) \ set (alluopairs xs). P x y" wenzelm@55814 28 then obtain x and y where xy: "(x, y) \ set (alluopairs xs)" and P: "P x y" wenzelm@49519 29 by blast+ wenzelm@55814 30 from xy have "x \ set xs \ y \ set xs" wenzelm@55814 31 using alluopairs_set1 by blast nipkow@41849 32 with P show "\x\set xs. \y\set xs. P x y" by blast nipkow@41849 33 qed nipkow@41849 34 nipkow@41849 35 lemma alluopairs_ex: wenzelm@49519 36 "\x y. P x y = P y x \ wenzelm@55814 37 (\x \ set xs. \y \ set xs. P x y) = (\(x, y) \ set (alluopairs xs). P x y)" wenzelm@49519 38 by (blast intro!: alluopairs_bex) nipkow@41849 39 nipkow@41849 40 end