author | haftmann |

Tue Aug 16 19:47:50 2011 +0200 (2011-08-16) | |

changeset 44242 | a5cb6aa77ffc |

parent 44228 | 5f974bead436 |

child 44243 | d58864221eef |

avoid Collect_def in proof

1.1 --- a/src/HOL/Quotient.thy Tue Aug 16 07:56:17 2011 -0700 1.2 +++ b/src/HOL/Quotient.thy Tue Aug 16 19:47:50 2011 +0200 1.3 @@ -643,10 +643,18 @@ 1.4 have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop) 1.5 then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto 1.6 have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" 1.7 - by (metis Collect_def abs_inverse) 1.8 + proof - 1.9 + assume "R r r" and "R s s" 1.10 + then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)" 1.11 + by (metis abs_inverse) 1.12 + also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))" 1.13 + by rule simp_all 1.14 + finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp 1.15 + qed 1.16 then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))" 1.17 using equivp[simplified part_equivp_def] by metis 1.18 qed 1.19 + 1.20 end 1.21 1.22 subsection {* ML setup *}