equal
deleted
inserted
replaced
243 |
243 |
244 lemma cons_left_idem: |
244 lemma cons_left_idem: |
245 "x # x # xs \<approx> x # xs" |
245 "x # x # xs \<approx> x # xs" |
246 by auto |
246 by auto |
247 |
247 |
248 lemma none_mem_nil: |
248 lemma none_memb_nil: |
249 "(\<forall>x. x \<notin> set xs) = (xs \<approx> [])" |
249 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
250 by simp |
250 by (simp add: memb_def) |
251 |
251 |
252 lemma fset_raw_strong_cases: |
252 lemma fset_raw_strong_cases: |
253 "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))" |
253 "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))" |
254 apply (induct xs) |
254 apply (induct xs) |
255 apply (simp) |
255 apply (simp) |
276 |
276 |
277 lemma memb_delete_raw: |
277 lemma memb_delete_raw: |
278 "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)" |
278 "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)" |
279 by (induct xs arbitrary: x y) (auto simp add: memb_def) |
279 by (induct xs arbitrary: x y) (auto simp add: memb_def) |
280 |
280 |
|
281 lemma delete_raw_rsp: |
|
282 "l \<approx> r \<Longrightarrow> delete_raw l x \<approx> delete_raw r x" |
|
283 by (simp add: memb_def[symmetric] memb_delete_raw) |
|
284 |
281 lemma [quot_respect]: |
285 lemma [quot_respect]: |
282 "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw" |
286 "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw" |
283 by (simp add: memb_def[symmetric] memb_delete_raw) |
287 by (simp add: memb_def[symmetric] memb_delete_raw) |
284 |
288 |
285 lemma memb_delete_raw_ident: |
289 lemma memb_delete_raw_ident: |
337 done |
341 done |
338 |
342 |
339 lemma ffold_raw_rsp_pre: |
343 lemma ffold_raw_rsp_pre: |
340 "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b" |
344 "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b" |
341 apply (induct a arbitrary: b) |
345 apply (induct a arbitrary: b) |
342 apply (simp add: hd_in_set memb_absorb memb_def none_mem_nil) |
346 apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil) |
343 apply (simp add: ffold_raw.simps) |
347 apply (simp add: ffold_raw.simps) |
344 apply (rule conjI) |
348 apply (rule conjI) |
345 apply (rule_tac [!] impI) |
349 apply (rule_tac [!] impI) |
346 apply (rule_tac [!] conjI) |
350 apply (rule_tac [!] conjI) |
347 apply (rule_tac [!] impI) |
351 apply (rule_tac [!] impI) |
477 lemma fset_to_set_simps[simp]: |
481 lemma fset_to_set_simps[simp]: |
478 "fset_to_set {||} = ({} :: 'a set)" |
482 "fset_to_set {||} = ({} :: 'a set)" |
479 "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)" |
483 "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)" |
480 by (lifting set.simps) |
484 by (lifting set.simps) |
481 |
485 |
482 thm memb_def[symmetric, THEN meta_eq_to_obj_eq] |
|
483 |
|
484 lemma in_fset_to_set: |
486 lemma in_fset_to_set: |
485 "x \<in> fset_to_set S \<equiv> x |\<in>| S" |
487 "x \<in> fset_to_set S \<equiv> x |\<in>| S" |
486 by (lifting memb_def[symmetric]) |
488 by (lifting memb_def[symmetric]) |
487 |
489 |
488 lemma none_fin_fempty: |
490 lemma none_fin_fempty: |
489 "(\<forall>x. x \<notin> fset_to_set S) = (S = {||})" |
491 "(\<forall>x. x |\<notin>| S) = (S = {||})" |
490 by (lifting none_mem_nil) |
492 by (lifting none_memb_nil) |
491 |
493 |
492 lemma fset_cong: |
494 lemma fset_cong: |
493 "(fset_to_set S = fset_to_set T) = (S = T)" |
495 "(fset_to_set S = fset_to_set T) = (S = T)" |
494 by (lifting set_cong) |
496 by (lifting set_cong) |
495 |
497 |