src/HOL/Lifting.thy
 changeset 58186 a6c3962ea907 parent 58177 166131276380 child 58821 11e226e8a095
1.1 --- a/src/HOL/Lifting.thy	Fri Sep 05 00:41:00 2014 +0200
1.2 +++ b/src/HOL/Lifting.thy	Fri Sep 05 00:41:01 2014 +0200
1.3 @@ -28,7 +28,7 @@
1.5  definition
1.6    "Quotient R Abs Rep T \<longleftrightarrow>
1.7 -     (\<forall>a. Abs (Rep a) = a) \<and>
1.8 +     (\<forall>a. Abs (Rep a) = a) \<and>
1.9       (\<forall>a. R (Rep a) (Rep a)) \<and>
1.10       (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
1.11       T = (\<lambda>x y. R x x \<and> Abs x = y)"
1.12 @@ -83,8 +83,8 @@
1.13    using a unfolding Quotient_def
1.14    by blast
1.16 -lemma Quotient_rep_abs_fold_unmap:
1.17 -  assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'"
1.18 +lemma Quotient_rep_abs_fold_unmap:
1.19 +  assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'"
1.20    shows "R (Rep' x') x"
1.21  proof -
1.22    have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto
1.23 @@ -92,7 +92,7 @@
1.24  qed
1.26  lemma Quotient_Rep_eq:
1.27 -  assumes "x' \<equiv> Abs x"
1.28 +  assumes "x' \<equiv> Abs x"
1.29    shows "Rep x' \<equiv> Rep x'"
1.30  by simp
1.32 @@ -120,7 +120,7 @@
1.33  end
1.35  lemma identity_quotient: "Quotient (op =) id id (op =)"
1.36 -unfolding Quotient_def by simp
1.37 +unfolding Quotient_def by simp
1.39  text {* TODO: Use one of these alternatives as the real definition. *}
1.41 @@ -221,7 +221,7 @@
1.42    shows "Quotient (op =) Abs Rep T"
1.43  proof -
1.44    interpret type_definition Rep Abs UNIV by fact
1.45 -  from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
1.46 +  from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
1.47      by (fastforce intro!: QuotientI fun_eq_iff)
1.48  qed
1.50 @@ -330,11 +330,11 @@
1.51  (* the following two theorems are here only for convinience *)
1.53  lemma typedef_right_unique: "right_unique T"
1.54 -  using T_def type Quotient_right_unique typedef_to_Quotient
1.55 +  using T_def type Quotient_right_unique typedef_to_Quotient
1.56    by blast
1.58  lemma typedef_right_total: "right_total T"
1.59 -  using T_def type Quotient_right_total typedef_to_Quotient
1.60 +  using T_def type Quotient_right_total typedef_to_Quotient
1.61    by blast
1.63  lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
1.64 @@ -503,7 +503,7 @@
1.65    assumes "(A ===> op=) P' P"
1.66    shows "Domainp (A OO B) = P'"
1.67  using assms
1.68 -unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def
1.69 +unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def
1.70  by (fast intro: fun_eq_iff)
1.72  lemma pcr_Domainp_par:
1.73 @@ -526,12 +526,12 @@
1.74    assumes "left_total B"
1.75    assumes "Domainp A = P"
1.76    shows "Domainp (A OO B) = P"
1.77 -using assms unfolding left_total_def
1.78 +using assms unfolding left_total_def
1.79  by fast
1.81  lemma Quotient_to_Domainp:
1.82    assumes "Quotient R Abs Rep T"
1.83 -  shows "Domainp T = (\<lambda>x. R x x)"
1.84 +  shows "Domainp T = (\<lambda>x. R x x)"
1.85  by (simp add: Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
1.87  lemma eq_onp_to_Domainp:
1.88 @@ -559,7 +559,7 @@
1.89  ML_file "Tools/Lifting/lifting_term.ML"
1.90  ML_file "Tools/Lifting/lifting_def.ML"
1.91  ML_file "Tools/Lifting/lifting_setup.ML"
1.92 -
1.93 +
1.94  hide_const (open) POS NEG
1.96  end