src/HOL/Algebra/IntRing.thy
author ballarin
Wed, 30 Jul 2008 19:03:33 +0200
changeset 27713 95b36bfe7fc4
parent 25919 8b1c0d434824
child 27717 21bbd410ba04
permissions -rw-r--r--
New locales for orders and lattices where the equivalence relation is not restricted to equality.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     1
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     2
  Title:     HOL/Algebra/IntRing.thy
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     3
  Id:        $Id$
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     4
  Author:    Stephan Hohe, TU Muenchen
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     5
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     6
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     7
theory IntRing
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 24131
diff changeset
     8
imports QuotRing Int
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     9
begin
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    10
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    11
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    12
section {* The Ring of Integers *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    13
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    14
subsection {* Some properties of @{typ int} *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    15
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    16
lemma dvds_imp_abseq:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    17
  "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    18
apply (subst abs_split, rule conjI)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    19
 apply (clarsimp, subst abs_split, rule conjI)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    20
  apply (clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    21
  apply (cases "k=0", simp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    22
  apply (cases "l=0", simp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    23
  apply (simp add: zdvd_anti_sym)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    24
 apply clarsimp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    25
 apply (cases "k=0", simp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    26
 apply (simp add: zdvd_anti_sym)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    27
apply (clarsimp, subst abs_split, rule conjI)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    28
 apply (clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    29
 apply (cases "l=0", simp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    30
 apply (simp add: zdvd_anti_sym)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    31
apply (clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    32
apply (subgoal_tac "-l = -k", simp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    33
apply (intro zdvd_anti_sym, simp+)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    34
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    35
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    36
lemma abseq_imp_dvd:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    37
  assumes a_lk: "abs l = abs (k::int)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    38
  shows "l dvd k"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    39
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    40
  from a_lk
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    41
      have "nat (abs l) = nat (abs k)" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    42
  hence "nat (abs l) dvd nat (abs k)" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    43
  hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    44
  hence "abs l dvd k" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    45
  thus "l dvd k" 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    46
  apply (unfold dvd_def, cases "l<0")
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    47
   defer 1 apply clarsimp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    48
  proof (clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    49
    fix k
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    50
    assume l0: "l < 0"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    51
    have "- (l * k) = l * (-k)" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    52
    thus "\<exists>ka. - (l * k) = l * ka" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    53
  qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    54
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    55
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    56
lemma dvds_eq_abseq:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    57
  "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    58
apply rule
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    59
 apply (simp add: dvds_imp_abseq)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    60
apply (rule conjI)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    61
 apply (simp add: abseq_imp_dvd)+
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    62
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    63
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    64
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    65
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    66
subsection {* The Set of Integers as Algebraic Structure *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    67
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    68
subsubsection {* Definition of @{text "\<Z>"} *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    69
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    70
constdefs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    71
  int_ring :: "int ring" ("\<Z>")
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    72
  "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    73
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
    74
lemma int_Zcarr [intro!, simp]:
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    75
  "k \<in> carrier \<Z>"
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
    76
  by (simp add: int_ring_def)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    77
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    78
lemma int_is_cring:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    79
  "cring \<Z>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    80
unfolding int_ring_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    81
apply (rule cringI)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    82
  apply (rule abelian_groupI, simp_all)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    83
  defer 1
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    84
  apply (rule comm_monoidI, simp_all)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    85
 apply (rule zadd_zmult_distrib)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    86
apply (fast intro: zadd_zminus_inverse2)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    87
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    88
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
    89
(*
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    90
lemma int_is_domain:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    91
  "domain \<Z>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    92
apply (intro domain.intro domain_axioms.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    93
  apply (rule int_is_cring)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    94
 apply (unfold int_ring_def, simp+)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    95
done
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
    96
*)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
    97
subsubsection {* Interpretations *}
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    98
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
    99
text {* Since definitions of derived operations are global, their
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   100
  interpretation needs to be done as early as possible --- that is,
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   101
  with as few assumptions as possible. *}
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   102
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   103
interpretation int: monoid ["\<Z>"]
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   104
  where "carrier \<Z> = UNIV"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   105
    and "mult \<Z> x y = x * y"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   106
    and "one \<Z> = 1"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   107
    and "pow \<Z> x n = x^n"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   108
proof -
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   109
  -- "Specification"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   110
  show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   111
  then interpret int: monoid ["\<Z>"] .
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   112
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   113
  -- "Carrier"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   114
  show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   115
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   116
  -- "Operations"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   117
  { fix x y show "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   118
  note mult = this
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   119
  show one: "one \<Z> = 1" by (simp add: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   120
  show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   121
qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   122
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   123
interpretation int: comm_monoid ["\<Z>"]
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   124
  where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   125
proof -
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   126
  -- "Specification"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   127
  show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   128
  then interpret int: comm_monoid ["\<Z>"] .
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   129
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   130
  -- "Operations"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   131
  { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   132
  note mult = this
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   133
  have one: "one \<Z> = 1" by (simp add: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   134
  show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   135
  proof (cases "finite A")
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   136
    case True then show ?thesis proof induct
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   137
      case empty show ?case by (simp add: one)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   138
    next
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   139
      case insert then show ?case by (simp add: Pi_def mult)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   140
    qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   141
  next
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   142
    case False then show ?thesis by (simp add: finprod_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   143
  qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   144
qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   145
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   146
interpretation int: abelian_monoid ["\<Z>"]
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   147
  where "zero \<Z> = 0"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   148
    and "add \<Z> x y = x + y"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   149
    and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   150
proof -
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   151
  -- "Specification"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   152
  show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   153
  then interpret int: abelian_monoid ["\<Z>"] .
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   154
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   155
  -- "Operations"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   156
  { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   157
  note add = this
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   158
  show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   159
  show "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   160
  proof (cases "finite A")
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   161
    case True then show ?thesis proof induct
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   162
      case empty show ?case by (simp add: zero)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   163
    next
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   164
      case insert then show ?case by (simp add: Pi_def add)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   165
    qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   166
  next
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   167
    case False then show ?thesis by (simp add: finsum_def finprod_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   168
  qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   169
qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   170
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   171
interpretation int: abelian_group ["\<Z>"]
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   172
  where "a_inv \<Z> x = - x"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   173
    and "a_minus \<Z> x y = x - y"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   174
proof -
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   175
  -- "Specification"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   176
  show "abelian_group \<Z>"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   177
  proof (rule abelian_groupI)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   178
    show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   179
      by (simp add: int_ring_def) arith
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   180
  qed (auto simp: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   181
  then interpret int: abelian_group ["\<Z>"] .
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   182
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   183
  -- "Operations"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   184
  { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   185
  note add = this
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   186
  have zero: "zero \<Z> = 0" by (simp add: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   187
  { fix x
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   188
    have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   189
    then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) }
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   190
  note a_inv = this
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   191
  show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   192
qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   193
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   194
interpretation int: "domain" ["\<Z>"]
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   195
  by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   196
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   197
24131
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   198
text {* Removal of occurrences of @{term UNIV} in interpretation result
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   199
  --- experimental. *}
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   200
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   201
lemma UNIV:
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   202
  "x \<in> UNIV = True"
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   203
  "A \<subseteq> UNIV = True"
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   204
  "(ALL x : UNIV. P x) = (ALL x. P x)"
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   205
  "(EX x : UNIV. P x) = (EX x. P x)"
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   206
  "(True --> Q) = Q"
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   207
  "(True ==> PROP R) == PROP R"
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   208
  by simp_all
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   209
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   210
interpretation int [unfolded UNIV]:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   211
  partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   212
  where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   213
    and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   214
    and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   215
proof -
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   216
  show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   217
    by unfold_locales simp_all
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   218
  show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
24131
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   219
    by simp
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   220
  show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
24131
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   221
    by simp
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   222
  show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   223
    by (simp add: lless_def) auto
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   224
qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   225
24131
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   226
interpretation int [unfolded UNIV]:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   227
  lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   228
  where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   229
    and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   230
proof -
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   231
  let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   232
  show "lattice ?Z"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   233
    apply unfold_locales
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   234
    apply (simp add: least_def Upper_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   235
    apply arith
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   236
    apply (simp add: greatest_def Lower_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   237
    apply arith
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   238
    done
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   239
  then interpret int: lattice ["?Z"] .
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   240
  show "join ?Z x y = max x y"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   241
    apply (rule int.joinI)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   242
    apply (simp_all add: least_def Upper_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   243
    apply arith
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   244
    done
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   245
  show "meet ?Z x y = min x y"
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   246
    apply (rule int.meetI)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   247
    apply (simp_all add: greatest_def Lower_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   248
    apply arith
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   249
    done
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   250
qed
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   251
24131
1099f6c73649 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents: 23957
diff changeset
   252
interpretation int [unfolded UNIV]:
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 25919
diff changeset
   253
  total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   254
  by unfold_locales clarsimp
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   255
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   256
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   257
subsubsection {* Generated Ideals of @{text "\<Z>"} *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   258
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   259
lemma int_Idl:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   260
  "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   261
  apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   262
  apply (simp add: cgenideal_def int_ring_def)
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   263
  done
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   264
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   265
lemma multiples_principalideal:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   266
  "principalideal {x * a | x. True } \<Z>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   267
apply (subst int_Idl[symmetric], rule principalidealI)
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   268
 apply (rule int.genideal_ideal, simp)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   269
apply fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   270
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   271
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   272
lemma prime_primeideal:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   273
  assumes prime: "prime (nat p)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   274
  shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   275
apply (rule primeidealI)
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   276
   apply (rule int.genideal_ideal, simp)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   277
  apply (rule int_is_cring)
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   278
 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   279
 apply (simp add: int_ring_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   280
 apply clarsimp defer 1
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   281
 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   282
 apply (simp add: int_ring_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   283
 apply (elim exE)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   284
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   285
  fix a b x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   286
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   287
  from prime
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   288
      have ppos: "0 <= p" by (simp add: prime_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   289
  have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   290
  proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   291
    fix x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   292
    assume "nat p dvd nat (abs x)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   293
    hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   294
    thus "p dvd x" by (simp add: ppos)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   295
  qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   296
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   297
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   298
  assume "a * b = x * p"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   299
  hence "p dvd a * b" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   300
  hence "nat p dvd nat (abs (a * b))"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   301
  apply (subst nat_dvd_iff, clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   302
  apply (rule conjI, clarsimp, simp add: zabs_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   303
  proof (clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   304
    assume a: " ~ 0 <= p"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   305
    from prime
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   306
        have "0 < p" by (simp add: prime_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   307
    from a and this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   308
        have "False" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   309
    thus "nat (abs (a * b)) = 0" ..
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   310
  qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   311
  hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   312
  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   313
  hence "p dvd a | p dvd b" by (fast intro: unnat)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   314
  thus "(EX x. a = x * p) | (EX x. b = x * p)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   315
  proof
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   316
    assume "p dvd a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   317
    hence "EX x. a = p * x" by (simp add: dvd_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   318
    from this obtain x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   319
        where "a = p * x" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   320
    hence "a = x * p" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   321
    hence "EX x. a = x * p" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   322
    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   323
  next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   324
    assume "p dvd b"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   325
    hence "EX x. b = p * x" by (simp add: dvd_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   326
    from this obtain x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   327
        where "b = p * x" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   328
    hence "b = x * p" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   329
    hence "EX x. b = x * p" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   330
    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   331
  qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   332
next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   333
  assume "UNIV = {uu. EX x. uu = x * p}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   334
  from this obtain x 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   335
      where "1 = x * p" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   336
  from this [symmetric]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   337
      have "p * x = 1" by (subst zmult_commute)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   338
  hence "\<bar>p * x\<bar> = 1" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   339
  hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   340
  from this and prime
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   341
      show "False" by (simp add: prime_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   342
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   343
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   344
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   345
subsubsection {* Ideals and Divisibility *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   346
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   347
lemma int_Idl_subset_ideal:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   348
  "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   349
by (rule int.Idl_subset_ideal', simp+)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   350
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   351
lemma Idl_subset_eq_dvd:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   352
  "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   353
apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   354
apply (rule, clarify)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   355
apply (simp add: dvd_def, clarify)
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   356
apply (simp add: int.m_comm)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   357
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   358
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   359
lemma dvds_eq_Idl:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   360
  "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   361
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   362
  have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   363
  have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   364
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   365
  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}))"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   366
  by (subst a, subst b, simp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   367
  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+)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   368
  finally
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   369
    show ?thesis .
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   370
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   371
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   372
lemma Idl_eq_abs:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   373
  "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   374
apply (subst dvds_eq_abseq[symmetric])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   375
apply (rule dvds_eq_Idl[symmetric])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   376
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   377
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   378
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   379
subsubsection {* Ideals and the Modulus *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   380
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   381
constdefs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   382
   ZMod :: "int => int => int set"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   383
  "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   384
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   385
lemmas ZMod_defs =
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   386
  ZMod_def genideal_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   387
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   388
lemma rcos_zfact:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   389
  assumes kIl: "k \<in> ZMod l r"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   390
  shows "EX x. k = x * l + r"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   391
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   392
  from kIl[unfolded ZMod_def]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   393
      have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   394
  from this obtain xl
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   395
      where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   396
      and k: "k = xl + r"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   397
      by auto
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   398
  from xl obtain x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   399
      where "xl = x * l"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   400
      by (simp add: int_Idl, fast)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   401
  from k and this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   402
      have "k = x * l + r" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   403
  thus "\<exists>x. k = x * l + r" ..
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   404
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   405
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   406
lemma ZMod_imp_zmod:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   407
  assumes zmods: "ZMod m a = ZMod m b"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   408
  shows "a mod m = b mod m"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   409
proof -
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   410
  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   411
  from zmods
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   412
      have "b \<in> ZMod m a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   413
      unfolding ZMod_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   414
      by (simp add: a_repr_independenceD)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   415
  from this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   416
      have "EX x. b = x * m + a" by (rule rcos_zfact)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   417
  from this obtain x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   418
      where "b = x * m + a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   419
      by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   420
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   421
  hence "b mod m = (x * m + a) mod m" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   422
  also
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   423
      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   424
  also
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   425
      have "\<dots> = a mod m" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   426
  finally
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   427
      have "b mod m = a mod m" .
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   428
  thus "a mod m = b mod m" ..
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   429
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   430
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   431
lemma ZMod_mod:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   432
  shows "ZMod m a = ZMod m (a mod m)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   433
proof -
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   434
  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   435
  show ?thesis
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   436
      unfolding ZMod_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   437
  apply (rule a_repr_independence'[symmetric])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   438
  apply (simp add: int_Idl a_r_coset_defs)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   439
  apply (simp add: int_ring_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   440
  proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   441
    have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   442
    hence "a = (a div m) * m + (a mod m)" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   443
    thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   444
  qed simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   445
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   446
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   447
lemma zmod_imp_ZMod:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   448
  assumes modeq: "a mod m = b mod m"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   449
  shows "ZMod m a = ZMod m b"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   450
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   451
  have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   452
  also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   453
  also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   454
  finally show ?thesis .
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   455
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   456
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   457
corollary ZMod_eq_mod:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   458
  shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   459
by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   460
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   461
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   462
subsubsection {* Factorization *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   463
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   464
constdefs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   465
  ZFact :: "int \<Rightarrow> int set ring"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   466
  "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   467
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   468
lemmas ZFact_defs = ZFact_def FactRing_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   469
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   470
lemma ZFact_is_cring:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   471
  shows "cring (ZFact k)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   472
apply (unfold ZFact_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   473
apply (rule ideal.quotient_is_cring)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   474
 apply (intro ring.genideal_ideal)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   475
  apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   476
 apply simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   477
apply (rule int_is_cring)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   478
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   479
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   480
lemma ZFact_zero:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   481
  "carrier (ZFact 0) = (\<Union>a. {{a}})"
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   482
apply (insert int.genideal_zero)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   483
apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   484
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   485
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   486
lemma ZFact_one:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   487
  "carrier (ZFact 1) = {UNIV}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   488
apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
23957
54fab60ddc97 Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents: 22063
diff changeset
   489
apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps])
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   490
apply (rule, rule, clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   491
 apply (rule, rule, clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   492
 apply (rule, clarsimp, arith)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   493
apply (rule, clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   494
apply (rule exI[of _ "0"], clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   495
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   496
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   497
lemma ZFact_prime_is_domain:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   498
  assumes pprime: "prime (nat p)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   499
  shows "domain (ZFact p)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   500
apply (unfold ZFact_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   501
apply (rule primeideal.quotient_is_domain)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   502
apply (rule prime_primeideal[OF pprime])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   503
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   504
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   505
end