src/HOL/Typedef.thy
changeset 23710 a8ac2305eaf2
parent 23433 c2c10abd2a1e
child 24269 4b2aac7669b3
     1.1 --- a/src/HOL/Typedef.thy	Tue Jul 10 17:30:50 2007 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Tue Jul 10 17:30:51 2007 +0200
     1.3 @@ -29,10 +29,10 @@
     1.4    "(Rep x = Rep y) = (x = y)"
     1.5  proof
     1.6    assume "Rep x = Rep y"
     1.7 -  hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
     1.8 -  also have "Abs (Rep x) = x" by (rule Rep_inverse)
     1.9 -  also have "Abs (Rep y) = y" by (rule Rep_inverse)
    1.10 -  finally show "x = y" .
    1.11 +  then have "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    1.12 +  moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
    1.13 +  moreover have "Abs (Rep y) = y" by (rule Rep_inverse)
    1.14 +  ultimately show "x = y" by simp
    1.15  next
    1.16    assume "x = y"
    1.17    thus "Rep x = Rep y" by (simp only:)
    1.18 @@ -43,10 +43,10 @@
    1.19    shows "(Abs x = Abs y) = (x = y)"
    1.20  proof
    1.21    assume "Abs x = Abs y"
    1.22 -  hence "Rep (Abs x) = Rep (Abs y)" by (simp only:)
    1.23 -  also from x have "Rep (Abs x) = x" by (rule Abs_inverse)
    1.24 -  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    1.25 -  finally show "x = y" .
    1.26 +  then have "Rep (Abs x) = Rep (Abs y)" by (simp only:)
    1.27 +  moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse)
    1.28 +  moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    1.29 +  ultimately show "x = y" by simp
    1.30  next
    1.31    assume "x = y"
    1.32    thus "Abs x = Abs y" by (simp only:)
    1.33 @@ -76,8 +76,8 @@
    1.34    shows "P y"
    1.35  proof -
    1.36    have "P (Rep (Abs y))" by (rule hyp)
    1.37 -  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    1.38 -  finally show "P y" .
    1.39 +  moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    1.40 +  ultimately show "P y" by simp
    1.41  qed
    1.42  
    1.43  lemma Abs_induct [induct type]:
    1.44 @@ -85,9 +85,9 @@
    1.45    shows "P x"
    1.46  proof -
    1.47    have "Rep x \<in> A" by (rule Rep)
    1.48 -  hence "P (Abs (Rep x))" by (rule r)
    1.49 -  also have "Abs (Rep x) = x" by (rule Rep_inverse)
    1.50 -  finally show "P x" .
    1.51 +  then have "P (Abs (Rep x))" by (rule r)
    1.52 +  moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
    1.53 +  ultimately show "P x" by simp
    1.54  qed
    1.55  
    1.56  lemma Rep_range: