equal
deleted
inserted
replaced
178 apply simp |
178 apply simp |
179 apply (rule_tac x="a" in exI) |
179 apply (rule_tac x="a" in exI) |
180 apply (simp add: memb_def) |
180 apply (simp add: memb_def) |
181 done |
181 done |
182 |
182 |
183 lemma mem_card_not_0: |
183 lemma memb_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 proof - |
186 proof - |
187 have "\<not>(\<forall>x. \<not> memb x A)" using a by auto |
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 |
188 then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp |
193 assumes a: "xs \<approx> ys" |
193 assumes a: "xs \<approx> ys" |
194 shows "fcard_raw xs = fcard_raw ys" |
194 shows "fcard_raw xs = fcard_raw ys" |
195 using a |
195 using a |
196 apply(induct xs arbitrary: ys) |
196 apply(induct xs arbitrary: ys) |
197 apply(auto simp add: memb_def) |
197 apply(auto simp add: memb_def) |
198 apply(metis) |
198 apply(subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)") |
|
199 apply simp |
|
200 apply auto |
|
201 apply (drule_tac x="x" in spec) |
|
202 apply blast |
199 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) |
200 apply(simp add: fcard_raw_delete_one) |
204 apply(simp add: fcard_raw_delete_one memb_def) |
201 apply(metis Suc_pred'[OF fcard_raw_gt_0] fcard_raw_delete_one memb_def) |
205 apply(metis Suc_pred'[OF fcard_raw_gt_0]) |
202 done |
206 done |
203 |
207 |
204 lemma fcard_raw_rsp[quot_respect]: |
208 lemma fcard_raw_rsp[quot_respect]: |
205 shows "(op \<approx> ===> op =) fcard_raw fcard_raw" |
209 shows "(op \<approx> ===> op =) fcard_raw fcard_raw" |
206 by (simp add: fcard_raw_rsp_aux) |
210 by (simp add: fcard_raw_rsp_aux) |
335 apply (simp add: ffold_raw.simps) |
339 apply (simp add: ffold_raw.simps) |
336 apply (rule conjI) |
340 apply (rule conjI) |
337 apply (rule_tac [!] impI) |
341 apply (rule_tac [!] impI) |
338 apply (rule_tac [!] conjI) |
342 apply (rule_tac [!] conjI) |
339 apply (rule_tac [!] impI) |
343 apply (rule_tac [!] impI) |
340 apply (simp add: in_set_code memb_cons_iff memb_def) |
344 apply (subgoal_tac "\<forall>e. memb e a2 = memb e b") |
341 apply (metis) |
345 apply (simp) |
|
346 apply (simp add: memb_cons_iff memb_def) |
|
347 apply auto |
|
348 apply (drule_tac x="e" in spec) |
|
349 apply blast |
|
350 apply (simp add: memb_cons_iff) |
342 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
351 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
343 length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
352 length_Suc_conv memb_absorb nil_not_cons(2)) |
344 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
353 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
345 apply (simp only:) |
354 apply (simp only:) |
346 apply (rule_tac f="f a1" in arg_cong) |
355 apply (rule_tac f="f a1" in arg_cong) |
347 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
356 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
348 apply simp |
357 apply simp |