tuned proofs;
authorwenzelm
Fri Mar 07 23:28:05 2014 +0100 (2014-03-07)
changeset 559913fa6e6c81788
parent 55990 41c6b99c5fb7
child 55992 1e7f04ba8196
tuned proofs;
src/HOL/Algebra/IntRing.thy
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Mar 07 22:30:58 2014 +0100
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Mar 07 23:28:05 2014 +0100
     1.3 @@ -12,7 +12,8 @@
     1.4  subsection {* Some properties of @{typ int} *}
     1.5  
     1.6  lemma dvds_eq_abseq:
     1.7 -  "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
     1.8 +  fixes k :: int
     1.9 +  shows "l dvd k \<and> k dvd l \<longleftrightarrow> abs l = abs k"
    1.10  apply rule
    1.11   apply (simp add: zdvd_antisym_abs)
    1.12  apply (simp add: dvd_if_abs_eq)
    1.13 @@ -21,16 +22,13 @@
    1.14  
    1.15  subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
    1.16  
    1.17 -abbreviation
    1.18 -  int_ring :: "int ring" ("\<Z>") where
    1.19 -  "int_ring == \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
    1.20 +abbreviation int_ring :: "int ring" ("\<Z>")
    1.21 +  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
    1.22  
    1.23 -lemma int_Zcarr [intro!, simp]:
    1.24 -  "k \<in> carrier \<Z>"
    1.25 +lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
    1.26    by simp
    1.27  
    1.28 -lemma int_is_cring:
    1.29 -  "cring \<Z>"
    1.30 +lemma int_is_cring: "cring \<Z>"
    1.31  apply (rule cringI)
    1.32    apply (rule abelian_groupI, simp_all)
    1.33    defer 1
    1.34 @@ -70,8 +68,7 @@
    1.35  
    1.36    -- "Operations"
    1.37    { fix x y show "mult \<Z> x y = x * y" by simp }
    1.38 -  note mult = this
    1.39 -  show one: "one \<Z> = 1" by simp
    1.40 +  show "one \<Z> = 1" by simp
    1.41    show "pow \<Z> x n = x^n" by (induct n) simp_all
    1.42  qed
    1.43  
    1.44 @@ -88,13 +85,18 @@
    1.45    have one: "one \<Z> = 1" by simp
    1.46    show "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
    1.47    proof (cases "finite A")
    1.48 -    case True then show ?thesis proof induct
    1.49 -      case empty show ?case by (simp add: one)
    1.50 +    case True
    1.51 +    then show ?thesis
    1.52 +    proof induct
    1.53 +      case empty
    1.54 +      show ?case by (simp add: one)
    1.55      next
    1.56 -      case insert then show ?case by (simp add: Pi_def mult)
    1.57 +      case insert
    1.58 +      then show ?case by (simp add: Pi_def mult)
    1.59      qed
    1.60    next
    1.61 -    case False then show ?thesis by (simp add: finprod_def)
    1.62 +    case False
    1.63 +    then show ?thesis by (simp add: finprod_def)
    1.64    qed
    1.65  qed
    1.66  
    1.67 @@ -114,16 +116,22 @@
    1.68    -- "Operations"
    1.69    { fix x y show "add \<Z> x y = x + y" by simp }
    1.70    note add = this
    1.71 -  show zero: "zero \<Z> = 0" by simp
    1.72 +  show zero: "zero \<Z> = 0"
    1.73 +    by simp
    1.74    show "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    1.75    proof (cases "finite A")
    1.76 -    case True then show ?thesis proof induct
    1.77 -      case empty show ?case by (simp add: zero)
    1.78 +    case True
    1.79 +    then show ?thesis
    1.80 +    proof induct
    1.81 +      case empty
    1.82 +      show ?case by (simp add: zero)
    1.83      next
    1.84 -      case insert then show ?case by (simp add: Pi_def add)
    1.85 +      case insert
    1.86 +      then show ?case by (simp add: Pi_def add)
    1.87      qed
    1.88    next
    1.89 -    case False then show ?thesis by (simp add: finsum_def finprod_def)
    1.90 +    case False
    1.91 +    then show ?thesis by (simp add: finsum_def finprod_def)
    1.92    qed
    1.93  qed
    1.94  
    1.95 @@ -142,7 +150,9 @@
    1.96    -- "Specification"
    1.97    show "abelian_group \<Z>"
    1.98    proof (rule abelian_groupI)
    1.99 -    show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
   1.100 +    fix x
   1.101 +    assume "x \<in> carrier \<Z>"
   1.102 +    then show "\<exists>y \<in> carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
   1.103        by simp arith
   1.104    qed auto
   1.105    then interpret int: abelian_group \<Z> .
   1.106 @@ -150,11 +160,16 @@
   1.107    { fix x y have "add \<Z> x y = x + y" by simp }
   1.108    note add = this
   1.109    have zero: "zero \<Z> = 0" by simp
   1.110 -  { fix x
   1.111 -    have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero)
   1.112 -    then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) }
   1.113 +  {
   1.114 +    fix x
   1.115 +    have "add \<Z> (- x) x = zero \<Z>"
   1.116 +      by (simp add: add zero)
   1.117 +    then show "a_inv \<Z> x = - x"
   1.118 +      by (simp add: int.minus_equality)
   1.119 +  }
   1.120    note a_inv = this
   1.121 -  show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
   1.122 +  show "a_minus \<Z> x y = x - y"
   1.123 +    by (simp add: int.minus_eq add a_inv)
   1.124  qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
   1.125  
   1.126  interpretation int: "domain" \<Z>
   1.127 @@ -165,21 +180,21 @@
   1.128      and "a_inv \<Z> x = - x"
   1.129      and "a_minus \<Z> x y = x - y"
   1.130  proof -
   1.131 -  show "domain \<Z>" by unfold_locales (auto simp: distrib_right distrib_left)
   1.132 -qed (simp
   1.133 -    add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
   1.134 +  show "domain \<Z>"
   1.135 +    by unfold_locales (auto simp: distrib_right distrib_left)
   1.136 +qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
   1.137  
   1.138  
   1.139  text {* Removal of occurrences of @{term UNIV} in interpretation result
   1.140    --- experimental. *}
   1.141  
   1.142  lemma UNIV:
   1.143 -  "x \<in> UNIV = True"
   1.144 -  "A \<subseteq> UNIV = True"
   1.145 -  "(ALL x : UNIV. P x) = (ALL x. P x)"
   1.146 -  "(EX x : UNIV. P x) = (EX x. P x)"
   1.147 -  "(True --> Q) = Q"
   1.148 -  "(True ==> PROP R) == PROP R"
   1.149 +  "x \<in> UNIV \<longleftrightarrow> True"
   1.150 +  "A \<subseteq> UNIV \<longleftrightarrow> True"
   1.151 +  "(\<forall>x \<in> UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
   1.152 +  "(EX x : UNIV. P x) \<longleftrightarrow> (EX x. P x)"
   1.153 +  "(True \<longrightarrow> Q) \<longleftrightarrow> Q"
   1.154 +  "(True \<Longrightarrow> PROP R) \<equiv> PROP R"
   1.155    by simp_all
   1.156  
   1.157  interpretation int (* FIXME [unfolded UNIV] *) :
   1.158 @@ -231,15 +246,13 @@
   1.159  
   1.160  subsection {* Generated Ideals of @{text "\<Z>"} *}
   1.161  
   1.162 -lemma int_Idl:
   1.163 -  "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
   1.164 +lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
   1.165    apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
   1.166    apply (simp add: cgenideal_def)
   1.167    done
   1.168  
   1.169 -lemma multiples_principalideal:
   1.170 -  "principalideal {x * a | x. True } \<Z>"
   1.171 -by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
   1.172 +lemma multiples_principalideal: "principalideal {x * a | x. True } \<Z>"
   1.173 +  by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
   1.174  
   1.175  lemma prime_primeideal:
   1.176    assumes prime: "prime p"
   1.177 @@ -254,15 +267,15 @@
   1.178  proof -
   1.179    fix a b x
   1.180    assume "a * b = x * int p"
   1.181 -  hence "p dvd a * b" by simp
   1.182 -  hence "p dvd a | p dvd b"
   1.183 +  then have "p dvd a * b" by simp
   1.184 +  then have "p dvd a \<or> p dvd b"
   1.185      by (metis prime prime_dvd_mult_eq_int)
   1.186 -  thus "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)"
   1.187 +  then show "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)"
   1.188      by (metis dvd_def mult_commute)
   1.189  next
   1.190    assume "UNIV = {uu. EX x. uu = x * int p}"
   1.191    then obtain x where "1 = x * int p" by best
   1.192 -  hence "\<bar>int p * x\<bar> = 1" by (simp add: mult_commute)
   1.193 +  then have "\<bar>int p * x\<bar> = 1" by (simp add: mult_commute)
   1.194    then show False
   1.195      by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
   1.196  qed
   1.197 @@ -270,42 +283,39 @@
   1.198  
   1.199  subsection {* Ideals and Divisibility *}
   1.200  
   1.201 -lemma int_Idl_subset_ideal:
   1.202 -  "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
   1.203 -by (rule int.Idl_subset_ideal', simp+)
   1.204 +lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
   1.205 +  by (rule int.Idl_subset_ideal') simp_all
   1.206  
   1.207 -lemma Idl_subset_eq_dvd:
   1.208 -  "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
   1.209 -apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
   1.210 -apply (rule, clarify)
   1.211 -apply (simp add: dvd_def)
   1.212 -apply (simp add: dvd_def mult_ac)
   1.213 -done
   1.214 +lemma Idl_subset_eq_dvd: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> l dvd k"
   1.215 +  apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
   1.216 +  apply (rule, clarify)
   1.217 +  apply (simp add: dvd_def)
   1.218 +  apply (simp add: dvd_def mult_ac)
   1.219 +  done
   1.220  
   1.221 -lemma dvds_eq_Idl:
   1.222 -  "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
   1.223 +lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
   1.224  proof -
   1.225 -  have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric])
   1.226 -  have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric])
   1.227 +  have a: "l dvd k \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})"
   1.228 +    by (rule Idl_subset_eq_dvd[symmetric])
   1.229 +  have b: "k dvd l \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})"
   1.230 +    by (rule Idl_subset_eq_dvd[symmetric])
   1.231  
   1.232 -  have "(l dvd k \<and> k dvd l) = ((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k}))"
   1.233 -  by (subst a, subst b, simp)
   1.234 -  also have "((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})" by (rule, fast+)
   1.235 -  finally
   1.236 -    show ?thesis .
   1.237 +  have "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<and> Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k}"
   1.238 +    by (subst a, subst b, simp)
   1.239 +  also have "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<and> Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k} \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
   1.240 +    by blast
   1.241 +  finally show ?thesis .
   1.242  qed
   1.243  
   1.244 -lemma Idl_eq_abs:
   1.245 -  "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)"
   1.246 -apply (subst dvds_eq_abseq[symmetric])
   1.247 -apply (rule dvds_eq_Idl[symmetric])
   1.248 -done
   1.249 +lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> abs l = abs k"
   1.250 +  apply (subst dvds_eq_abseq[symmetric])
   1.251 +  apply (rule dvds_eq_Idl[symmetric])
   1.252 +  done
   1.253  
   1.254  
   1.255  subsection {* Ideals and the Modulus *}
   1.256  
   1.257 -definition
   1.258 -  ZMod :: "int => int => int set"
   1.259 +definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set"
   1.260    where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
   1.261  
   1.262  lemmas ZMod_defs =
   1.263 @@ -313,59 +323,56 @@
   1.264  
   1.265  lemma rcos_zfact:
   1.266    assumes kIl: "k \<in> ZMod l r"
   1.267 -  shows "EX x. k = x * l + r"
   1.268 +  shows "\<exists>x. k = x * l + r"
   1.269  proof -
   1.270 -  from kIl[unfolded ZMod_def]
   1.271 -      have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs)
   1.272 -  then obtain xl
   1.273 -      where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
   1.274 -      and k: "k = xl + r"
   1.275 -      by auto
   1.276 -  from xl obtain x
   1.277 -      where "xl = x * l"
   1.278 -      by (simp add: int_Idl, fast)
   1.279 -  from k and this
   1.280 -      have "k = x * l + r" by simp
   1.281 -  thus "\<exists>x. k = x * l + r" ..
   1.282 +  from kIl[unfolded ZMod_def] have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r"
   1.283 +    by (simp add: a_r_coset_defs)
   1.284 +  then obtain xl where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" and k: "k = xl + r"
   1.285 +    by auto
   1.286 +  from xl obtain x where "xl = x * l"
   1.287 +    by (auto simp: int_Idl)
   1.288 +  with k have "k = x * l + r"
   1.289 +    by simp
   1.290 +  then show "\<exists>x. k = x * l + r" ..
   1.291  qed
   1.292  
   1.293  lemma ZMod_imp_zmod:
   1.294    assumes zmods: "ZMod m a = ZMod m b"
   1.295    shows "a mod m = b mod m"
   1.296  proof -
   1.297 -  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
   1.298 -  from zmods
   1.299 -      have "b \<in> ZMod m a"
   1.300 -      unfolding ZMod_def
   1.301 -      by (simp add: a_repr_independenceD)
   1.302 -  then
   1.303 -      have "EX x. b = x * m + a" by (rule rcos_zfact)
   1.304 -  then obtain x
   1.305 -      where "b = x * m + a"
   1.306 -      by fast
   1.307 -
   1.308 -  hence "b mod m = (x * m + a) mod m" by simp
   1.309 -  also
   1.310 -      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq)
   1.311 -  also
   1.312 -      have "\<dots> = a mod m" by simp
   1.313 -  finally
   1.314 -      have "b mod m = a mod m" .
   1.315 -  thus "a mod m = b mod m" ..
   1.316 +  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
   1.317 +    by (rule int.genideal_ideal) fast
   1.318 +  from zmods have "b \<in> ZMod m a"
   1.319 +    unfolding ZMod_def by (simp add: a_repr_independenceD)
   1.320 +  then have "\<exists>x. b = x * m + a"
   1.321 +    by (rule rcos_zfact)
   1.322 +  then obtain x where "b = x * m + a"
   1.323 +    by fast
   1.324 +  then have "b mod m = (x * m + a) mod m"
   1.325 +    by simp
   1.326 +  also have "\<dots> = ((x * m) mod m) + (a mod m)"
   1.327 +    by (simp add: mod_add_eq)
   1.328 +  also have "\<dots> = a mod m"
   1.329 +    by simp
   1.330 +  finally have "b mod m = a mod m" .
   1.331 +  then show "a mod m = b mod m" ..
   1.332  qed
   1.333  
   1.334 -lemma ZMod_mod:
   1.335 -  shows "ZMod m a = ZMod m (a mod m)"
   1.336 +lemma ZMod_mod: "ZMod m a = ZMod m (a mod m)"
   1.337  proof -
   1.338 -  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
   1.339 +  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
   1.340 +    by (rule int.genideal_ideal) fast
   1.341    show ?thesis
   1.342 -      unfolding ZMod_def
   1.343 -  apply (rule a_repr_independence'[symmetric])
   1.344 -  apply (simp add: int_Idl a_r_coset_defs)
   1.345 +    unfolding ZMod_def
   1.346 +    apply (rule a_repr_independence'[symmetric])
   1.347 +    apply (simp add: int_Idl a_r_coset_defs)
   1.348    proof -
   1.349 -    have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
   1.350 -    hence "a = (a div m) * m + (a mod m)" by simp
   1.351 -    thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast
   1.352 +    have "a = m * (a div m) + (a mod m)"
   1.353 +      by (simp add: zmod_zdiv_equality)
   1.354 +    then have "a = (a div m) * m + (a mod m)"
   1.355 +      by simp
   1.356 +    then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m"
   1.357 +      by fast
   1.358    qed simp
   1.359  qed
   1.360  
   1.361 @@ -373,58 +380,59 @@
   1.362    assumes modeq: "a mod m = b mod m"
   1.363    shows "ZMod m a = ZMod m b"
   1.364  proof -
   1.365 -  have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod)
   1.366 -  also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
   1.367 -  also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
   1.368 +  have "ZMod m a = ZMod m (a mod m)"
   1.369 +    by (rule ZMod_mod)
   1.370 +  also have "\<dots> = ZMod m (b mod m)"
   1.371 +    by (simp add: modeq[symmetric])
   1.372 +  also have "\<dots> = ZMod m b"
   1.373 +    by (rule ZMod_mod[symmetric])
   1.374    finally show ?thesis .
   1.375  qed
   1.376  
   1.377 -corollary ZMod_eq_mod:
   1.378 -  shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
   1.379 -by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
   1.380 +corollary ZMod_eq_mod: "ZMod m a = ZMod m b \<longleftrightarrow> a mod m = b mod m"
   1.381 +  apply (rule iffI)
   1.382 +  apply (erule ZMod_imp_zmod)
   1.383 +  apply (erule zmod_imp_ZMod)
   1.384 +  done
   1.385  
   1.386  
   1.387  subsection {* Factorization *}
   1.388  
   1.389 -definition
   1.390 -  ZFact :: "int \<Rightarrow> int set ring"
   1.391 +definition ZFact :: "int \<Rightarrow> int set ring"
   1.392    where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
   1.393  
   1.394  lemmas ZFact_defs = ZFact_def FactRing_def
   1.395  
   1.396 -lemma ZFact_is_cring:
   1.397 -  shows "cring (ZFact k)"
   1.398 -apply (unfold ZFact_def)
   1.399 -apply (rule ideal.quotient_is_cring)
   1.400 - apply (intro ring.genideal_ideal)
   1.401 -  apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
   1.402 - apply simp
   1.403 -apply (rule int_is_cring)
   1.404 -done
   1.405 +lemma ZFact_is_cring: "cring (ZFact k)"
   1.406 +  apply (unfold ZFact_def)
   1.407 +  apply (rule ideal.quotient_is_cring)
   1.408 +   apply (intro ring.genideal_ideal)
   1.409 +    apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
   1.410 +   apply simp
   1.411 +  apply (rule int_is_cring)
   1.412 +  done
   1.413  
   1.414 -lemma ZFact_zero:
   1.415 -  "carrier (ZFact 0) = (\<Union>a. {{a}})"
   1.416 -apply (insert int.genideal_zero)
   1.417 -apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
   1.418 -done
   1.419 +lemma ZFact_zero: "carrier (ZFact 0) = (\<Union>a. {{a}})"
   1.420 +  apply (insert int.genideal_zero)
   1.421 +  apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def)
   1.422 +  done
   1.423  
   1.424 -lemma ZFact_one:
   1.425 -  "carrier (ZFact 1) = {UNIV}"
   1.426 -apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
   1.427 -apply (subst int.genideal_one)
   1.428 -apply (rule, rule, clarsimp)
   1.429 - apply (rule, rule, clarsimp)
   1.430 - apply (rule, clarsimp, arith)
   1.431 -apply (rule, clarsimp)
   1.432 -apply (rule exI[of _ "0"], clarsimp)
   1.433 -done
   1.434 +lemma ZFact_one: "carrier (ZFact 1) = {UNIV}"
   1.435 +  apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
   1.436 +  apply (subst int.genideal_one)
   1.437 +  apply (rule, rule, clarsimp)
   1.438 +   apply (rule, rule, clarsimp)
   1.439 +   apply (rule, clarsimp, arith)
   1.440 +  apply (rule, clarsimp)
   1.441 +  apply (rule exI[of _ "0"], clarsimp)
   1.442 +  done
   1.443  
   1.444  lemma ZFact_prime_is_domain:
   1.445    assumes pprime: "prime p"
   1.446    shows "domain (ZFact p)"
   1.447 -apply (unfold ZFact_def)
   1.448 -apply (rule primeideal.quotient_is_domain)
   1.449 -apply (rule prime_primeideal[OF pprime])
   1.450 -done
   1.451 +  apply (unfold ZFact_def)
   1.452 +  apply (rule primeideal.quotient_is_domain)
   1.453 +  apply (rule prime_primeideal[OF pprime])
   1.454 +  done
   1.455  
   1.456  end