src/HOL/Lifting.thy
 changeset 47369 f483be2fecb9 parent 47368 4c522dff1f4d parent 47361 87c0eaf04bad child 47376 776254f89a18
```     1.1 --- a/src/HOL/Lifting.thy	Wed Apr 04 16:48:39 2012 +0200
1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 04 20:45:19 2012 +0200
1.3 @@ -236,16 +236,17 @@
1.4    shows "invariant P x x \<equiv> P x"
1.5  using assms by (auto simp add: invariant_def)
1.6
1.7 -lemma copy_type_to_Quotient:
1.8 +lemma UNIV_typedef_to_Quotient:
1.9    assumes "type_definition Rep Abs UNIV"
1.10 -  and T_def: "T \<equiv> (\<lambda>x y. Abs x = y)"
1.11 +  and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
1.12    shows "Quotient (op =) Abs Rep T"
1.13  proof -
1.14    interpret type_definition Rep Abs UNIV by fact
1.15 -  from Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI)
1.16 +  from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
1.17 +    by (fastforce intro!: QuotientI fun_eq_iff)
1.18  qed
1.19
1.20 -lemma copy_type_to_equivp:
1.21 +lemma UNIV_typedef_to_equivp:
1.22    fixes Abs :: "'a \<Rightarrow> 'b"
1.23    and Rep :: "'b \<Rightarrow> 'a"
1.24    assumes "type_definition Rep Abs (UNIV::'a set)"
1.25 @@ -253,6 +254,28 @@
1.26  by (rule identity_equivp)
1.27
1.28  lemma typedef_to_Quotient:
1.29 +  assumes "type_definition Rep Abs S"
1.30 +  and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
1.31 +  shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
1.32 +proof -
1.33 +  interpret type_definition Rep Abs S by fact
1.34 +  from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
1.35 +    by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
1.36 +qed
1.37 +
1.38 +lemma typedef_to_part_equivp:
1.39 +  assumes "type_definition Rep Abs S"
1.40 +  shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
1.41 +proof (intro part_equivpI)
1.42 +  interpret type_definition Rep Abs S by fact
1.43 +  show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
1.44 +next
1.45 +  show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
1.46 +next
1.47 +  show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
1.48 +qed
1.49 +
1.50 +lemma open_typedef_to_Quotient:
1.51    assumes "type_definition Rep Abs {x. P x}"
1.52    and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
1.53    shows "Quotient (invariant P) Abs Rep T"
1.54 @@ -262,16 +285,7 @@
1.55      by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
1.56  qed
1.57
1.58 -lemma invariant_type_to_Quotient:
1.59 -  assumes "type_definition Rep Abs {x. P x}"
1.60 -  and T_def: "T \<equiv> (\<lambda>x y. (invariant P) x x \<and> Abs x = y)"
1.61 -  shows "Quotient (invariant P) Abs Rep T"
1.62 -proof -
1.63 -  interpret type_definition Rep Abs "{x. P x}" by fact
1.64 -  from Rep Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI simp: invariant_def)
1.65 -qed
1.66 -
1.67 -lemma invariant_type_to_part_equivp:
1.68 +lemma open_typedef_to_part_equivp:
1.69    assumes "type_definition Rep Abs {x. P x}"
1.70    shows "part_equivp (invariant P)"
1.71  proof (intro part_equivpI)
```