equal
deleted
inserted
replaced
200 apply auto |
200 apply auto |
201 apply (drule_tac x="x" in spec) |
201 apply (drule_tac x="x" in spec) |
202 apply blast |
202 apply blast |
203 apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec) |
203 apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec) |
204 apply(simp add: fcard_raw_delete_one memb_def) |
204 apply(simp add: fcard_raw_delete_one memb_def) |
205 apply(metis Suc_pred'[OF fcard_raw_gt_0]) |
205 apply (case_tac "a \<in> set ys") |
|
206 apply (simp only: if_True) |
|
207 apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)") |
|
208 apply (drule Suc_pred'[OF fcard_raw_gt_0]) |
|
209 apply auto |
206 done |
210 done |
207 |
211 |
208 lemma fcard_raw_rsp[quot_respect]: |
212 lemma fcard_raw_rsp[quot_respect]: |
209 shows "(op \<approx> ===> op =) fcard_raw fcard_raw" |
213 shows "(op \<approx> ===> op =) fcard_raw fcard_raw" |
210 by (simp add: fcard_raw_rsp_aux) |
214 by (simp add: fcard_raw_rsp_aux) |