author | haftmann |

Tue Jul 10 17:30:51 2007 +0200 (2007-07-10) | |

changeset 23710 | a8ac2305eaf2 |

parent 23709 | fd31da8f752a |

child 23711 | dc452e8641aa |

removed proof dependency on transitivity theorems

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: