src/HOL/Typedef.thy
 author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 61799 4cf66f21b764 child 63434 c956d995bec6 permissions -rw-r--r--
generalize more theorems to support enat and ennreal
 wenzelm@11608 1 (* Title: HOL/Typedef.thy wenzelm@11608 2 Author: Markus Wenzel, TU Munich wenzelm@11743 3 *) wenzelm@11608 4 wenzelm@60758 5 section \HOL type definitions\ wenzelm@11608 6 nipkow@15131 7 theory Typedef nipkow@15140 8 imports Set wenzelm@46950 9 keywords "typedef" :: thy_goal and "morphisms" nipkow@15131 10 begin wenzelm@11608 11 wenzelm@13412 12 locale type_definition = wenzelm@13412 13 fixes Rep and Abs and A wenzelm@13412 14 assumes Rep: "Rep x \ A" wenzelm@13412 15 and Rep_inverse: "Abs (Rep x) = x" wenzelm@61102 16 and Abs_inverse: "y \ A \ Rep (Abs y) = y" wenzelm@61799 17 \ \This will be axiomatized for each typedef!\ haftmann@23247 18 begin wenzelm@11608 19 wenzelm@61102 20 lemma Rep_inject: "Rep x = Rep y \ x = y" wenzelm@13412 21 proof wenzelm@13412 22 assume "Rep x = Rep y" haftmann@23710 23 then have "Abs (Rep x) = Abs (Rep y)" by (simp only:) haftmann@23710 24 moreover have "Abs (Rep x) = x" by (rule Rep_inverse) haftmann@23710 25 moreover have "Abs (Rep y) = y" by (rule Rep_inverse) haftmann@23710 26 ultimately show "x = y" by simp wenzelm@13412 27 next wenzelm@13412 28 assume "x = y" wenzelm@61102 29 then show "Rep x = Rep y" by (simp only:) wenzelm@13412 30 qed wenzelm@11608 31 haftmann@23247 32 lemma Abs_inject: wenzelm@61102 33 assumes "x \ A" and "y \ A" wenzelm@61102 34 shows "Abs x = Abs y \ x = y" wenzelm@13412 35 proof wenzelm@13412 36 assume "Abs x = Abs y" haftmann@23710 37 then have "Rep (Abs x) = Rep (Abs y)" by (simp only:) wenzelm@61102 38 moreover from \x \ A\ have "Rep (Abs x) = x" by (rule Abs_inverse) wenzelm@61102 39 moreover from \y \ A\ have "Rep (Abs y) = y" by (rule Abs_inverse) haftmann@23710 40 ultimately show "x = y" by simp wenzelm@13412 41 next wenzelm@13412 42 assume "x = y" wenzelm@61102 43 then show "Abs x = Abs y" by (simp only:) wenzelm@11608 44 qed wenzelm@11608 45 haftmann@23247 46 lemma Rep_cases [cases set]: wenzelm@61102 47 assumes "y \ A" wenzelm@61102 48 and hyp: "\x. y = Rep x \ P" wenzelm@13412 49 shows P wenzelm@13412 50 proof (rule hyp) wenzelm@61102 51 from \y \ A\ have "Rep (Abs y) = y" by (rule Abs_inverse) wenzelm@61102 52 then show "y = Rep (Abs y)" .. wenzelm@11608 53 qed wenzelm@11608 54 haftmann@23247 55 lemma Abs_cases [cases type]: wenzelm@61102 56 assumes r: "\y. x = Abs y \ y \ A \ P" wenzelm@13412 57 shows P wenzelm@13412 58 proof (rule r) wenzelm@13412 59 have "Abs (Rep x) = x" by (rule Rep_inverse) wenzelm@61102 60 then show "x = Abs (Rep x)" .. wenzelm@13412 61 show "Rep x \ A" by (rule Rep) wenzelm@11608 62 qed wenzelm@11608 63 haftmann@23247 64 lemma Rep_induct [induct set]: wenzelm@13412 65 assumes y: "y \ A" wenzelm@61102 66 and hyp: "\x. P (Rep x)" wenzelm@13412 67 shows "P y" wenzelm@11608 68 proof - wenzelm@13412 69 have "P (Rep (Abs y))" by (rule hyp) haftmann@23710 70 moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse) haftmann@23710 71 ultimately show "P y" by simp wenzelm@11608 72 qed wenzelm@11608 73 haftmann@23247 74 lemma Abs_induct [induct type]: wenzelm@61102 75 assumes r: "\y. y \ A \ P (Abs y)" wenzelm@13412 76 shows "P x" wenzelm@11608 77 proof - wenzelm@13412 78 have "Rep x \ A" by (rule Rep) haftmann@23710 79 then have "P (Abs (Rep x))" by (rule r) haftmann@23710 80 moreover have "Abs (Rep x) = x" by (rule Rep_inverse) haftmann@23710 81 ultimately show "P x" by simp wenzelm@11608 82 qed wenzelm@11608 83 huffman@27295 84 lemma Rep_range: "range Rep = A" huffman@24269 85 proof wenzelm@61102 86 show "range Rep \ A" using Rep by (auto simp add: image_def) wenzelm@61102 87 show "A \ range Rep" nipkow@23433 88 proof wenzelm@61102 89 fix x assume "x \ A" wenzelm@61102 90 then have "x = Rep (Abs x)" by (rule Abs_inverse [symmetric]) wenzelm@61102 91 then show "x \ range Rep" by (rule range_eqI) nipkow@23433 92 qed nipkow@23433 93 qed nipkow@23433 94 huffman@27295 95 lemma Abs_image: "Abs ` A = UNIV" huffman@27295 96 proof wenzelm@61102 97 show "Abs ` A \ UNIV" by (rule subset_UNIV) wenzelm@61102 98 show "UNIV \ Abs ` A" huffman@27295 99 proof huffman@27295 100 fix x huffman@27295 101 have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) wenzelm@61102 102 moreover have "Rep x \ A" by (rule Rep) wenzelm@61102 103 ultimately show "x \ Abs ` A" by (rule image_eqI) huffman@27295 104 qed huffman@27295 105 qed huffman@27295 106 haftmann@23247 107 end haftmann@23247 108 blanchet@58239 109 ML_file "Tools/typedef.ML" wenzelm@11608 110 wenzelm@11608 111 end