src/HOL/Lifting.thy
changeset 47651 8e4f50afd21a
parent 47575 b90cd7016d4f
child 47652 1b722b100301
equal deleted 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