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

src/HOL/Decision_Procs/DP_Library.thy

author | blanchet |

Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) | |

changeset 58306 | 117ba6cbe414 |

parent 55814 | aefa1db74d9d |

permissions | -rw-r--r-- |

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

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 "x\<in> set xs \<Longrightarrow> y \<in> set xs \<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) \<longleftrightarrow> (\<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"

31 using alluopairs_set1 by blast

32 with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast

33 qed

35 lemma alluopairs_ex:

36 "\<forall>x y. P x y = P y x \<Longrightarrow>

37 (\<exists>x \<in> set xs. \<exists>y \<in> set xs. P x y) = (\<exists>(x, y) \<in> set (alluopairs xs). P x y)"

38 by (blast intro!: alluopairs_bex)

40 end