[STATEMENT]
lemma iDM3_rel: "iDM3 \<eta> \<Longrightarrow> DM3 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
assume idm3: "iDM3 \<eta>"
[PROOF STATE]
proof (state)
this:
iDM3 \<eta>

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
iDM3 \<eta>

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
fix a::"\<sigma>" and b::"\<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
let ?S="\<lambda>Z. Z=a \<or> Z=b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
have "\<^bold>\<Or>Ra[\<eta>|?S] = \<^bold>\<exists>\<^sup>R\<lparr>?S\<rparr> \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))
[PROOF STEP]
using Ra_restr_ex
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>Ra[?\<pi>|?D] = (\<lambda>w. nonEmpty (\<lambda>X. ?D X \<and> ?\<pi> X w))

goal (1 subgoal):
 1. \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
have "\<^bold>\<exists>\<^sup>R\<lparr>?S\<rparr> \<eta> = (\<eta> a) \<^bold>\<or> (\<eta> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b
[PROOF STEP]
using join_def
[PROOF STATE]
proof (prove)
using this:
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w

goal (1 subgoal):
 1. (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))
(\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b
[PROOF STEP]
have "\<^bold>\<Or>Ra[\<eta>|?S] = (\<eta> a) \<^bold>\<or> (\<eta> b)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))
(\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b

goal (1 subgoal):
 1. \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
have "\<^bold>\<And>?S = a \<^bold>\<and> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b
[PROOF STEP]
using infimum_def meet_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<And>?S \<equiv> \<lambda>w. contains (\<lambda>X. X w) ?S
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w

goal (1 subgoal):
 1. \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
from idm3
[PROOF STATE]
proof (chain)
picking this:
iDM3 \<eta>
[PROOF STEP]
have "\<eta>(\<^bold>\<And>?S) \<^bold>\<preceq> \<^bold>\<Or>Ra[\<eta>|?S]"
[PROOF STATE]
proof (prove)
using this:
iDM3 \<eta>

goal (1 subgoal):
 1. contains \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] (\<eta> \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b)
[PROOF STEP]
by (simp add: iDM3_def)
[PROOF STATE]
proof (state)
this:
contains \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] (\<eta> \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b)

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b
\<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b
contains \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] (\<eta> \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b)
[PROOF STEP]
have "\<eta>(a \<^bold>\<and> b) \<^bold>\<preceq> (\<eta> a) \<^bold>\<or> (\<eta> b)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b
\<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b
contains \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] (\<eta> \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b)

goal (1 subgoal):
 1. contains (\<eta> a \<^bold>\<or> \<eta> b) (\<eta> (a \<^bold>\<and> b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
contains (\<eta> a \<^bold>\<or> \<eta> b) (\<eta> (a \<^bold>\<and> b))

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
contains (\<eta> ?a2 \<^bold>\<or> \<eta> ?b2) (\<eta> (?a2 \<^bold>\<and> ?b2))

goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> DM3 \<eta>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
contains (\<eta> ?a2 \<^bold>\<or> \<eta> ?b2) (\<eta> (?a2 \<^bold>\<and> ?b2))

goal (1 subgoal):
 1. DM3 \<eta>
[PROOF STEP]
by (simp add: DM3_def)
[PROOF STATE]
proof (state)
this:
DM3 \<eta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iDM4_rel: "iDM4 \<eta> \<Longrightarrow> DM4 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
assume idm4: "iDM4 \<eta>"
[PROOF STATE]
proof (state)
this:
iDM4 \<eta>

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
iDM4 \<eta>

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
fix a::"\<sigma>" and b::"\<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
let ?S="\<lambda>Z. Z=a \<or> Z=b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
have "\<^bold>\<And>Ra[\<eta>|?S] = \<^bold>\<forall>\<^sup>R\<lparr>?S\<rparr> \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))
[PROOF STEP]
using Ra_restr_all
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<And>Ra[?\<pi>|?D] = (\<lambda>w. contains (\<lambda>X. ?\<pi> X w) ?D)

goal (1 subgoal):
 1. \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
have "\<^bold>\<forall>\<^sup>R\<lparr>?S\<rparr> \<eta> = (\<eta> a) \<^bold>\<and> (\<eta> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b
[PROOF STEP]
using meet_def
[PROOF STATE]
proof (prove)
using this:
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w

goal (1 subgoal):
 1. (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))
(\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b
[PROOF STEP]
have "\<^bold>\<And>Ra[\<eta>|?S] = (\<eta> a) \<^bold>\<and> (\<eta> b)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))
(\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b

goal (1 subgoal):
 1. \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
have "\<^bold>\<Or>?S = a \<^bold>\<or> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b
[PROOF STEP]
using supremum_def join_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>?S \<equiv> \<lambda>w. nonEmpty (\<lambda>X. ?S X \<and> X w)
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w

goal (1 subgoal):
 1. \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
from idm4
[PROOF STATE]
proof (chain)
picking this:
iDM4 \<eta>
[PROOF STEP]
have "\<^bold>\<And>Ra[\<eta>|?S] \<^bold>\<preceq> \<eta>(\<^bold>\<Or>?S)"
[PROOF STATE]
proof (prove)
using this:
iDM4 \<eta>

goal (1 subgoal):
 1. contains (\<eta> \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b) \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b]
[PROOF STEP]
by (simp add: iDM4_def)
[PROOF STATE]
proof (state)
this:
contains (\<eta> \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b) \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b]

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b
\<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b
contains (\<eta> \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b) \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b]
[PROOF STEP]
have "(\<eta> a) \<^bold>\<and> (\<eta> b) \<^bold>\<preceq> \<eta>(a \<^bold>\<or> b)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b
\<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b
contains (\<eta> \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b) \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b]

