Theory IntMod

header {* Integers mod n *}

theory IntMod
imports NumeralType
begin

subsection {* Locale for modular arithmetic subtypes *}

locale mod_type =
  fixes n :: int
  and Rep :: "'a::{zero,one,plus,times,minus,power} => int"
  and Abs :: "int => 'a::{zero,one,plus,times,minus,power}"
  assumes type: "type_definition Rep Abs {0..<n}" and size1: "1 < n"
  and zero_def: "0 ≡ Abs 0"
  and one_def:  "1 ≡ Abs 1"
  and add_def:  "x + y ≡ Abs ((Rep x + Rep y) mod n)"
  and mult_def: "x * y ≡ Abs ((Rep x * Rep y) mod n)"
  and diff_def: "x - y ≡ Abs ((Rep x - Rep y) mod n)"
  and minus_def: "- x ≡ Abs ((- Rep x) mod n)"
  and power_def: "x ^ k ≡ Abs (Rep x ^ k mod n)"

lemma (in mod_type) size0: "0 < n"
by (cut_tac size1, simp)

lemmas (in mod_type) definitions =
  zero_def one_def add_def mult_def minus_def diff_def power_def

lemma (in mod_type) Rep_less_n: "Rep x < n"
by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])

lemma (in mod_type) Rep_le_n: "Rep x ≤ n"
by (rule Rep_less_n [THEN order_less_imp_le])

lemma (in mod_type) Rep_inject_sym: "(x = y) = (Rep x = Rep y)"
by (rule type_definition.Rep_inject [OF type, symmetric])

lemma (in mod_type) Rep_inverse: "Abs (Rep x) = x"
by (rule type_definition.Rep_inverse [OF type])

lemma (in mod_type) Abs_inverse: "m ∈ {0..<n} ==> Rep (Abs m) = m"
by (rule type_definition.Abs_inverse [OF type])

lemma (in mod_type) Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
by (simp add: Abs_inverse IntDiv.pos_mod_conj [OF size0])

lemma (in mod_type) Rep_Abs_0: "Rep (Abs 0) = 0"
by (simp add: Abs_inverse size0)

lemma (in mod_type) Rep_0: "Rep 0 = 0"
by (simp add: zero_def Rep_Abs_0)

lemma (in mod_type) Rep_Abs_1: "Rep (Abs 1) = 1"
by (simp add: Abs_inverse size1)

lemma (in mod_type) Rep_1: "Rep 1 = 1"
by (simp add: one_def Rep_Abs_1)

lemma (in mod_type) Rep_mod: "Rep x mod n = Rep x"
apply (rule_tac x=x in type_definition.Abs_cases [OF type])
apply (simp add: type_definition.Abs_inverse [OF type])
apply (simp add: mod_pos_pos_trivial)
done

text "The following 3 lemmas belong in Integ/IntDiv.thy"

lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
by (simp only: zmod_zminus1_eq_if mod_mod_trivial)

lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
by (simp only: diff_def zmod_zadd_left_eq [symmetric])

lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
proof -
  have "(x + - (y mod m) mod m) mod m = (x + - y mod m) mod m"
    by (simp only: zminus_zmod)
  hence "(x + - (y mod m)) mod m = (x + - y) mod m"
    by (simp only: zmod_zadd_right_eq [symmetric])
  thus "(x - y mod m) mod m = (x - y) mod m"
    by (simp only: diff_def)
qed

lemmas zmod_simps =
  IntDiv.zmod_zadd_left_eq  [symmetric]
  IntDiv.zmod_zadd_right_eq [symmetric]
  IntDiv.zmod_zmult1_eq     [symmetric]
  IntDiv.zmod_zmult1_eq'    [symmetric]
  IntDiv.zpower_zmod
  zminus_zmod zdiff_zmod_left zdiff_zmod_right

lemmas (in mod_type) Rep_simps =
  Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1

lemma (in mod_type) comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
apply (intro_classes, unfold definitions)
apply (simp_all add: Rep_simps zmod_simps add_ac mult_ac ring_distrib)
done

lemma (in mod_type) recpower: "OFCLASS('a, recpower_class)"
apply (intro_classes, unfold definitions)
apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc
                     mod_pos_pos_trivial size1)
done

locale (open) mod_ring = mod_type +
  constrains n :: int
  and Rep :: "'a::{number_ring,power} => int"
  and Abs :: "int => 'a::{number_ring,power}"

