summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Quotient.thy

changeset 10278 | ea1bf4b6255c |

parent 10250 | ca93fe25a84b |

child 10285 | 6949e17f314a |

1.1 --- a/src/HOL/Library/Quotient.thy Thu Oct 19 21:22:44 2000 +0200 1.2 +++ b/src/HOL/Library/Quotient.thy Thu Oct 19 21:23:15 2000 +0200 1.3 @@ -162,51 +162,6 @@ 1.4 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" 1.5 by (unfold quot_def) blast 1.6 1.7 - 1.8 -text {* 1.9 - \medskip Standard properties of type-definitions.\footnote{(FIXME) 1.10 - Better incorporate these into the typedef package?} 1.11 -*} 1.12 - 1.13 -theorem Rep_quot_inject: "(Rep_quot x = Rep_quot y) = (x = y)" 1.14 -proof 1.15 - assume "Rep_quot x = Rep_quot y" 1.16 - hence "Abs_quot (Rep_quot x) = Abs_quot (Rep_quot y)" by (simp only:) 1.17 - thus "x = y" by (simp only: Rep_quot_inverse) 1.18 -next 1.19 - assume "x = y" 1.20 - thus "Rep_quot x = Rep_quot y" by simp 1.21 -qed 1.22 - 1.23 -theorem Abs_quot_inject: 1.24 - "x \<in> quot ==> y \<in> quot ==> (Abs_quot x = Abs_quot y) = (x = y)" 1.25 -proof 1.26 - assume "Abs_quot x = Abs_quot y" 1.27 - hence "Rep_quot (Abs_quot x) = Rep_quot (Abs_quot y)" by simp 1.28 - also assume "x \<in> quot" hence "Rep_quot (Abs_quot x) = x" by (rule Abs_quot_inverse) 1.29 - also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse) 1.30 - finally show "x = y" . 1.31 -next 1.32 - assume "x = y" 1.33 - thus "Abs_quot x = Abs_quot y" by simp 1.34 -qed 1.35 - 1.36 -theorem Rep_quot_induct: "y \<in> quot ==> (!!x. P (Rep_quot x)) ==> P y" 1.37 -proof - 1.38 - assume "!!x. P (Rep_quot x)" hence "P (Rep_quot (Abs_quot y))" . 1.39 - also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse) 1.40 - finally show "P y" . 1.41 -qed 1.42 - 1.43 -theorem Abs_quot_induct: "(!!y. y \<in> quot ==> P (Abs_quot y)) ==> P x" 1.44 -proof - 1.45 - assume r: "!!y. y \<in> quot ==> P (Abs_quot y)" 1.46 - have "Rep_quot x \<in> quot" by (rule Rep_quot) 1.47 - hence "P (Abs_quot (Rep_quot x))" by (rule r) 1.48 - also have "Abs_quot (Rep_quot x) = x" by (rule Rep_quot_inverse) 1.49 - finally show "P x" . 1.50 -qed 1.51 - 1.52 text {* 1.53 \medskip Abstracted equivalence classes are the canonical 1.54 representation of elements of a quotient type. 1.55 @@ -217,13 +172,11 @@ 1.56 "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" 1.57 1.58 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>" 1.59 -proof (unfold eqv_class_def) 1.60 - show "\<exists>a. A = Abs_quot {x. a \<sim> x}" 1.61 - proof (induct A rule: Abs_quot_induct) 1.62 - fix R assume "R \<in> quot" 1.63 - hence "\<exists>a. R = {x. a \<sim> x}" by blast 1.64 - thus "\<exists>a. Abs_quot R = Abs_quot {x. a \<sim> x}" by blast 1.65 - qed 1.66 +proof (cases A) 1.67 + fix R assume R: "A = Abs_quot R" 1.68 + assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast 1.69 + with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast 1.70 + thus ?thesis by (unfold eqv_class_def) 1.71 qed 1.72 1.73 lemma quot_cases [case_names rep, cases type: quot]: 1.74 @@ -302,10 +255,10 @@ 1.75 show "a \<in> domain" .. 1.76 qed 1.77 1.78 -theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)" (* FIXME tune proof *) 1.79 +theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)" 1.80 proof (cases A) 1.81 fix a assume a: "A = \<lfloor>a\<rfloor>" 1.82 - hence "pick A \<sim> a" by (simp only: pick_eqv) 1.83 + hence "pick A \<sim> a" by simp 1.84 hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp 1.85 with a show ?thesis by simp 1.86 qed