misc tuning and modernization;
authorwenzelm
Thu Sep 03 17:14:57 2015 +0200 (2015-09-03)
changeset 611020ec9fd8d8119
parent 61101 7b915ca69af1
child 61103 8ed21464e260
misc tuning and modernization;
src/HOL/Typedef.thy
     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