1(* Title: HOL/Typedef.thy 2 Author: Markus Wenzel, TU Munich 3*) 4 5section \<open>HOL type definitions\<close> 6 7theory Typedef 8imports Set 9keywords 10 "typedef" :: thy_goal and 11 "morphisms" :: quasi_command 12begin 13 14locale type_definition = 15 fixes Rep and Abs and A 16 assumes Rep: "Rep x \<in> A" 17 and Rep_inverse: "Abs (Rep x) = x" 18 and Abs_inverse: "y \<in> A \<Longrightarrow> Rep (Abs y) = y" 19 \<comment> \<open>This will be axiomatized for each typedef!\<close> 20begin 21 22lemma Rep_inject: "Rep x = Rep y \<longleftrightarrow> x = y" 23proof 24 assume "Rep x = Rep y" 25 then have "Abs (Rep x) = Abs (Rep y)" by (simp only:) 26 moreover have "Abs (Rep x) = x" by (rule Rep_inverse) 27 moreover have "Abs (Rep y) = y" by (rule Rep_inverse) 28 ultimately show "x = y" by simp 29next 30 assume "x = y" 31 then show "Rep x = Rep y" by (simp only:) 32qed 33 34lemma Abs_inject: 35 assumes "x \<in> A" and "y \<in> A" 36 shows "Abs x = Abs y \<longleftrightarrow> x = y" 37proof 38 assume "Abs x = Abs y" 39 then have "Rep (Abs x) = Rep (Abs y)" by (simp only:) 40 moreover from \<open>x \<in> A\<close> have "Rep (Abs x) = x" by (rule Abs_inverse) 41 moreover from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse) 42 ultimately show "x = y" by simp 43next 44 assume "x = y" 45 then show "Abs x = Abs y" by (simp only:) 46qed 47 48lemma Rep_cases [cases set]: 49 assumes "y \<in> A" 50 and hyp: "\<And>x. y = Rep x \<Longrightarrow> P" 51 shows P 52proof (rule hyp) 53 from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse) 54 then show "y = Rep (Abs y)" .. 55qed 56 57lemma Abs_cases [cases type]: 58 assumes r: "\<And>y. x = Abs y \<Longrightarrow> y \<in> A \<Longrightarrow> P" 59 shows P 60proof (rule r) 61 have "Abs (Rep x) = x" by (rule Rep_inverse) 62 then show "x = Abs (Rep x)" .. 63 show "Rep x \<in> A" by (rule Rep) 64qed 65 66lemma Rep_induct [induct set]: 67 assumes y: "y \<in> A" 68 and hyp: "\<And>x. P (Rep x)" 69 shows "P y" 70proof - 71 have "P (Rep (Abs y))" by (rule hyp) 72 moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse) 73 ultimately show "P y" by simp 74qed 75 76lemma Abs_induct [induct type]: 77 assumes r: "\<And>y. y \<in> A \<Longrightarrow> P (Abs y)" 78 shows "P x" 79proof - 80 have "Rep x \<in> A" by (rule Rep) 81 then have "P (Abs (Rep x))" by (rule r) 82 moreover have "Abs (Rep x) = x" by (rule Rep_inverse) 83 ultimately show "P x" by simp 84qed 85 86lemma Rep_range: "range Rep = A" 87proof 88 show "range Rep \<subseteq> A" using Rep by (auto simp add: image_def) 89 show "A \<subseteq> range Rep" 90 proof 91 fix x assume "x \<in> A" 92 then have "x = Rep (Abs x)" by (rule Abs_inverse [symmetric]) 93 then show "x \<in> range Rep" by (rule range_eqI) 94 qed 95qed 96 97lemma Abs_image: "Abs ` A = UNIV" 98proof 99 show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV) 100 show "UNIV \<subseteq> Abs ` A" 101 proof 102 fix x 103 have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) 104 moreover have "Rep x \<in> A" by (rule Rep) 105 ultimately show "x \<in> Abs ` A" by (rule image_eqI) 106 qed 107qed 108 109end 110 111ML_file "Tools/typedef.ML" 112 113end 114