[STATEMENT]
lemma rel_sym:
  assumes "x \<sim> y" "x \<in> R \<times> S" "y \<in> R \<times> S" shows "y \<sim> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sim> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<sim> x
[PROOF STEP]
obtain rx sx ry sy s
    where \<section>: "rx \<in> R" "sx \<in> S" "ry \<in> R" "s \<in> S" "sy \<in> S" "s \<cdot> (sy \<cdot> rx - sx \<cdot> ry) = \<zero>" "x = (rx,sx)" "y = (ry,sy)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>rx sx ry s sy. \<lbrakk>rx \<in> R; sx \<in> S; ry \<in> R; s \<in> S; sy \<in> S; s \<cdot> (sy \<cdot> rx - sx \<cdot> ry) = \<zero>; x = (rx, sx); y = (ry, sy)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sim> y
x \<in> R \<times> S
y \<in> R \<times> S

goal (1 subgoal):
 1. (\<And>rx sx ry s sy. \<lbrakk>rx \<in> R; sx \<in> S; ry \<in> R; s \<in> S; sy \<in> S; s \<cdot> (sy \<cdot> rx - sx \<cdot> ry) = \<zero>; x = (rx, sx); y = (ry, sy)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: rel_def)
[PROOF STATE]
proof (state)
this:
rx \<in> R
sx \<in> S
ry \<in> R
s \<in> S
sy \<in> S
s \<cdot> (sy \<cdot> rx - sx \<cdot> ry) = \<zero>
x = (rx, sx)
y = (ry, sy)

goal (1 subgoal):
 1. y \<sim> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rx \<in> R
sx \<in> S
ry \<in> R
s \<in> S
sy \<in> S
s \<cdot> (sy \<cdot> rx - sx \<cdot> ry) = \<zero>
x = (rx, sx)
y = (ry, sy)
[PROOF STEP]
have "s \<cdot> (sx \<cdot> ry - sy \<cdot> rx) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
rx \<in> R
sx \<in> S
ry \<in> R
s \<in> S
sy \<in> S
s \<cdot> (sy \<cdot> rx - sx \<cdot> ry) = \<zero>
x = (rx, sx)
y = (ry, sy)

goal (1 subgoal):
 1. s \<cdot> (sx \<cdot> ry - sy \<cdot> rx) = \<zero>
[PROOF STEP]
by (metis sub comm.additive.cancel_imp_equal comm.inverse_distributive(1) comm.multiplicative.composition_closed)
[PROOF STATE]
proof (state)
this:
s \<cdot> (sx \<cdot> ry - sy \<cdot> rx) = \<zero>

goal (1 subgoal):
 1. y \<sim> x
[PROOF STEP]
with \<section>
[PROOF STATE]
proof (chain)
picking this:
rx \<in> R
sx \<in> S
ry \<in> R
s \<in> S
sy \<in> S
s \<cdot> (sy \<cdot> rx - sx \<cdot> ry) = \<zero>
x = (rx, sx)
y = (ry, sy)
s \<cdot> (sx \<cdot> ry - sy \<cdot> rx) = \<zero>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rx \<in> R
sx \<in> S
ry \<in> R
s \<in> S
sy \<in> S
s \<cdot> (sy \<cdot> rx - sx \<cdot> ry) = \<zero>
x = (rx, sx)
y = (ry, sy)
s \<cdot> (sx \<cdot> ry - sy \<cdot> rx) = \<zero>

goal (1 subgoal):
 1. y \<sim> x
[PROOF STEP]
by (auto simp: rel_def)
[PROOF STATE]
proof (state)
this:
y \<sim> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_trans:
  assumes "x \<sim> y" "y \<sim> z" "x \<in> R \<times> S" "y \<in> R \<times> S" "z \<in> R \<times> S" shows "x \<sim> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sim> z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sim> y
y \<sim> z
x \<in> R \<times> S
y \<in> R \<times> S
z \<in> R \<times> S

goal (1 subgoal):
 1. x \<sim> z
