summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Typedef.thy

changeset 61102 | 0ec9fd8d8119 |

parent 60758 | d8d85a8172b5 |

child 61799 | 4cf66f21b764 |

1.1 --- a/src/HOL/Typedef.thy Thu Sep 03 16:41:43 2015 +0200 1.2 +++ b/src/HOL/Typedef.thy Thu Sep 03 17:14:57 2015 +0200 1.3 @@ -13,12 +13,11 @@ 1.4 fixes Rep and Abs and A 1.5 assumes Rep: "Rep x \<in> A" 1.6 and Rep_inverse: "Abs (Rep x) = x" 1.7 - and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y" 1.8 + and Abs_inverse: "y \<in> A \<Longrightarrow> Rep (Abs y) = y" 1.9 -- \<open>This will be axiomatized for each typedef!\<close> 1.10 begin 1.11 1.12 -lemma Rep_inject: 1.13 - "(Rep x = Rep y) = (x = y)" 1.14 +lemma Rep_inject: "Rep x = Rep y \<longleftrightarrow> x = y" 1.15 proof 1.16 assume "Rep x = Rep y" 1.17 then have "Abs (Rep x) = Abs (Rep y)" by (simp only:) 1.18 @@ -27,44 +26,44 @@ 1.19 ultimately show "x = y" by simp 1.20 next 1.21 assume "x = y" 1.22 - thus "Rep x = Rep y" by (simp only:) 1.23 + then show "Rep x = Rep y" by (simp only:) 1.24 qed 1.25 1.26 lemma Abs_inject: 1.27 - assumes x: "x \<in> A" and y: "y \<in> A" 1.28 - shows "(Abs x = Abs y) = (x = y)" 1.29 + assumes "x \<in> A" and "y \<in> A" 1.30 + shows "Abs x = Abs y \<longleftrightarrow> x = y" 1.31 proof 1.32 assume "Abs x = Abs y" 1.33 then have "Rep (Abs x) = Rep (Abs y)" by (simp only:) 1.34 - moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse) 1.35 - moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse) 1.36 + moreover from \<open>x \<in> A\<close> have "Rep (Abs x) = x" by (rule Abs_inverse) 1.37 + moreover from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse) 1.38 ultimately show "x = y" by simp 1.39 next 1.40 assume "x = y" 1.41 - thus "Abs x = Abs y" by (simp only:) 1.42 + then show "Abs x = Abs y" by (simp only:) 1.43 qed 1.44 1.45 lemma Rep_cases [cases set]: 1.46 - assumes y: "y \<in> A" 1.47 - and hyp: "!!x. y = Rep x ==> P" 1.48 + assumes "y \<in> A" 1.49 + and hyp: "\<And>x. y = Rep x \<Longrightarrow> P" 1.50 shows P 1.51 proof (rule hyp) 1.52 - from y have "Rep (Abs y) = y" by (rule Abs_inverse) 1.53 - thus "y = Rep (Abs y)" .. 1.54 + from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse) 1.55 + then show "y = Rep (Abs y)" .. 1.56 qed 1.57 1.58 lemma Abs_cases [cases type]: 1.59 - assumes r: "!!y. x = Abs y ==> y \<in> A ==> P" 1.60 + assumes r: "\<And>y. x = Abs y \<Longrightarrow> y \<in> A \<Longrightarrow> P" 1.61 shows P 1.62 proof (rule r) 1.63 have "Abs (Rep x) = x" by (rule Rep_inverse) 1.64 - thus "x = Abs (Rep x)" .. 1.65 + then show "x = Abs (Rep x)" .. 1.66 show "Rep x \<in> A" by (rule Rep) 1.67 qed 1.68 1.69 lemma Rep_induct [induct set]: 1.70 assumes y: "y \<in> A" 1.71 - and hyp: "!!x. P (Rep x)" 1.72 + and hyp: "\<And>x. P (Rep x)" 1.73 shows "P y" 1.74 proof - 1.75 have "P (Rep (Abs y))" by (rule hyp) 1.76 @@ -73,7 +72,7 @@ 1.77 qed 1.78 1.79 lemma Abs_induct [induct type]: 1.80 - assumes r: "!!y. y \<in> A ==> P (Abs y)" 1.81 + assumes r: "\<And>y. y \<in> A \<Longrightarrow> P (Abs y)" 1.82 shows "P x" 1.83 proof - 1.84 have "Rep x \<in> A" by (rule Rep) 1.85 @@ -84,25 +83,24 @@ 1.86 1.87 lemma Rep_range: "range Rep = A" 1.88 proof 1.89 - show "range Rep <= A" using Rep by (auto simp add: image_def) 1.90 - show "A <= range Rep" 1.91 + show "range Rep \<subseteq> A" using Rep by (auto simp add: image_def) 1.92 + show "A \<subseteq> range Rep" 1.93 proof 1.94 - fix x assume "x : A" 1.95 - hence "x = Rep (Abs x)" by (rule Abs_inverse [symmetric]) 1.96 - thus "x : range Rep" by (rule range_eqI) 1.97 + fix x assume "x \<in> A" 1.98 + then have "x = Rep (Abs x)" by (rule Abs_inverse [symmetric]) 1.99 + then show "x \<in> range Rep" by (rule range_eqI) 1.100 qed 1.101 qed 1.102 1.103 lemma Abs_image: "Abs ` A = UNIV" 1.104 proof 1.105 - show "Abs ` A <= UNIV" by (rule subset_UNIV) 1.106 -next 1.107 - show "UNIV <= Abs ` A" 1.108 + show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV) 1.109 + show "UNIV \<subseteq> Abs ` A" 1.110 proof 1.111 fix x 1.112 have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) 1.113 - moreover have "Rep x : A" by (rule Rep) 1.114 - ultimately show "x : Abs ` A" by (rule image_eqI) 1.115 + moreover have "Rep x \<in> A" by (rule Rep) 1.116 + ultimately show "x \<in> Abs ` A" by (rule image_eqI) 1.117 qed 1.118 qed 1.119