[STATEMENT]
lemma fund_sol_minimal'':
  assumes "nontriv_solution z"
  shows   "fst fund_sol \<le> fst z" "snd fund_sol \<le> snd z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst fund_sol \<le> fst z &&& snd fund_sol \<le> snd z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst fund_sol \<le> fst z
 2. snd fund_sol \<le> snd z
[PROOF STEP]
have "pell_valuation (fst fund_sol, snd fund_sol) \<le> pell_valuation (fst z, snd z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (case (fst fund_sol, snd fund_sol) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (fst z, snd z) of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
using fund_sol_minimal'[OF assms]
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. pell_valuation (case (fst fund_sol, snd fund_sol) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (fst z, snd z) of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by (simp add: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
pell_valuation (case (fst fund_sol, snd fund_sol) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (fst z, snd z) of (x, y) \<Rightarrow> (int x, int y))

goal (2 subgoals):
 1. fst fund_sol \<le> fst z
 2. snd fund_sol \<le> snd z
[PROOF STEP]
hence "fst fund_sol \<le> fst z \<and> snd fund_sol \<le> snd z"
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case (fst fund_sol, snd fund_sol) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (fst z, snd z) of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. fst fund_sol \<le> fst z \<and> snd fund_sol \<le> snd z
[PROOF STEP]
using assms fund_sol_is_nontriv_solution
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case (fst fund_sol, snd fund_sol) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (fst z, snd z) of (x, y) \<Rightarrow> (int x, int y))
nontriv_solution z
nontriv_solution fund_sol

goal (1 subgoal):
 1. fst fund_sol \<le> fst z \<and> snd fund_sol \<le> snd z
[PROOF STEP]
by (subst solutions_le_iff_pell_valuation_le) (auto simp: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
fst fund_sol \<le> fst z \<and> snd fund_sol \<le> snd z

goal (2 subgoals):
 1. fst fund_sol \<le> fst z
 2. snd fund_sol \<le> snd z
[PROOF STEP]
thus "fst fund_sol \<le> fst z" "snd fund_sol \<le> snd z"
[PROOF STATE]
proof (prove)
using this:
fst fund_sol \<le> fst z \<and> snd fund_sol \<le> snd z

goal (1 subgoal):
 1. fst fund_sol \<le> fst z &&& snd fund_sol \<le> snd z
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
fst fund_sol \<le> fst z
snd fund_sol \<le> snd z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pell_cnj_snd_0 [simp]: "snd z = 0 \<Longrightarrow> pell_cnj z = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd z = (0::'a) \<Longrightarrow> pell_cnj z = z
[PROOF STEP]
by (cases z) (simp_all add: pell_cnj_def)


[STATEMENT]
lemma pell_mul_commutes: "pell_mul z1 z2 = pell_mul z2 z1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_mul z1 z2 = pell_mul z2 z1
[PROOF STEP]
by (auto simp: pell_mul_def algebra_simps case_prod_unfold)


[STATEMENT]
lemma pell_mul_assoc: "pell_mul z1 (pell_mul z2 z3) = pell_mul (pell_mul z1 z2) z3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_mul z1 (pell_mul z2 z3) = pell_mul (pell_mul z1 z2) z3
[PROOF STEP]
by (auto simp: pell_mul_def algebra_simps case_prod_unfold)


[STATEMENT]
lemma pell_mul_trivial_left [simp]: "pell_mul (1, 0) z = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_mul (1::'a, 0::'a) z = z
[PROOF STEP]
by (auto simp: pell_mul_def algebra_simps case_prod_unfold)


[STATEMENT]
lemma pell_mul_trivial_right [simp]: "pell_mul z (1, 0) = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_mul z (1::'a, 0::'a) = z
[PROOF STEP]
by (auto simp: pell_mul_def algebra_simps case_prod_unfold)


[STATEMENT]
lemma pell_mul_trivial_left_nat [simp]: "pell_mul (Suc 0, 0) z = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_mul (Suc 0, 0) z = z
[PROOF STEP]
by (auto simp: pell_mul_def algebra_simps case_prod_unfold)


[STATEMENT]
lemma pell_mul_trivial_right_nat [simp]: "pell_mul z (Suc 0, 0) = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_mul z (Suc 0, 0) = z
[PROOF STEP]
by (auto simp: pell_mul_def algebra_simps case_prod_unfold)


[STATEMENT]
lemma pell_power_0 [simp]: "pell_power z 0 = (1, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_power z 0 = (1::'a, 0::'a)
[PROOF STEP]
by (simp add: pell_power_def)


[STATEMENT]
lemma pell_power_one [simp]: "pell_power (1, 0) n = (1, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_power (1::'a, 0::'a) n = (1::'a, 0::'a)
[PROOF STEP]
by (induction n) (auto simp: pell_power_def)


[STATEMENT]
lemma pell_power_one_right [simp]: "pell_power z 1 = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_power z 1 = z
[PROOF STEP]
by (simp add: pell_power_def)


[STATEMENT]
lemma pell_power_Suc: "pell_power z (Suc n) = pell_mul z (pell_power z n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_power z (Suc n) = pell_mul z (pell_power z n)
[PROOF STEP]
by (simp add: pell_power_def pell_mul_commutes)


[STATEMENT]
lemma pell_power_add: "pell_power z (m + n) = pell_mul (pell_power z m) (pell_power z n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_power z (m + n) = pell_mul (pell_power z m) (pell_power z n)
[PROOF STEP]
by (induction m arbitrary: z )
     (simp_all add: funpow_add o_def pell_power_Suc pell_mul_assoc)


[STATEMENT]
lemma pell_valuation_mult [simp]:
  "pell_valuation (pell_mul z1 z2) = pell_valuation z1 * pell_valuation z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (pell_mul z1 z2) = pell_valuation z1 * pell_valuation z2
[PROOF STEP]
by (simp add: pell_valuation_def pell_mul_def case_prod_unfold algebra_simps)


[STATEMENT]
lemma pell_valuation_mult_nat [simp]:
  "pell_valuation (case pell_mul z1 z2 of (a, b) \<Rightarrow> (int a, int b)) =
     pell_valuation z1 * pell_valuation z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (case pell_mul z1 z2 of (a, b) \<Rightarrow> (int a, int b)) = pell_valuation (case z1 of (x, y) \<Rightarrow> (int x, int y)) * pell_valuation (case z2 of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by (simp add: pell_valuation_def pell_mul_def case_prod_unfold algebra_simps)


[STATEMENT]
lemma pell_valuation_trivial [simp]: "pell_valuation (1, 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (1, 0) = 1
[PROOF STEP]
by (simp add: pell_valuation_def)


[STATEMENT]
lemma pell_valuation_trivial_nat [simp]: "pell_valuation (Suc 0, 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (case (Suc 0, 0) of (x, y) \<Rightarrow> (int x, y)) = 1
[PROOF STEP]
by (simp add: pell_valuation_def)


[STATEMENT]
lemma pell_valuation_cnj: "pell_valuation (pell_cnj z) = fst z - snd z * sqrt D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (pell_cnj z) = fst (case z of (x, y) \<Rightarrow> (real_of_int x, y)) - snd (case z of (x, y) \<Rightarrow> (x, real_of_int y)) * sqrt (real D)
[PROOF STEP]
by (simp add: pell_valuation_def pell_cnj_def case_prod_unfold)


[STATEMENT]
lemma pell_valuation_snd_0 [simp]: "pell_valuation (a, 0) = of_int a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (a, 0) = real_of_int a
[PROOF STEP]
by (simp add: pell_valuation_def)


[STATEMENT]
lemma pell_valuation_0_iff [simp]: "pell_valuation z = 0 \<longleftrightarrow> z = (0, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pell_valuation z = 0) = (z = (0, 0))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pell_valuation z = 0 \<Longrightarrow> z = (0, 0)
 2. z = (0, 0) \<Longrightarrow> pell_valuation z = 0
[PROOF STEP]
assume *: "pell_valuation z = 0"
[PROOF STATE]
proof (state)
this:
pell_valuation z = 0

goal (2 subgoals):
 1. pell_valuation z = 0 \<Longrightarrow> z = (0, 0)
 2. z = (0, 0) \<Longrightarrow> pell_valuation z = 0
[PROOF STEP]
have "snd z = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd z = 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. snd z \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "snd z \<noteq> 0"
[PROOF STATE]
proof (state)
this:
snd z \<noteq> 0

goal (1 subgoal):
 1. snd z \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
pell_valuation z = 0
snd z \<noteq> 0
[PROOF STEP]
have "sqrt D = -fst z / snd z"
[PROOF STATE]
proof (prove)
using this:
pell_valuation z = 0
snd z \<noteq> 0

goal (1 subgoal):
 1. sqrt (real D) = real_of_int (- fst z) / real_of_int (snd z)
[PROOF STEP]
by (simp add: pell_valuation_def case_prod_unfold field_simps)
[PROOF STATE]
proof (state)
this:
sqrt (real D) = real_of_int (- fst z) / real_of_int (snd z)

goal (1 subgoal):
 1. snd z \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqrt (real D) = real_of_int (- fst z) / real_of_int (snd z)

goal (1 subgoal):
 1. snd z \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<in> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (- fst z) / real_of_int (snd z) \<in> \<rat>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int (- fst z) / real_of_int (snd z) \<in> \<rat>

goal (1 subgoal):
 1. snd z \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sqrt (real D) \<in> \<rat>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
sqrt (real D) \<in> \<rat>

goal (1 subgoal):
 1. False
[PROOF STEP]
using nonsquare_D irrat_sqrt_nonsquare
[PROOF STATE]
proof (prove)
using this:
sqrt (real D) \<in> \<rat>
\<not> is_square D
\<not> is_square ?n \<Longrightarrow> sqrt (real ?n) \<notin> \<rat>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
snd z = 0

goal (2 subgoals):
 1. pell_valuation z = 0 \<Longrightarrow> z = (0, 0)
 2. z = (0, 0) \<Longrightarrow> pell_valuation z = 0
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
pell_valuation z = 0
snd z = 0
[PROOF STEP]
have "fst z = 0"
[PROOF STATE]
proof (prove)
using this:
pell_valuation z = 0
snd z = 0

goal (1 subgoal):
 1. fst z = 0
[PROOF STEP]
by (simp add: pell_valuation_def case_prod_unfold)
[PROOF STATE]
proof (state)
this:
fst z = 0

goal (2 subgoals):
 1. pell_valuation z = 0 \<Longrightarrow> z = (0, 0)
 2. z = (0, 0) \<Longrightarrow> pell_valuation z = 0
[PROOF STEP]
with \<open>snd z = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
snd z = 0
fst z = 0
[PROOF STEP]
show "z = (0, 0)"
[PROOF STATE]
proof (prove)
using this:
snd z = 0
fst z = 0

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

goal (1 subgoal):
 1. z = (0, 0) \<Longrightarrow> pell_valuation z = 0
[PROOF STEP]
qed (auto simp: pell_valuation_def)


[STATEMENT]
lemma pell_valuation_solution_pos_nat:
  fixes z :: "nat \<times> nat"
  assumes "solution z"
  shows   "pell_valuation z > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
solution z
[PROOF STEP]
have "z \<noteq> (0, 0)"
[PROOF STATE]
proof (prove)
using this:
solution z

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

goal (1 subgoal):
 1. 0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
hence "pell_valuation z \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> (0, 0)

goal (1 subgoal):
 1. pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) \<noteq> 0
[PROOF STEP]
by (auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) \<noteq> 0

goal (1 subgoal):
 1. 0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) \<noteq> 0

goal (1 subgoal):
 1. 0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
have "pell_valuation z \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by (intro pell_valuation_nonneg) (auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
0 \<le> pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. 0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) \<noteq> 0
0 \<le> pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) \<noteq> 0
0 \<le> pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. 0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pell_valuation_cnj_solution:
  fixes z :: "nat \<times> nat"
  assumes "solution z"
  shows   "pell_valuation (pell_cnj z) = 1 / pell_valuation z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) = 1 / pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) = 1 / pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
