632 done |
632 done |
633 |
633 |
634 lemma insert_preserve2: |
634 lemma insert_preserve2: |
635 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
635 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
636 (id ---> rep_fset ---> abs_fset) op #" |
636 (id ---> rep_fset ---> abs_fset) op #" |
637 by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset]) |
637 by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset]) |
638 |
638 |
639 lemma [quot_preserve]: |
639 lemma [quot_preserve]: |
640 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
640 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
641 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
641 by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset] |
642 abs_o_rep[OF Quotient_fset] map_id finsert_def) |
642 abs_o_rep[OF Quotient_fset] map_id finsert_def) |
643 |
643 |
644 lemma [quot_preserve]: |
644 lemma [quot_preserve]: |
645 "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion" |
645 "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion" |
646 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
646 by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset] |
647 abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
647 abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
648 |
648 |
649 lemma list_all2_app_l: |
649 lemma list_all2_app_l: |
650 assumes a: "reflp R" |
650 assumes a: "reflp R" |
651 and b: "list_all2 R l r" |
651 and b: "list_all2 R l r" |
856 shows "(x \<approx> y) = (set x = set y)" |
856 shows "(x \<approx> y) = (set x = set y)" |
857 by auto |
857 by auto |
858 |
858 |
859 lemma inj_map_eq_iff: |
859 lemma inj_map_eq_iff: |
860 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
860 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
861 by (simp add: expand_set_eq[symmetric] inj_image_eq_iff) |
861 by (simp add: set_eq_iff[symmetric] inj_image_eq_iff) |
862 |
862 |
863 text {* alternate formulation with a different decomposition principle |
863 text {* alternate formulation with a different decomposition principle |
864 and a proof of equivalence *} |
864 and a proof of equivalence *} |
865 |
865 |
866 inductive |
866 inductive |
1269 by (simp add: fminus_red) |
1269 by (simp add: fminus_red) |
1270 |
1270 |
1271 lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)" |
1271 lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)" |
1272 by (simp add: fminus_red) |
1272 by (simp add: fminus_red) |
1273 |
1273 |
1274 lemma expand_fset_eq: |
1274 lemma fset_eq_iff: |
1275 "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))" |
1275 "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))" |
1276 by (lifting list_eq.simps[simplified memb_def[symmetric]]) |
1276 by (lifting list_eq.simps[simplified memb_def[symmetric]]) |
1277 |
1277 |
1278 (* We cannot write it as "assumes .. shows" since Isabelle changes |
1278 (* We cannot write it as "assumes .. shows" since Isabelle changes |
1279 the quantifiers to schematic variables and reintroduces them in |
1279 the quantifiers to schematic variables and reintroduces them in |