equal
deleted
inserted
replaced
58 "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D)) |
58 "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D)) |
59 \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})" |
59 \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})" |
60 by simp |
60 by simp |
61 |
61 |
62 lemma |
62 lemma |
63 "finite {s'. EX s:S. s' = f a e s}" |
63 "finite S ==> finite {s'. EX s:S. s' = f a e s}" |
64 unfolding Bex_def |
64 by simp |
65 apply simp |
|
66 oops |
|
67 |
65 |
68 schematic_lemma (* check interaction with schematics *) |
66 schematic_lemma (* check interaction with schematics *) |
69 "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b} |
67 "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b} |
70 = finite ((\<lambda>(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \<times> UNIV))" |
68 = finite ((\<lambda>(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \<times> UNIV))" |
71 by simp |
69 by simp |