author wenzelm Thu Sep 03 17:14:57 2015 +0200 (2015-09-03) changeset 61102 0ec9fd8d8119 parent 61101 7b915ca69af1 child 61103 8ed21464e260
misc tuning and modernization;
 src/HOL/Typedef.thy file | annotate | diff | revisions
```     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
```