wenzelm@11608: (* Title: HOL/Typedef.thy
wenzelm@11608: Author: Markus Wenzel, TU Munich
wenzelm@11743: *)
wenzelm@11608:
wenzelm@11979: header {* HOL type definitions *}
wenzelm@11608:
nipkow@15131: theory Typedef
nipkow@15140: imports Set
haftmann@20426: uses
haftmann@31723: ("Tools/typedef.ML")
haftmann@31723: ("Tools/typecopy.ML")
haftmann@20426: ("Tools/typedef_codegen.ML")
nipkow@15131: begin
wenzelm@11608:
haftmann@23247: ML {*
haftmann@23247: structure HOL = struct val thy = theory "HOL" end;
haftmann@23247: *} -- "belongs to theory HOL"
haftmann@23247:
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@13412: and Abs_inverse: "y \ A ==> Rep (Abs y) = y"
wenzelm@13412: -- {* This will be axiomatized for each typedef! *}
haftmann@23247: begin
wenzelm@11608:
haftmann@23247: lemma Rep_inject:
wenzelm@13412: "(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@13412: thus "Rep x = Rep y" by (simp only:)
wenzelm@13412: qed
wenzelm@11608:
haftmann@23247: lemma Abs_inject:
wenzelm@13412: assumes x: "x \ A" and y: "y \ A"
wenzelm@13412: 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:)
haftmann@23710: moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse)
haftmann@23710: moreover from y 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@13412: thus "Abs x = Abs y" by (simp only:)
wenzelm@11608: qed
wenzelm@11608:
haftmann@23247: lemma Rep_cases [cases set]:
wenzelm@13412: assumes y: "y \ A"
wenzelm@13412: and hyp: "!!x. y = Rep x ==> P"
wenzelm@13412: shows P
wenzelm@13412: proof (rule hyp)
wenzelm@13412: from y have "Rep (Abs y) = y" by (rule Abs_inverse)
wenzelm@13412: thus "y = Rep (Abs y)" ..
wenzelm@11608: qed
wenzelm@11608:
haftmann@23247: lemma Abs_cases [cases type]:
wenzelm@13412: 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@13412: thus "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@13412: 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@13412: 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
huffman@24269: show "range Rep <= A" using Rep by (auto simp add: image_def)
huffman@24269: show "A <= range Rep"
nipkow@23433: proof
nipkow@23433: fix x assume "x : A"
huffman@24269: hence "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])
huffman@24269: thus "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
huffman@27295: show "Abs ` A <= UNIV" by (rule subset_UNIV)
huffman@27295: next
huffman@27295: show "UNIV <= Abs ` A"
huffman@27295: proof
huffman@27295: fix x
huffman@27295: have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
huffman@27295: moreover have "Rep x : A" by (rule Rep)
huffman@27295: ultimately show "x : Abs ` A" by (rule image_eqI)
huffman@27295: qed
huffman@27295: qed
huffman@27295:
haftmann@23247: end
haftmann@23247:
haftmann@31723: use "Tools/typedef.ML" setup Typedef.setup
haftmann@31723: use "Tools/typecopy.ML" setup Typecopy.setup
wenzelm@29056: use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
wenzelm@11608:
wenzelm@11608: end