src/HOL/Typedef.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 16417 9bc16273c2d4 child 19459 2041d472fc17 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
 wenzelm@11608 1 (* Title: HOL/Typedef.thy wenzelm@11608 2 ID: \$Id\$ wenzelm@11608 3 Author: Markus Wenzel, TU Munich wenzelm@11743 4 *) wenzelm@11608 5 wenzelm@11979 6 header {* HOL type definitions *} wenzelm@11608 7 nipkow@15131 8 theory Typedef nipkow@15140 9 imports Set haftmann@16417 10 uses ("Tools/typedef_package.ML") nipkow@15131 11 begin wenzelm@11608 12 wenzelm@13412 13 locale type_definition = wenzelm@13412 14 fixes Rep and Abs and A wenzelm@13412 15 assumes Rep: "Rep x \ A" wenzelm@13412 16 and Rep_inverse: "Abs (Rep x) = x" wenzelm@13412 17 and Abs_inverse: "y \ A ==> Rep (Abs y) = y" wenzelm@13412 18 -- {* This will be axiomatized for each typedef! *} wenzelm@11608 19 wenzelm@13412 20 lemma (in type_definition) Rep_inject: wenzelm@13412 21 "(Rep x = Rep y) = (x = y)" wenzelm@13412 22 proof wenzelm@13412 23 assume "Rep x = Rep y" wenzelm@13412 24 hence "Abs (Rep x) = Abs (Rep y)" by (simp only:) wenzelm@13412 25 also have "Abs (Rep x) = x" by (rule Rep_inverse) wenzelm@13412 26 also have "Abs (Rep y) = y" by (rule Rep_inverse) wenzelm@13412 27 finally show "x = y" . wenzelm@13412 28 next wenzelm@13412 29 assume "x = y" wenzelm@13412 30 thus "Rep x = Rep y" by (simp only:) wenzelm@13412 31 qed wenzelm@11608 32 wenzelm@13412 33 lemma (in type_definition) Abs_inject: wenzelm@13412 34 assumes x: "x \ A" and y: "y \ A" wenzelm@13412 35 shows "(Abs x = Abs y) = (x = y)" wenzelm@13412 36 proof wenzelm@13412 37 assume "Abs x = Abs y" wenzelm@13412 38 hence "Rep (Abs x) = Rep (Abs y)" by (simp only:) wenzelm@13412 39 also from x have "Rep (Abs x) = x" by (rule Abs_inverse) wenzelm@13412 40 also from y have "Rep (Abs y) = y" by (rule Abs_inverse) wenzelm@13412 41 finally show "x = y" . wenzelm@13412 42 next wenzelm@13412 43 assume "x = y" wenzelm@13412 44 thus "Abs x = Abs y" by (simp only:) wenzelm@11608 45 qed wenzelm@11608 46 wenzelm@13412 47 lemma (in type_definition) Rep_cases [cases set]: wenzelm@13412 48 assumes y: "y \ A" wenzelm@13412 49 and hyp: "!!x. y = Rep x ==> P" wenzelm@13412 50 shows P wenzelm@13412 51 proof (rule hyp) wenzelm@13412 52 from y have "Rep (Abs y) = y" by (rule Abs_inverse) wenzelm@13412 53 thus "y = Rep (Abs y)" .. wenzelm@11608 54 qed wenzelm@11608 55 wenzelm@13412 56 lemma (in type_definition) Abs_cases [cases type]: wenzelm@13412 57 assumes r: "!!y. x = Abs y ==> y \ A ==> P" wenzelm@13412 58 shows P wenzelm@13412 59 proof (rule r) wenzelm@13412 60 have "Abs (Rep x) = x" by (rule Rep_inverse) wenzelm@13412 61 thus "x = Abs (Rep x)" .. wenzelm@13412 62 show "Rep x \ A" by (rule Rep) wenzelm@11608 63 qed wenzelm@11608 64 wenzelm@13412 65 lemma (in type_definition) Rep_induct [induct set]: wenzelm@13412 66 assumes y: "y \ A" wenzelm@13412 67 and hyp: "!!x. P (Rep x)" wenzelm@13412 68 shows "P y" wenzelm@11608 69 proof - wenzelm@13412 70 have "P (Rep (Abs y))" by (rule hyp) wenzelm@13412 71 also from y have "Rep (Abs y) = y" by (rule Abs_inverse) wenzelm@13412 72 finally show "P y" . wenzelm@11608 73 qed wenzelm@11608 74 wenzelm@13412 75 lemma (in type_definition) Abs_induct [induct type]: wenzelm@13412 76 assumes r: "!!y. y \ A ==> P (Abs y)" wenzelm@13412 77 shows "P x" wenzelm@11608 78 proof - wenzelm@13412 79 have "Rep x \ A" by (rule Rep) wenzelm@11608 80 hence "P (Abs (Rep x))" by (rule r) wenzelm@13412 81 also have "Abs (Rep x) = x" by (rule Rep_inverse) wenzelm@13412 82 finally show "P x" . wenzelm@11608 83 qed wenzelm@11608 84 wenzelm@11608 85 use "Tools/typedef_package.ML" wenzelm@11608 86 berghofe@15260 87 setup TypedefPackage.setup berghofe@15260 88 wenzelm@11608 89 end