equal
deleted
inserted
replaced
624 apply auto |
624 apply auto |
625 apply (rule_tac b="x # ba" in pred_compI) |
625 apply (rule_tac b="x # ba" in pred_compI) |
626 apply auto |
626 apply auto |
627 done |
627 done |
628 |
628 |
|
629 lemma insert_preserve2: |
|
630 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
|
631 (id ---> rep_fset ---> abs_fset) op #" |
|
632 by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset]) |
|
633 |
629 lemma [quot_preserve]: |
634 lemma [quot_preserve]: |
630 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
635 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
631 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
636 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
632 abs_o_rep[OF Quotient_fset] map_id finsert_def) |
637 abs_o_rep[OF Quotient_fset] map_id finsert_def) |
633 |
638 |