178 proof (rule card_bij'[where f="\<lambda>V. V - {?l}" and g="insert ?l"]) |
178 proof (rule card_bij'[where f="\<lambda>V. V - {?l}" and g="insert ?l"]) |
179 have *: "\<And>m V. m \<in> {1..a + Suc b} \<Longrightarrow> {0..<m} \<inter> (V - {?l}) = {0..<m} \<inter> V" |
179 have *: "\<And>m V. m \<in> {1..a + Suc b} \<Longrightarrow> {0..<m} \<inter> (V - {?l}) = {0..<m} \<inter> V" |
180 by auto |
180 by auto |
181 show "(\<lambda>V. V - {?l}) \<in> ?V (\<lambda>V. ?l \<in> V) \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)}" |
181 show "(\<lambda>V. V - {?l}) \<in> ?V (\<lambda>V. ?l \<in> V) \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)}" |
182 by (auto simp: Ico_subset_finite *) |
182 by (auto simp: Ico_subset_finite *) |
183 { fix V assume "V \<subseteq> {0..<?l}" |
183 { fix V assume V: "V \<subseteq> {0..<?l}" |
184 moreover then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V" |
184 then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V" |
185 by (auto dest: finite_subset) |
185 by (auto dest: finite_subset) |
186 ultimately have "card (insert ?l V) = Suc (card V)" |
186 with V have "card (insert ?l V) = Suc (card V)" |
187 "card ({0..<m} \<inter> insert ?l V) = (if m = Suc ?l then Suc (card V) else card ({0..<m} \<inter> V))" |
187 "card ({0..<m} \<inter> insert ?l V) = (if m = Suc ?l then Suc (card V) else card ({0..<m} \<inter> V))" |
188 if "m \<le> Suc ?l" for m |
188 if "m \<le> Suc ?l" for m |
189 using that by auto } |
189 using that by auto } |
190 then show "insert ?l \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)} \<rightarrow> ?V (\<lambda>V. ?l \<in> V)" |
190 then show "insert ?l \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)} \<rightarrow> ?V (\<lambda>V. ?l \<in> V)" |
191 using \<open>b < a\<close> by auto |
191 using \<open>b < a\<close> by auto |