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.4  
     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.15  
    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.25  
    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.31  
    1.32 @@ -120,7 +120,7 @@
    1.33  end
    1.34  
    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.38  
    1.39  text {* TODO: Use one of these alternatives as the real definition. *}
    1.40  
    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.49  
    1.50 @@ -330,11 +330,11 @@
    1.51  (* the following two theorems are here only for convinience *)
    1.52  
    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.57  
    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.62  
    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.71  
    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.80  
    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.86  
    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.95  
    1.96  end