summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 20 Oct 2000 19:46:53 +0200 | |

changeset 10284 | ec98fc455272 |

parent 10283 | ff003e2b790c |

child 10285 | 6949e17f314a |

tuned;

--- a/src/HOL/subset.thy Fri Oct 20 14:17:08 2000 +0200 +++ b/src/HOL/subset.thy Fri Oct 20 19:46:53 2000 +0200 @@ -50,6 +50,24 @@ qed qed +theorem Abs_inject: + "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)" +proof - + assume tydef: "type_definition Rep Abs A" + assume x: "x \<in> A" and y: "y \<in> A" + show ?thesis + proof + assume "Abs x = Abs y" + hence "Rep (Abs x) = Rep (Abs y)" by simp + moreover note x hence "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef]) + moreover note y hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) + ultimately show "x = y" by (simp only:) + next + assume "x = y" + thus "Abs x = Abs y" by simp + qed +qed + theorem Rep_cases: "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P" proof - @@ -75,24 +93,6 @@ qed qed -theorem Abs_inject: - "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)" -proof - - assume tydef: "type_definition Rep Abs A" - assume x: "x \<in> A" and y: "y \<in> A" - show ?thesis - proof - assume "Abs x = Abs y" - hence "Rep (Abs x) = Rep (Abs y)" by simp - moreover note x hence "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef]) - moreover note y hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) - ultimately show "x = y" by (simp only:) - next - assume "x = y" - thus "Abs x = Abs y" by simp - qed -qed - theorem Rep_induct: "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y" proof -