[PROOF STEP]
proof (clarsimp simp: rel_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb s1 s1a. \<lbrakk>xa \<in> R; ya \<in> S; x = (xa, ya); xaa \<in> R; yaa \<in> S; y = (xaa, yaa); xb \<in> R; yb \<in> S; z = (xb, yb); s1 \<in> S; s1 \<cdot> (yaa \<cdot> xa - ya \<cdot> xaa) = \<zero>; s1a \<in> S; s1a \<cdot> (yb \<cdot> xaa - yaa \<cdot> xb) = \<zero>\<rbrakk> \<Longrightarrow> \<exists>s1. s1 \<in> S \<and> s1 \<cdot> (yb \<cdot> xa - ya \<cdot> xb) = \<zero>
[PROOF STEP]
fix r s r2 s2 r1 s1 sx sy
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb s1 s1a. \<lbrakk>xa \<in> R; ya \<in> S; x = (xa, ya); xaa \<in> R; yaa \<in> S; y = (xaa, yaa); xb \<in> R; yb \<in> S; z = (xb, yb); s1 \<in> S; s1 \<cdot> (yaa \<cdot> xa - ya \<cdot> xaa) = \<zero>; s1a \<in> S; s1a \<cdot> (yb \<cdot> xaa - yaa \<cdot> xb) = \<zero>\<rbrakk> \<Longrightarrow> \<exists>s1. s1 \<in> S \<and> s1 \<cdot> (yb \<cdot> xa - ya \<cdot> xb) = \<zero>
[PROOF STEP]
assume \
: "r \<in> R" "s \<in> S" "r1 \<in> R" "s1 \<in> S" "sx \<in> S" "r2 \<in> R" "s2 \<in> S" "sy \<in> S"
    and sx0: "sx \<cdot> (s1 \<cdot> r2 - s2 \<cdot> r1) = \<zero>" and sy0: "sy \<cdot> (s2 \<cdot> r - s \<cdot> r2) = \<zero>"
[PROOF STATE]
proof (state)
this:
r \<in> R
s \<in> S
r1 \<in> R
s1 \<in> S
sx \<in> S
r2 \<in> R
s2 \<in> S
sy \<in> S
sx \<cdot> (s1 \<cdot> r2 - s2 \<cdot> r1) = \<zero>
sy \<cdot> (s2 \<cdot> r - s \<cdot> r2) = \<zero>

goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb s1 s1a. \<lbrakk>xa \<in> R; ya \<in> S; x = (xa, ya); xaa \<in> R; yaa \<in> S; y = (xaa, yaa); xb \<in> R; yb \<in> S; z = (xb, yb); s1 \<in> S; s1 \<cdot> (yaa \<cdot> xa - ya \<cdot> xaa) = \<zero>; s1a \<in> S; s1a \<cdot> (yb \<cdot> xaa - yaa \<cdot> xb) = \<zero>\<rbrakk> \<Longrightarrow> \<exists>s1. s1 \<in> S \<and> s1 \<cdot> (yb \<cdot> xa - ya \<cdot> xb) = \<zero>
[PROOF STEP]
show "\<exists>u. u \<in> S \<and> u \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. u \<in> S \<and> u \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
proof (intro exI conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?u \<in> S
 2. ?u \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
show "sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<in> S
[PROOF STEP]
using \

[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> S
r1 \<in> R
s1 \<in> S
sx \<in> S
r2 \<in> R
s2 \<in> S
sy \<in> S

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<in> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<in> S

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
have sx: "sx \<cdot> s1 \<cdot> r2 = sx \<cdot> s2 \<cdot> r1" and sy: "sy \<cdot> s2 \<cdot> r = sy \<cdot> s \<cdot> r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sx \<cdot> s1 \<cdot> r2 = sx \<cdot> s2 \<cdot> r1 &&& sy \<cdot> s2 \<cdot> r = sy \<cdot> s \<cdot> r2
[PROOF STEP]
using sx0 sy0 \
 comm.additive.cancel_imp_equal comm.inverse_distributive(1)
        comm.multiplicative.associative comm.multiplicative.composition_closed sub
[PROOF STATE]
proof (prove)
using this:
sx \<cdot> (s1 \<cdot> r2 - s2 \<cdot> r1) = \<zero>
sy \<cdot> (s2 \<cdot> r - s \<cdot> r2) = \<zero>
r \<in> R
s \<in> S
r1 \<in> R
s1 \<in> S
sx \<in> S
r2 \<in> R
s2 \<in> S
sy \<in> S
\<lbrakk>?u - ?v = \<zero>; ?u \<in> R; ?v \<in> R\<rbrakk> \<Longrightarrow> ?u = ?v
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (?b - ?c) = ?a \<cdot> ?b - ?a \<cdot> ?c
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<in> R
?a \<in> S \<Longrightarrow> ?a \<in> R

goal (1 subgoal):
 1. sx \<cdot> s1 \<cdot> r2 = sx \<cdot> s2 \<cdot> r1 &&& sy \<cdot> s2 \<cdot> r = sy \<cdot> s \<cdot> r2
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
sx \<cdot> s1 \<cdot> r2 = sx \<cdot> s2 \<cdot> r1
sy \<cdot> s2 \<cdot> r = sy \<cdot> s \<cdot> r2

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sx \<cdot> s1 \<cdot> r2 = sx \<cdot> s2 \<cdot> r1
sy \<cdot> s2 \<cdot> r = sy \<cdot> s \<cdot> r2
[PROOF STEP]
have "sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s1 \<cdot> r - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1"
[PROOF STATE]
proof (prove)
using this:
sx \<cdot> s1 \<cdot> r2 = sx \<cdot> s2 \<cdot> r1
sy \<cdot> s2 \<cdot> r = sy \<cdot> s \<cdot> r2

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s1 \<cdot> r - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1
[PROOF STEP]
using "\
" \<open>sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<in> S\<close>
        comm.inverse_distributive(1) comm.multiplicative.associative comm.multiplicative.composition_closed
        sub
[PROOF STATE]
proof (prove)
using this:
sx \<cdot> s1 \<cdot> r2 = sx \<cdot> s2 \<cdot> r1
sy \<cdot> s2 \<cdot> r = sy \<cdot> s \<cdot> r2
r \<in> R
s \<in> S
r1 \<in> R
s1 \<in> S
sx \<in> S
r2 \<in> R
s2 \<in> S
sy \<in> S
sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<in> S
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (?b - ?c) = ?a \<cdot> ?b - ?a \<cdot> ?c
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<in> R
?a \<in> S \<Longrightarrow> ?a \<in> R

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s1 \<cdot> r - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s1 \<cdot> r - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s1 \<cdot> r - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
have "... = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s1 \<cdot> r - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1 = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1
[PROOF STEP]
using \

[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> S
r1 \<in> R
s1 \<in> S
sx \<in> S
r2 \<in> R
s2 \<in> S
sy \<in> S

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s1 \<cdot> r - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1 = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1
[PROOF STEP]
by (smt sy comm.comm_mult comm.multiplicative.associative comm.multiplicative.composition_closed sub)
[PROOF STATE]
proof (state)
this:
sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s1 \<cdot> r - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1 = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s1 \<cdot> r - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1 = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
have "... = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s1 \<cdot> s \<cdot> r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1 = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s1 \<cdot> s \<cdot> r2
[PROOF STEP]
using \

[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> S
r1 \<in> R
s1 \<in> S
sx \<in> S
r2 \<in> R
s2 \<in> S
sy \<in> S

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1 = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s1 \<cdot> s \<cdot> r2
[PROOF STEP]
by (smt sx comm.comm_mult comm.multiplicative.associative
          comm.multiplicative.composition_closed sub)
[PROOF STATE]
proof (state)
this:
sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1 = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s1 \<cdot> s \<cdot> r2

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> s \<cdot> r1 = sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s1 \<cdot> s \<cdot> r2

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
have "... = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s1 \<cdot> s \<cdot> r2 = \<zero>
[PROOF STEP]
using \

[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> S
r1 \<in> R
s1 \<in> S
sx \<in> S
r2 \<in> R
s2 \<in> S
sy \<in> S

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s1 \<cdot> s \<cdot> r2 = \<zero>
[PROOF STEP]
by (simp add: comm.ring_mult_ac)
[PROOF STATE]
proof (state)
this:
sx \<cdot> sy \<cdot> s1 \<cdot> s \<cdot> s1 \<cdot> r2 - sx \<cdot> sy \<cdot> s1 \<cdot> s1 \<cdot> s \<cdot> r2 = \<zero>

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
show "sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>

goal (1 subgoal):
 1. sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sx \<cdot> sy \<cdot> s1 \<cdot> s2 \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in> S \<and> u \<cdot> (s1 \<cdot> r - s \<cdot> r1) = \<zero>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frac_Pow:"(r, s) \<in> R \<times> S \<Longrightarrow> frac r s \<in> Pow (R \<times> S) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r, s) \<in> R \<times> S \<Longrightarrow> r / s \<in> Pow (R \<times> S)
[PROOF STEP]
using local.frac_def rel.Class_closed2
[PROOF STATE]
proof (prove)
using this:
?r / ?s \<equiv> rel.Class (?r, ?s)
?a \<in> R \<times> S \<Longrightarrow> rel.Class ?a \<subseteq> R \<times> S

goal (1 subgoal):
 1. (r, s) \<in> R \<times> S \<Longrightarrow> r / s \<in> Pow (R \<times> S)
[PROOF STEP]
by auto


[STATEMENT]
lemma frac_eqI:
  assumes "s1\<in>S" and "(r, s) \<in> R \<times> S" "(r', s') \<in> R \<times> S"
     and eq:"s1 \<cdot> s' \<cdot> r = s1 \<cdot> s \<cdot> r'"
  shows "frac r s = frac r' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r / s = r' / s'
[PROOF STEP]
unfolding frac_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel.Class (r, s) = rel.Class (r', s')
[PROOF STEP]
proof (rule rel.Class_eq)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((r, s), r', s') \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y}
[PROOF STEP]
have "s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>
[PROOF STEP]
using assms comm.inverse_distributive(1) comm.multiplicative.associative
[PROOF STATE]
proof (prove)
using this:
s1 \<in> S
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
s1 \<cdot> s' \<cdot> r = s1 \<cdot> s \<cdot> r'
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (?b - ?c) = ?a \<cdot> ?b - ?a \<cdot> ?c
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1. s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>

goal (1 subgoal):
 1. ((r, s), r', s') \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y}
[PROOF STEP]
with \<open>s1\<in>S\<close>
[PROOF STATE]
proof (chain)
picking this:
s1 \<in> S
s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>
[PROOF STEP]
have "(r, s) \<sim> (r', s')"
[PROOF STATE]
proof (prove)
using this:
s1 \<in> S
s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>

goal (1 subgoal):
 1. (r, s) \<sim> (r', s')
[PROOF STEP]
unfolding rel_def
[PROOF STATE]
proof (prove)
using this:
s1 \<in> S
s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>

goal (1 subgoal):
 1. \<exists>s1. s1 \<in> S \<and> s1 \<cdot> (snd (r', s') \<cdot> fst (r, s) - snd (r, s) \<cdot> fst (r', s')) = \<zero>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(r, s) \<sim> (r', s')

goal (1 subgoal):
 1. ((r, s), r', s') \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(r, s) \<sim> (r', s')
[PROOF STEP]
show "((r, s), r', s') \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y}"
[PROOF STATE]
proof (prove)
using this:
(r, s) \<sim> (r', s')

goal (1 subgoal):
 1. ((r, s), r', s') \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y}
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
(r, s) \<sim> (r', s')
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S

goal (1 subgoal):
 1. ((r, s), r', s') \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((r, s), r', s') \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frac_eq_Ex:
  assumes "(r, s) \<in> R \<times> S" "(r', s') \<in> R \<times> S" "frac r s = frac r' s'"
  obtains s1 where "s1\<in>S" "s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "(r, s) \<sim> (r', s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r, s) \<sim> (r', s')
[PROOF STEP]
using \<open>frac r s = frac r' s'\<close> rel.Class_equivalence[OF assms(1,2)]
[PROOF STATE]
proof (prove)
using this:
r / s = r' / s'
(rel.Class (r, s) = rel.Class (r', s')) = (((r, s), r', s') \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y})

goal (1 subgoal):
 1. (r, s) \<sim> (r', s')
[PROOF STEP]
unfolding frac_def
[PROOF STATE]
proof (prove)
using this:
rel.Class (r, s) = rel.Class (r', s')
(rel.Class (r, s) = rel.Class (r', s')) = (((r, s), r', s') \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y})

goal (1 subgoal):
 1. (r, s) \<sim> (r', s')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(r, s) \<sim> (r', s')

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(r, s) \<sim> (r', s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(r, s) \<sim> (r', s')

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding rel_def
[PROOF STATE]
proof (prove)
using this:
\<exists>s1. s1 \<in> S \<and> s1 \<cdot> (snd (r', s') \<cdot> fst (r, s) - snd (r, s) \<cdot> fst (r', s')) = \<zero>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (metis fst_conv snd_conv that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frac_cancel:
  assumes "s1\<in>S" and "(r, s) \<in> R \<times> S"
  shows "frac (s1\<cdot>r) (s1\<cdot>s) = frac r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s1 \<cdot> r) / (s1 \<cdot> s) = r / s
[PROOF STEP]
apply (rule frac_eqI[of \<one>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<one> \<in> S
 2. (s1 \<cdot> r, s1 \<cdot> s) \<in> R \<times> S
 3. (r, s) \<in> R \<times> S
 4. \<one> \<cdot> s \<cdot> (s1 \<cdot> r) = \<one> \<cdot> (s1 \<cdot> s) \<cdot> r
[PROOF STEP]
using assms comm_ring_simps
[PROOF STATE]
proof (prove)
using this:
s1 \<in> S
(r, s) \<in> R \<times> S
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a + ?b + ?c = ?a + (?b + ?c)
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b = ?b \<cdot> ?a
\<lbrakk>?x \<in> R; ?y \<in> R\<rbrakk> \<Longrightarrow> ?x + ?y = ?y + ?x
plus ?a (- ?a) = (0::?'a)

goal (4 subgoals):
 1. \<one> \<in> S
 2. (s1 \<cdot> r, s1 \<cdot> s) \<in> R \<times> S
 3. (r, s) \<in> R \<times> S
 4. \<one> \<cdot> s \<cdot> (s1 \<cdot> r) = \<one> \<cdot> (s1 \<cdot> s) \<cdot> r
[PROOF STEP]
by auto


[STATEMENT]
lemma frac_eq_obtains:
  assumes "(r,s) \<in> R \<times> S" and x_def:"x=(SOME x. x\<in>(frac r s))"
  obtains s1 where "s1\<in>S" "s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r" and "x \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x\<in>(r/s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> r / s
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. x \<in> r / s) \<in> r / s
[PROOF STEP]
apply (rule someI[of _ "(r,s)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r, s) \<in> r / s
[PROOF STEP]
using assms(1) local.frac_def
[PROOF STATE]
proof (prove)
using this:
(r, s) \<in> R \<times> S
?r / ?s \<equiv> rel.Class (?r, ?s)

goal (1 subgoal):
 1. (r, s) \<in> r / s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> r / s

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from rel.ClassD[OF this[unfolded frac_def] \<open>(r,s) \<in> R \<times> S\<close>]
[PROOF STATE]
proof (chain)
picking this:
(x, r, s) \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y}
[PROOF STEP]
have x_RS:"x\<in>R \<times> S" and "x \<sim> (r,s)"
[PROOF STATE]
proof (prove)
using this:
(x, r, s) \<in> {(x, y). (x, y) \<in> (R \<times> S) \<times> R \<times> S \<and> x \<sim> y}

goal (1 subgoal):
 1. x \<in> R \<times> S &&& x \<sim> (r, s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> R \<times> S
x \<sim> (r, s)

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
x \<sim> (r, s)
[PROOF STEP]
obtain s1 where "s1\<in>S" and "s1 \<cdot> (s \<cdot> fst x - snd x \<cdot> r) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
x \<sim> (r, s)

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> (s \<cdot> fst x - snd x \<cdot> r) = \<zero>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rel_def
[PROOF STATE]
proof (prove)
using this:
\<exists>s1. s1 \<in> S \<and> s1 \<cdot> (snd (r, s) \<cdot> fst x - snd x \<cdot> fst (r, s)) = \<zero>

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> (s \<cdot> fst x - snd x \<cdot> r) = \<zero>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<in> S
s1 \<cdot> (s \<cdot> fst x - snd x \<cdot> r) = \<zero>

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 \<in> S
s1 \<cdot> (s \<cdot> fst x - snd x \<cdot> r) = \<zero>
[PROOF STEP]
have x_eq:"s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r"
[PROOF STATE]
proof (prove)
using this:
s1 \<in> S
s1 \<cdot> (s \<cdot> fst x - snd x \<cdot> r) = \<zero>

goal (1 subgoal):
 1. s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r
[PROOF STEP]
using comm.distributive x_RS assms(1)
[PROOF STATE]
proof (prove)
using this:
s1 \<in> S
s1 \<cdot> (s \<cdot> fst x - snd x \<cdot> r) = \<zero>
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> (?b + ?c) \<cdot> ?a = ?b \<cdot> ?a + ?c \<cdot> ?a
x \<in> R \<times> S
(r, s) \<in> R \<times> S

goal (1 subgoal):
 1. s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r
[PROOF STEP]
by (smt comm.additive.group_axioms group.cancel_imp_equal comm.inverse_distributive(1)
        mem_Sigma_iff comm.multiplicative.associative comm.multiplicative.composition_closed prod.collapse sub)
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that x_RS \<open>s1\<in>S\<close>
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r
\<lbrakk>?s1.3 \<in> S; ?s1.3 \<cdot> s \<cdot> fst x = ?s1.3 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis
x \<in> R \<times> S
s1 \<in> S

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frac_non_empty[simp]:"(a,b) \<in> R \<times> S \<Longrightarrow> valid_frac (frac a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> R \<times> S \<Longrightarrow> valid_frac (a / b)
[PROOF STEP]
unfolding frac_def valid_frac_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> R \<times> S \<Longrightarrow> \<exists>r\<in>R. \<exists>s\<in>S. rel.Class (r, s) = rel.Class (a, b)
[PROOF STEP]
by blast


[STATEMENT]
lemma valid_frac_add[intro,simp]:
  assumes "valid_frac X" "valid_frac Y"
  shows "valid_frac (add_rel X Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_frac (add_rel X Y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_frac (add_rel X Y)
[PROOF STEP]
obtain r s r' s' where "r\<in>R" "s\<in>S" "r'\<in>R" "s'\<in>S"
      and *:"add_rel X Y = (r\<cdot>s' + r'\<cdot>s) / (s\<cdot>s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define x where "x=(SOME x. x\<in>X)"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> X)

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define y where "y=(SOME y. y\<in>Y)"
[PROOF STATE]
proof (state)
this:
y = (SOME y. y \<in> Y)

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x\<in>X" "y\<in>Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X &&& y \<in> Y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
valid_frac X
valid_frac Y

goal (1 subgoal):
 1. x \<in> X &&& y \<in> Y
[PROOF STEP]
unfolding x_def y_def valid_frac_def some_in_eq local.frac_def
[PROOF STATE]
proof (prove)
using this:
\<exists>r\<in>R. \<exists>s\<in>S. rel.Class (r, s) = X
\<exists>r\<in>R. \<exists>s\<in>S. rel.Class (r, s) = Y

goal (1 subgoal):
 1. X \<noteq> {} &&& Y \<noteq> {}
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
x \<in> X
y \<in> Y

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
y \<in> Y
[PROOF STEP]
obtain "x \<in> R \<times> S" "y \<in> R \<times> S"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
y \<in> Y

goal (1 subgoal):
 1. (\<lbrakk>x \<in> R \<times> S; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> X
y \<in> Y
valid_frac X
valid_frac Y

goal (1 subgoal):
 1. (\<lbrakk>x \<in> R \<times> S; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: valid_frac_def x_def y_def) (metis frac_eq_obtains mem_Sigma_iff)
[PROOF STATE]
proof (state)
this:
x \<in> R \<times> S
y \<in> R \<times> S

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> R \<times> S
y \<in> R \<times> S

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "add_rel X Y = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel X Y = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)
[PROOF STEP]
unfolding add_rel_def add_rel_aux_def x_def y_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (SOME x. x \<in> X) \<cdot> snd (SOME y. y \<in> Y) + fst (SOME y. y \<in> Y) \<cdot> snd (SOME x. x \<in> X)) / (snd (SOME x. x \<in> X) \<cdot> snd (SOME y. y \<in> Y)) = (fst (SOME x. x \<in> X) \<cdot> snd (SOME y. y \<in> Y) + fst (SOME y. y \<in> Y) \<cdot> snd (SOME x. x \<in> X)) / (snd (SOME x. x \<in> X) \<cdot> snd (SOME y. y \<in> Y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
add_rel X Y = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> R \<times> S
y \<in> R \<times> S
add_rel X Y = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> R \<times> S
y \<in> R \<times> S
add_rel X Y = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> R \<times> S
y \<in> R \<times> S
add_rel X Y = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)
\<lbrakk>?r3 \<in> R; ?s3 \<in> S; ?r'3 \<in> R; ?s'3 \<in> S; add_rel X Y = (?r3 \<cdot> ?s'3 + ?r'3 \<cdot> ?s3) / (?s3 \<cdot> ?s'3)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<in> R
s \<in> S
r' \<in> R
s' \<in> S
add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')

goal (1 subgoal):
 1. valid_frac (add_rel X Y)
[PROOF STEP]
from this(1-4)
[PROOF STATE]
proof (chain)
picking this:
r \<in> R
s \<in> S
r' \<in> R
s' \<in> S
[PROOF STEP]
have "(r\<cdot>s' + r'\<cdot>s,s\<cdot>s') \<in> R \<times> S"
[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> S
r' \<in> R
s' \<in> S

goal (1 subgoal):
 1. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S

goal (1 subgoal):
 1. valid_frac (add_rel X Y)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
(r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
add_rel X Y = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
(r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S

goal (1 subgoal):
 1. valid_frac (add_rel X Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_frac (add_rel X Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uminus_rel_frac:
  assumes "(r,s) \<in> R \<times> S"
  shows "uminus_rel (r/s) = (comm.additive.inverse r) / s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_rel (r / s) = comm.additive.inverse r / s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uminus_rel (r / s) = comm.additive.inverse r / s
[PROOF STEP]
define x where "x=(SOME x. x\<in>(r/s))"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> r / s)

goal (1 subgoal):
 1. uminus_rel (r / s) = comm.additive.inverse r / s
[PROOF STEP]
obtain s1 where [simp]:"s1 \<in> S" and x_eq:"s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r" and x_RS:"x \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using frac_eq_obtains[OF \<open>(r,s) \<in> R \<times> S\<close> x_def]
[PROOF STATE]
proof (prove)
using this:
(\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<in> S
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r
x \<in> R \<times> S

goal (1 subgoal):
 1. uminus_rel (r / s) = comm.additive.inverse r / s
[PROOF STEP]
have "uminus_rel (r/s)= (comm.additive.inverse (fst x)) / (snd x )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_rel (r / s) = comm.additive.inverse (fst x) / snd x
[PROOF STEP]
unfolding uminus_rel_def x_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm.additive.inverse (fst (SOME x. x \<in> r / s)) / snd (SOME x. x \<in> r / s) = comm.additive.inverse (fst (SOME x. x \<in> r / s)) / snd (SOME x. x \<in> r / s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uminus_rel (r / s) = comm.additive.inverse (fst x) / snd x

goal (1 subgoal):
 1. uminus_rel (r / s) = comm.additive.inverse r / s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
uminus_rel (r / s) = comm.additive.inverse (fst x) / snd x

goal (1 subgoal):
 1. uminus_rel (r / s) = comm.additive.inverse r / s
[PROOF STEP]
have "... = (comm.additive.inverse r) / s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm.additive.inverse (fst x) / snd x = comm.additive.inverse r / s
[PROOF STEP]
apply (rule frac_eqI[of s1])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. s1 \<in> S
 2. (comm.additive.inverse (fst x), snd x) \<in> R \<times> S
 3. (comm.additive.inverse r, s) \<in> R \<times> S
 4. s1 \<cdot> s \<cdot> comm.additive.inverse (fst x) = s1 \<cdot> snd x \<cdot> comm.additive.inverse r
[PROOF STEP]
using x_RS assms x_eq
[PROOF STATE]
proof (prove)
using this:
x \<in> R \<times> S
(r, s) \<in> R \<times> S
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r

goal (4 subgoals):
 1. s1 \<in> S
 2. (comm.additive.inverse (fst x), snd x) \<in> R \<times> S
 3. (comm.additive.inverse r, s) \<in> R \<times> S
 4. s1 \<cdot> s \<cdot> comm.additive.inverse (fst x) = s1 \<cdot> snd x \<cdot> comm.additive.inverse r
[PROOF STEP]
by (auto simp add: comm.right_minus)
[PROOF STATE]
proof (state)
this:
comm.additive.inverse (fst x) / snd x = comm.additive.inverse r / s

goal (1 subgoal):
 1. uminus_rel (r / s) = comm.additive.inverse r / s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
uminus_rel (r / s) = comm.additive.inverse r / s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uminus_rel (r / s) = comm.additive.inverse r / s

goal (1 subgoal):
 1. uminus_rel (r / s) = comm.additive.inverse r / s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
uminus_rel (r / s) = comm.additive.inverse r / s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_frac_uminus[intro,simp]:
  assumes "valid_frac X"
  shows "valid_frac (uminus_rel X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_frac (uminus_rel X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_frac (uminus_rel X)
[PROOF STEP]
obtain r s where "r\<in>R" "s\<in>S"
      and *:"uminus_rel X = (comm.additive.inverse r) / s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> S; uminus_rel X = comm.additive.inverse r / s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> S; uminus_rel X = comm.additive.inverse r / s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define x where "x=(SOME x. x\<in>X)"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> X)

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> S; uminus_rel X = comm.additive.inverse r / s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x\<in>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
valid_frac X

goal (1 subgoal):
 1. x \<in> X
[PROOF STEP]
unfolding x_def valid_frac_def some_in_eq local.frac_def
[PROOF STATE]
proof (prove)
using this:
\<exists>r\<in>R. \<exists>s\<in>S. rel.Class (r, s) = X

goal (1 subgoal):
 1. X \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> S; uminus_rel X = comm.additive.inverse r / s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
have "x\<in> R \<times> S"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. x \<in> R \<times> S
[PROOF STEP]
using assms valid_frac_def
[PROOF STATE]
proof (prove)
using this:
x \<in> X
valid_frac X
valid_frac ?X \<equiv> \<exists>r\<in>R. \<exists>s\<in>S. r / s = ?X

goal (1 subgoal):
 1. x \<in> R \<times> S
[PROOF STEP]
by (metis frac_eq_obtains mem_Sigma_iff x_def)
[PROOF STATE]
proof (state)
this:
x \<in> R \<times> S

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> S; uminus_rel X = comm.additive.inverse r / s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> R \<times> S

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> S; uminus_rel X = comm.additive.inverse r / s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "uminus_rel X = (comm.additive.inverse (fst x) ) / (snd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_rel X = comm.additive.inverse (fst x) / snd x
[PROOF STEP]
unfolding uminus_rel_def x_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm.additive.inverse (fst (SOME x. x \<in> X)) / snd (SOME x. x \<in> X) = comm.additive.inverse (fst (SOME x. x \<in> X)) / snd (SOME x. x \<in> X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uminus_rel X = comm.additive.inverse (fst x) / snd x

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> S; uminus_rel X = comm.additive.inverse r / s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> R \<times> S
uminus_rel X = comm.additive.inverse (fst x) / snd x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> R \<times> S
uminus_rel X = comm.additive.inverse (fst x) / snd x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> R \<times> S
uminus_rel X = comm.additive.inverse (fst x) / snd x
\<lbrakk>?r3 \<in> R; ?s3 \<in> S; uminus_rel X = comm.additive.inverse ?r3 / ?s3\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<in> R
s \<in> S
uminus_rel X = comm.additive.inverse r / s

goal (1 subgoal):
 1. valid_frac (uminus_rel X)
[PROOF STEP]
from this(1-3)
[PROOF STATE]
proof (chain)
picking this:
r \<in> R
s \<in> S
uminus_rel X = comm.additive.inverse r / s
[PROOF STEP]
have "(comm.additive.inverse r,s) \<in> R \<times> S"
[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> S
uminus_rel X = comm.additive.inverse r / s

goal (1 subgoal):
 1. (comm.additive.inverse r, s) \<in> R \<times> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(comm.additive.inverse r, s) \<in> R \<times> S

goal (1 subgoal):
 1. valid_frac (uminus_rel X)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
uminus_rel X = comm.additive.inverse r / s
(comm.additive.inverse r, s) \<in> R \<times> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uminus_rel X = comm.additive.inverse r / s
(comm.additive.inverse r, s) \<in> R \<times> S

goal (1 subgoal):
 1. valid_frac (uminus_rel X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_frac (uminus_rel X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_rel_frac:
  assumes "(r,s) \<in> R \<times> S" "(r',s')\<in> R \<times> S"
  shows "mult_rel (r/s) (r'/s') = (r\<cdot> r') / (s\<cdot>s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
define x where "x=(SOME x. x\<in>(r/s))"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> r / s)

goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
define y where "y=(SOME y. y\<in>(r'/s'))"
[PROOF STATE]
proof (state)
this:
y = (SOME y. y \<in> r' / s')

goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
obtain s1 where [simp]:"s1 \<in> S" and x_eq:"s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r" and x_RS:"x \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using frac_eq_obtains[OF \<open>(r,s) \<in> R \<times> S\<close> x_def]
[PROOF STATE]
proof (prove)
using this:
(\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<in> S
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r
x \<in> R \<times> S

goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
obtain s2 where [simp]:"s2 \<in> S" and y_eq:"s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'" and y_RS:"y \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>s2 \<in> S; s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using frac_eq_obtains[OF \<open>(r',s') \<in> R \<times> S\<close> y_def]
[PROOF STATE]
proof (prove)
using this:
(\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s' \<cdot> fst y = s1 \<cdot> snd y \<cdot> r'; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>s2 \<in> S; s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s2 \<in> S
s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'
y \<in> R \<times> S

goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
have "mult_rel (r/s) (r'/s') = (fst x \<cdot> fst y ) / (snd x \<cdot> snd y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (fst x \<cdot> fst y) / (snd x \<cdot> snd y)
[PROOF STEP]
unfolding mult_rel_def mult_rel_aux_def x_def y_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (SOME x. x \<in> r / s) \<cdot> fst (SOME y. y \<in> r' / s')) / (snd (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s')) = (fst (SOME x. x \<in> r / s) \<cdot> fst (SOME y. y \<in> r' / s')) / (snd (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mult_rel (r / s) (r' / s') = (fst x \<cdot> fst y) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mult_rel (r / s) (r' / s') = (fst x \<cdot> fst y) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
have "... = (r\<cdot> r') / (s\<cdot>s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst x \<cdot> fst y) / (snd x \<cdot> snd y) = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
proof (rule frac_eqI[of "s1 \<cdot> s2"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> fst y, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> r', s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> fst y) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> r')
[PROOF STEP]
have "(s1 \<cdot> s \<cdot> fst x) \<cdot> (s2 \<cdot> s' \<cdot> fst y)  = (s1 \<cdot> snd x \<cdot> r) \<cdot> (s2 \<cdot> snd y \<cdot> r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 \<cdot> s \<cdot> fst x \<cdot> (s2 \<cdot> s' \<cdot> fst y) = s1 \<cdot> snd x \<cdot> r \<cdot> (s2 \<cdot> snd y \<cdot> r')
[PROOF STEP]
using x_eq y_eq
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r
s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'

goal (1 subgoal):
 1. s1 \<cdot> s \<cdot> fst x \<cdot> (s2 \<cdot> s' \<cdot> fst y) = s1 \<cdot> snd x \<cdot> r \<cdot> (s2 \<cdot> snd y \<cdot> r')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s \<cdot> fst x \<cdot> (s2 \<cdot> s' \<cdot> fst y) = s1 \<cdot> snd x \<cdot> r \<cdot> (s2 \<cdot> snd y \<cdot> r')

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> fst y, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> r', s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> fst y) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> r')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 \<cdot> s \<cdot> fst x \<cdot> (s2 \<cdot> s' \<cdot> fst y) = s1 \<cdot> snd x \<cdot> r \<cdot> (s2 \<cdot> snd y \<cdot> r')
[PROOF STEP]
show "s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> fst y) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> r')"
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s \<cdot> fst x \<cdot> (s2 \<cdot> s' \<cdot> fst y) = s1 \<cdot> snd x \<cdot> r \<cdot> (s2 \<cdot> snd y \<cdot> r')

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> fst y) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> r')
[PROOF STEP]
using comm.multiplicative.associative assms x_RS y_RS comm.distributive comm.comm_mult
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s \<cdot> fst x \<cdot> (s2 \<cdot> s' \<cdot> fst y) = s1 \<cdot> snd x \<cdot> r \<cdot> (s2 \<cdot> snd y \<cdot> r')
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> (?b + ?c) \<cdot> ?a = ?b \<cdot> ?a + ?c \<cdot> ?a
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b = ?b \<cdot> ?a

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> fst y) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> r')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> fst y) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> r')

goal (3 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> fst y, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> r', s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
show "s1 \<cdot> s2 \<in> S" "(fst x \<cdot> fst y, snd x \<cdot> snd y) \<in> R \<times> S"
        "(r \<cdot> r', s \<cdot> s') \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 \<cdot> s2 \<in> S &&& (fst x \<cdot> fst y, snd x \<cdot> snd y) \<in> R \<times> S &&& (r \<cdot> r', s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
using assms x_RS y_RS
[PROOF STATE]
proof (prove)
using this:
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S

goal (1 subgoal):
 1. s1 \<cdot> s2 \<in> S &&& (fst x \<cdot> fst y, snd x \<cdot> snd y) \<in> R \<times> S &&& (r \<cdot> r', s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<in> S
(fst x \<cdot> fst y, snd x \<cdot> snd y) \<in> R \<times> S
(r \<cdot> r', s \<cdot> s') \<in> R \<times> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(fst x \<cdot> fst y) / (snd x \<cdot> snd y) = (r \<cdot> r') / (s \<cdot> s')

goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')

goal (1 subgoal):
 1. mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mult_rel (r / s) (r' / s') = (r \<cdot> r') / (s \<cdot> s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_frac_mult[intro,simp]:
  assumes "valid_frac X" "valid_frac Y"
  shows "valid_frac (mult_rel X Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_frac (mult_rel X Y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_frac (mult_rel X Y)
[PROOF STEP]
obtain r s r' s' where "r\<in>R" "s\<in>S" "r'\<in>R" "s'\<in>S"
      and *:"mult_rel X Y = (r\<cdot> r') / (s\<cdot>s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define x where "x=(SOME x. x\<in>X)"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> X)

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define y where "y=(SOME y. y\<in>Y)"
[PROOF STATE]
proof (state)
this:
y = (SOME y. y \<in> Y)

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x\<in>X" "y\<in>Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X &&& y \<in> Y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
valid_frac X
valid_frac Y

goal (1 subgoal):
 1. x \<in> X &&& y \<in> Y
[PROOF STEP]
unfolding x_def y_def valid_frac_def some_in_eq local.frac_def
[PROOF STATE]
proof (prove)
using this:
\<exists>r\<in>R. \<exists>s\<in>S. rel.Class (r, s) = X
\<exists>r\<in>R. \<exists>s\<in>S. rel.Class (r, s) = Y

goal (1 subgoal):
 1. X \<noteq> {} &&& Y \<noteq> {}
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
x \<in> X
y \<in> Y

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
y \<in> Y
[PROOF STEP]
obtain "x \<in> R \<times> S" "y \<in> R \<times> S"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
y \<in> Y

goal (1 subgoal):
 1. (\<lbrakk>x \<in> R \<times> S; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> X
y \<in> Y
valid_frac X
valid_frac Y

goal (1 subgoal):
 1. (\<lbrakk>x \<in> R \<times> S; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: valid_frac_def x_def y_def) (metis frac_eq_obtains mem_Sigma_iff)
[PROOF STATE]
proof (state)
this:
x \<in> R \<times> S
y \<in> R \<times> S

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> R \<times> S
y \<in> R \<times> S

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "mult_rel X Y = (fst x \<cdot> fst y) / (snd x \<cdot> snd y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel X Y = (fst x \<cdot> fst y) / (snd x \<cdot> snd y)
[PROOF STEP]
unfolding mult_rel_def mult_rel_aux_def x_def y_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (SOME x. x \<in> X) \<cdot> fst (SOME y. y \<in> Y)) / (snd (SOME x. x \<in> X) \<cdot> snd (SOME y. y \<in> Y)) = (fst (SOME x. x \<in> X) \<cdot> fst (SOME y. y \<in> Y)) / (snd (SOME x. x \<in> X) \<cdot> snd (SOME y. y \<in> Y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mult_rel X Y = (fst x \<cdot> fst y) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. (\<And>r s r' s'. \<lbrakk>r \<in> R; s \<in> S; r' \<in> R; s' \<in> S; mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> R \<times> S
y \<in> R \<times> S
mult_rel X Y = (fst x \<cdot> fst y) / (snd x \<cdot> snd y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> R \<times> S
y \<in> R \<times> S
mult_rel X Y = (fst x \<cdot> fst y) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> R \<times> S
y \<in> R \<times> S
mult_rel X Y = (fst x \<cdot> fst y) / (snd x \<cdot> snd y)
\<lbrakk>?r3 \<in> R; ?s3 \<in> S; ?r'3 \<in> R; ?s'3 \<in> S; mult_rel X Y = (?r3 \<cdot> ?r'3) / (?s3 \<cdot> ?s'3)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<in> R
s \<in> S
r' \<in> R
s' \<in> S
mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')

goal (1 subgoal):
 1. valid_frac (mult_rel X Y)
[PROOF STEP]
from this(1-4)
[PROOF STATE]
proof (chain)
picking this:
r \<in> R
s \<in> S
r' \<in> R
s' \<in> S
[PROOF STEP]
have "(r\<cdot>r',s\<cdot>s') \<in> R \<times> S"
[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> S
r' \<in> R
s' \<in> S

goal (1 subgoal):
 1. (r \<cdot> r', s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(r \<cdot> r', s \<cdot> s') \<in> R \<times> S

goal (1 subgoal):
 1. valid_frac (mult_rel X Y)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')
(r \<cdot> r', s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mult_rel X Y = (r \<cdot> r') / (s \<cdot> s')
(r \<cdot> r', s \<cdot> s') \<in> R \<times> S

goal (1 subgoal):
 1. valid_frac (mult_rel X Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_frac (mult_rel X Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_frac_zero[simp]:
  "valid_frac zero_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_frac zero_rel
[PROOF STEP]
unfolding zero_rel_def valid_frac_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r\<in>R. \<exists>s\<in>S. r / s = \<zero> / \<one>
[PROOF STEP]
by blast


[STATEMENT]
lemma valid_frac_one[simp]:
  "valid_frac one_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_frac one_rel
[PROOF STEP]
unfolding one_rel_def valid_frac_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r\<in>R. \<exists>s\<in>S. r / s = \<one> / \<one>
[PROOF STEP]
by blast


[STATEMENT]
lemma carrier_quotient_ring_iff[iff]: "X \<in> carrier_quotient_ring \<longleftrightarrow> valid_frac X "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<in> carrier_quotient_ring) = valid_frac X
[PROOF STEP]
unfolding valid_frac_def carrier_quotient_ring_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<in> rel.Partition) = (\<exists>r\<in>R. \<exists>s\<in>S. r / s = X)
[PROOF STEP]
using local.frac_def rel.natural.map_closed rel.representant_exists
[PROOF STATE]
proof (prove)
using this:
?r / ?s \<equiv> rel.Class (?r, ?s)
?a \<in> R \<times> S \<Longrightarrow> rel.Class ?a \<in> rel.Partition
?A \<in> rel.Partition \<Longrightarrow> \<exists>a\<in>R \<times> S. a \<in> ?A \<and> ?A = rel.Class a

goal (1 subgoal):
 1. (X \<in> rel.Partition) = (\<exists>r\<in>R. \<exists>s\<in>S. r / s = X)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma frac_from_carrier:
  assumes "X \<in> carrier_quotient_ring"
  obtains r s where "r \<in> R" "s \<in> S" "X = rel.Class (r,s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> S; X = rel.Class (r, s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms carrier_quotient_ring_def
[PROOF STATE]
proof (prove)
using this:
X \<in> carrier_quotient_ring
carrier_quotient_ring \<equiv> rel.Partition

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> S; X = rel.Class (r, s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, lifting) SigmaE rel.representant_exists)


[STATEMENT]
lemma add_minus_zero_rel:
  assumes "valid_frac a"
  shows "add_rel a (uminus_rel a) = zero_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
obtain a1 a2 where a_RS:"(a1, a2)\<in>R \<times> S" and a12:"a = a1 / a2 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a1 a2. \<lbrakk>(a1, a2) \<in> R \<times> S; a = a1 / a2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>valid_frac a\<close>
[PROOF STATE]
proof (prove)
using this:
valid_frac a

goal (1 subgoal):
 1. (\<And>a1 a2. \<lbrakk>(a1, a2) \<in> R \<times> S; a = a1 / a2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding valid_frac_def
[PROOF STATE]
proof (prove)
using this:
\<exists>r\<in>R. \<exists>s\<in>S. r / s = a

goal (1 subgoal):
 1. (\<And>a1 a2. \<lbrakk>(a1, a2) \<in> R \<times> S; a = a1 / a2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a1, a2) \<in> R \<times> S
a = a1 / a2

goal (1 subgoal):
 1. add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
have "add_rel a (uminus_rel a) =  \<zero> / (a2 \<cdot> a2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel a (uminus_rel a) = \<zero> / (a2 \<cdot> a2)
[PROOF STEP]
unfolding a12
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel (a1 / a2) (uminus_rel (a1 / a2)) = \<zero> / (a2 \<cdot> a2)
[PROOF STEP]
using comm_ring_simps a_RS
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a + ?b + ?c = ?a + (?b + ?c)
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b = ?b \<cdot> ?a
\<lbrakk>?x \<in> R; ?y \<in> R\<rbrakk> \<Longrightarrow> ?x + ?y = ?y + ?x
plus ?a (- ?a) = (0::?'a)
(a1, a2) \<in> R \<times> S

goal (1 subgoal):
 1. add_rel (a1 / a2) (uminus_rel (a1 / a2)) = \<zero> / (a2 \<cdot> a2)
[PROOF STEP]
by (simp add:add_rel_frac uminus_rel_frac comm.right_minus)
[PROOF STATE]
proof (state)
this:
add_rel a (uminus_rel a) = \<zero> / (a2 \<cdot> a2)

goal (1 subgoal):
 1. add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
add_rel a (uminus_rel a) = \<zero> / (a2 \<cdot> a2)

goal (1 subgoal):
 1. add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
have "... = \<zero> / \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> / (a2 \<cdot> a2) = \<zero> / \<one>
[PROOF STEP]
apply (rule frac_eqI[of \<one>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<one> \<in> S
 2. (\<zero>, a2 \<cdot> a2) \<in> R \<times> S
 3. (\<zero>, \<one>) \<in> R \<times> S
 4. \<one> \<cdot> \<one> \<cdot> \<zero> = \<one> \<cdot> (a2 \<cdot> a2) \<cdot> \<zero>
[PROOF STEP]
using a_RS
[PROOF STATE]
proof (prove)
using this:
(a1, a2) \<in> R \<times> S

goal (4 subgoals):
 1. \<one> \<in> S
 2. (\<zero>, a2 \<cdot> a2) \<in> R \<times> S
 3. (\<zero>, \<one>) \<in> R \<times> S
 4. \<one> \<cdot> \<one> \<cdot> \<zero> = \<one> \<cdot> (a2 \<cdot> a2) \<cdot> \<zero>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<zero> / (a2 \<cdot> a2) = \<zero> / \<one>

goal (1 subgoal):
 1. add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<zero> / (a2 \<cdot> a2) = \<zero> / \<one>

goal (1 subgoal):
 1. add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
have "... = zero_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> / \<one> = zero_rel
[PROOF STEP]
unfolding zero_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> / \<one> = \<zero> / \<one>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<zero> / \<one> = zero_rel

goal (1 subgoal):
 1. add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
show "add_rel a (uminus_rel a) = zero_rel"
[PROOF STATE]
proof (prove)
using this:
add_rel a (uminus_rel a) = zero_rel

goal (1 subgoal):
 1. add_rel a (uminus_rel a) = zero_rel
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
add_rel a (uminus_rel a) = zero_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma submonoid_pr_ideal:
  shows "submonoid (R \<setminus> I) R (\<cdot>) \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid (R\<setminus>I) R (\<cdot>) \<one>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. R\<setminus>I \<subseteq> R
 2. \<And>a b. \<lbrakk>a \<in> R\<setminus>I; b \<in> R\<setminus>I\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> R\<setminus>I
 3. \<one> \<in> R\<setminus>I
[PROOF STEP]
show "a \<cdot> b \<in> R\<setminus>I" if "a \<in> R\<setminus>I" "b \<in> R\<setminus>I" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> b \<in> R\<setminus>I
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> R\<setminus>I
b \<in> R\<setminus>I

goal (1 subgoal):
 1. a \<cdot> b \<in> R\<setminus>I
[PROOF STEP]
by (metis Diff_iff absorbent comm.multiplicative.composition_closed)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a3 \<in> R\<setminus>I; ?b3 \<in> R\<setminus>I\<rbrakk> \<Longrightarrow> ?a3 \<cdot> ?b3 \<in> R\<setminus>I

goal (2 subgoals):
 1. R\<setminus>I \<subseteq> R
 2. \<one> \<in> R\<setminus>I
[PROOF STEP]
show "\<one> \<in> R\<setminus>I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one> \<in> R\<setminus>I
[PROOF STEP]
using ideal.ideal(2) ideal_axioms pr_ideal.carrier_neq pr_ideal_axioms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ideal ?I ?R ?addition ?multiplication ?zero ?unit; ?a \<in> ?R; ?b \<in> ?I\<rbrakk> \<Longrightarrow> ?multiplication ?b ?a \<in> ?I
ideal I R (+) (\<cdot>) \<zero> \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> ?I \<noteq> ?R
pr_ideal R I (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. \<one> \<in> R\<setminus>I
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<one> \<in> R\<setminus>I

goal (1 subgoal):
 1. R\<setminus>I \<subseteq> R
[PROOF STEP]
qed auto


[STATEMENT]
lemma frac_from_carrier_local:
  assumes "X \<in> carrier_local_ring_at"
  obtains r s where "r \<in> R" "s \<in> R" "s \<notin> I" "X = local.frac r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> R; s \<notin> I; X = local.frac r s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> R; s \<notin> I; X = local.frac r s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "X \<in> (R \<setminus> I)\<^sup>\<inverse> R\<^bsub>(+) (\<cdot>) \<zero>\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> local.carrier_quotient_ring
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X \<in> carrier_local_ring_at

goal (1 subgoal):
 1. X \<in> local.carrier_quotient_ring
[PROOF STEP]
by (simp add: carrier_local_ring_at_def)
[PROOF STATE]
proof (state)
this:
X \<in> local.carrier_quotient_ring

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> R; s \<notin> I; X = local.frac r s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<in> local.carrier_quotient_ring
[PROOF STEP]
have "X \<in> quotient_ring.carrier_quotient_ring (R \<setminus> I) R (+) (\<cdot>) \<zero>"
[PROOF STATE]
proof (prove)
using this:
X \<in> local.carrier_quotient_ring

goal (1 subgoal):
 1. X \<in> local.carrier_quotient_ring
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X \<in> local.carrier_quotient_ring

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> R; s \<notin> I; X = local.frac r s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<in> local.carrier_quotient_ring
[PROOF STEP]
obtain r s where "r \<in> R" "s \<in> (R \<setminus> I)" "X = local.frac r s"
[PROOF STATE]
proof (prove)
using this:
X \<in> local.carrier_quotient_ring

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> R\<setminus>I; X = local.frac r s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using local.frac_from_carrier
[PROOF STATE]
proof (prove)
using this:
X \<in> local.carrier_quotient_ring
\<lbrakk>?X \<in> local.carrier_quotient_ring; \<And>r s. \<lbrakk>r \<in> R; s \<in> R\<setminus>I; ?X = equivalence.Class (R \<times> (R\<setminus>I)) {(x, y). (x, y) \<in> (R \<times> (R\<setminus>I)) \<times> R \<times> (R\<setminus>I) \<and> local.rel x y} (r, s)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> R\<setminus>I; X = local.frac r s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis local.frac_def)
[PROOF STATE]
proof (state)
this:
r \<in> R
s \<in> R\<setminus>I
X = local.frac r s

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> R; s \<notin> I; X = local.frac r s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus thesis
[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> R\<setminus>I
X = local.frac r s

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> R\<setminus>I
X = local.frac r s
\<lbrakk>?r3 \<in> R; ?s3 \<in> R; ?s3 \<notin> I; X = local.frac ?r3 ?s3\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_from_eq_frac:
  assumes "local.frac r s = local.frac r' s'"
    and "s \<in> (R \<setminus> I)" and "s' \<in> (R \<setminus> I)" and "r \<in> R" "r' \<in> R"
  obtains h where "h \<in> (R \<setminus> I)" "h \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> R\<setminus>I; h \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using local.frac_eq_Ex[of r s r' s'] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(r, s) \<in> R \<times> (R\<setminus>I); (r', s') \<in> R \<times> (R\<setminus>I); local.frac r s = local.frac r' s'; \<And>s1. \<lbrakk>s1 \<in> R\<setminus>I; s1 \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
local.frac r s = local.frac r' s'
s \<in> R\<setminus>I
s' \<in> R\<setminus>I
r \<in> R
r' \<in> R

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> R\<setminus>I; h \<cdot> (s' \<cdot> r - s \<cdot> r') = \<zero>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma spectrum_imp_cxt_quotient_ring:
  "\<pp> \<in> Spec \<Longrightarrow> quotient_ring (R \<setminus> \<pp>) R (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> Spec \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
apply (intro_locales)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> Spec \<Longrightarrow> submonoid_axioms (R\<setminus>\<pp>) R (\<cdot>) \<one>
[PROOF STEP]
using pr_ideal.submonoid_pr_ideal spectrum_def submonoid_def
[PROOF STATE]
proof (prove)
using this:
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> submonoid (?R\<setminus>?I) ?R ?multiplication ?unit
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
submonoid ?N ?M ?composition ?unit \<equiv> Group_Theory.monoid ?M ?composition ?unit \<and> submonoid_axioms ?N ?M ?composition ?unit

goal (1 subgoal):
 1. \<pp> \<in> Spec \<Longrightarrow> submonoid_axioms (R\<setminus>\<pp>) R (\<cdot>) \<one>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma spectrum_imp_pr:
  "\<pp> \<in> Spec \<Longrightarrow> pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> Spec \<Longrightarrow> pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
unfolding spectrum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>} \<Longrightarrow> pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto


[STATEMENT]
lemma frac_in_carrier_local:
  assumes "\<pp> \<in> Spec" and "r \<in> R" and "s \<in> R" and "s \<notin> \<pp>"
  shows "(quotient_ring.frac (R \<setminus> \<pp>) R (+) (\<cdot>) \<zero> r s) \<in> R\<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_ring.frac (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> r s \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quotient_ring.frac (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> r s \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret qr:quotient_ring "R \<setminus> \<pp>" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using spectrum_imp_cxt_quotient_ring[OF \<open>\<pp> \<in> Spec\<close>]
[PROOF STATE]
proof (prove)
using this:
Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qr.frac r s \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret pi:pr_ideal R \<pp> "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using spectrum_imp_pr[OF \<open>\<pp> \<in> Spec\<close>]
[PROOF STATE]
proof (prove)
using this:
pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qr.frac r s \<in> pi.carrier_local_ring_at
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qr.frac r s \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding pi.carrier_local_ring_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qr.frac r s \<in> qr.carrier_quotient_ring
[PROOF STEP]
using assms(2-)
[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> R
s \<notin> \<pp>

goal (1 subgoal):
 1. qr.frac r s \<in> qr.carrier_quotient_ring
[PROOF STEP]
by (auto intro:qr.frac_non_empty)
[PROOF STATE]
proof (state)
this:
qr.frac r s \<in> pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_locally_frac_subset:
  assumes "is_locally_frac s U" "V \<subseteq> U"
  shows "is_locally_frac s V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_locally_frac s V
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_locally_frac s U
V \<subseteq> U

goal (1 subgoal):
 1. is_locally_frac s V
[PROOF STEP]
unfolding is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>U. f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)
V \<subseteq> U

goal (1 subgoal):
 1. \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)
[PROOF STEP]
by (meson subsetD)


[STATEMENT]
lemma is_locally_frac_cong:
  assumes "\<And>x. x\<in>U \<Longrightarrow> f x=g x"
  shows "is_locally_frac f U = is_locally_frac g U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_locally_frac f U = is_locally_frac g U
[PROOF STEP]
unfolding is_locally_frac_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>r fa. r \<in> R \<and> fa \<in> R \<and> (\<forall>\<qq>\<in>U. fa \<notin> \<qq> \<and> f \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r fa)) = (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>U. f \<notin> \<qq> \<and> g \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> U \<Longrightarrow> f ?x3 = g ?x3

goal (1 subgoal):
 1. (\<exists>r fa. r \<in> R \<and> fa \<in> R \<and> (\<forall>\<qq>\<in>U. fa \<notin> \<qq> \<and> f \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r fa)) = (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>U. f \<notin> \<qq> \<and> g \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f))
[PROOF STEP]
by simp


[STATEMENT]
lemma map_on_empty_is_regular:
  fixes s:: "'a set \<Rightarrow> ('a \<times> 'a) set"
  shows "is_regular s {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular s {}
[PROOF STEP]
by (simp add: is_regular_def)


[STATEMENT]
lemma cring0_is_regular [simp]: "cring0.is_regular x = (\<lambda>U. U={})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring0.is_regular x = (\<lambda>U. U = {})
[PROOF STEP]
unfolding cring0.is_regular_def cring0_is_zariski_open
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>U. \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. V = {} \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> cring0.is_locally_frac x V)) = (\<lambda>U. U = {})
[PROOF STEP]
by blast


[STATEMENT]
lemma cring0_sheaf_spec_empty [simp]: "cring0.sheaf_spec {} = {\<lambda>x. undefined}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring0.sheaf_spec {} = {\<lambda>x. undefined}
[PROOF STEP]
by (simp add: cring0.sheaf_spec_def)


[STATEMENT]
lemma sec_has_right_codom:
  assumes "s \<in> \<O> U" and "\<pp> \<in> U"
  shows "s \<pp> \<in> (R\<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
using assms sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
s \<in> \<O> U
\<pp> \<in> U
\<O> ?U \<equiv> {s \<in> \<Pi>\<^sub>E \<pp>\<in>?U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s ?U}

goal (1 subgoal):
 1. s \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
by auto


[STATEMENT]
lemma is_regular_has_right_codom:
  assumes "U \<subseteq> Spec" "\<pp> \<in> U" "is_regular s U"
  shows "s \<pp> \<in> R\<setminus>\<pp> \<^sup>\<inverse> R\<^bsub>(+) (\<cdot>) \<zero>\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<pp> \<in> R\<setminus>\<pp> \<^sup>\<inverse> R \<^bsub>(+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<pp> \<in> R\<setminus>\<pp> \<^sup>\<inverse> R \<^bsub>(+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret qr:quotient_ring "(R \<setminus> \<pp>)" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using spectrum_imp_cxt_quotient_ring assms
[PROOF STATE]
proof (prove)
using this:
?\<pp> \<in> Spec \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>) R (+) (\<cdot>) \<zero> \<one>
U \<subseteq> Spec
\<pp> \<in> U
is_regular s U

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> Spec
\<pp> \<in> U
is_regular s U

goal (1 subgoal):
 1. s \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
by (smt frac_in_carrier_local is_locally_frac_def is_regular_def
          pr_ideal.carrier_local_ring_at_def spectrum_imp_pr subset_eq)
[PROOF STATE]
proof (state)
this:
s \<pp> \<in> qr.carrier_quotient_ring

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sec_is_extensional:
  assumes "s \<in> \<O> U"
  shows "s \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> extensional U
[PROOF STEP]
using assms sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
s \<in> \<O> U
\<O> ?U \<equiv> {s \<in> \<Pi>\<^sub>E \<pp>\<in>?U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s ?U}

goal (1 subgoal):
 1. s \<in> extensional U
[PROOF STEP]
by (simp add: PiE_iff)


[STATEMENT]
lemma \<O>_on_emptyset: "\<O> {} = {\<O>b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<O> {} = {\<O>b}
[PROOF STEP]
unfolding sheaf_spec_def \<O>b_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s \<in> \<Pi>\<^sub>E \<pp>\<in>{}. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s {}} = {\<lambda>\<pp>. undefined}
[PROOF STEP]
by (auto simp:Set_Theory.map_def map_on_empty_is_regular)


[STATEMENT]
lemma sheaf_spec_of_empty_is_singleton:
  fixes U:: "'a set set"
  assumes "U = {}" and "s \<in> extensional U" and "t \<in> extensional U"
  shows "s = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
U = {}
s \<in> extensional U
t \<in> extensional U

goal (1 subgoal):
 1. s = t
[PROOF STEP]
by (simp add: Set_Theory.map_def)


[STATEMENT]
lemma add_sheaf_spec_in_sheaf_spec:
  assumes "s \<in> \<O> U" and "t \<in> \<O> U" and "U \<subseteq> Spec"
  shows "add_sheaf_spec U s t \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
have "add_sheaf_spec U s t \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>"
      if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U s t \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_sheaf_spec U s t \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret qr:quotient_ring "(R\<setminus>\<pp>)" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
apply (rule spectrum_imp_cxt_quotient_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
using that \<open>U \<subseteq> Spec\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
U \<subseteq> Spec

goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_sheaf_spec U s t \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret pi:pr_ideal R \<pp> "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using that \<open>U \<subseteq> Spec\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
U \<subseteq> Spec

goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (auto intro:spectrum_imp_pr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
have "qr.valid_frac (s \<pp>)" "qr.valid_frac (t \<pp>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qr.valid_frac (s \<pp>) &&& qr.valid_frac (t \<pp>)
[PROOF STEP]
using sec_has_right_codom[OF _ that] \<open>s \<in> \<O> U\<close> \<open>t \<in> \<O> U\<close>
[PROOF STATE]
proof (prove)
using this:
?s \<in> \<O> U \<Longrightarrow> ?s \<pp> \<in> pi.carrier_local_ring_at
s \<in> \<O> U
t \<in> \<O> U

goal (1 subgoal):
 1. qr.valid_frac (s \<pp>) &&& qr.valid_frac (t \<pp>)
[PROOF STEP]
by (auto simp:pi.carrier_local_ring_at_def)
[PROOF STATE]
proof (state)
this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)

goal (1 subgoal):
 1. add_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)

goal (1 subgoal):
 1. add_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)
\<pp> \<in> U

goal (1 subgoal):
 1. add_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding add_sheaf_spec_def pi.carrier_local_ring_at_def
[PROOF STATE]
proof (prove)
using this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (t \<pp>)) \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
have "is_regular (add_sheaf_spec U s t) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (add_sheaf_spec U s t) U
[PROOF STEP]
using \<open>s \<in> \<O> U\<close> \<open>t \<in> \<O> U\<close> \<open>U \<subseteq> Spec\<close> is_regular_add_sheaf_spec
[PROOF STATE]
proof (prove)
using this:
s \<in> \<O> U
t \<in> \<O> U
U \<subseteq> Spec
\<lbrakk>is_regular ?s ?U; is_regular ?s' ?U; ?U \<subseteq> Spec\<rbrakk> \<Longrightarrow> is_regular (add_sheaf_spec ?U ?s ?s') ?U

goal (1 subgoal):
 1. is_regular (add_sheaf_spec U s t) U
[PROOF STEP]
unfolding sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
s \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
t \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
U \<subseteq> Spec
\<lbrakk>is_regular ?s ?U; is_regular ?s' ?U; ?U \<subseteq> Spec\<rbrakk> \<Longrightarrow> is_regular (add_sheaf_spec ?U ?s ?s') ?U

goal (1 subgoal):
 1. is_regular (add_sheaf_spec U s t) U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_regular (add_sheaf_spec U s t) U

goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_regular (add_sheaf_spec U s t) U

goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
have "add_sheaf_spec U s t \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> extensional U
[PROOF STEP]
unfolding add_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (t \<pp>)) \<in> extensional U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U s t \<in> extensional U

goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (add_sheaf_spec U s t) U
add_sheaf_spec U s t \<in> extensional U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (add_sheaf_spec U s t) U
add_sheaf_spec U s t \<in> extensional U

goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
unfolding sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (add_sheaf_spec U s t) U
add_sheaf_spec U s t \<in> extensional U

goal (1 subgoal):
 1. add_sheaf_spec U s t \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
[PROOF STEP]
by (simp add: PiE_iff)
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U s t \<in> \<O> U

goal:
No subgoals!
[PROOF STEP]
qed