equal
deleted
inserted
replaced
174 |
174 |
175 lemma set_transfer [transfer_rule]: |
175 lemma set_transfer [transfer_rule]: |
176 "(list_all2 A ===> set_rel A) set set" |
176 "(list_all2 A ===> set_rel A) set set" |
177 unfolding set_def by transfer_prover |
177 unfolding set_def by transfer_prover |
178 |
178 |
|
179 lemma lists_transfer [transfer_rule]: |
|
180 "(set_rel A ===> set_rel (list_all2 A)) lists lists" |
|
181 apply (rule fun_relI, rule set_relI) |
|
182 apply (erule lists.induct, simp) |
|
183 apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons) |
|
184 apply (erule lists.induct, simp) |
|
185 apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons) |
|
186 done |
|
187 |
179 subsection {* Setup for lifting package *} |
188 subsection {* Setup for lifting package *} |
180 |
189 |
181 lemma Quotient_list[quot_map]: |
190 lemma Quotient_list[quot_map]: |
182 assumes "Quotient R Abs Rep T" |
191 assumes "Quotient R Abs Rep T" |
183 shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)" |
192 shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)" |