equal
deleted
inserted
replaced
85 |
85 |
86 lemma Ball_weaken: "\<lbrakk>Ball s P; \<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q" |
86 lemma Ball_weaken: "\<lbrakk>Ball s P; \<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q" |
87 by auto |
87 by auto |
88 |
88 |
89 lemma finite_SetCompr2: |
89 lemma finite_SetCompr2: |
90 "finite (Collect P) \<Longrightarrow> \<forall>y. P y \<longrightarrow> finite (range (f y)) \<Longrightarrow> |
90 "finite {f y x |x y. P y}" if "finite (Collect P)" |
91 finite {f y x |x y. P y}" |
91 "\<forall>y. P y \<longrightarrow> finite (range (f y))" |
92 apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (\<lambda>y. range (f y))") |
92 proof - |
93 prefer 2 apply fast |
93 have "{f y x |x y. P y} = (\<Union>y\<in>Collect P. range (f y))" |
94 apply (erule ssubst) |
94 by auto |
95 apply (erule finite_UN_I) |
95 with that show ?thesis by simp |
96 apply fast |
96 qed |
97 done |
|
98 |
97 |
99 lemma list_all2_trans: "\<forall>a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow> |
98 lemma list_all2_trans: "\<forall>a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow> |
100 \<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3" |
99 \<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3" |
101 apply (induct_tac xs1) |
100 apply (induct_tac xs1) |
102 apply simp |
101 apply simp |