lemma (in mod_ring) of_nat_eq: "of_nat k = Abs (int k mod n)"
apply (induct k)
apply (simp add: zero_def)
apply (simp add: Rep_simps add_def one_def zmod_simps add_ac)
done

lemma (in mod_ring) of_int_eq: "of_int z = Abs (z mod n)"
apply (cases z rule: int_diff_cases)
apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
done

lemma (in mod_ring) Rep_number_of:
  "Rep (number_of w) = number_of w mod n"
by (simp add: number_of_eq of_int_eq Rep_Abs_mod)

lemma (in mod_ring) iszero_number_of:
  "iszero (number_of w::'a) = (number_of w mod n = 0)"
by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_def)

lemma (in mod_ring) cases:
  assumes 1: "!!z. [|(x::'a) = of_int z; 0 ≤ z; z < n|] ==> P"
  shows "P"
apply (cases x rule: type_definition.Abs_cases [OF type])
apply (rule_tac z="y" in 1)
apply (simp_all add: of_int_eq mod_pos_pos_trivial)
done

lemma (in mod_ring) induct:
  "(!!z. [|0 ≤ z; z < n|] ==> P (of_int z)) ==> P (x::'a)"
by (cases x rule: cases) simp

subsection {* Type Constructor for Integers mod n *}

typedef (open) 'a intmod = "{0..<int_of_type TYPE('a::numeral2)}"
by (rule_tac x=0 in exI, simp add: zero_less_int_of_type)

constdefs
  Abs_intmod' :: "int => 'a::numeral2 intmod"
  "Abs_intmod' x ≡ Abs_intmod (x mod (int_of_type TYPE('a)))"

instance intmod :: (numeral1) "{zero,one,plus,times,minus,power}" ..

defs (overloaded)
  zero_intmod_def: "0 ≡ Abs_intmod 0"
  one_intmod_def:  "1 ≡ Abs_intmod 1"
  add_intmod_def:  "x + y ≡ Abs_intmod' (Rep_intmod x + Rep_intmod y)"
  mult_intmod_def: "x * y ≡ Abs_intmod' (Rep_intmod x * Rep_intmod y)"
  diff_intmod_def: "x - y ≡ Abs_intmod' (Rep_intmod x - Rep_intmod y)"
  minus_intmod_def: "- x ≡ Abs_intmod' (- Rep_intmod x)"
  power_intmod_def: "x ^ k ≡ Abs_intmod' (Rep_intmod x ^ k)"

interpretation intmod:
  mod_type ["int_of_type TYPE('a::numeral2)"
            "Rep_intmod::'a::numeral2 intmod => int"
            "Abs_intmod::int => 'a::numeral2 intmod"]
apply (rule mod_type.intro)
apply (rule type_definition_intmod)
apply (rule one_less_int_of_type)
apply (rule zero_intmod_def)
apply (rule one_intmod_def)
apply (rule add_intmod_def [unfolded Abs_intmod'_def])
apply (rule mult_intmod_def [unfolded Abs_intmod'_def])
apply (rule diff_intmod_def [unfolded Abs_intmod'_def])
apply (rule minus_intmod_def [unfolded Abs_intmod'_def])
apply (rule power_intmod_def [unfolded Abs_intmod'_def])
done

instance intmod :: (numeral2) comm_ring_1
by (rule intmod.comm_ring_1)

instance intmod :: (numeral2) recpower
by (rule intmod.recpower)

instance intmod :: (numeral2) number ..

defs (overloaded)
  number_intmod_def: "number_of w::'a::numeral2 intmod ≡ of_int w"

instance intmod :: (numeral2) number_ring
by intro_classes (simp only: number_intmod_def)

interpretation intmod:
  mod_ring ["int_of_type TYPE('a::numeral2)"
            "Rep_intmod::'a::numeral2 intmod => int"
            "Abs_intmod::int => 'a::numeral2 intmod"] .

lemmas intmod_cases [cases type: intmod, case_names of_int] =
  intmod.cases [unfolded int_of_type_def]

lemmas intmod_induct [induct type: intmod, case_names of_int] =
  intmod.induct [unfolded int_of_type_def]

lemma intmod_iszero_number_of [unfolded int_of_type_def, simp]:
  "iszero (number_of w::'a::numeral2 intmod) =
   (number_of w mod int_of_type TYPE('a) = 0)"
by (rule intmod.iszero_number_of)

syntax
  "intmod" :: "type => type"  ("Z[_]" [1000] 1000)

syntax (xsymbols)
  "intmod" :: "type => type"  ("\<int>_" [1000] 1000)

end