have "pell_valuation (pell_cnj z) * pell_valuation z = pell_valuation (pell_mul (pell_cnj z) z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) * pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (pell_mul (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) (case z of (x, y) \<Rightarrow> (int x, int y)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) * pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (pell_mul (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) (case z of (x, y) \<Rightarrow> (int x, int y)))

goal (1 subgoal):
 1. pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) = 1 / pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) * pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (pell_mul (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) (case z of (x, y) \<Rightarrow> (int x, int y)))

goal (1 subgoal):
 1. pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) = 1 / pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
solution z
[PROOF STEP]
have "pell_mul (pell_cnj z) z = (1, 0)"
[PROOF STATE]
proof (prove)
using this:
solution z

goal (1 subgoal):
 1. pell_mul (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) (case z of (x, y) \<Rightarrow> (int x, int y)) = (1, 0)
[PROOF STEP]
by (subst pell_mul_cnj_left) (auto simp: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
pell_mul (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) (case z of (x, y) \<Rightarrow> (int x, int y)) = (1, 0)

goal (1 subgoal):
 1. pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) = 1 / pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) * pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (1, 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) * pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (1, 0)

goal (1 subgoal):
 1. pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) = 1 / pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
using pell_valuation_solution_pos_nat[OF assms]
[PROOF STATE]
proof (prove)
using this:
pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) * pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (1, 0)
0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) = 1 / pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by (auto simp: divide_simps)
[PROOF STATE]
proof (state)
this:
pell_valuation (pell_cnj (case z of (x, y) \<Rightarrow> (int x, int y))) = 1 / pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pell_valuation_power [simp]: "pell_valuation (pell_power z n) = pell_valuation z ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (pell_power z n) = pell_valuation z ^ n
[PROOF STEP]
by (induction n) (simp_all add: pell_power_Suc)


[STATEMENT]
lemma pell_valuation_power_nat [simp]:
  "pell_valuation (case pell_power z n of (a, b) \<Rightarrow> (int a, int b)) = pell_valuation z ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (case pell_power z n of (a, b) \<Rightarrow> (int a, int b)) = pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y)) ^ n
[PROOF STEP]
by (induction n) (simp_all add: pell_power_Suc)


[STATEMENT]
lemma solution_pell_mul [intro]:
  assumes "solution z1" "solution z2"
  shows   "solution (pell_mul z1 z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (pell_mul z1 z2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solution (pell_mul z1 z2)
[PROOF STEP]
obtain a b where [simp]: "z1 = (a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. z1 = (a, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z1)
[PROOF STATE]
proof (state)
this:
z1 = (a, b)

goal (1 subgoal):
 1. solution (pell_mul z1 z2)
[PROOF STEP]
obtain c d where [simp]: "z2 = (c, d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c d. z2 = (c, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z2)
[PROOF STATE]
proof (state)
this:
z2 = (c, d)

goal (1 subgoal):
 1. solution (pell_mul z1 z2)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
solution z1
solution z2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
solution z1
solution z2

goal (1 subgoal):
 1. solution (pell_mul z1 z2)
