src/HOL/Lifting.thy
 changeset 47651 8e4f50afd21a parent 47575 b90cd7016d4f child 47652 1b722b100301
equal inserted replaced
47650:33ecf14d5ee9 47651:8e4f50afd21a
`   268 `
`   268 `
`   269 lemma open_typedef_to_Quotient:`
`   269 lemma open_typedef_to_Quotient:`
`   270   assumes "type_definition Rep Abs {x. P x}"`
`   270   assumes "type_definition Rep Abs {x. P x}"`
`   271   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"`
`   271   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"`
`   272   shows "Quotient (invariant P) Abs Rep T"`
`   272   shows "Quotient (invariant P) Abs Rep T"`
`   273 proof -`
`   273   using typedef_to_Quotient [OF assms] by simp`
`   274   interpret type_definition Rep Abs "{x. P x}" by fact`
`       `
`   275   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis`
`       `
`   276     by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)`
`       `
`   277 qed`
`       `
`   278 `
`   274 `
`   279 lemma open_typedef_to_part_equivp:`
`   275 lemma open_typedef_to_part_equivp:`
`   280   assumes "type_definition Rep Abs {x. P x}"`
`   276   assumes "type_definition Rep Abs {x. P x}"`
`   281   shows "part_equivp (invariant P)"`
`   277   shows "part_equivp (invariant P)"`
`   282 proof (intro part_equivpI)`
`   278   using typedef_to_part_equivp [OF assms] by simp`
`   283   interpret type_definition Rep Abs "{x. P x}" by fact`
`       `
`   284   show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)`
`       `
`   285 next`
`       `
`   286   show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)`
`       `
`   287 next`
`       `
`   288   show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)`
`       `
`   289 qed`
`       `
`   290 `
`   279 `
`   291 text {* Generating transfer rules for quotients. *}`
`   280 text {* Generating transfer rules for quotients. *}`
`   292 `
`   281 `
`   293 context`
`   282 context`
`   294   fixes R Abs Rep T`
`   283   fixes R Abs Rep T`