wenzelm@11608: (* Title: HOL/Typedef.thy
wenzelm@11608: Author: Markus Wenzel, TU Munich
wenzelm@11743: *)
wenzelm@11608:
wenzelm@60758: section \HOL type definitions\
wenzelm@11608:
nipkow@15131: theory Typedef
nipkow@15140: imports Set
wenzelm@63434: keywords
wenzelm@69913: "typedef" :: thy_goal_defn and
wenzelm@63434: "morphisms" :: quasi_command
nipkow@15131: begin
wenzelm@11608:
wenzelm@13412: locale type_definition =
wenzelm@13412: fixes Rep and Abs and A
wenzelm@13412: assumes Rep: "Rep x \ A"
wenzelm@13412: and Rep_inverse: "Abs (Rep x) = x"
wenzelm@61102: and Abs_inverse: "y \ A \ Rep (Abs y) = y"
wenzelm@61799: \ \This will be axiomatized for each typedef!\
haftmann@23247: begin
wenzelm@11608:
wenzelm@61102: lemma Rep_inject: "Rep x = Rep y \ x = y"
wenzelm@13412: proof
wenzelm@13412: assume "Rep x = Rep y"
haftmann@23710: then have "Abs (Rep x) = Abs (Rep y)" by (simp only:)
haftmann@23710: moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
haftmann@23710: moreover have "Abs (Rep y) = y" by (rule Rep_inverse)
haftmann@23710: ultimately show "x = y" by simp
wenzelm@13412: next
wenzelm@13412: assume "x = y"
wenzelm@61102: then show "Rep x = Rep y" by (simp only:)
wenzelm@13412: qed
wenzelm@11608:
haftmann@23247: lemma Abs_inject:
wenzelm@61102: assumes "x \ A" and "y \ A"
wenzelm@61102: shows "Abs x = Abs y \ x = y"
wenzelm@13412: proof
wenzelm@13412: assume "Abs x = Abs y"
haftmann@23710: then have "Rep (Abs x) = Rep (Abs y)" by (simp only:)
wenzelm@61102: moreover from \x \ A\ have "Rep (Abs x) = x" by (rule Abs_inverse)
wenzelm@61102: moreover from \y \ A\ have "Rep (Abs y) = y" by (rule Abs_inverse)
haftmann@23710: ultimately show "x = y" by simp
wenzelm@13412: next
wenzelm@13412: assume "x = y"
wenzelm@61102: then show "Abs x = Abs y" by (simp only:)
wenzelm@11608: qed
wenzelm@11608:
haftmann@23247: lemma Rep_cases [cases set]:
wenzelm@61102: assumes "y \ A"
wenzelm@61102: and hyp: "\x. y = Rep x \ P"
wenzelm@13412: shows P
wenzelm@13412: proof (rule hyp)
wenzelm@61102: from \y \ A\ have "Rep (Abs y) = y" by (rule Abs_inverse)
wenzelm@61102: then show "y = Rep (Abs y)" ..
wenzelm@11608: qed
wenzelm@11608:
haftmann@23247: lemma Abs_cases [cases type]:
wenzelm@61102: assumes r: "\y. x = Abs y \ y \ A \ P"
wenzelm@13412: shows P
wenzelm@13412: proof (rule r)
wenzelm@13412: have "Abs (Rep x) = x" by (rule Rep_inverse)
wenzelm@61102: then show "x = Abs (Rep x)" ..
wenzelm@13412: show "Rep x \ A" by (rule Rep)
wenzelm@11608: qed
wenzelm@11608:
haftmann@23247: lemma Rep_induct [induct set]:
wenzelm@13412: assumes y: "y \ A"
wenzelm@61102: and hyp: "\x. P (Rep x)"
wenzelm@13412: shows "P y"
wenzelm@11608: proof -
wenzelm@13412: have "P (Rep (Abs y))" by (rule hyp)
haftmann@23710: moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
haftmann@23710: ultimately show "P y" by simp
wenzelm@11608: qed
wenzelm@11608:
haftmann@23247: lemma Abs_induct [induct type]:
wenzelm@61102: assumes r: "\y. y \ A \ P (Abs y)"
wenzelm@13412: shows "P x"
wenzelm@11608: proof -
wenzelm@13412: have "Rep x \ A" by (rule Rep)
haftmann@23710: then have "P (Abs (Rep x))" by (rule r)
haftmann@23710: moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
haftmann@23710: ultimately show "P x" by simp
wenzelm@11608: qed
wenzelm@11608:
huffman@27295: lemma Rep_range: "range Rep = A"
huffman@24269: proof
wenzelm@61102: show "range Rep \ A" using Rep by (auto simp add: image_def)
wenzelm@61102: show "A \ range Rep"
nipkow@23433: proof
wenzelm@61102: fix x assume "x \ A"
wenzelm@61102: then have "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])
wenzelm@61102: then show "x \ range Rep" by (rule range_eqI)
nipkow@23433: qed
nipkow@23433: qed
nipkow@23433:
huffman@27295: lemma Abs_image: "Abs ` A = UNIV"
huffman@27295: proof
wenzelm@61102: show "Abs ` A \ UNIV" by (rule subset_UNIV)
wenzelm@61102: show "UNIV \ Abs ` A"
huffman@27295: proof
huffman@27295: fix x
huffman@27295: have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
wenzelm@61102: moreover have "Rep x \ A" by (rule Rep)
wenzelm@61102: ultimately show "x \ Abs ` A" by (rule image_eqI)
huffman@27295: qed
huffman@27295: qed
huffman@27295:
haftmann@23247: end
haftmann@23247:
wenzelm@69605: ML_file \Tools/typedef.ML\
wenzelm@11608:
wenzelm@11608: end