[STATEMENT]
lemma padic_int_is_cring:
  assumes "prime p"
  shows "cring (padic_int p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (padic_int p)
[PROOF STEP]
proof (rule cringI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. abelian_group (padic_int p)
 2. Group.comm_monoid (padic_int p)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
show "abelian_group (padic_int p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abelian_group (padic_int p)
[PROOF STEP]
by (simp add: assms padic_is_abelian_group)
[PROOF STATE]
proof (state)
this:
abelian_group (padic_int p)

goal (2 subgoals):
 1. Group.comm_monoid (padic_int p)
 2. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
show "Group.comm_monoid (padic_int p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group.comm_monoid (padic_int p)
[PROOF STEP]
by (simp add: assms padic_is_comm_monoid)
[PROOF STATE]
proof (state)
this:
Group.comm_monoid (padic_int p)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
show "\<And>x y z.
       x \<in> carrier (padic_int p) \<Longrightarrow>
       y \<in> carrier (padic_int p) \<Longrightarrow>
       z \<in> carrier (padic_int p) \<Longrightarrow>
       (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z =
         x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
fix x y z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
assume Ax: " x \<in> carrier (padic_int p)"
[PROOF STATE]
proof (state)
this:
x \<in> carrier (padic_int p)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
assume Ay: " y \<in> carrier (padic_int p)"
[PROOF STATE]
proof (state)
this:
y \<in> carrier (padic_int p)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
assume Az: " z \<in> carrier (padic_int p)"
[PROOF STATE]
proof (state)
this:
z \<in> carrier (padic_int p)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
show "(x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z 
          = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
have Ex: " (x n) \<in> carrier (residue_ring (p^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
using Ax padic_set_def padic_int_simps
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier (padic_int p)
padic_set ?p = {f. (\<forall>m. f m \<in> carrier (residue_ring (?p ^ m))) \<and> (\<forall>n m. m < n \<longrightarrow> residue (?p ^ m) (f n) = f m)}
\<one>\<^bsub>padic_int ?p\<^esub> = padic_one ?p
\<zero>\<^bsub>padic_int ?p\<^esub> = padic_zero ?p
(\<oplus>\<^bsub>padic_int ?p\<^esub>) = padic_add ?p
(\<otimes>\<^bsub>padic_int ?p\<^esub>) = padic_mult ?p
carrier (padic_int ?p) = padic_set ?p

goal (1 subgoal):
 1. x n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x n \<in> carrier (residue_ring (p ^ n))

goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
have Ey: " (y n) \<in> carrier (residue_ring (p^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
using Ay padic_set_def padic_int_simps
[PROOF STATE]
proof (prove)
using this:
y \<in> carrier (padic_int p)
padic_set ?p = {f. (\<forall>m. f m \<in> carrier (residue_ring (?p ^ m))) \<and> (\<forall>n m. m < n \<longrightarrow> residue (?p ^ m) (f n) = f m)}
\<one>\<^bsub>padic_int ?p\<^esub> = padic_one ?p
\<zero>\<^bsub>padic_int ?p\<^esub> = padic_zero ?p
(\<oplus>\<^bsub>padic_int ?p\<^esub>) = padic_add ?p
(\<otimes>\<^bsub>padic_int ?p\<^esub>) = padic_mult ?p
carrier (padic_int ?p) = padic_set ?p

goal (1 subgoal):
 1. y n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y n \<in> carrier (residue_ring (p ^ n))

goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
have Ez: " (z n) \<in> carrier (residue_ring (p^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
using Az padic_set_def padic_int_simps
[PROOF STATE]
proof (prove)
using this:
z \<in> carrier (padic_int p)
padic_set ?p = {f. (\<forall>m. f m \<in> carrier (residue_ring (?p ^ m))) \<and> (\<forall>n m. m < n \<longrightarrow> residue (?p ^ m) (f n) = f m)}
\<one>\<^bsub>padic_int ?p\<^esub> = padic_one ?p
\<zero>\<^bsub>padic_int ?p\<^esub> = padic_zero ?p
(\<oplus>\<^bsub>padic_int ?p\<^esub>) = padic_add ?p
(\<otimes>\<^bsub>padic_int ?p\<^esub>) = padic_mult ?p
carrier (padic_int ?p) = padic_set ?p

goal (1 subgoal):
 1. z n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z n \<in> carrier (residue_ring (p ^ n))

goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
show "( (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n 
            = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
proof(cases "n=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
 2. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
 2. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
by (metis Ax Ay Az assms padic_add_closed padic_int_simps(4) padic_int_simps(5) padic_mult_in_padic_set padic_set_zero_res)
[PROOF STATE]
proof (state)
this:
((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
have "residues (p^n)"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. residues (p ^ n)
[PROOF STEP]
by (simp add: assms residues_n)
[PROOF STATE]
proof (state)
this:
residues (p ^ n)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
residues (p ^ n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
residues (p ^ n)

goal (1 subgoal):
 1. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
using Ex Ey Ez cring.cring_simprules(13) padic_add_res padic_int_simps
            padic_mult_res residues.cring
[PROOF STATE]
proof (prove)
using this:
residues (p ^ n)
x n \<in> carrier (residue_ring (p ^ n))
y n \<in> carrier (residue_ring (p ^ n))
z n \<in> carrier (residue_ring (p ^ n))
\<lbrakk>cring ?R; ?x \<in> carrier ?R; ?y \<in> carrier ?R; ?z \<in> carrier ?R\<rbrakk> \<Longrightarrow> (?x \<oplus>\<^bsub>?R\<^esub> ?y) \<otimes>\<^bsub>?R\<^esub> ?z = ?x \<otimes>\<^bsub>?R\<^esub> ?z \<oplus>\<^bsub>?R\<^esub> ?y \<otimes>\<^bsub>?R\<^esub> ?z
padic_add ?p ?f ?g ?n = ?f ?n \<oplus>\<^bsub>residue_ring (?p ^ ?n)\<^esub> ?g ?n
\<one>\<^bsub>padic_int ?p\<^esub> = padic_one ?p
\<zero>\<^bsub>padic_int ?p\<^esub> = padic_zero ?p
(\<oplus>\<^bsub>padic_int ?p\<^esub>) = padic_add ?p
(\<otimes>\<^bsub>padic_int ?p\<^esub>) = padic_mult ?p
carrier (padic_int ?p) = padic_set ?p
padic_mult ?p ?f ?g ?n = ?f ?n \<otimes>\<^bsub>residue_ring (?p ^ ?n)\<^esub> ?g ?n
residues ?m \<Longrightarrow> cring (residue_ring ?m)

goal (1 subgoal):
 1. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> carrier (padic_int p); ?y \<in> carrier (padic_int p); ?z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (?x \<oplus>\<^bsub>padic_int p\<^esub> ?y) \<otimes>\<^bsub>padic_int p\<^esub> ?z = ?x \<otimes>\<^bsub>padic_int p\<^esub> ?z \<oplus>\<^bsub>padic_int p\<^esub> ?y \<otimes>\<^bsub>padic_int p\<^esub> ?z

goal:
No subgoals!
[PROOF STEP]
qed