improved typedef;
authorwenzelm
Thu Oct 19 21:23:15 2000 +0200 (2000-10-19)
changeset 10278ea1bf4b6255c
parent 10277 081c8641aa11
child 10279 b223a9a3350e
improved typedef;
tuned proofs;
src/HOL/Library/Quotient.thy
     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