[PROOF STEP]
by (simp add: solution_def pell_mul_def case_prod_unfold power2_eq_square algebra_simps)
[PROOF STATE]
proof (state)
this:
solution (pell_mul z1 z2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solution_pell_cnj [intro]:
  assumes "solution z"
  shows   "solution (pell_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (pell_cnj z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
solution z

goal (1 subgoal):
 1. solution (pell_cnj z)
[PROOF STEP]
by (auto simp: solution_def pell_cnj_def)


[STATEMENT]
lemma solution_pell_power [simp, intro]: "solution z \<Longrightarrow> solution (pell_power z n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution z \<Longrightarrow> solution (pell_power z n)
[PROOF STEP]
by (induction n) (auto simp: pell_power_Suc)


[STATEMENT]
lemma pell_mul_eq_trivial_nat_iff:
  "pell_mul z1 z2 = (Suc 0, 0) \<longleftrightarrow> z1 = (Suc 0, 0) \<and> z2 = (Suc 0, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pell_mul z1 z2 = (Suc 0, 0)) = (z1 = (Suc 0, 0) \<and> z2 = (Suc 0, 0))
[PROOF STEP]
using D_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < D

goal (1 subgoal):
 1. (pell_mul z1 z2 = (Suc 0, 0)) = (z1 = (Suc 0, 0) \<and> z2 = (Suc 0, 0))
[PROOF STEP]
by (cases z1; cases z2) (auto simp: pell_mul_def)


[STATEMENT]
lemma nontriv_solution_pell_nat_mul1:
  "solution (z1 :: nat \<times> nat) \<Longrightarrow> nontriv_solution z2 \<Longrightarrow> nontriv_solution (pell_mul z1 z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>solution z1; nontriv_solution z2\<rbrakk> \<Longrightarrow> nontriv_solution (pell_mul z1 z2)
[PROOF STEP]
by (auto simp: nontriv_solution_altdef pell_mul_eq_trivial_nat_iff)


[STATEMENT]
lemma nontriv_solution_pell_nat_mul2:
  "nontriv_solution (z1 :: nat \<times> nat) \<Longrightarrow> solution z2 \<Longrightarrow> nontriv_solution (pell_mul z1 z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nontriv_solution z1; solution z2\<rbrakk> \<Longrightarrow> nontriv_solution (pell_mul z1 z2)
[PROOF STEP]
by (auto simp: nontriv_solution_altdef pell_mul_eq_trivial_nat_iff)


[STATEMENT]
lemma nontriv_solution_power_nat [intro]:
  assumes "nontriv_solution (z :: nat \<times> nat)" "n > 0"
  shows   "nontriv_solution (pell_power z n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nontriv_solution (pell_power z n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nontriv_solution (pell_power z n)
[PROOF STEP]
have "nontriv_solution (pell_power z n) \<or> n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nontriv_solution (pell_power z n) \<or> n = 0
[PROOF STEP]
by (induction n)
       (insert assms(1), auto intro: nontriv_solution_pell_nat_mul1 simp: pell_power_Suc)
[PROOF STATE]
proof (state)
this:
nontriv_solution (pell_power z n) \<or> n = 0

goal (1 subgoal):
 1. nontriv_solution (pell_power z n)
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
0 < n
nontriv_solution (pell_power z n) \<or> n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < n
nontriv_solution (pell_power z n) \<or> n = 0

goal (1 subgoal):
 1. nontriv_solution (pell_power z n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nontriv_solution (pell_power z n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pell_valuation_pos_neg:
  assumes "x > 0" "y < 0" "solution (x, y)"
  shows   "pell_valuation (x, y) \<in> {0<..<1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (x, y) \<in> {0<..<1}
[PROOF STEP]
using pell_valuation_pos_neg_aux[of x "-y"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < x; 0 < - y; solution (x, - y)\<rbrakk> \<Longrightarrow> pell_valuation (x, - (- y)) \<in> {0<..<1}
0 < x
y < 0
solution (x, y)

goal (1 subgoal):
 1. pell_valuation (x, y) \<in> {0<..<1}
[PROOF STEP]
by simp


[STATEMENT]
lemma pell_valuation_neg_neg:
  assumes "x < 0" "y < 0" "solution (x, y)"
  shows   "pell_valuation (x, y) < -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (x, y) < - 1
[PROOF STEP]
using pell_valuation_pos_pos[of "-x" "-y"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < - x; 0 < - y; solution (- x, - y)\<rbrakk> \<Longrightarrow> 1 < pell_valuation (- x, - y)
x < 0
y < 0
solution (x, y)

goal (1 subgoal):
 1. pell_valuation (x, y) < - 1
[PROOF STEP]
by simp


[STATEMENT]
lemma pell_valuation_neg_pos:
  assumes "x < 0" "y > 0" "solution (x, y)"
  shows   "pell_valuation (x, y) \<in> {-1<..<0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (x, y) \<in> {- 1<..<0}
[PROOF STEP]
using pell_valuation_pos_neg[of "-x" "-y"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < - x; - y < 0; solution (- x, - y)\<rbrakk> \<Longrightarrow> pell_valuation (- x, - y) \<in> {0<..<1}
x < 0
0 < y
solution (x, y)

goal (1 subgoal):
 1. pell_valuation (x, y) \<in> {- 1<..<0}
[PROOF STEP]
by simp


[STATEMENT]
lemma pell_valuation_solution_gt1D:
  assumes "solution z" "pell_valuation z > 1"
  shows   "fst z > 0 \<and> snd z > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < fst z \<and> 0 < snd z
[PROOF STEP]
using pell_valuation_pos_pos[of "fst z" "snd z"] pell_valuation_pos_neg[of "fst z" "snd z"]
        pell_valuation_neg_pos[of "fst z" "snd z"] pell_valuation_neg_neg[of "fst z" "snd z"]
        assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < fst z; 0 < snd z; solution (fst z, snd z)\<rbrakk> \<Longrightarrow> 1 < pell_valuation (fst z, snd z)
\<lbrakk>0 < fst z; snd z < 0; solution (fst z, snd z)\<rbrakk> \<Longrightarrow> pell_valuation (fst z, snd z) \<in> {0<..<1}
\<lbrakk>fst z < 0; 0 < snd z; solution (fst z, snd z)\<rbrakk> \<Longrightarrow> pell_valuation (fst z, snd z) \<in> {- 1<..<0}
\<lbrakk>fst z < 0; snd z < 0; solution (fst z, snd z)\<rbrakk> \<Longrightarrow> pell_valuation (fst z, snd z) < - 1
solution z
1 < pell_valuation z

goal (1 subgoal):
 1. 0 < fst z \<and> 0 < snd z
[PROOF STEP]
by (cases "fst z" "0 :: int" rule: linorder_cases;
      cases "snd z" "0 :: int" rule: linorder_cases;
      cases z) auto


[STATEMENT]
lemma pell_valuation_nth_solution [simp]:
  "pell_valuation (nth_solution n) = pell_valuation fund_sol ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ n
[PROOF STEP]
by (simp add: nth_solution_def)


[STATEMENT]
theorem nth_solution_inj: "inj nth_solution"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj nth_solution
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; nth_solution x = nth_solution y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix m n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; nth_solution x = nth_solution y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "nth_solution m = nth_solution n"
[PROOF STATE]
proof (state)
this:
nth_solution m = nth_solution n

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; nth_solution x = nth_solution y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "pell_valuation (nth_solution m) = pell_valuation (nth_solution n)"
[PROOF STATE]
proof (prove)
using this:
nth_solution m = nth_solution n

goal (1 subgoal):
 1. pell_valuation (case nth_solution m of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by (simp only: )
[PROOF STATE]
proof (state)
this:
pell_valuation (case nth_solution m of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; nth_solution x = nth_solution y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pell_valuation (case nth_solution m of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; nth_solution x = nth_solution y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "pell_valuation (nth_solution m) = pell_valuation fund_sol ^ m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (case nth_solution m of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pell_valuation (case nth_solution m of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ m

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; nth_solution x = nth_solution y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pell_valuation (case nth_solution m of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ m

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; nth_solution x = nth_solution y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "pell_valuation (nth_solution n) = pell_valuation fund_sol ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ n

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; nth_solution x = nth_solution y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ m = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ n
[PROOF STEP]
show "m = n"
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ m = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ n

goal (1 subgoal):
 1. m = n
[PROOF STEP]
using pell_valuation_fund_sol_ge_2
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ m = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) ^ n
2 \<le> pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. m = n
[PROOF STEP]
by (subst (asm) power_inject_exp) auto
[PROOF STATE]
proof (state)
this:
m = n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem nth_solution_sound [intro]: "solution (nth_solution n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (nth_solution n)
[PROOF STEP]
using fund_sol_is_nontriv_solution
[PROOF STATE]
proof (prove)
using this:
nontriv_solution fund_sol

goal (1 subgoal):
 1. solution (nth_solution n)
[PROOF STEP]
by (auto simp: nth_solution_def)


[STATEMENT]
theorem nth_solution_sound' [intro]: "n > 0 \<Longrightarrow> nontriv_solution (nth_solution n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> nontriv_solution (nth_solution n)
[PROOF STEP]
using fund_sol_is_nontriv_solution
[PROOF STATE]
proof (prove)
using this:
nontriv_solution fund_sol

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> nontriv_solution (nth_solution n)
[PROOF STEP]
by (auto simp: nth_solution_def)


[STATEMENT]
theorem nth_solution_complete:
  fixes z :: "nat \<times> nat"
  assumes "solution z"
  shows   "z \<in> range nth_solution"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> range nth_solution
[PROOF STEP]
proof (cases "z = (1, 0)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = (1, 0) \<Longrightarrow> z \<in> range nth_solution
 2. z \<noteq> (1, 0) \<Longrightarrow> z \<in> range nth_solution
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
z = (1, 0)

goal (2 subgoals):
 1. z = (1, 0) \<Longrightarrow> z \<in> range nth_solution
 2. z \<noteq> (1, 0) \<Longrightarrow> z \<in> range nth_solution
[PROOF STEP]
hence "z = nth_solution 0"
[PROOF STATE]
proof (prove)
using this:
z = (1, 0)

goal (1 subgoal):
 1. z = nth_solution 0
[PROOF STEP]
by (simp add: nth_solution_def)
[PROOF STATE]
proof (state)
this:
z = nth_solution 0

goal (2 subgoals):
 1. z = (1, 0) \<Longrightarrow> z \<in> range nth_solution
 2. z \<noteq> (1, 0) \<Longrightarrow> z \<in> range nth_solution
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z = nth_solution 0

goal (1 subgoal):
 1. z \<in> range nth_solution
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> range nth_solution

goal (1 subgoal):
 1. z \<noteq> (1, 0) \<Longrightarrow> z \<in> range nth_solution
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<noteq> (1, 0) \<Longrightarrow> z \<in> range nth_solution
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> (1, 0)

goal (1 subgoal):
 1. z \<noteq> (1, 0) \<Longrightarrow> z \<in> range nth_solution
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
solution z
z \<noteq> (1, 0)
[PROOF STEP]
have "nontriv_solution z"
[PROOF STATE]
proof (prove)
using this:
solution z
z \<noteq> (1, 0)

goal (1 subgoal):
 1. nontriv_solution z
[PROOF STEP]
by (auto simp: nontriv_solution_altdef)
[PROOF STATE]
proof (state)
this:
nontriv_solution z

goal (1 subgoal):
 1. z \<noteq> (1, 0) \<Longrightarrow> z \<in> range nth_solution
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> range nth_solution
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
z \<notin> range nth_solution

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
hence *: "pell_power fund_sol n \<noteq> z" for n
[PROOF STATE]
proof (prove)
using this:
z \<notin> range nth_solution

goal (1 subgoal):
 1. pell_power fund_sol n \<noteq> z
[PROOF STEP]
unfolding nth_solution_def
[PROOF STATE]
proof (prove)
using this:
z \<notin> range (pell_power fund_sol)

goal (1 subgoal):
 1. pell_power fund_sol n \<noteq> z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pell_power fund_sol ?n4 \<noteq> z

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
define u where "u = pell_valuation fund_sol"
[PROOF STATE]
proof (state)
this:
u = pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
define v where "v = pell_valuation z"
[PROOF STATE]
proof (state)
this:
v = pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
define n where "n = nat \<lfloor>log u v\<rfloor>"
[PROOF STATE]
proof (state)
this:
n = nat \<lfloor>log u v\<rfloor>

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
have u_ge_2: "u \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> u
[PROOF STEP]
using pell_valuation_fund_sol_ge_2
[PROOF STATE]
proof (prove)
using this:
2 \<le> pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. 2 \<le> u
[PROOF STEP]
by (auto simp: u_def)
[PROOF STATE]
proof (state)
this:
2 \<le> u

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
have v_pos: "v > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < v
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
solution z

goal (1 subgoal):
 1. 0 < pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by (intro pell_valuation_solution_pos_nat) auto
[PROOF STATE]
proof (state)
this:
0 < v

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
have u_le_v: "u \<le> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> v
[PROOF STEP]
unfolding u_def v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by (rule fund_sol_minimal') fact
[PROOF STATE]
proof (state)
this:
u \<le> v

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
have u_power_neq_v: "u ^ k \<noteq> v" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ^ k \<noteq> v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u ^ k = v \<Longrightarrow> False
[PROOF STEP]
assume "u ^ k = v"
[PROOF STATE]
proof (state)
this:
u ^ k = v

goal (1 subgoal):
 1. u ^ k = v \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u ^ k = v

goal (1 subgoal):
 1. u ^ k = v \<Longrightarrow> False
[PROOF STEP]
have "u ^ k = pell_valuation (pell_power fund_sol k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ^ k = pell_valuation (case pell_power fund_sol k of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by (simp add: u_def)
[PROOF STATE]
proof (state)
this:
u ^ k = pell_valuation (case pell_power fund_sol k of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. u ^ k = v \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u ^ k = pell_valuation (case pell_power fund_sol k of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. u ^ k = v \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = v \<longleftrightarrow> pell_power fund_sol k = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pell_valuation (case pell_power fund_sol k of (x, y) \<Rightarrow> (int x, int y)) = v) = (pell_power fund_sol k = z)
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pell_valuation (case pell_power fund_sol k of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case z of (x, y) \<Rightarrow> (int x, int y))) = (pell_power fund_sol k = z)
[PROOF STEP]
by (subst pell_valuation_eq_iff) (auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
(pell_valuation (case pell_power fund_sol k of (x, y) \<Rightarrow> (int x, int y)) = v) = (pell_power fund_sol k = z)

goal (1 subgoal):
 1. u ^ k = v \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pell_power fund_sol k = z
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
pell_power fund_sol k = z

goal (1 subgoal):
 1. False
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
pell_power fund_sol k = z
pell_power fund_sol ?n4 \<noteq> z

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u ^ ?k4 \<noteq> v

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
from u_le_v v_pos u_ge_2
[PROOF STATE]
proof (chain)
picking this:
u \<le> v
0 < v
2 \<le> u
[PROOF STEP]
have log_ge_1: "log u v \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
u \<le> v
0 < v
2 \<le> u

goal (1 subgoal):
 1. 1 \<le> log u v
[PROOF STEP]
by (subst one_le_log_cancel_iff) auto
[PROOF STATE]
proof (state)
this:
1 \<le> log u v

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
define z' where "z' = pell_mul z (pell_power (pell_cnj fund_sol) n)"
[PROOF STATE]
proof (state)
this:
z' = pell_mul (case z of (x, y) \<Rightarrow> (int x, int y)) (pell_power (pell_cnj (case fund_sol of (x, y) \<Rightarrow> (int x, int y))) n)

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
define x and y where "x = nat \<bar>fst z'\<bar>" and "y = nat \<bar>snd z'\<bar>"
[PROOF STATE]
proof (state)
this:
x = nat \<bar>fst z'\<bar>
y = nat \<bar>snd z'\<bar>

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
have "solution z'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution z'
[PROOF STEP]
using assms fund_sol_is_nontriv_solution
[PROOF STATE]
proof (prove)
using this:
solution z
nontriv_solution fund_sol

goal (1 subgoal):
 1. solution z'
[PROOF STEP]
unfolding z'_def
[PROOF STATE]
proof (prove)
using this:
solution z
nontriv_solution fund_sol

goal (1 subgoal):
 1. solution (pell_mul (case z of (x, y) \<Rightarrow> (int x, int y)) (pell_power (pell_cnj (case fund_sol of (x, y) \<Rightarrow> (int x, int y))) n))
[PROOF STEP]
by (intro solution_pell_mul solution_pell_power solution_pell_cnj) (auto simp: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
solution z'

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
have "u ^ n < v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ^ n < v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u ^ n < v
[PROOF STEP]
from u_ge_2
[PROOF STATE]
proof (chain)
picking this:
2 \<le> u
[PROOF STEP]
have "u ^ n = u powr real n"
[PROOF STATE]
proof (prove)
using this:
2 \<le> u

goal (1 subgoal):
 1. u ^ n = u powr real n
[PROOF STEP]
by (subst powr_realpow) auto
[PROOF STATE]
proof (state)
this:
u ^ n = u powr real n

goal (1 subgoal):
 1. u ^ n < v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u ^ n = u powr real n

goal (1 subgoal):
 1. u ^ n < v
[PROOF STEP]
have "\<dots> \<le> u powr log u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u powr real n \<le> u powr log u v
[PROOF STEP]
using u_ge_2 log_ge_1
[PROOF STATE]
proof (prove)
using this:
2 \<le> u
1 \<le> log u v

goal (1 subgoal):
 1. u powr real n \<le> u powr log u v
[PROOF STEP]
by (intro powr_mono) (auto simp: n_def)
[PROOF STATE]
proof (state)
this:
u powr real n \<le> u powr log u v

goal (1 subgoal):
 1. u ^ n < v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u powr real n \<le> u powr log u v

goal (1 subgoal):
 1. u ^ n < v
[PROOF STEP]
have "\<dots> = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u powr log u v = v
[PROOF STEP]
using u_ge_2 v_pos
[PROOF STATE]
proof (prove)
using this:
2 \<le> u
0 < v

goal (1 subgoal):
 1. u powr log u v = v
[PROOF STEP]
by (subst powr_log_cancel) auto
[PROOF STATE]
proof (state)
this:
u powr log u v = v

goal (1 subgoal):
 1. u ^ n < v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u ^ n \<le> v
[PROOF STEP]
have "u ^ n \<le> v"
[PROOF STATE]
proof (prove)
using this:
u ^ n \<le> v

goal (1 subgoal):
 1. u ^ n \<le> v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
u ^ n \<le> v

goal (1 subgoal):
 1. u ^ n < v
[PROOF STEP]
with u_power_neq_v[of n]
[PROOF STATE]
proof (chain)
picking this:
u ^ n \<noteq> v
u ^ n \<le> v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u ^ n \<noteq> v
u ^ n \<le> v

goal (1 subgoal):
 1. u ^ n < v
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
u ^ n < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u ^ n < v

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u ^ n < v

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
have "v < u ^ Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
have "v = u powr log u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = u powr log u v
[PROOF STEP]
using u_ge_2 v_pos
[PROOF STATE]
proof (prove)
using this:
2 \<le> u
0 < v

goal (1 subgoal):
 1. v = u powr log u v
[PROOF STEP]
by (subst powr_log_cancel) auto
[PROOF STATE]
proof (state)
this:
v = u powr log u v

goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v = u powr log u v

goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
have "log u v \<le> 1 + real_of_int \<lfloor>log u v\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log u v \<le> 1 + real_of_int \<lfloor>log u v\<rfloor>
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
log u v \<le> 1 + real_of_int \<lfloor>log u v\<rfloor>

goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
hence "u powr log u v \<le> u powr real (Suc n)"
[PROOF STATE]
proof (prove)
using this:
log u v \<le> 1 + real_of_int \<lfloor>log u v\<rfloor>

goal (1 subgoal):
 1. u powr log u v \<le> u powr real (Suc n)
[PROOF STEP]
using u_ge_2 log_ge_1
[PROOF STATE]
proof (prove)
using this:
log u v \<le> 1 + real_of_int \<lfloor>log u v\<rfloor>
2 \<le> u
1 \<le> log u v

goal (1 subgoal):
 1. u powr log u v \<le> u powr real (Suc n)
[PROOF STEP]
by (intro powr_mono) (auto simp: n_def)
[PROOF STATE]
proof (state)
this:
u powr log u v \<le> u powr real (Suc n)

goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u powr log u v \<le> u powr real (Suc n)

goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
have "\<dots> = u ^ Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u powr real (Suc n) = u ^ Suc n
[PROOF STEP]
using u_ge_2
[PROOF STATE]
proof (prove)
using this:
2 \<le> u

goal (1 subgoal):
 1. u powr real (Suc n) = u ^ Suc n
[PROOF STEP]
by (subst powr_realpow) auto
[PROOF STATE]
proof (state)
this:
u powr real (Suc n) = u ^ Suc n

goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
v \<le> u ^ Suc n
[PROOF STEP]
have "u ^ Suc n \<ge> v"
[PROOF STATE]
proof (prove)
using this:
v \<le> u ^ Suc n

goal (1 subgoal):
 1. v \<le> u ^ Suc n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
v \<le> u ^ Suc n

goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
with u_power_neq_v[of "Suc n"]
[PROOF STATE]
proof (chain)
picking this:
u ^ Suc n \<noteq> v
v \<le> u ^ Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u ^ Suc n \<noteq> v
v \<le> u ^ Suc n

goal (1 subgoal):
 1. v < u ^ Suc n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
v < u ^ Suc n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v < u ^ Suc n

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u ^ n < v
v < u ^ Suc n
[PROOF STEP]
have "v / u ^ n \<in> {1<..<u}"
[PROOF STATE]
proof (prove)
using this:
u ^ n < v
v < u ^ Suc n

goal (1 subgoal):
 1. v / u ^ n \<in> {1<..<u}
[PROOF STEP]
using u_ge_2
[PROOF STATE]
proof (prove)
using this:
u ^ n < v
v < u ^ Suc n
2 \<le> u

goal (1 subgoal):
 1. v / u ^ n \<in> {1<..<u}
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
v / u ^ n \<in> {1<..<u}

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v / u ^ n \<in> {1<..<u}

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
have "v / u ^ n = pell_valuation z'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v / u ^ n = pell_valuation z'
[PROOF STEP]
using fund_sol_is_nontriv_solution
[PROOF STATE]
proof (prove)
using this:
nontriv_solution fund_sol

goal (1 subgoal):
 1. v / u ^ n = pell_valuation z'
[PROOF STEP]
by (auto simp add: z'_def u_def v_def pell_valuation_cnj_solution field_simps)
[PROOF STATE]
proof (state)
this:
v / u ^ n = pell_valuation z'

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pell_valuation z' \<in> {1<..<u}
[PROOF STEP]
have val: "pell_valuation z' \<in> {1<..<u}"
[PROOF STATE]
proof (prove)
using this:
pell_valuation z' \<in> {1<..<u}

goal (1 subgoal):
 1. pell_valuation z' \<in> {1<..<u}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
pell_valuation z' \<in> {1<..<u}

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
from val and \<open>solution z'\<close>
[PROOF STATE]
proof (chain)
picking this:
pell_valuation z' \<in> {1<..<u}
solution z'
[PROOF STEP]
have "nontriv_solution z'"
[PROOF STATE]
proof (prove)
using this:
pell_valuation z' \<in> {1<..<u}
solution z'

goal (1 subgoal):
 1. nontriv_solution z'
[PROOF STEP]
by (auto simp: nontriv_solution_altdef)
[PROOF STATE]
proof (state)
this:
nontriv_solution z'

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
from \<open>solution z'\<close> and val
[PROOF STATE]
proof (chain)
picking this:
solution z'
pell_valuation z' \<in> {1<..<u}
[PROOF STEP]
have "fst z' > 0 \<and> snd z' > 0"
[PROOF STATE]
proof (prove)
using this:
solution z'
pell_valuation z' \<in> {1<..<u}

goal (1 subgoal):
 1. 0 < fst z' \<and> 0 < snd z'
[PROOF STEP]
by (intro pell_valuation_solution_gt1D) auto
[PROOF STATE]
proof (state)
this:
0 < fst z' \<and> 0 < snd z'

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
hence [simp]: "z' = (int x, int y)"
[PROOF STATE]
proof (prove)
using this:
0 < fst z' \<and> 0 < snd z'

goal (1 subgoal):
 1. z' = (int x, int y)
[PROOF STEP]
by (auto simp: x_def y_def)
[PROOF STATE]
proof (state)
this:
z' = (int x, int y)

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
from \<open>nontriv_solution z'\<close>
[PROOF STATE]
proof (chain)
picking this:
nontriv_solution z'
[PROOF STEP]
have "pell_valuation (int x, int y) \<ge> u"
[PROOF STATE]
proof (prove)
using this:
nontriv_solution z'

goal (1 subgoal):
 1. u \<le> pell_valuation (int x, int y)
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
using this:
nontriv_solution z'

goal (1 subgoal):
 1. pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (int x, int y)
[PROOF STEP]
by (intro fund_sol_minimal) auto
[PROOF STATE]
proof (state)
this:
u \<le> pell_valuation (int x, int y)

goal (1 subgoal):
 1. z \<notin> range nth_solution \<Longrightarrow> False
[PROOF STEP]
with val
[PROOF STATE]
proof (chain)
picking this:
pell_valuation z' \<in> {1<..<u}
u \<le> pell_valuation (int x, int y)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
pell_valuation z' \<in> {1<..<u}
u \<le> pell_valuation (int x, int y)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> range nth_solution

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strict_mono_pell_valuation_nth_solution: "strict_mono (pell_valuation \<circ> nth_solution)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono (pell_valuation \<circ> (\<lambda>x. case nth_solution x of (x, y) \<Rightarrow> (int x, int y)))
[PROOF STEP]
using pell_valuation_fund_sol_ge_2
[PROOF STATE]
proof (prove)
using this:
2 \<le> pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. strict_mono (pell_valuation \<circ> (\<lambda>x. case nth_solution x of (x, y) \<Rightarrow> (int x, int y)))
[PROOF STEP]
by (auto simp: strict_mono_def intro!: power_strict_increasing)


[STATEMENT]
lemma strict_mono_nth_solution:
  "strict_mono (fst \<circ> nth_solution)" "strict_mono (snd \<circ> nth_solution)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono (fst \<circ> nth_solution) &&& strict_mono (snd \<circ> nth_solution)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. strict_mono (fst \<circ> nth_solution)
 2. strict_mono (snd \<circ> nth_solution)
[PROOF STEP]
let ?g = nth_solution
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. strict_mono (fst \<circ> nth_solution)
 2. strict_mono (snd \<circ> nth_solution)
[PROOF STEP]
have "fst (?g m) < fst (?g n) \<and> snd (?g m) < snd (?g n)" if "m < n" for m n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (nth_solution m) < fst (nth_solution n) \<and> snd (nth_solution m) < snd (nth_solution n)
[PROOF STEP]
using pell_valuation_fund_sol_ge_2 that
[PROOF STATE]
proof (prove)
using this:
2 \<le> pell_valuation (case fund_sol of (x, y) \<Rightarrow> (int x, int y))
m < n

goal (1 subgoal):
 1. fst (nth_solution m) < fst (nth_solution n) \<and> snd (nth_solution m) < snd (nth_solution n)
[PROOF STEP]
by (subst solutions_less_iff_pell_valuation_less) auto
[PROOF STATE]
proof (state)
this:
?m4 < ?n4 \<Longrightarrow> fst (nth_solution ?m4) < fst (nth_solution ?n4) \<and> snd (nth_solution ?m4) < snd (nth_solution ?n4)

goal (2 subgoals):
 1. strict_mono (fst \<circ> nth_solution)
 2. strict_mono (snd \<circ> nth_solution)
[PROOF STEP]
thus "strict_mono (fst \<circ> nth_solution)" "strict_mono (snd \<circ> nth_solution)"
[PROOF STATE]
proof (prove)
using this:
?m4 < ?n4 \<Longrightarrow> fst (nth_solution ?m4) < fst (nth_solution ?n4) \<and> snd (nth_solution ?m4) < snd (nth_solution ?n4)

goal (1 subgoal):
 1. strict_mono (fst \<circ> nth_solution) &&& strict_mono (snd \<circ> nth_solution)
[PROOF STEP]
by (auto simp: strict_mono_def)
[PROOF STATE]
proof (state)
this:
strict_mono (fst \<circ> nth_solution)
strict_mono (snd \<circ> nth_solution)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pell_square_minus1: "pell (a\<^sup>2 - Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell (a\<^sup>2 - Suc 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_square (a\<^sup>2 - Suc 0)
[PROOF STEP]
show "\<not>is_square (a\<^sup>2 - Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_square (a\<^sup>2 - Suc 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_square (a\<^sup>2 - Suc 0) \<Longrightarrow> False
[PROOF STEP]
assume "is_square (a\<^sup>2 - Suc 0)"
[PROOF STATE]
proof (state)
this:
is_square (a\<^sup>2 - Suc 0)

goal (1 subgoal):
 1. is_square (a\<^sup>2 - Suc 0) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_square (a\<^sup>2 - Suc 0)
[PROOF STEP]
obtain k where "k\<^sup>2 = a\<^sup>2 - 1"
[PROOF STATE]
proof (prove)
using this:
is_square (a\<^sup>2 - Suc 0)

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

goal (1 subgoal):
 1. is_square (a\<^sup>2 - Suc 0) \<Longrightarrow> False
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
1 < a
k\<^sup>2 = a\<^sup>2 - 1
[PROOF STEP]
have "a\<^sup>2 = Suc (k\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
1 < a
k\<^sup>2 = a\<^sup>2 - 1

goal (1 subgoal):
 1. a\<^sup>2 = Suc (k\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a\<^sup>2 = Suc (k\<^sup>2)

goal (1 subgoal):
 1. is_square (a\<^sup>2 - Suc 0) \<Longrightarrow> False
[PROOF STEP]
hence "a = 1"
[PROOF STATE]
proof (prove)
using this:
a\<^sup>2 = Suc (k\<^sup>2)

goal (1 subgoal):
 1. a = 1
[PROOF STEP]
using pell_square_solution_nat_iff[of "1" a k]
[PROOF STATE]
proof (prove)
using this:
a\<^sup>2 = Suc (k\<^sup>2)
is_square 1 \<Longrightarrow> (a\<^sup>2 = 1 + 1 * k\<^sup>2) = (a = 1 \<and> (1 = 0 \<or> k = 0))

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

goal (1 subgoal):
 1. is_square (a\<^sup>2 - Suc 0) \<Longrightarrow> False
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
1 < a
a = 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
1 < a
a = 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> is_square (a\<^sup>2 - Suc 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fund_sol_square_minus1: "fund_sol = (a, 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fund_sol = (a, 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fund_sol = (a, 1)
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
1 < a
[PROOF STEP]
have sol: "nontriv_solution (a, 1)"
[PROOF STATE]
proof (prove)
using this:
1 < a

goal (1 subgoal):
 1. nontriv_solution (a, 1)
[PROOF STEP]
by (simp add: nontriv_solution_def)
[PROOF STATE]
proof (state)
this:
nontriv_solution (a, 1)

goal (1 subgoal):
 1. fund_sol = (a, 1)
[PROOF STEP]
from sol
[PROOF STATE]
proof (chain)
picking this:
nontriv_solution (a, 1)
[PROOF STEP]
have "snd fund_sol \<le> 1"
[PROOF STATE]
proof (prove)
using this:
nontriv_solution (a, 1)

goal (1 subgoal):
 1. snd fund_sol \<le> 1
[PROOF STEP]
using fund_sol_minimal''[of "(a, 1)"]
[PROOF STATE]
proof (prove)
using this:
nontriv_solution (a, 1)
nontriv_solution (a, 1) \<Longrightarrow> fst fund_sol \<le> fst (a, 1)
nontriv_solution (a, 1) \<Longrightarrow> snd fund_sol \<le> snd (a, 1)

goal (1 subgoal):
 1. snd fund_sol \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd fund_sol \<le> 1

goal (1 subgoal):
 1. fund_sol = (a, 1)
[PROOF STEP]
with solutions_linorder_strict[of a 1 "fst fund_sol" "snd fund_sol"]
       fund_sol_is_nontriv_solution sol
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>solution (a, 1); solution (fst fund_sol, snd fund_sol)\<rbrakk> \<Longrightarrow> (a, 1) = (fst fund_sol, snd fund_sol) \<or> a < fst fund_sol \<and> 1 < snd fund_sol \<or> fst fund_sol < a \<and> snd fund_sol < 1
nontriv_solution fund_sol
nontriv_solution (a, 1)
snd fund_sol \<le> 1
[PROOF STEP]
show "fund_sol = (a, 1)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>solution (a, 1); solution (fst fund_sol, snd fund_sol)\<rbrakk> \<Longrightarrow> (a, 1) = (fst fund_sol, snd fund_sol) \<or> a < fst fund_sol \<and> 1 < snd fund_sol \<or> fst fund_sol < a \<and> snd fund_sol < 1
nontriv_solution fund_sol
nontriv_solution (a, 1)
snd fund_sol \<le> 1

goal (1 subgoal):
 1. fund_sol = (a, 1)
[PROOF STEP]
by (cases fund_sol) (auto simp: nontriv_solution_altdef)
[PROOF STATE]
proof (state)
this:
fund_sol = (a, 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem pell_solutions:
 fixes D :: nat
 assumes "\<nexists>k. D = k\<^sup>2"
 obtains x\<^sub>0 y\<^sub>0 :: nat
 where   "\<forall>(x::int) (y::int).
            x\<^sup>2 - D * y\<^sup>2 = 1 \<longleftrightarrow>
            (\<exists>n::nat. nat \<bar>x\<bar> + sqrt D * nat \<bar>y\<bar> = (x\<^sub>0 + sqrt D * y\<^sub>0) ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x\<^sub>0 y\<^sub>0. \<forall>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real x\<^sub>0 + sqrt (real D) * real y\<^sub>0) ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x\<^sub>0 y\<^sub>0. \<forall>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real x\<^sub>0 + sqrt (real D) * real y\<^sub>0) ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<nexists>k. D = k\<^sup>2
[PROOF STEP]
interpret pell
[PROOF STATE]
proof (prove)
using this:
\<nexists>k. D = k\<^sup>2

goal (1 subgoal):
 1. pell D
[PROOF STEP]
by unfold_locales (auto simp: is_nth_power_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x\<^sub>0 y\<^sub>0. \<forall>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real x\<^sub>0 + sqrt (real D) * real y\<^sub>0) ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule that[of "fst fund_sol" "snd fund_sol"], intro allI, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
case (1 x y)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
have "(x\<^sup>2 - int D * y\<^sup>2 = 1) \<longleftrightarrow> solution (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>2 - int D * y\<^sup>2 = 1) = solution (x, y)
[PROOF STEP]
by (auto simp: solution_def)
[PROOF STATE]
proof (state)
this:
(x\<^sup>2 - int D * y\<^sup>2 = 1) = solution (x, y)

goal (1 subgoal):
 1. \<And>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x\<^sup>2 - int D * y\<^sup>2 = 1) = solution (x, y)

goal (1 subgoal):
 1. \<And>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<exists>n. (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = nth_solution n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (x, y) = (\<exists>n. (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = nth_solution n)
[PROOF STEP]
by (subst solution_iff_nth_solution') blast
[PROOF STATE]
proof (state)
this:
solution (x, y) = (\<exists>n. (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = nth_solution n)

goal (1 subgoal):
 1. \<And>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
solution (x, y) = (\<exists>n. (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = nth_solution n)

goal (1 subgoal):
 1. \<And>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
have "(\<lambda>n. (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = nth_solution n) =
                 (\<lambda>n. pell_valuation (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = pell_valuation (nth_solution n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = nth_solution n) = (\<lambda>n. pell_valuation (case (nat \<bar>x\<bar>, nat \<bar>y\<bar>) of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y)))
[PROOF STEP]
by (subst pell_valuation_eq_iff) (auto simp add: case_prod_unfold prod_eq_iff fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = nth_solution n) = (\<lambda>n. pell_valuation (case (nat \<bar>x\<bar>, nat \<bar>y\<bar>) of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y)))

goal (1 subgoal):
 1. \<And>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = nth_solution n) = (\<lambda>n. pell_valuation (case (nat \<bar>x\<bar>, nat \<bar>y\<bar>) of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y)))

goal (1 subgoal):
 1. \<And>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
have "\<dots> = (\<lambda>n. nat \<bar>x\<bar> + sqrt D * nat \<bar>y\<bar> = (fst fund_sol + sqrt D * snd fund_sol) ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. pell_valuation (case (nat \<bar>x\<bar>, nat \<bar>y\<bar>) of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y))) = (\<lambda>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
by (subst pell_valuation_nth_solution)
         (simp add: pell_valuation_def case_prod_unfold mult_ac)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. pell_valuation (case (nat \<bar>x\<bar>, nat \<bar>y\<bar>) of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case nth_solution n of (x, y) \<Rightarrow> (int x, int y))) = (\<lambda>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)

goal (1 subgoal):
 1. \<And>x y. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)

goal (1 subgoal):
 1. (x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(x\<^sup>2 - int D * y\<^sup>2 = 1) = (\<exists>n. real (nat \<bar>x\<bar>) + sqrt (real D) * real (nat \<bar>y\<bar>) = (real (fst fund_sol) + sqrt (real D) * real (snd fund_sol)) ^ n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hextI: "\<forall>a C S. h a = Some(C,S) \<longrightarrow> (\<exists>S'. h' a = Some(C,S')) \<Longrightarrow> h \<unlhd> h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a C S. h a = \<lfloor>(C, S)\<rfloor> \<longrightarrow> (\<exists>S'. h' a = \<lfloor>(C, S')\<rfloor>) \<Longrightarrow> h \<unlhd> h'
[PROOF STEP]
apply (unfold hext_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a C S. h a = \<lfloor>(C, S)\<rfloor> \<longrightarrow> (\<exists>S'. h' a = \<lfloor>(C, S')\<rfloor>) \<Longrightarrow> \<forall>a C S. h a = \<lfloor>(C, S)\<rfloor> \<longrightarrow> (\<exists>S'. h' a = \<lfloor>(C, S')\<rfloor>)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hext_objD: "\<lbrakk> h \<unlhd> h'; h a = Some(C,S) \<rbrakk> \<Longrightarrow> \<exists>S'. h' a = Some(C,S')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; h a = \<lfloor>(C, S)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>S'. h' a = \<lfloor>(C, S')\<rfloor>
[PROOF STEP]
apply (unfold hext_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a C S. h a = \<lfloor>(C, S)\<rfloor> \<longrightarrow> (\<exists>S'. h' a = \<lfloor>(C, S')\<rfloor>); h a = \<lfloor>(C, S)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>S'. h' a = \<lfloor>(C, S')\<rfloor>
[PROOF STEP]
apply (force)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hext_refl [iff]: "h \<unlhd> h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<unlhd> h
[PROOF STEP]
apply (rule hextI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a C S. h a = \<lfloor>(C, S)\<rfloor> \<longrightarrow> (\<exists>S'. h a = \<lfloor>(C, S')\<rfloor>)
[PROOF STEP]
apply (fast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hext_new [simp]: "h a = None \<Longrightarrow> h \<unlhd> h(a\<mapsto>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h a = None \<Longrightarrow> h \<unlhd> h(a \<mapsto> x)
[PROOF STEP]
apply (rule hextI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h a = None \<Longrightarrow> \<forall>aa C S. h aa = \<lfloor>(C, S)\<rfloor> \<longrightarrow> (\<exists>S'. (h(a \<mapsto> x)) aa = \<lfloor>(C, S')\<rfloor>)
[PROOF STEP]
apply (auto simp:fun_upd_apply)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hext_trans: "\<lbrakk> h \<unlhd> h'; h' \<unlhd> h'' \<rbrakk> \<Longrightarrow> h \<unlhd> h''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; h' \<unlhd> h''\<rbrakk> \<Longrightarrow> h \<unlhd> h''
[PROOF STEP]
apply (rule hextI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; h' \<unlhd> h''\<rbrakk> \<Longrightarrow> \<forall>a C S. h a = \<lfloor>(C, S)\<rfloor> \<longrightarrow> (\<exists>S'. h'' a = \<lfloor>(C, S')\<rfloor>)
[PROOF STEP]
apply (fast dest: hext_objD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hext_upd_obj: "h a = Some (C,S) \<Longrightarrow> h \<unlhd> h(a\<mapsto>(C,S'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h a = \<lfloor>(C, S)\<rfloor> \<Longrightarrow> h \<unlhd> h(a \<mapsto> (C, S'))
[PROOF STEP]
apply (rule hextI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h a = \<lfloor>(C, S)\<rfloor> \<Longrightarrow> \<forall>aa Ca S. h aa = \<lfloor>(Ca, S)\<rfloor> \<longrightarrow> (\<exists>S'a. (h(a \<mapsto> (C, S'))) aa = \<lfloor>(Ca, S'a)\<rfloor>)
[PROOF STEP]
apply (auto simp:fun_upd_apply)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma preallocated_hext:
  "\<lbrakk> preallocated h; h \<unlhd> h' \<rbrakk> \<Longrightarrow> preallocated h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preallocated h; h \<unlhd> h'\<rbrakk> \<Longrightarrow> preallocated h'
[PROOF STEP]
by (simp add: preallocated_def hext_def)


[STATEMENT]
lemma red_hext_incr: "P,E \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow> \<langle>e',(h',l')\<rangle>  \<Longrightarrow> h \<unlhd> h'"
  and reds_hext_incr: "P,E \<turnstile> \<langle>es,(h,l)\<rangle> [\<rightarrow>] \<langle>es',(h',l')\<rangle>  \<Longrightarrow> h \<unlhd> h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle> \<Longrightarrow> h \<unlhd> h') &&& (P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<rightarrow>] \<langle>es',(h', l')\<rangle> \<Longrightarrow> h \<unlhd> h')
[PROOF STEP]
proof(induct rule:red_reds_inducts)
[PROOF STATE]
proof (state)
goal (61 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C)))\<rbrakk> \<Longrightarrow> h \<unlhd> h'
 2. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 4. \<And>E C a b. a \<unlhd> a
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 6. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 9. \<And>E C a b. a \<unlhd> a
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
A total of 61 subgoals...
[PROOF STEP]
case RedNew
[PROOF STATE]
proof (state)
this:
new_Addr h_ = \<lfloor>a_\<rfloor>
h'_ = h_(a_ \<mapsto> (C_, Collect (init_obj P C_)))

goal (61 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C)))\<rbrakk> \<Longrightarrow> h \<unlhd> h'
 2. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 4. \<And>E C a b. a \<unlhd> a
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 6. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 9. \<And>E C a b. a \<unlhd> a
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
A total of 61 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
new_Addr h_ = \<lfloor>a_\<rfloor>
h'_ = h_(a_ \<mapsto> (C_, Collect (init_obj P C_)))

goal (1 subgoal):
 1. h_ \<unlhd> h'_
[PROOF STEP]
by(fastforce dest:new_Addr_SomeD simp:hext_def split:if_splits)
[PROOF STATE]
proof (state)
this:
h_ \<unlhd> h'_

goal (60 subgoals):
 1. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 2. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 3. \<And>E C a b. a \<unlhd> a
 4. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 5. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
 6. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 7. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 8. \<And>E C a b. a \<unlhd> a
 9. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 10. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
A total of 60 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (60 subgoals):
 1. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 2. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 3. \<And>E C a b. a \<unlhd> a
 4. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 5. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
 6. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 7. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 8. \<And>E C a b. a \<unlhd> a
 9. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 10. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
A total of 60 subgoals...
[PROOF STEP]
case RedFAss
[PROOF STATE]
proof (state)
this:
h_ a_ = \<lfloor>(D_, S_)\<rfloor>
P \<turnstile> last Cs'_ has least F_:T_ via Cs_
P \<turnstile> T_ casts v_ to v'_
Ds_ = Cs'_ @\<^sub>p Cs_
(Ds_, fs_) \<in> S_

goal (60 subgoals):
 1. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 2. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 3. \<And>E C a b. a \<unlhd> a
 4. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 5. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
 6. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 7. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 8. \<And>E C a b. a \<unlhd> a
 9. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 10. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
A total of 60 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
h_ a_ = \<lfloor>(D_, S_)\<rfloor>
P \<turnstile> last Cs'_ has least F_:T_ via Cs_
P \<turnstile> T_ casts v_ to v'_
Ds_ = Cs'_ @\<^sub>p Cs_
(Ds_, fs_) \<in> S_

goal (1 subgoal):
 1. h_ \<unlhd> h_(a_ \<mapsto> (D_, insert (Ds_, fs_(F_ \<mapsto> v'_)) (S_ - {(Ds_, fs_)})))
[PROOF STEP]
by(simp add:hext_def split:if_splits)
[PROOF STATE]
proof (state)
this:
h_ \<unlhd> h_(a_ \<mapsto> (D_, insert (Ds_, fs_(F_ \<mapsto> v'_)) (S_ - {(Ds_, fs_)})))

goal (59 subgoals):
 1. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 2. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 3. \<And>E C a b. a \<unlhd> a
 4. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 5. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
 6. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 7. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 8. \<And>E C a b. a \<unlhd> a
 9. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> aa \<unlhd> aa
 10. \<And>E C a Cs Cs' aa b. aa \<unlhd> aa
A total of 59 subgoals...
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma step_hext_incr: "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>  \<Longrightarrow> hp s \<unlhd> hp s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle> \<Longrightarrow> hp s \<unlhd> hp s'
[PROOF STEP]
proof(induct rule:converse_rtrancl_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hp s' \<unlhd> hp s'
 2. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. hp s' \<unlhd> hp s'
 2. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hp s' \<unlhd> hp s'
[PROOF STEP]
by(rule hext_refl)
[PROOF STATE]
proof (state)
this:
hp s' \<unlhd> hp s'

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
case (step e s e'' s'')
[PROOF STATE]
proof (state)
this:
((e, s), e'', s'') \<in> Red P E
P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
hp s'' \<unlhd> hp s'

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
have Red:"((e, s), e'', s'') \<in> Red P E"
    and hext:"hp s'' \<unlhd> hp s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((e, s), e'', s'') \<in> Red P E &&& hp s'' \<unlhd> hp s'
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
((e, s), e'', s'') \<in> Red P E
hp s'' \<unlhd> hp s'

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
from Red
[PROOF STATE]
proof (chain)
picking this:
((e, s), e'', s'') \<in> Red P E
[PROOF STEP]
have "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
((e, s), e'', s'') \<in> Red P E

goal (1 subgoal):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
hence "hp s \<unlhd> hp s''"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>

goal (1 subgoal):
 1. hp s \<unlhd> hp s''
[PROOF STEP]
by(cases s,cases s'')(auto dest:red_hext_incr)
[PROOF STATE]
proof (state)
this:
hp s \<unlhd> hp s''

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
with hext
[PROOF STATE]
proof (chain)
picking this:
hp s'' \<unlhd> hp s'
hp s \<unlhd> hp s''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hp s'' \<unlhd> hp s'
hp s \<unlhd> hp s''

goal (1 subgoal):
 1. hp s \<unlhd> hp s'
[PROOF STEP]
by-(rule hext_trans)
[PROOF STATE]
proof (state)
this:
hp s \<unlhd> hp s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma steps_hext_incr: "P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>  \<Longrightarrow> hp s \<unlhd> hp s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle> \<Longrightarrow> hp s \<unlhd> hp s'
[PROOF STEP]
proof(induct rule:converse_rtrancl_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hp s' \<unlhd> hp s'
 2. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. hp s' \<unlhd> hp s'
 2. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hp s' \<unlhd> hp s'
[PROOF STEP]
by(rule hext_refl)
[PROOF STATE]
proof (state)
this:
hp s' \<unlhd> hp s'

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
case (step es s es'' s'')
[PROOF STATE]
proof (state)
this:
((es, s), es'', s'') \<in> Reds P E
P,E \<turnstile> \<langle>es'',s''\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>
hp s'' \<unlhd> hp s'

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
have Reds:"((es, s), es'', s'') \<in> Reds P E"
    and hext:"hp s'' \<unlhd> hp s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((es, s), es'', s'') \<in> Reds P E &&& hp s'' \<unlhd> hp s'
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
((es, s), es'', s'') \<in> Reds P E
hp s'' \<unlhd> hp s'

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
from Reds
[PROOF STATE]
proof (chain)
picking this:
((es, s), es'', s'') \<in> Reds P E
[PROOF STEP]
have "P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
((es, s), es'', s'') \<in> Reds P E

goal (1 subgoal):
 1. P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
hence "hp s \<unlhd> hp s''"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>

goal (1 subgoal):
 1. hp s \<unlhd> hp s''
[PROOF STEP]
by(cases s,cases s'',auto dest:reds_hext_incr)
[PROOF STATE]
proof (state)
this:
hp s \<unlhd> hp s''

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; hp ba \<unlhd> hp s'\<rbrakk> \<Longrightarrow> hp b \<unlhd> hp s'
[PROOF STEP]
with hext
[PROOF STATE]
proof (chain)
picking this:
hp s'' \<unlhd> hp s'
hp s \<unlhd> hp s''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hp s'' \<unlhd> hp s'
hp s \<unlhd> hp s''

goal (1 subgoal):
 1. hp s \<unlhd> hp s'
[PROOF STEP]
by-(rule hext_trans)
[PROOF STATE]
proof (state)
this:
hp s \<unlhd> hp s'

goal:
No subgoals!
[PROOF STEP]
qed