equal
deleted
inserted
replaced
69 |
69 |
70 lemma abs_fset_eq_iff: "abs_fset xs = abs_fset ys \<longleftrightarrow> list_eq xs ys" |
70 lemma abs_fset_eq_iff: "abs_fset xs = abs_fset ys \<longleftrightarrow> list_eq xs ys" |
71 using Quotient_rel [OF Quotient_fset] by simp |
71 using Quotient_rel [OF Quotient_fset] by simp |
72 |
72 |
73 lift_definition fconcat :: "'a fset fset \<Rightarrow> 'a fset" is concat parametric concat_transfer |
73 lift_definition fconcat :: "'a fset fset \<Rightarrow> 'a fset" is concat parametric concat_transfer |
74 proof - |
74 proof (simp only: fset.pcr_cr_eq) |
75 fix xss yss :: "'a list list" |
75 fix xss yss :: "'a list list" |
76 assume "(list_all2 cr_fset OO list_eq OO (list_all2 cr_fset)\<inverse>\<inverse>) xss yss" |
76 assume "(list_all2 cr_fset OO list_eq OO (list_all2 cr_fset)\<inverse>\<inverse>) xss yss" |
77 then obtain uss vss where |
77 then obtain uss vss where |
78 "list_all2 cr_fset xss uss" and "list_eq uss vss" and |
78 "list_all2 cr_fset xss uss" and "list_eq uss vss" and |
79 "list_all2 cr_fset yss vss" by clarsimp |
79 "list_all2 cr_fset yss vss" by clarsimp |