equal
deleted
inserted
replaced
181 done |
181 done |
182 |
182 |
183 lemma mem_card_not_0: |
183 lemma mem_card_not_0: |
184 assumes a: "memb a A" |
184 assumes a: "memb a A" |
185 shows "\<not>(fcard_raw A = 0)" |
185 shows "\<not>(fcard_raw A = 0)" |
186 by (metis a fcard_raw_0 none_memb_nil) |
186 proof - |
|
187 have "\<not>(\<forall>x. \<not> memb x A)" using a by auto |
|
188 then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp |
|
189 then show ?thesis using fcard_raw_0[of A] by simp |
|
190 qed |
187 |
191 |
188 lemma fcard_raw_rsp_aux: |
192 lemma fcard_raw_rsp_aux: |
189 assumes a: "xs \<approx> ys" |
193 assumes a: "xs \<approx> ys" |
190 shows "fcard_raw xs = fcard_raw ys" |
194 shows "fcard_raw xs = fcard_raw ys" |
191 using a |
195 using a |
341 apply (simp only:) |
345 apply (simp only:) |
342 apply (rule_tac f="f a1" in arg_cong) |
346 apply (rule_tac f="f a1" in arg_cong) |
343 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
347 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
344 apply simp |
348 apply simp |
345 apply (simp add: memb_delete_raw) |
349 apply (simp add: memb_delete_raw) |
346 apply (metis memb_cons_iff) |
350 apply (auto simp add: memb_cons_iff)[1] |
347 apply (erule memb_commute_ffold_raw) |
351 apply (erule memb_commute_ffold_raw) |
348 apply (drule_tac x="a1" in spec) |
352 apply (drule_tac x="a1" in spec) |
349 apply (simp add: memb_cons_iff) |
353 apply (simp add: memb_cons_iff) |
350 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
354 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
351 length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
355 length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |