src/HOL/Lifting.thy
 changeset 57398 882091eb1e9a parent 56524 f4ba736040fa child 57961 10b2f60b70f0
equal inserted replaced
57397:5004aca20821 57398:882091eb1e9a
`   161     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"`
`   161     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"`
`   162   unfolding Quotient_alt_def3 fun_eq_iff by auto`
`   162   unfolding Quotient_alt_def3 fun_eq_iff by auto`
`   163 `
`   163 `
`   164 lemma Quotient_alt_def5:`
`   164 lemma Quotient_alt_def5:`
`   165   "Quotient R Abs Rep T \<longleftrightarrow>`
`   165   "Quotient R Abs Rep T \<longleftrightarrow>`
`   166     T \<le> BNF_Util.Grp UNIV Abs \<and> BNF_Util.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"`
`   166     T \<le> BNF_Def.Grp UNIV Abs \<and> BNF_Def.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"`
`   167   unfolding Quotient_alt_def4 Grp_def by blast`
`   167   unfolding Quotient_alt_def4 Grp_def by blast`
`   168 `
`   168 `
`   169 lemma fun_quotient:`
`   169 lemma fun_quotient:`
`   170   assumes 1: "Quotient R1 abs1 rep1 T1"`
`   170   assumes 1: "Quotient R1 abs1 rep1 T1"`
`   171   assumes 2: "Quotient R2 abs2 rep2 T2"`
`   171   assumes 2: "Quotient R2 abs2 rep2 T2"`