goal (1 subgoal):
 1. contains (\<eta> (a \<^bold>\<or> b)) (\<eta> a \<^bold>\<and> \<eta> b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains (\<eta> (a \<^bold>\<or> b)) (\<eta> a \<^bold>\<and> \<eta> b)

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
contains (\<eta> (?a2 \<^bold>\<or> ?b2)) (\<eta> ?a2 \<^bold>\<and> \<eta> ?b2)

goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> DM4 \<eta>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
contains (\<eta> (?a2 \<^bold>\<or> ?b2)) (\<eta> ?a2 \<^bold>\<and> \<eta> ?b2)

goal (1 subgoal):
 1. DM4 \<eta>
[PROOF STEP]
by (simp add: DM4_def)
[PROOF STATE]
proof (state)
this:
DM4 \<eta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "DM3 \<eta> \<Longrightarrow> iDM3 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DM3 \<eta> \<Longrightarrow> iDM3 \<eta>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DM3 \<eta> \<Longrightarrow> iDM3 \<eta>
[PROOF STEP]
oops


[STATEMENT]
lemma "DM4 \<eta> \<Longrightarrow> iDM4 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DM4 \<eta> \<Longrightarrow> iDM4 \<eta>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DM4 \<eta> \<Longrightarrow> iDM4 \<eta>
[PROOF STEP]
oops


[STATEMENT]
lemma iDM1_trad: "iDM1 \<eta> \<Longrightarrow> \<forall>\<pi>. \<eta>(\<^bold>\<exists>x. \<pi> x)  \<^bold>\<preceq>  (\<^bold>\<forall>x. \<eta>(\<pi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> \<forall>\<pi>. contains (\<lambda>w. \<forall>X. \<eta> (\<pi> X) w) (\<eta> (mexistsB \<pi>))
[PROOF STEP]
by (metis (mono_tags, lifting) CoPw_def DM1_CoPw iDM1_rel)


[STATEMENT]
lemma iDM2_trad: "iDM2 \<eta> \<Longrightarrow> \<forall>\<pi>. (\<^bold>\<exists>x. \<eta>(\<pi> x)) \<^bold>\<preceq> \<eta>(\<^bold>\<forall>x. \<pi> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> \<forall>\<pi>. contains (\<eta> (mforallB \<pi>)) (\<lambda>w. nonEmpty (\<lambda>X. \<eta> (\<pi> X) w))
[PROOF STEP]
by (metis (mono_tags, lifting) CoPw_def DM2_CoPw iDM2_rel)


[STATEMENT]
lemma "iDM1 \<eta> \<Longrightarrow> \<forall>\<pi>. piDM1 \<pi> \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> \<forall>\<pi>. contains \<^bold>\<And>Ra[\<eta>|Ra\<pi>] (\<eta> \<^bold>\<Or>Ra\<pi>)
[PROOF STEP]
by (simp add: iDM1_def)


[STATEMENT]
lemma "iDM2 \<eta> \<Longrightarrow> \<forall>\<pi>. piDM2 \<pi> \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> \<forall>\<pi>. contains (\<eta> \<^bold>\<And>Ra\<pi>) \<^bold>\<Or>Ra[\<eta>|Ra\<pi>]
[PROOF STEP]
by (simp add: iDM2_def)


[STATEMENT]
lemma "iDM3 \<eta> \<Longrightarrow> \<forall>\<pi>. piDM3 \<pi> \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> \<forall>\<pi>. contains \<^bold>\<Or>Ra[\<eta>|Ra\<pi>] (\<eta> \<^bold>\<And>Ra\<pi>)
[PROOF STEP]
by (simp add: iDM3_def)


[STATEMENT]
lemma "iDM4 \<eta> \<Longrightarrow> \<forall>\<pi>. piDM4 \<pi> \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> \<forall>\<pi>. contains (\<eta> \<^bold>\<Or>Ra\<pi>) \<^bold>\<And>Ra[\<eta>|Ra\<pi>]
[PROOF STEP]
by (simp add: iDM4_def)


[STATEMENT]
lemma iDM3_aux: "piDM3 \<pi> \<eta> \<equiv> \<eta>(\<^bold>\<forall>\<pi>) \<^bold>\<preceq> \<^bold>\<exists>[\<eta>|\<lparr>Ra \<pi>\<rparr>]\<^sup>N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains \<^bold>\<Or>Ra[\<eta>|Ra\<pi>] (\<eta> \<^bold>\<And>Ra\<pi>) \<equiv> contains (\<lambda>w. nonEmpty (\<lambda>X. Ra\<pi> X \<and> \<eta> X w)) (\<eta> (mforallB \<pi>))
[PROOF STEP]
unfolding Ra_all Ra_ex_restr
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains (\<lambda>w. nonEmpty (\<lambda>X. Ra\<pi> X \<and> \<eta> X w)) (\<eta> (mforallB \<pi>)) \<equiv> contains (\<lambda>w. nonEmpty (\<lambda>X. Ra\<pi> X \<and> \<eta> X w)) (\<eta> (mforallB \<pi>))
[PROOF STEP]
by simp


[STATEMENT]
lemma iDM4_aux: "piDM4 \<pi> \<eta> \<equiv> \<^bold>\<forall>[\<eta>|\<lparr>Ra \<pi>\<rparr>]\<^sup>P \<^bold>\<preceq> \<eta>(\<^bold>\<exists>\<pi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains (\<eta> \<^bold>\<Or>Ra\<pi>) \<^bold>\<And>Ra[\<eta>|Ra\<pi>] \<equiv> contains (\<eta> (mexistsB \<pi>)) (\<lambda>w. contains (\<lambda>X. \<eta> X w) Ra\<pi>)
[PROOF STEP]
unfolding Ra_ex Ra_all_restr
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains (\<eta> (mexistsB \<pi>)) (\<lambda>w. contains (\<lambda>X. \<eta> X w) Ra\<pi>) \<equiv> contains (\<eta> (mexistsB \<pi>)) (\<lambda>w. contains (\<lambda>X. \<eta> X w) Ra\<pi>)
[PROOF STEP]
by simp


[STATEMENT]
lemma iDM3_trad: "iDM3 \<eta> \<Longrightarrow> \<forall>\<pi>. \<eta>(\<^bold>\<forall>x. \<pi> x)  \<^bold>\<preceq>  (\<^bold>\<exists>x. \<eta>(\<pi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM3 \<eta> \<Longrightarrow> \<forall>\<pi>. contains (\<lambda>w. nonEmpty (\<lambda>X. \<eta> (\<pi> X) w)) (\<eta> (mforallB \<pi>))
[PROOF STEP]
by (metis Ra_ex_comp2 iDM3_def iDM3_aux comp_apply)


[STATEMENT]
lemma iDM4_trad: "iDM4 \<eta> \<Longrightarrow> \<forall>\<pi>. (\<^bold>\<forall>x. \<eta>(\<pi> x)) \<^bold>\<preceq> \<eta>(\<^bold>\<exists>x. \<pi> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM4 \<eta> \<Longrightarrow> \<forall>\<pi>. contains (\<eta> (mexistsB \<pi>)) (\<lambda>w. \<forall>X. \<eta> (\<pi> X) w)
[PROOF STEP]
by (metis Ra_all_comp1 iDM4_def iDM4_aux comp_apply)


[STATEMENT]
lemma gcd_int_nonpos_iff [simp]: "gcd x (y :: int) \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gcd x y \<le> 0) = (x = 0 \<and> y = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. gcd x y \<le> 0 \<Longrightarrow> x = 0 \<and> y = 0
 2. x = 0 \<and> y = 0 \<Longrightarrow> gcd x y \<le> 0
[PROOF STEP]
assume "gcd x y \<le> 0"
[PROOF STATE]
proof (state)
this:
gcd x y \<le> 0

goal (2 subgoals):
 1. gcd x y \<le> 0 \<Longrightarrow> x = 0 \<and> y = 0
 2. x = 0 \<and> y = 0 \<Longrightarrow> gcd x y \<le> 0
[PROOF STEP]
with gcd_ge_0_int[of x y]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> gcd x y
gcd x y \<le> 0
[PROOF STEP]
have "gcd x y = 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> gcd x y
gcd x y \<le> 0

goal (1 subgoal):
 1. gcd x y = 0
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
gcd x y = 0

goal (2 subgoals):
 1. gcd x y \<le> 0 \<Longrightarrow> x = 0 \<and> y = 0
 2. x = 0 \<and> y = 0 \<Longrightarrow> gcd x y \<le> 0
[PROOF STEP]
thus "x = 0 \<and> y = 0"
[PROOF STATE]
proof (prove)
using this:
gcd x y = 0

goal (1 subgoal):
 1. x = 0 \<and> y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = 0 \<and> y = 0

goal (1 subgoal):
 1. x = 0 \<and> y = 0 \<Longrightarrow> gcd x y \<le> 0
[PROOF STEP]
qed auto


[STATEMENT]
lemma minus_in_Ints_iff [simp]:
  "-x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- x \<in> \<int>) = (x \<in> \<int>)
[PROOF STEP]
using Ints_minus[of x] Ints_minus[of "-x"]
[PROOF STATE]
proof (prove)
using this:
x \<in> \<int> \<Longrightarrow> - x \<in> \<int>
- x \<in> \<int> \<Longrightarrow> - (- x) \<in> \<int>

goal (1 subgoal):
 1. (- x \<in> \<int>) = (x \<in> \<int>)
[PROOF STEP]
by auto


[STATEMENT]
lemma nonneg_sqrt_nat_or_irrat:
  assumes "x ^ 2 = real a" and "x \<ge> 0"
  shows   "x \<in> \<nat> \<or> x \<notin> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<nat> \<or> x \<notin> \<rat>
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "x \<notin> \<nat>" and "x \<in> \<rat>"
[PROOF STATE]
proof (state)
this:
x \<notin> \<nat>
x \<in> \<rat>

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from Rats_abs_nat_div_natE[OF this(2)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>m n. \<lbrakk>n \<noteq> 0; \<bar>x\<bar> = real m / real n; coprime m n\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain p q :: nat where q_nz [simp]: "q \<noteq> 0" and "abs x = p / q" and coprime: "coprime p q"
[PROOF STATE]
proof (prove)
using this:
(\<And>m n. \<lbrakk>n \<noteq> 0; \<bar>x\<bar> = real m / real n; coprime m n\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>q p. \<lbrakk>q \<noteq> 0; \<bar>x\<bar> = real p / real q; coprime p q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
q \<noteq> 0
\<bar>x\<bar> = real p / real q
coprime p q

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>x \<ge> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x
q \<noteq> 0
\<bar>x\<bar> = real p / real q
coprime p q
[PROOF STEP]
have x: "x = p / q"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x
q \<noteq> 0
\<bar>x\<bar> = real p / real q
coprime p q

goal (1 subgoal):
 1. x = real p / real q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = real p / real q

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sup>2 = real a
0 \<le> x
x = real p / real q
[PROOF STEP]
have "real (q ^ 2) * real a = real (p ^ 2)"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 = real a
0 \<le> x
x = real p / real q

goal (1 subgoal):
 1. real (q\<^sup>2) * real a = real (p\<^sup>2)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
real (q\<^sup>2) * real a = real (p\<^sup>2)

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (q\<^sup>2) * real a = real (p\<^sup>2)

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "real (q ^ 2) * real a = real (q ^ 2 * a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (q\<^sup>2) * real a = real (q\<^sup>2 * a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (q\<^sup>2) * real a = real (q\<^sup>2 * a)

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (q\<^sup>2 * a) = real (p\<^sup>2)
[PROOF STEP]
have "p ^ 2 = q ^ 2 * a"
[PROOF STATE]
proof (prove)
using this:
real (q\<^sup>2 * a) = real (p\<^sup>2)

goal (1 subgoal):
 1. p\<^sup>2 = q\<^sup>2 * a
[PROOF STEP]
by (subst (asm) of_nat_eq_iff) auto
[PROOF STATE]
proof (state)
this:
p\<^sup>2 = q\<^sup>2 * a

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "q ^ 2 dvd p ^ 2"
[PROOF STATE]
proof (prove)
using this:
p\<^sup>2 = q\<^sup>2 * a

goal (1 subgoal):
 1. q\<^sup>2 dvd p\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q\<^sup>2 dvd p\<^sup>2

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "q dvd p"
[PROOF STATE]
proof (prove)
using this:
q\<^sup>2 dvd p\<^sup>2

goal (1 subgoal):
 1. q dvd p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q dvd p

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with coprime
[PROOF STATE]
proof (chain)
picking this:
coprime p q
q dvd p
[PROOF STEP]
have "q = 1"
[PROOF STATE]
proof (prove)
using this:
coprime p q
q dvd p

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

goal (1 subgoal):
 1. \<lbrakk>x \<notin> \<nat>; x \<in> \<rat>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with x and \<open>x \<notin> \<nat>\<close>
[PROOF STATE]
proof (chain)
picking this:
x = real p / real q
x \<notin> \<nat>
q = 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x = real p / real q
x \<notin> \<nat>
q = 1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pell_square_solution_nat_aux:
  fixes x y :: nat
  assumes "D > 0" and "x ^ 2 = 1 + D * y ^ 2"
  shows "(x, y) = (1, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < D
x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have x_nz: "x > 0"
[PROOF STATE]
proof (prove)
using this:
0 < D
x\<^sup>2 = 1 + D * y\<^sup>2

goal (1 subgoal):
 1. 0 < x
[PROOF STEP]
by (auto intro!: Nat.gr0I)
[PROOF STATE]
proof (state)
this:
0 < x

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
from square_D
[PROOF STATE]
proof (chain)
picking this:
is_square D
[PROOF STEP]
obtain d where [simp]: "D = d\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
is_square D

goal (1 subgoal):
 1. (\<And>d. D = d\<^sup>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_nth_powerE)
[PROOF STATE]
proof (state)
this:
D = d\<^sup>2

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
have "int x ^ 2 = int (x ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int x)\<^sup>2 = int (x\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(int x)\<^sup>2 = int (x\<^sup>2)

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(int x)\<^sup>2 = int (x\<^sup>2)

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
note assms(2)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = 1 + D * y\<^sup>2

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = 1 + D * y\<^sup>2

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
have "int (1 + D * y ^ 2) = 1 + int D * int y ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (1 + D * y\<^sup>2) = 1 + int D * (int y)\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int (1 + D * y\<^sup>2) = 1 + int D * (int y)\<^sup>2

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(int x)\<^sup>2 = 1 + int D * (int y)\<^sup>2
[PROOF STEP]
have "(int x + int d * int y) * (int x - int d * int y) = 1"
[PROOF STATE]
proof (prove)
using this:
(int x)\<^sup>2 = 1 + int D * (int y)\<^sup>2

goal (1 subgoal):
 1. (int x + int d * int y) * (int x - int d * int y) = 1
[PROOF STEP]
by (simp add: algebra_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
(int x + int d * int y) * (int x - int d * int y) = 1

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
hence *: "int x + int d * int y = 1 \<and> int x - int d * int y = 1"
[PROOF STATE]
proof (prove)
using this:
(int x + int d * int y) * (int x - int d * int y) = 1

goal (1 subgoal):
 1. int x + int d * int y = 1 \<and> int x - int d * int y = 1
[PROOF STEP]
using x_nz
[PROOF STATE]
proof (prove)
using this:
(int x + int d * int y) * (int x - int d * int y) = 1
0 < x

goal (1 subgoal):
 1. int x + int d * int y = 1 \<and> int x - int d * int y = 1
[PROOF STEP]
by (subst (asm) pos_zmult_eq_1_iff) (auto intro: add_pos_nonneg)
[PROOF STATE]
proof (state)
this:
int x + int d * int y = 1 \<and> int x - int d * int y = 1

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
int x + int d * int y = 1 \<and> int x - int d * int y = 1
[PROOF STEP]
have [simp]: "x = 1"
[PROOF STATE]
proof (prove)
using this:
int x + int d * int y = 1 \<and> int x - int d * int y = 1

goal (1 subgoal):
 1. x = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = 1

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = 1

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
from * and assms(1)
[PROOF STATE]
proof (chain)
picking this:
int x + int d * int y = 1 \<and> int x - int d * int y = 1
0 < D
[PROOF STEP]
have "y = 0"
[PROOF STATE]
proof (prove)
using this:
int x + int d * int y = 1 \<and> int x - int d * int y = 1
0 < D

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

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = 1
y = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 1
y = 0

goal (1 subgoal):
 1. (x, y) = (1, 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) = (1, 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pell_square_solution_int_aux:
  fixes x y :: int
  assumes "D > 0" and "x ^ 2 = 1 + D * y ^ 2"
  shows "x \<in> {-1, 1} \<and> y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
define x' y' where "x' = nat \<bar>x\<bar>" and "y' = nat \<bar>y\<bar>"
[PROOF STATE]
proof (state)
this:
x' = nat \<bar>x\<bar>
y' = nat \<bar>y\<bar>

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
have x: "x = sgn x * x'" and y: "y = sgn y * y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = sgn x * int x' &&& y = sgn y * int y'
[PROOF STEP]
by (auto simp: sgn_if x'_def y'_def)
[PROOF STATE]
proof (state)
this:
x = sgn x * int x'
y = sgn y * int y'

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
have zero_iff: "x = 0 \<longleftrightarrow> x' = 0" "y = 0 \<longleftrightarrow> y' = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = 0) = (x' = 0) &&& (y = 0) = (y' = 0)
[PROOF STEP]
by (auto simp: x'_def y'_def)
[PROOF STATE]
proof (state)
this:
(x = 0) = (x' = 0)
(y = 0) = (y' = 0)

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
note assms(2)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = 1 + int D * y\<^sup>2

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = 1 + int D * y\<^sup>2

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
have "x ^ 2 = int (x' ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 = int (x'\<^sup>2)
[PROOF STEP]
by (subst x) (auto simp: sgn_if zero_iff)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = int (x'\<^sup>2)

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = int (x'\<^sup>2)

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
have "1 + D * y ^ 2 = int (1 + D * y' ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + int D * y\<^sup>2 = int (1 + D * y'\<^sup>2)
[PROOF STEP]
by (subst y) (auto simp: sgn_if zero_iff)
[PROOF STATE]
proof (state)
this:
1 + int D * y\<^sup>2 = int (1 + D * y'\<^sup>2)

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + int D * y\<^sup>2 = int (1 + D * y'\<^sup>2)

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
note of_nat_eq_iff
[PROOF STATE]
proof (state)
this:
(of_nat ?m = of_nat ?n) = (?m = ?n)

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x'\<^sup>2 = 1 + D * y'\<^sup>2
[PROOF STEP]
have "x'\<^sup>2 = 1 + D * y'\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
x'\<^sup>2 = 1 + D * y'\<^sup>2

goal (1 subgoal):
 1. x'\<^sup>2 = 1 + D * y'\<^sup>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x'\<^sup>2 = 1 + D * y'\<^sup>2

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
from \<open>D > 0\<close> and this
[PROOF STATE]
proof (chain)
picking this:
0 < D
x'\<^sup>2 = 1 + D * y'\<^sup>2
[PROOF STEP]
have "(x', y') = (1, 0)"
[PROOF STATE]
proof (prove)
using this:
0 < D
x'\<^sup>2 = 1 + D * y'\<^sup>2

goal (1 subgoal):
 1. (x', y') = (1, 0)
[PROOF STEP]
by (rule pell_square_solution_nat_aux)
[PROOF STATE]
proof (state)
this:
(x', y') = (1, 0)

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(x', y') = (1, 0)

goal (1 subgoal):
 1. x \<in> {- 1, 1} \<and> y = 0
[PROOF STEP]
by (auto simp: x'_def y'_def)
[PROOF STATE]
proof (state)
this:
x \<in> {- 1, 1} \<and> y = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pell_square_solution_nat_iff:
  fixes x y :: nat
  shows "x ^ 2 = 1 + D * y ^ 2  \<longleftrightarrow>  x = 1 \<and> (D = 0 \<or> y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>2 = 1 + D * y\<^sup>2) = (x = 1 \<and> (D = 0 \<or> y = 0))
[PROOF STEP]
using pell_square_solution_nat_aux[of x y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < D; x\<^sup>2 = 1 + D * y\<^sup>2\<rbrakk> \<Longrightarrow> (x, y) = (1, 0)

goal (1 subgoal):
 1. (x\<^sup>2 = 1 + D * y\<^sup>2) = (x = 1 \<and> (D = 0 \<or> y = 0))
[PROOF STEP]
by (cases "D = 0") auto


[STATEMENT]
lemma pell_square_solution_int_iff:
  fixes x y :: int
  shows "x ^ 2 = 1 + D * y ^ 2  \<longleftrightarrow>  x \<in> {-1, 1} \<and> (D = 0 \<or> y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>2 = 1 + int D * y\<^sup>2) = (x \<in> {- 1, 1} \<and> (D = 0 \<or> y = 0))
[PROOF STEP]
using pell_square_solution_int_aux[of x y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < D; x\<^sup>2 = 1 + int D * y\<^sup>2\<rbrakk> \<Longrightarrow> x \<in> {- 1, 1} \<and> y = 0

goal (1 subgoal):
 1. (x\<^sup>2 = 1 + int D * y\<^sup>2) = (x \<in> {- 1, 1} \<and> (D = 0 \<or> y = 0))
[PROOF STEP]
by (cases "D = 0") (auto simp: power2_eq_1_iff)


[STATEMENT]
lemma pell_approximation_lemma:
  fixes s :: nat and x :: real
  assumes s: "s > 0"
  shows "\<exists>u::nat. \<exists>t::int. u > 0 \<and> coprime u t \<and> 1 / s \<in> {\<bar>t - u * x\<bar><..1 / u}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
define f where "f = (\<lambda>u. \<lceil>u * x\<rceil>)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>u. \<lceil>u * x\<rceil>)

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
define g :: "nat \<Rightarrow> int" where "g = (\<lambda>u. \<lfloor>frac (u * x) * s\<rfloor>)"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>xa. \<lfloor>frac (real xa * x) * real s\<rfloor>)

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g = (\<lambda>xa. \<lfloor>frac (real xa * x) * real s\<rfloor>)

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
fix u :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
assume u: "u \<le> s"
[PROOF STATE]
proof (state)
this:
u \<le> s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
hence "frac (u * x) * real s < 1 * real s"
[PROOF STATE]
proof (prove)
using this:
u \<le> s

goal (1 subgoal):
 1. frac (real u * x) * real s < 1 * real s
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
u \<le> s
0 < s

goal (1 subgoal):
 1. frac (real u * x) * real s < 1 * real s
[PROOF STEP]
by (intro mult_strict_right_mono) (auto simp: frac_lt_1)
[PROOF STATE]
proof (state)
this:
frac (real u * x) * real s < 1 * real s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
hence "g u < int s"
[PROOF STATE]
proof (prove)
using this:
frac (real u * x) * real s < 1 * real s

goal (1 subgoal):
 1. g u < int s
[PROOF STEP]
by (auto simp: floor_less_iff g_def)
[PROOF STATE]
proof (state)
this:
g u < int s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?u2 \<le> s \<Longrightarrow> g ?u2 < int s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
hence "g ` {..s} \<subseteq> {0..<s}"
[PROOF STATE]
proof (prove)
using this:
?u2 \<le> s \<Longrightarrow> g ?u2 < int s

goal (1 subgoal):
 1. g ` {..s} \<subseteq> {0..<int s}
[PROOF STEP]
by (auto simp: g_def floor_less_iff)
[PROOF STATE]
proof (state)
this:
g ` {..s} \<subseteq> {0..<int s}

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
hence "card (g ` {..s}) \<le> card {0..<int s}"
[PROOF STATE]
proof (prove)
using this:
g ` {..s} \<subseteq> {0..<int s}

goal (1 subgoal):
 1. card (g ` {..s}) \<le> card {0..<int s}
[PROOF STEP]
by (intro card_mono) auto
[PROOF STATE]
proof (state)
this:
card (g ` {..s}) \<le> card {0..<int s}

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (g ` {..s}) \<le> card {0..<int s}

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have "\<dots> < card {..s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {0..<int s} < card {..s}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {0..<int s} < card {..s}

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (g ` {..s}) < card {..s}
[PROOF STEP]
have "\<not>inj_on g {..s}"
[PROOF STATE]
proof (prove)
using this:
card (g ` {..s}) < card {..s}

goal (1 subgoal):
 1. \<not> inj_on g {..s}
[PROOF STEP]
by (rule pigeonhole)
[PROOF STATE]
proof (state)
this:
\<not> inj_on g {..s}

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> inj_on g {..s}
[PROOF STEP]
obtain a b where ab: "a \<le> s" "b \<le> s" "a \<noteq> b" "g a = g b"
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on g {..s}

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<le> s; b \<le> s; a \<noteq> b; g a = g b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: inj_on_def)
[PROOF STATE]
proof (state)
this:
a \<le> s
b \<le> s
a \<noteq> b
g a = g b

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
define u1 and u2 where "u1 = max a b" and "u2 = min a b"
[PROOF STATE]
proof (state)
this:
u1 = max a b
u2 = min a b

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have u12: "u1 \<le> s" "u2 \<le> s" "u2 < u1" "g u1 = g u2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u1 \<le> s &&& u2 \<le> s) &&& u2 < u1 &&& g u1 = g u2
[PROOF STEP]
using ab
[PROOF STATE]
proof (prove)
using this:
a \<le> s
b \<le> s
a \<noteq> b
g a = g b

goal (1 subgoal):
 1. (u1 \<le> s &&& u2 \<le> s) &&& u2 < u1 &&& g u1 = g u2
[PROOF STEP]
by (auto simp: u1_def u2_def)
[PROOF STATE]
proof (state)
this:
u1 \<le> s
u2 \<le> s
u2 < u1
g u1 = g u2

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
define u t where "u = u1 - u2" and "t = \<lfloor>u1 * x\<rfloor> - \<lfloor>u2 * x\<rfloor>"
[PROOF STATE]
proof (state)
this:
u = u1 - u2
t = \<lfloor>real u1 * x\<rfloor> - \<lfloor>real u2 * x\<rfloor>

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have u: "u > 0" "\<bar>u\<bar> \<le> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < u &&& \<bar>int u\<bar> \<le> int s
[PROOF STEP]
using u12
[PROOF STATE]
proof (prove)
using this:
u1 \<le> s
u2 \<le> s
u2 < u1
g u1 = g u2

goal (1 subgoal):
 1. 0 < u &&& \<bar>int u\<bar> \<le> int s
[PROOF STEP]
by (simp_all add: u_def)
[PROOF STATE]
proof (state)
this:
0 < u
\<bar>int u\<bar> \<le> int s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
from \<open>g u1 = g u2\<close>
[PROOF STATE]
proof (chain)
picking this:
g u1 = g u2
[PROOF STEP]
have "\<bar>frac (u2 * x) * s - frac (u1 * x) * s\<bar> < 1"
[PROOF STATE]
proof (prove)
using this:
g u1 = g u2

goal (1 subgoal):
 1. \<bar>frac (real u2 * x) * real s - frac (real u1 * x) * real s\<bar> < 1
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
\<lfloor>frac (real u1 * x) * real s\<rfloor> = \<lfloor>frac (real u2 * x) * real s\<rfloor>

goal (1 subgoal):
 1. \<bar>frac (real u2 * x) * real s - frac (real u1 * x) * real s\<bar> < 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<bar>frac (real u2 * x) * real s - frac (real u1 * x) * real s\<bar> < 1

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>frac (real u2 * x) * real s - frac (real u1 * x) * real s\<bar> < 1

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have "\<bar>frac (u2 * x) * s - frac (u1 * x) * s\<bar> =
               \<bar>real s\<bar> * \<bar>frac (u2 * x) - frac (u1 * x)\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>frac (real u2 * x) * real s - frac (real u1 * x) * real s\<bar> = \<bar>real s\<bar> * \<bar>frac (real u2 * x) - frac (real u1 * x)\<bar>
[PROOF STEP]
by (subst abs_mult [symmetric]) (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
\<bar>frac (real u2 * x) * real s - frac (real u1 * x) * real s\<bar> = \<bar>real s\<bar> * \<bar>frac (real u2 * x) - frac (real u1 * x)\<bar>

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>real s\<bar> * \<bar>frac (real u2 * x) - frac (real u1 * x)\<bar> < 1
[PROOF STEP]
have "\<bar>t - u * x\<bar> * s < 1"
[PROOF STATE]
proof (prove)
using this:
\<bar>real s\<bar> * \<bar>frac (real u2 * x) - frac (real u1 * x)\<bar> < 1

goal (1 subgoal):
 1. \<bar>real_of_int t - real u * x\<bar> * real s < 1
[PROOF STEP]
using \<open>u1 > u2\<close>
[PROOF STATE]
proof (prove)
using this:
\<bar>real s\<bar> * \<bar>frac (real u2 * x) - frac (real u1 * x)\<bar> < 1
u2 < u1

goal (1 subgoal):
 1. \<bar>real_of_int t - real u * x\<bar> * real s < 1
[PROOF STEP]
by (simp add: g_def u_def t_def frac_def algebra_simps of_nat_diff)
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t - real u * x\<bar> * real s < 1

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
with \<open>s > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < s
\<bar>real_of_int t - real u * x\<bar> * real s < 1
[PROOF STEP]
have less: "\<bar>t - u * x\<bar> < 1 / s"
[PROOF STATE]
proof (prove)
using this:
0 < s
\<bar>real_of_int t - real u * x\<bar> * real s < 1

goal (1 subgoal):
 1. \<bar>real_of_int t - real u * x\<bar> < 1 / real s
[PROOF STEP]
by (simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t - real u * x\<bar> < 1 / real s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
define d where "d = gcd (nat \<bar>t\<bar>) u"
[PROOF STATE]
proof (state)
this:
d = gcd (nat \<bar>t\<bar>) u

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
define t' :: int and u' :: nat where "t'= t div d" and "u' = u div d"
[PROOF STATE]
proof (state)
this:
t' = t div int d
u' = u div d

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
from u
[PROOF STATE]
proof (chain)
picking this:
0 < u
\<bar>int u\<bar> \<le> int s
[PROOF STEP]
have "d \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 < u
\<bar>int u\<bar> \<le> int s

goal (1 subgoal):
 1. d \<noteq> 0
[PROOF STEP]
by (intro notI) (auto simp: d_def)
[PROOF STATE]
proof (state)
this:
d \<noteq> 0

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have "int (gcd (nat \<bar>t\<bar>) u) = gcd \<bar>t\<bar> (int u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (gcd (nat \<bar>t\<bar>) u) = gcd \<bar>t\<bar> (int u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int (gcd (nat \<bar>t\<bar>) u) = gcd \<bar>t\<bar> (int u)

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
hence t'_u': "t = t' * d" "u = u' * d"
[PROOF STATE]
proof (prove)
using this:
int (gcd (nat \<bar>t\<bar>) u) = gcd \<bar>t\<bar> (int u)

goal (1 subgoal):
 1. t = t' * int d &&& u = u' * d
[PROOF STEP]
by (auto simp: t'_def u'_def d_def nat_dvd_iff)
[PROOF STATE]
proof (state)
this:
t = t' * int d
u = u' * d

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
from \<open>d \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
d \<noteq> 0
[PROOF STEP]
have "\<bar>t' - u' * x\<bar> * 1 \<le> \<bar>t' - u' * x\<bar> * \<bar>real d\<bar>"
[PROOF STATE]
proof (prove)
using this:
d \<noteq> 0

goal (1 subgoal):
 1. \<bar>real_of_int t' - real u' * x\<bar> * 1 \<le> \<bar>real_of_int t' - real u' * x\<bar> * \<bar>real d\<bar>
[PROOF STEP]
by (intro mult_left_mono) auto
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t' - real u' * x\<bar> * 1 \<le> \<bar>real_of_int t' - real u' * x\<bar> * \<bar>real d\<bar>

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t' - real u' * x\<bar> * 1 \<le> \<bar>real_of_int t' - real u' * x\<bar> * \<bar>real d\<bar>

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have "\<dots> = \<bar>t - u * x\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int t' - real u' * x\<bar> * \<bar>real d\<bar> = \<bar>real_of_int t - real u * x\<bar>
[PROOF STEP]
by (subst abs_mult [symmetric]) (simp add: algebra_simps t'_u')
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t' - real u' * x\<bar> * \<bar>real d\<bar> = \<bar>real_of_int t - real u * x\<bar>

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t' - real u' * x\<bar> * \<bar>real d\<bar> = \<bar>real_of_int t - real u * x\<bar>

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
note less
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t - real u * x\<bar> < 1 / real s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>real_of_int t' - real u' * x\<bar> * 1 < 1 / real s
[PROOF STEP]
have "\<bar>t' - u' * x\<bar> < 1 / s"
[PROOF STATE]
proof (prove)
using this:
\<bar>real_of_int t' - real u' * x\<bar> * 1 < 1 / real s

goal (1 subgoal):
 1. \<bar>real_of_int t' - real u' * x\<bar> < 1 / real s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t' - real u' * x\<bar> < 1 / real s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t' - real u' * x\<bar> < 1 / real s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t' - real u' * x\<bar> < 1 / real s

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
from \<open>s > 0\<close> and u
[PROOF STATE]
proof (chain)
picking this:
0 < s
0 < u
\<bar>int u\<bar> \<le> int s
[PROOF STEP]
have "1 / s \<le> 1 / u"
[PROOF STATE]
proof (prove)
using this:
0 < s
0 < u
\<bar>int u\<bar> \<le> int s

goal (1 subgoal):
 1. 1 / real s \<le> 1 / real u
[PROOF STEP]
by (simp add: divide_simps u_def)
[PROOF STATE]
proof (state)
this:
1 / real s \<le> 1 / real u

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / real s \<le> 1 / real u

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have "\<dots> = 1 / u' / d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real u = 1 / real u' / real d
[PROOF STEP]
by (simp add: t'_u' divide_simps)
[PROOF STATE]
proof (state)
this:
1 / real u = 1 / real u' / real d

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / real u = 1 / real u' / real d

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have "\<dots> \<le> 1 / u' / 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real u' / real d \<le> 1 / real u' / 1
[PROOF STEP]
using \<open>d \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
d \<noteq> 0

goal (1 subgoal):
 1. 1 / real u' / real d \<le> 1 / real u' / 1
[PROOF STEP]
by (intro divide_left_mono) auto
[PROOF STATE]
proof (state)
this:
1 / real u' / real d \<le> 1 / real u' / 1

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 / real s \<le> 1 / real u' / 1
[PROOF STEP]
have "1 / s \<le> 1 / u'"
[PROOF STATE]
proof (prove)
using this:
1 / real s \<le> 1 / real u' / 1

goal (1 subgoal):
 1. 1 / real s \<le> 1 / real u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / real s \<le> 1 / real u'

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
1 / real s \<le> 1 / real u'

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>real_of_int t' - real u' * x\<bar> < 1 / real s
1 / real s \<le> 1 / real u'
[PROOF STEP]
have "1 / s \<in> {\<bar>t' - u' * x\<bar><..1 / u'}"
[PROOF STATE]
proof (prove)
using this:
\<bar>real_of_int t' - real u' * x\<bar> < 1 / real s
1 / real s \<le> 1 / real u'

goal (1 subgoal):
 1. 1 / real s \<in> {\<bar>real_of_int t' - real u' * x\<bar><..1 / real u'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / real s \<in> {\<bar>real_of_int t' - real u' * x\<bar><..1 / real u'}

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 / real s \<in> {\<bar>real_of_int t' - real u' * x\<bar><..1 / real u'}

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
from \<open>u > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < u
[PROOF STEP]
have "u' > 0"
[PROOF STATE]
proof (prove)
using this:
0 < u

goal (1 subgoal):
 1. 0 < u'
[PROOF STEP]
by (auto simp: t'_u')
[PROOF STATE]
proof (state)
this:
0 < u'

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < u'

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 < u'

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have "gcd u t = gcd t' u' * int d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (int u) t = gcd t' (int u') * int d
[PROOF STEP]
by (simp add: t'_u' gcd_mult_right gcd.commute)
[PROOF STATE]
proof (state)
this:
gcd (int u) t = gcd t' (int u') * int d

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gcd (int u) t = gcd t' (int u') * int d

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
have "int d = gcd u t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int d = gcd (int u) t
[PROOF STEP]
by (simp add: d_def gcd.commute)
[PROOF STATE]
proof (state)
this:
int d = gcd (int u) t

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gcd (int u) t = gcd t' (int u') * gcd (int u) t
[PROOF STEP]
have "gcd u' t' = 1"
[PROOF STATE]
proof (prove)
using this:
gcd (int u) t = gcd t' (int u') * gcd (int u) t

goal (1 subgoal):
 1. gcd (int u') t' = 1
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
gcd (int u) t = gcd t' (int u') * gcd (int u) t
0 < u
\<bar>int u\<bar> \<le> int s

goal (1 subgoal):
 1. gcd (int u') t' = 1
[PROOF STEP]
by (simp add: gcd.commute)
[PROOF STATE]
proof (state)
this:
gcd (int u') t' = 1

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
gcd (int u') t' = 1

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 / real s \<in> {\<bar>real_of_int t' - real u' * x\<bar><..1 / real u'}
0 < u'
gcd (int u') t' = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 / real s \<in> {\<bar>real_of_int t' - real u' * x\<bar><..1 / real u'}
0 < u'
gcd (int u') t' = 1

goal (1 subgoal):
 1. \<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>u t. 0 < u \<and> coprime (int u) t \<and> 1 / real s \<in> {\<bar>real_of_int t - real u * x\<bar><..1 / real u}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma D_gt_1: "D > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < D
[PROOF STEP]
from nonsquare_D
[PROOF STATE]
proof (chain)
picking this:
\<not> is_square D
[PROOF STEP]
have "D \<noteq> 0" "D \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
\<not> is_square D

goal (1 subgoal):
 1. D \<noteq> 0 &&& D \<noteq> 1
[PROOF STEP]
by (auto intro!: Nat.gr0I)
[PROOF STATE]
proof (state)
this:
D \<noteq> 0
D \<noteq> 1

goal (1 subgoal):
 1. 1 < D
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
D \<noteq> 0
D \<noteq> 1

goal (1 subgoal):
 1. 1 < D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma D_pos: "D > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < D
[PROOF STEP]
using nonsquare_D
[PROOF STATE]
proof (prove)
using this:
\<not> is_square D

goal (1 subgoal):
 1. 0 < D
[PROOF STEP]
by (intro Nat.gr0I) auto