[STATEMENT]
lemma valid_cert_Cons2 [code]:
  "valid_cert (Triple p a x # xs) \<longleftrightarrow> x > 0 \<and> p > 1 \<and> (x = 1 \<or> (
     (\<exists>t\<in>set xs. case t of Prime _ \<Rightarrow> False |
        Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and>
        (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p-1) div q) p \<noteq> 1)))) \<and> valid_cert xs"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_cert (Triple p a x # xs) = (0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. valid_cert (Triple p a x # xs) \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
 2. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
valid_cert (Triple p a x # xs)

goal (2 subgoals):
 1. valid_cert (Triple p a x # xs) \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
 2. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
from \<open>?lhs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_cert (Triple p a x # xs)
[PROOF STEP]
have pos: "x > 0" and gt_1: "p > 1" and valid: "valid_cert xs"
[PROOF STATE]
proof (prove)
using this:
valid_cert (Triple p a x # xs)

goal (1 subgoal):
 1. 0 < x &&& 1 < p &&& valid_cert xs
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < x
1 < p
valid_cert xs

goal (2 subgoals):
 1. valid_cert (Triple p a x # xs) \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
 2. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
proof (cases "x = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
 2. x \<noteq> 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 1

goal (2 subgoals):
 1. x = 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
 2. x \<noteq> 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
with \<open>?lhs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_cert (Triple p a x # xs)
x = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_cert (Triple p a x # xs)
x = 1

goal (1 subgoal):
 1. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 1

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
with \<open>?lhs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_cert (Triple p a x # xs)
x \<noteq> 1
[PROOF STEP]
have "(\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs
      \<and> [a^((p - 1) div q) \<noteq> 1] (mod p))"
[PROOF STATE]
proof (prove)
using this:
valid_cert (Triple p a x # xs)
x \<noteq> 1

goal (1 subgoal):
 1. \<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)
[PROOF STEP]
obtain q y where qy:
      "x = q * y"
      "Prime q \<in> set xs"
      "Triple p a y \<in> set xs"
      "[a ^ ((p - 1) div q) \<noteq> 1] (mod p)"
[PROOF STATE]
proof (prove)
using this:
\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. (\<And>q y. \<lbrakk>x = q * y; Prime q \<in> set xs; Triple p a y \<in> set xs; [a ^ ((p - 1) div q) \<noteq> 1] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = q * y
Prime q \<in> set xs
Triple p a y \<in> set xs
[a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
hence "(\<exists>t\<in>set xs. case t of Prime _ \<Rightarrow> False |
        Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and>
        (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p-1) div q) p \<noteq> 1))"
[PROOF STATE]
proof (prove)
using this:
x = q * y
Prime q \<in> set xs
Triple p a y \<in> set xs
[a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. \<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)
[PROOF STEP]
using pos gt_1
[PROOF STATE]
proof (prove)
using this:
x = q * y
Prime q \<in> set xs
Triple p a y \<in> set xs
[a ^ ((p - 1) div q) \<noteq> 1] (mod p)
0 < x
1 < p

goal (1 subgoal):
 1. \<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)
[PROOF STEP]
by (intro bexI [of _ "Triple p a y"])
      (auto simp: Suc_0_mod_eq_Suc_0_iff Suc_0_eq_Suc_0_mod_iff cong_def mod_exp_nat_def)
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
with pos gt_1 valid
[PROOF STATE]
proof (chain)
picking this:
0 < x
1 < p
valid_cert xs
\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x
1 < p
valid_cert xs
\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)

goal (1 subgoal):
 1. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs

goal (1 subgoal):
 1. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs

goal (1 subgoal):
 1. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
hence pos: "x > 0" and gt_1: "p > 1" and valid: "valid_cert xs"
[PROOF STATE]
proof (prove)
using this:
0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs

goal (1 subgoal):
 1. 0 < x &&& 1 < p &&& valid_cert xs
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < x
1 < p
valid_cert xs

goal (1 subgoal):
 1. 0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_cert (Triple p a x # xs)
[PROOF STEP]
proof (cases "x = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
 2. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 1

goal (2 subgoals):
 1. x = 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
 2. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
with \<open>?rhs\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
x = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
x = 1

goal (1 subgoal):
 1. valid_cert (Triple p a x # xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_cert (Triple p a x # xs)

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 1

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
with \<open>?rhs\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
x \<noteq> 1
[PROOF STEP]
obtain t where t: "t \<in> set xs" "case t of Prime x \<Rightarrow> False
         | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y
              in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)"
[PROOF STATE]
proof (prove)
using this:
0 < x \<and> 1 < p \<and> (x = 1 \<or> (\<exists>t\<in>set xs. case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1))) \<and> valid_cert xs
x \<noteq> 1

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> set xs; case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> set xs
case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> set xs
case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)
[PROOF STEP]
obtain y where y: "t = Triple p a y" "y dvd x" "let q = x div y in Prime q \<in> set xs \<and>
                              mod_exp_nat a ((p - 1) div q) p \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
t \<in> set xs
case t of Prime x \<Rightarrow> False | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>t = Triple p a y; y dvd x; let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases t rule: pratt.exhaust) auto
[PROOF STATE]
proof (state)
this:
t = Triple p a y
y dvd x
let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
with gt_1
[PROOF STATE]
proof (chain)
picking this:
1 < p
t = Triple p a y
y dvd x
let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1
[PROOF STEP]
have y': "let q = x div y in Prime q \<in> set xs \<and> [a^((p - 1) div q) \<noteq> 1] (mod p)"
[PROOF STATE]
proof (prove)
using this:
1 < p
t = Triple p a y
y dvd x
let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1

goal (1 subgoal):
 1. let q = x div y in Prime q \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)
[PROOF STEP]
by (auto simp: cong_def Let_def mod_exp_nat_def Suc_0_mod_eq_Suc_0_iff Suc_0_eq_Suc_0_mod_iff)
[PROOF STATE]
proof (state)
this:
let q = x div y in Prime q \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
define q where "q = x div y"
[PROOF STATE]
proof (state)
this:
q = x div y

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
have "\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs
                     \<and> [a^((p - 1) div q) \<noteq> 1] (mod p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)
[PROOF STEP]
by (rule exI[of _ q], rule exI[of _ y]) (insert t y y', auto simp: Let_def q_def)
[PROOF STATE]
proof (state)
this:
\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. x \<noteq> 1 \<Longrightarrow> valid_cert (Triple p a x # xs)
[PROOF STEP]
with pos gt_1 valid
[PROOF STATE]
proof (chain)
picking this:
0 < x
1 < p
valid_cert xs
\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x
1 < p
valid_cert xs
\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs \<and> [a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. valid_cert (Triple p a x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_cert (Triple p a x # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_cert (Triple p a x # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gfp_little_fusion:
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
  and g :: "'b::complete_lattice \<Rightarrow> 'b"
  assumes "mono f"
  assumes "h \<circ> f \<le> g \<circ> h"
  shows "h (gfp f) \<le> gfp g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h (gfp f) \<le> gfp g
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h (gfp f) \<le> gfp g
[PROOF STEP]
have "h (f (gfp f)) \<le> g (h (gfp f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h (f (gfp f)) \<le> g (h (gfp f))
[PROOF STEP]
using assms(2) le_funD
[PROOF STATE]
proof (prove)
using this:
h \<circ> f \<le> g \<circ> h
?f \<le> ?g \<Longrightarrow> ?f ?x \<le> ?g ?x

goal (1 subgoal):
 1. h (f (gfp f)) \<le> g (h (gfp f))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
h (f (gfp f)) \<le> g (h (gfp f))

goal (1 subgoal):
 1. h (gfp f) \<le> gfp g
[PROOF STEP]
hence "h (gfp f) \<le> g (h (gfp f))"
[PROOF STATE]
proof (prove)
using this:
h (f (gfp f)) \<le> g (h (gfp f))

goal (1 subgoal):
 1. h (gfp f) \<le> g (h (gfp f))
[PROOF STEP]
by (simp add: assms(1) gfp_fixpoint)
[PROOF STATE]
proof (state)
this:
h (gfp f) \<le> g (h (gfp f))

goal (1 subgoal):
 1. h (gfp f) \<le> gfp g
[PROOF STEP]
thus "h (gfp f) \<le> gfp g"
[PROOF STATE]
proof (prove)
using this:
h (gfp f) \<le> g (h (gfp f))

goal (1 subgoal):
 1. h (gfp f) \<le> gfp g
[PROOF STEP]
by (simp add: gfp_upperbound)
[PROOF STATE]
proof (state)
this:
h (gfp f) \<le> gfp g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lalternate_finite_helper: (* The other direction is proved later, added as SIMP rule *)
  assumes "lfinite (lalternate xs)"
  shows "lfinite xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lfinite (lalternate xs)

goal (1 subgoal):
 1. lfinite xs
[PROOF STEP]
proof(induct "lalternate xs" arbitrary:xs rule:lfinite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. lnull (lalternate xs) \<Longrightarrow> lfinite xs
 2. \<And>xs. \<lbrakk>lfinite (lalternate xs); \<not> lnull (lalternate xs); \<And>xsa. ltl (lalternate xs) = lalternate xsa \<Longrightarrow> lfinite xsa\<rbrakk> \<Longrightarrow> lfinite xs
[PROOF STEP]
case LNil
[PROOF STATE]
proof (state)
this:
lnull (lalternate xs)

goal (2 subgoals):
 1. \<And>xs. lnull (lalternate xs) \<Longrightarrow> lfinite xs
 2. \<And>xs. \<lbrakk>lfinite (lalternate xs); \<not> lnull (lalternate xs); \<And>xsa. ltl (lalternate xs) = lalternate xsa \<Longrightarrow> lfinite xsa\<rbrakk> \<Longrightarrow> lfinite xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lnull (lalternate xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lnull (lalternate xs)

goal (1 subgoal):
 1. lfinite xs
[PROOF STEP]
unfolding lalternate.code[of xs]
[PROOF STATE]
proof (prove)
using this:
lnull (case xs of LNil \<Rightarrow> LNil | LCons x xs \<Rightarrow> LCons x (lalternate (ltl xs)))

goal (1 subgoal):
 1. lfinite xs
[PROOF STEP]
by(cases xs;auto)
[PROOF STATE]
proof (state)
this:
lfinite xs

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>lfinite (lalternate xs); \<not> lnull (lalternate xs); \<And>xsa. ltl (lalternate xs) = lalternate xsa \<Longrightarrow> lfinite xsa\<rbrakk> \<Longrightarrow> lfinite xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>lfinite (lalternate xs); \<not> lnull (lalternate xs); \<And>xsa. ltl (lalternate xs) = lalternate xsa \<Longrightarrow> lfinite xsa\<rbrakk> \<Longrightarrow> lfinite xs
[PROOF STEP]
case (LCons xs)
[PROOF STATE]
proof (state)
this:
lfinite (lalternate xs)
\<not> lnull (lalternate xs)
ltl (lalternate xs) = lalternate ?xs \<Longrightarrow> lfinite ?xs

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>lfinite (lalternate xs); \<not> lnull (lalternate xs); \<And>xsa. ltl (lalternate xs) = lalternate xsa \<Longrightarrow> lfinite xsa\<rbrakk> \<Longrightarrow> lfinite xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lfinite (lalternate xs)
\<not> lnull (lalternate xs)
ltl (lalternate xs) = lalternate ?xs \<Longrightarrow> lfinite ?xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lfinite (lalternate xs)
\<not> lnull (lalternate xs)
ltl (lalternate xs) = lalternate ?xs \<Longrightarrow> lfinite ?xs

goal (1 subgoal):
 1. lfinite xs
[PROOF STEP]
unfolding lalternate.code[of xs]
[PROOF STATE]
proof (prove)
using this:
lfinite (case xs of LNil \<Rightarrow> LNil | LCons x xs \<Rightarrow> LCons x (lalternate (ltl xs)))
\<not> lnull (case xs of LNil \<Rightarrow> LNil | LCons x xs \<Rightarrow> LCons x (lalternate (ltl xs)))
ltl (case xs of LNil \<Rightarrow> LNil | LCons x xs \<Rightarrow> LCons x (lalternate (ltl xs))) = lalternate ?xs \<Longrightarrow> lfinite ?xs

goal (1 subgoal):
 1. lfinite xs
[PROOF STEP]
by(cases "xs";cases "ltl xs";auto)
[PROOF STATE]
proof (state)
this:
lfinite xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_within_upper_squarefree:
  assumes "rsquarefree p"
  shows  "card (proots_within p {x. Im x >0}) = (let
            pp = smult (inverse (lead_coeff p)) p;
            pI = map_poly Im pp;
            pR = map_poly Re pp;
            g = gcd pR pI
        in
            nat ((degree p - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2)
      )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
define pp where "pp = smult (inverse (lead_coeff p)) p"
[PROOF STATE]
proof (state)
this:
pp = smult (inverse (lead_coeff p)) p

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
define pI where "pI = map_poly Im pp"
[PROOF STATE]
proof (state)
this:
pI = map_poly Im pp

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
define pR where "pR = map_poly Re pp"
[PROOF STATE]
proof (state)
this:
pR = map_poly Re pp

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
define g where  "g = gcd pR pI"
[PROOF STATE]
proof (state)
this:
g = gcd pR pI

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
have "card (proots_within p {x. Im x >0}) = proots_upper p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = proots_upper p
[PROOF STEP]
unfolding proots_upper_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = proots_count p {z. 0 < Im z}
[PROOF STEP]
using card_proots_within_rsquarefree[OF assms]
[PROOF STATE]
proof (prove)
using this:
proots_count p ?s = card (proots_within p ?s)

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = proots_count p {z. 0 < Im z}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (proots_within p {x. 0 < Im x}) = proots_upper p

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (proots_within p {x. 0 < Im x}) = proots_upper p

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
have "... = proots_upper pp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_upper p = proots_upper pp
[PROOF STEP]
unfolding proots_upper_def pp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p {z. 0 < Im z} = proots_count (smult (inverse (lead_coeff p)) p) {z. 0 < Im z}
[PROOF STEP]
apply (subst proots_count_smult)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inverse (lead_coeff p) \<noteq> 0
 2. proots_count p {z. 0 < Im z} = proots_count p {z. 0 < Im z}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rsquarefree p

goal (2 subgoals):
 1. inverse (lead_coeff p) \<noteq> 0
 2. proots_count p {z. 0 < Im z} = proots_count p {z. 0 < Im z}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_upper p = proots_upper pp

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proots_upper p = proots_upper pp

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
have "... = (degree pp - proots_count pp {x. Im x = 0} - cindex_poly_ubd pI pR) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
define rr where "rr = proots_count pp {x. Im x = 0}"
[PROOF STATE]
proof (state)
this:
rr = proots_count pp {x. Im x = 0}

goal (1 subgoal):
 1. int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
define cpp where "cpp = cindex_poly_ubd pI pR"
[PROOF STATE]
proof (state)
this:
cpp = cindex_poly_ubd pI pR

goal (1 subgoal):
 1. int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
have *:"proots_upper pp = (degree pp - rr - cpp) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (proots_upper pp) = real_of_int (int (degree pp - rr) - cpp) / 2
[PROOF STEP]
apply (rule proots_upper_cindex_eq'[of pp,folded rr_def cpp_def pR_def pI_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monic pp
[PROOF STEP]
unfolding pp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monic (smult (inverse (lead_coeff p)) p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rsquarefree p

goal (1 subgoal):
 1. monic (smult (inverse (lead_coeff p)) p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (proots_upper pp) = real_of_int (int (degree pp - rr) - cpp) / 2

goal (1 subgoal):
 1. int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (proots_upper pp) = real_of_int (int (degree pp - rr) - cpp) / 2

goal (1 subgoal):
 1. int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
have "... = (degree pp - rr - cpp) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (int (degree pp - rr) - cpp) / 2 = real_of_int ((int (degree pp - rr) - cpp) div 2)
[PROOF STEP]
proof (subst real_of_int_div)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. even (int (degree pp - rr) - cpp)
 2. real_of_int (int (degree pp - rr) - cpp) / 2 = real_of_int (int (degree pp - rr) - cpp) / real_of_int 2
[PROOF STEP]
define tt where "tt=int (degree pp - rr) - cpp"
[PROOF STATE]
proof (state)
this:
tt = int (degree pp - rr) - cpp

goal (2 subgoals):
 1. even (int (degree pp - rr) - cpp)
 2. real_of_int (int (degree pp - rr) - cpp) / 2 = real_of_int (int (degree pp - rr) - cpp) / real_of_int 2
[PROOF STEP]
have "real_of_int tt=2*proots_upper pp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int tt = real (2 * proots_upper pp)
[PROOF STEP]
by (simp add:*[folded tt_def])
[PROOF STATE]
proof (state)
this:
real_of_int tt = real (2 * proots_upper pp)

goal (2 subgoals):
 1. even (int (degree pp - rr) - cpp)
 2. real_of_int (int (degree pp - rr) - cpp) / 2 = real_of_int (int (degree pp - rr) - cpp) / real_of_int 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int tt = real (2 * proots_upper pp)
[PROOF STEP]
show "even tt"
[PROOF STATE]
proof (prove)
using this:
real_of_int tt = real (2 * proots_upper pp)

goal (1 subgoal):
 1. even tt
[PROOF STEP]
by (metis dvd_triv_left even_of_nat of_int_eq_iff of_int_of_nat_eq)
[PROOF STATE]
proof (state)
this:
even tt

goal (1 subgoal):
 1. real_of_int (int (degree pp - rr) - cpp) / 2 = real_of_int (int (degree pp - rr) - cpp) / real_of_int 2
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
real_of_int (int (degree pp - rr) - cpp) / 2 = real_of_int ((int (degree pp - rr) - cpp) div 2)

goal (1 subgoal):
 1. int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (proots_upper pp) = real_of_int ((int (degree pp - rr) - cpp) div 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real (proots_upper pp) = real_of_int ((int (degree pp - rr) - cpp) div 2)

goal (1 subgoal):
 1. int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
unfolding rr_def cpp_def
[PROOF STATE]
proof (prove)
using this:
real (proots_upper pp) = real_of_int ((int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2)

goal (1 subgoal):
 1. int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (proots_upper pp) = (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
have "... = (degree pp - changes_R_smods g (pderiv g)
                        - cindex_poly_ubd pI pR) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
have "rsquarefree pp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rsquarefree pp
[PROOF STEP]
using assms rsquarefree_smult_iff
[PROOF STATE]
proof (prove)
using this:
rsquarefree p
?s \<noteq> (0::?'a) \<Longrightarrow> rsquarefree (smult ?s ?p) = rsquarefree ?p

goal (1 subgoal):
 1. rsquarefree pp
[PROOF STEP]
unfolding pp_def
[PROOF STATE]
proof (prove)
using this:
rsquarefree p
?s \<noteq> (0::?'a) \<Longrightarrow> rsquarefree (smult ?s ?p) = rsquarefree ?p

goal (1 subgoal):
 1. rsquarefree (smult (inverse (lead_coeff p)) p)
[PROOF STEP]
by (metis inverse_eq_imp_eq inverse_zero leading_coeff_neq_0 rsquarefree_0)
[PROOF STATE]
proof (state)
this:
rsquarefree pp

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
from card_proots_within_rsquarefree[OF this]
[PROOF STATE]
proof (chain)
picking this:
proots_count pp ?s = card (proots_within pp ?s)
[PROOF STEP]
have "proots_count pp {x. Im x = 0} = card (proots_within pp {x. Im x = 0})"
[PROOF STATE]
proof (prove)
using this:
proots_count pp ?s = card (proots_within pp ?s)

goal (1 subgoal):
 1. proots_count pp {x. Im x = 0} = card (proots_within pp {x. Im x = 0})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proots_count pp {x. Im x = 0} = card (proots_within pp {x. Im x = 0})

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proots_count pp {x. Im x = 0} = card (proots_within pp {x. Im x = 0})

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
have "... = card (proots_within pp (unbounded_line 0 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within pp {x. Im x = 0}) = card (proots_within pp (unbounded_line 0 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (proots_within pp {x. Im x = 0}) = card (proots_within pp (unbounded_line 0 1))
[PROOF STEP]
have "{x. Im x = 0} = unbounded_line 0 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. Im x = 0} = unbounded_line 0 1
[PROOF STEP]
unfolding unbounded_line_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. Im x = 0} = {x. \<exists>u. x = (1 - u) *\<^sub>R 0 + u *\<^sub>R 1}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Im x = 0 \<Longrightarrow> \<exists>u. x = u *\<^sub>R 1
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x = 0 \<Longrightarrow> \<exists>u. x = u *\<^sub>R 1
[PROOF STEP]
apply (rule_tac x="Re x" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x = 0 \<Longrightarrow> x = Re x *\<^sub>R 1
[PROOF STEP]
by (metis complex_is_Real_iff of_real_Re of_real_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{x. Im x = 0} = unbounded_line 0 1

goal (1 subgoal):
 1. card (proots_within pp {x. Im x = 0}) = card (proots_within pp (unbounded_line 0 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{x. Im x = 0} = unbounded_line 0 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{x. Im x = 0} = unbounded_line 0 1

goal (1 subgoal):
 1. card (proots_within pp {x. Im x = 0}) = card (proots_within pp (unbounded_line 0 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (proots_within pp {x. Im x = 0}) = card (proots_within pp (unbounded_line 0 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (proots_within pp {x. Im x = 0}) = card (proots_within pp (unbounded_line 0 1))

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (proots_within pp {x. Im x = 0}) = card (proots_within pp (unbounded_line 0 1))

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
have "... = changes_R_smods g (pderiv g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (card (proots_within pp (unbounded_line 0 1))) = changes_R_smods g (pderiv g)
[PROOF STEP]
unfolding card_proots_unbounded_line[of 0 1 pp,simplified,folded pI_def pR_def] g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (let g = gcd pR pI in nat (changes_R_smods g (pderiv g))) = changes_R_smods (gcd pR pI) (pderiv (gcd pR pI))
[PROOF STEP]
by (auto simp add:Let_def sturm_R[symmetric])
[PROOF STATE]
proof (state)
this:
int (card (proots_within pp (unbounded_line 0 1))) = changes_R_smods g (pderiv g)

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (proots_count pp {x. Im x = 0}) = changes_R_smods g (pderiv g)
[PROOF STEP]
have "proots_count pp {x. Im x = 0} = changes_R_smods g (pderiv g)"
[PROOF STATE]
proof (prove)
using this:
int (proots_count pp {x. Im x = 0}) = changes_R_smods g (pderiv g)

goal (1 subgoal):
 1. int (proots_count pp {x. Im x = 0}) = changes_R_smods g (pderiv g)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (proots_count pp {x. Im x = 0}) = changes_R_smods g (pderiv g)

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
int (proots_count pp {x. Im x = 0}) = changes_R_smods g (pderiv g)

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
have "degree pp \<ge> proots_count pp {x. Im x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count pp {x. Im x = 0} \<le> degree pp
[PROOF STEP]
by (metis \<open>rsquarefree pp\<close> proots_count_leq_degree rsquarefree_0)
[PROOF STATE]
proof (state)
this:
proots_count pp {x. Im x = 0} \<le> degree pp

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
int (proots_count pp {x. Im x = 0}) = changes_R_smods g (pderiv g)
proots_count pp {x. Im x = 0} \<le> degree pp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
int (proots_count pp {x. Im x = 0}) = changes_R_smods g (pderiv g)
proots_count pp {x. Im x = 0} \<le> degree pp

goal (1 subgoal):
 1. (int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(int (degree pp - proots_count pp {x. Im x = 0}) - cindex_poly_ubd pI pR) div 2 = (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
have "... = (degree p - changes_R_smods g (pderiv g)
                        - changes_R_smods pR pI) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2 = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2
[PROOF STEP]
using cindex_poly_ubd_code
[PROOF STATE]
proof (prove)
using this:
cindex_poly_ubd ?q ?p = changes_R_smods ?p ?q

goal (1 subgoal):
 1. (int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2 = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2
[PROOF STEP]
unfolding pp_def
[PROOF STATE]
proof (prove)
using this:
cindex_poly_ubd ?q ?p = changes_R_smods ?p ?q

goal (1 subgoal):
 1. (int (degree (smult (inverse (lead_coeff p)) p)) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2 = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(int (degree pp) - changes_R_smods g (pderiv g) - cindex_poly_ubd pI pR) div 2 = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (card (proots_within p {x. 0 < Im x})) = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2
[PROOF STEP]
have "card (proots_within p {x. 0 < Im x}) = (degree p - changes_R_smods g (pderiv g) -
                  changes_R_smods pR pI) div 2"
[PROOF STATE]
proof (prove)
using this:
int (card (proots_within p {x. 0 < Im x})) = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2

goal (1 subgoal):
 1. int (card (proots_within p {x. 0 < Im x})) = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (card (proots_within p {x. 0 < Im x})) = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int (card (proots_within p {x. 0 < Im x})) = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
int (card (proots_within p {x. 0 < Im x})) = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
using this:
int (card (proots_within p {x. 0 < Im x})) = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2

goal (1 subgoal):
 1. card (proots_within p {x. 0 < Im x}) = nat ((int (degree p) - changes_R_smods (gcd (map_poly Re (smult (inverse (lead_coeff p)) p)) (map_poly Im (smult (inverse (lead_coeff p)) p))) (pderiv (gcd (map_poly Re (smult (inverse (lead_coeff p)) p)) (map_poly Im (smult (inverse (lead_coeff p)) p)))) - changes_R_smods (map_poly Re (smult (inverse (lead_coeff p)) p)) (map_poly Im (smult (inverse (lead_coeff p)) p))) div 2)
[PROOF STEP]
apply (fold pp_def pR_def pI_def g_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (card (proots_within p {x. 0 < Im x})) = (int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2 \<Longrightarrow> card (proots_within p {x. 0 < Im x}) = nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2)
[PROOF STEP]
by (simp add: pp_def)
[PROOF STATE]
proof (state)
this:
card (proots_within p {x. 0 < Im x}) = (let pp = smult (inverse (lead_coeff p)) p; pI = map_poly Im pp; pR = map_poly Re pp; g = gcd pR pI in nat ((int (degree p) - changes_R_smods g (pderiv g) - changes_R_smods pR pI) div 2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  "\<lfloor>\<^bold>\<forall>A .(\<^bold>\<box>((\<^bold>\<forall>\<phi>.((A \<phi>) \<^bold>\<rightarrow>  (\<P> \<phi>))) \<^bold>\<rightarrow> (\<P> (\<Delta> A))))\<rfloor> \<equiv> \<lfloor>\<^bold>\<forall>\<Z>.((\<P>\<o>\<s> \<Z>) \<^bold>\<rightarrow> (\<^bold>\<forall>X.((X\<Sqinter>\<^sup>p\<Z>) \<^bold>\<rightarrow> (\<P> X))))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (\<^bold>\<box>(\<lambda>v. (\<forall>xa. (xa\<^bold>\<in>x \<^bold>\<rightarrow> xa\<^bold>\<in>\<P>) v) \<longrightarrow> \<lambda>xa w. \<forall>xb. (xb\<^bold>\<in>x \<^bold>\<rightarrow> xb xa) w\<^bold>\<in>\<P> v)) w\<rfloor> \<equiv> \<lfloor>\<lambda>w. \<forall>x. (\<forall>xa. (xa\<^bold>\<in>x \<^bold>\<rightarrow> xa\<^bold>\<in>\<P>) w) \<longrightarrow> (\<forall>xa. (\<^bold>\<box>(\<lambda>v. \<forall>xb. xa xb v = (\<forall>xa. (xa\<^bold>\<in>x \<^bold>\<rightarrow> xa xb) v)) \<^bold>\<rightarrow> xa\<^bold>\<in>\<P>) w)\<rfloor>
[PROOF STEP]
by (smt (verit, ccfv_threshold) Axiom1 axM') \<comment>\<open>proof found\<close>


[STATEMENT]
lemma atCs_empty:
  "atCs cs = {} \<longleftrightarrow> cs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atCs cs = {}) = (cs = [])
[PROOF STEP]
by (induct cs) (auto simp: atC_not_empty)


[STATEMENT]
lemma ctxt_inj:
  assumes "(E, fctxt) \<in> ctxt"
  assumes "E x = E y"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(E, fctxt) \<in> ctxt
E x = E y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (induct set: ctxt) auto


[STATEMENT]
lemma min_eds_Nil: "min_eds [] ys = map Ins ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_eds [] ys = map Ins ys
[PROOF STEP]
by (induction ys) auto


[STATEMENT]
lemma execute'_correct:
      assumes V: "s\<in>valid_states"
      assumes "enabled name s"      (* Intentionally put this here, also we could resolve non-enabled case by reflexivity (undefined=undefined) *)
      shows "execute' problem name s = execute name s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute' problem name s = execute name s
[PROOF STEP]
unfolding execute'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case lookup_operator' problem name of Some \<pi> \<Rightarrow> execute_opr' \<pi> s) = execute name s
[PROOF STEP]
using execute_opr'_correct[OF V] \<open>enabled name s\<close>
[PROOF STATE]
proof (prove)
using this:
lookup_operator ?name = Some ?\<pi> \<Longrightarrow> execute_opr' ?\<pi> s = execute ?name s
enabled name s

goal (1 subgoal):
 1. (case lookup_operator' problem name of Some \<pi> \<Rightarrow> execute_opr' \<pi> s) = execute name s
[PROOF STEP]
by (auto split: option.splits simp: enabled_def lookup_operator'_correct)


[STATEMENT]
lemma get_document_ptr_simp [simp]:
  "get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)
     = (if ptr = cast document_ptr then cast obj else get document_ptr h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get document_ptr (put ptr obj h) = (if ptr = cast document_ptr then cast obj else get document_ptr h)
[PROOF STEP]
by(auto simp add: get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def split: option.splits Option.bind_splits)


[STATEMENT]
lemma new_character_data_is_l_new_character_data [instances]:
  "l_new_character_data type_wf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_new_character_data DocumentClass.type_wf
[PROOF STEP]
using l_new_character_data.intro new_character_data_type_wf_preserved
[PROOF STATE]
proof (prove)
using this:
(\<And>h h'. h \<turnstile> new_character_data \<rightarrow>\<^sub>h h' \<Longrightarrow> ?type_wf h = ?type_wf h') \<Longrightarrow> l_new_character_data ?type_wf
?h \<turnstile> new_character_data \<rightarrow>\<^sub>h ?h' \<Longrightarrow> DocumentClass.type_wf ?h = DocumentClass.type_wf ?h'

goal (1 subgoal):
 1. l_new_character_data DocumentClass.type_wf
[PROOF STEP]
by blast


[STATEMENT]
lemma ord0_less_imp_le: "(x::ord0) < y \<Longrightarrow> x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> x \<le> y
[PROOF STEP]
by (rule ord0_leI[rule_format], rule ord0_less_trans)


[STATEMENT]
lemma fds_converges_norm_iff':
  fixes f :: "'a :: {nat_power_normed_field,banach} fds"
  shows "fds_converges (fds_norm f) s \<longleftrightarrow> fds_abs_converges f (of_real s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_converges (fds_norm f) s = fds_abs_converges f (of_real s)
[PROOF STEP]
unfolding fds_converges_def fds_abs_converges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. fds_nth (fds_norm f) n / nat_power n s) = summable (\<lambda>n. norm (fds_nth f n / nat_power n (of_real s)))
[PROOF STEP]
by (rule summable_cong [OF eventually_mono[OF eventually_gt_at_top[of 0]]])
     (simp add: fds_abs_converges_def fds_norm_def fds_nth_fds' norm_divide norm_nat_power)


[STATEMENT]
lemma seq_extract_empty [simp]: "{} \<upharpoonleft>\<^sub>l xs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<upharpoonleft>\<^sub>l xs = []
[PROOF STEP]
by (simp add: seq_extract_def)


[STATEMENT]
lemma aodv_ex_label [intro]: "\<exists>l. l\<in>labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. l \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p
[PROOF STEP]
by (metis aodv_labels_not_empty all_not_in_conv)


[STATEMENT]
lemma UNION_set_zip:
  "(\<Union>x \<in> set (zip [0..<length xs] (map f xs)). g x) = (\<Union>i < length xs. g (i, f (xs ! i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (g ` set (zip [0..<length xs] (map f xs))) = (\<Union>i<length xs. g (i, f (xs ! i)))
[PROOF STEP]
by (auto simp: set_conv_nth)


[STATEMENT]
lemma pass_separator_ATC_failure_left :
  assumes "observable M"
  and     "observable S"
  and     "(inputs S) = (inputs M)"
  and     "is_separator M q1 q2 A t1 t2"
  and     "\<not> pass_separator_ATC S A s1 t2"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  and     "q1 \<noteq> q2"
  and     "s1 \<in> states S"
shows "LS S s1 - LS M q1 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
have p1: "is_ATC A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ATC A
[PROOF STEP]
using separator_is_ATC[OF assms(4,1,6)]
[PROOF STATE]
proof (prove)
using this:
is_ATC A

goal (1 subgoal):
 1. is_ATC A
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
is_ATC A

goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
have p2: "observable (from_FSM S s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. observable (from_FSM S s1)
[PROOF STEP]
using from_FSM_observable[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
observable (from_FSM S ?q)

goal (1 subgoal):
 1. observable (from_FSM S s1)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
observable (from_FSM S s1)

goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
have p3: "observable (from_FSM M q1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. observable (from_FSM M q1)
[PROOF STEP]
using from_FSM_observable[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
observable (from_FSM M ?q)

goal (1 subgoal):
 1. observable (from_FSM M q1)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
observable (from_FSM M q1)

goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
have p4: "(inputs A) \<subseteq> (inputs (from_FSM M q1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.inputs A \<subseteq> FSM.inputs (from_FSM M q1)
[PROOF STEP]
using is_separator_simps(16)[OF assms(4)]
[PROOF STATE]
proof (prove)
using this:
FSM.inputs A \<subseteq> FSM.inputs M

goal (1 subgoal):
 1. FSM.inputs A \<subseteq> FSM.inputs (from_FSM M q1)
[PROOF STEP]
unfolding from_FSM_simps[OF \<open>q1 \<in> states M\<close>] is_submachine.simps canonical_separator_simps assms(3)
[PROOF STATE]
proof (prove)
using this:
FSM.inputs A \<subseteq> FSM.inputs M

goal (1 subgoal):
 1. FSM.inputs A \<subseteq> FSM.inputs M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.inputs A \<subseteq> FSM.inputs (from_FSM M q1)

goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
have p5: "(inputs (from_FSM S s1)) = (inputs (from_FSM M q1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.inputs (from_FSM S s1) = FSM.inputs (from_FSM M q1)
[PROOF STEP]
using assms(3,6,9)
[PROOF STATE]
proof (prove)
using this:
FSM.inputs S = FSM.inputs M
q1 \<in> FSM.states M
s1 \<in> FSM.states S

goal (1 subgoal):
 1. FSM.inputs (from_FSM S s1) = FSM.inputs (from_FSM M q1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
FSM.inputs (from_FSM S s1) = FSM.inputs (from_FSM M q1)

goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
have p6: "pass_ATC (from_FSM M q1) A {t2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_ATC (from_FSM M q1) A {t2}
[PROOF STEP]
using pass_separator_ATC_from_separator_left[OF assms(1,6,7,4)]
[PROOF STATE]
proof (prove)
using this:
pass_separator_ATC M A q1 t2

goal (1 subgoal):
 1. pass_ATC (from_FSM M q1) A {t2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pass_ATC (from_FSM M q1) A {t2}

goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
have p7: "\<not> pass_ATC (from_FSM S s1) A {t2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> pass_ATC (from_FSM S s1) A {t2}
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
\<not> pass_separator_ATC S A s1 t2

goal (1 subgoal):
 1. \<not> pass_ATC (from_FSM S s1) A {t2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> pass_ATC (from_FSM S s1) A {t2}

goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
using pass_ATC_fail_no_reduction[OF p1 p2 p3 p4 p5 p6 p7]
[PROOF STATE]
proof (prove)
using this:
\<not> L (from_FSM S s1) \<subseteq> L (from_FSM M q1)

goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
unfolding from_FSM_language[OF \<open>q1 \<in> states M\<close>] from_FSM_language[OF \<open>s1 \<in> states S\<close>]
[PROOF STATE]
proof (prove)
using this:
\<not> LS S s1 \<subseteq> LS M q1

goal (1 subgoal):
 1. LS S s1 - LS M q1 \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LS S s1 - LS M q1 \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linear_limit_linear:
  fixes f :: \<open>_ \<Rightarrow> ('a::real_vector \<Rightarrow> 'b::real_normed_vector)\<close>
  assumes  \<open>\<And>n. linear (f n)\<close> and \<open>f \<midarrow>pointwise\<rightarrow> F\<close>
  shows \<open>linear F\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear F
[PROOF STEP]
text\<open>
  Explanation: If a family of linear operators converges pointwise, then the limit is also a linear
  operator.
\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b1 b2. F (b1 + b2) = F b1 + F b2
 2. \<And>r b. F (r *\<^sub>R b) = r *\<^sub>R F b
[PROOF STEP]
show "F (x + y) = F x + F y" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
have "\<forall>a. F a = lim (\<lambda>n. f n a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. F a = lim (\<lambda>n. f n a)
[PROOF STEP]
using \<open>f \<midarrow>pointwise\<rightarrow> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<midarrow>pointwise\<rightarrow> F

goal (1 subgoal):
 1. \<forall>a. F a = lim (\<lambda>n. f n a)
[PROOF STEP]
unfolding pointwise_convergent_to_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t. (\<lambda>n. f n t) \<longlonglongrightarrow> F t

goal (1 subgoal):
 1. \<forall>a. F a = lim (\<lambda>n. f n a)
[PROOF STEP]
by (metis (full_types) limI)
[PROOF STATE]
proof (state)
this:
\<forall>a. F a = lim (\<lambda>n. f n a)

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>a. F a = lim (\<lambda>n. f n a)

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
have "\<forall>f b c g. (lim (\<lambda>n. g n + f n) = (b::'b) + c \<or> \<not> f \<longlonglongrightarrow> c) \<or> \<not> g \<longlonglongrightarrow> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f b c g. (lim (\<lambda>n. g n + f n) = b + c \<or> \<not> f \<longlonglongrightarrow> c) \<or> \<not> g \<longlonglongrightarrow> b
[PROOF STEP]
by (metis (no_types) limI tendsto_add)
[PROOF STATE]
proof (state)
this:
\<forall>f b c g. (lim (\<lambda>n. g n + f n) = b + c \<or> \<not> f \<longlonglongrightarrow> c) \<or> \<not> g \<longlonglongrightarrow> b

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>f b c g. (lim (\<lambda>n. g n + f n) = b + c \<or> \<not> f \<longlonglongrightarrow> c) \<or> \<not> g \<longlonglongrightarrow> b

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
have "\<And>a. (\<lambda>n. f n a) \<longlonglongrightarrow> F a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. (\<lambda>n. f n a) \<longlonglongrightarrow> F a
[PROOF STEP]
using assms(2) pointwise_convergent_to_def
[PROOF STATE]
proof (prove)
using this:
f \<midarrow>pointwise\<rightarrow> F
?x \<midarrow>pointwise\<rightarrow> ?l = (\<forall>t. (\<lambda>n. ?x n t) \<longlonglongrightarrow> ?l t)

goal (1 subgoal):
 1. \<And>a. (\<lambda>n. f n a) \<longlonglongrightarrow> F a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n ?a) \<longlonglongrightarrow> F ?a

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>a. F a = lim (\<lambda>n. f n a)
\<forall>f b c g. (lim (\<lambda>n. g n + f n) = b + c \<or> \<not> f \<longlonglongrightarrow> c) \<or> \<not> g \<longlonglongrightarrow> b
(\<lambda>n. f n ?a) \<longlonglongrightarrow> F ?a
[PROOF STEP]
have
      lim_sum: \<open>lim (\<lambda> n. (f n) x + (f n) y) = lim (\<lambda> n. (f n) x) + lim (\<lambda> n. (f n) y)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>a. F a = lim (\<lambda>n. f n a)
\<forall>f b c g. (lim (\<lambda>n. g n + f n) = b + c \<or> \<not> f \<longlonglongrightarrow> c) \<or> \<not> g \<longlonglongrightarrow> b
(\<lambda>n. f n ?a) \<longlonglongrightarrow> F ?a

goal (1 subgoal):
 1. lim (\<lambda>n. f n x + f n y) = lim (\<lambda>n. f n x) + lim (\<lambda>n. f n y)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lim (\<lambda>n. f n x + f n y) = lim (\<lambda>n. f n x) + lim (\<lambda>n. f n y)

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
have \<open>(f n) (x + y) = (f n) x + (f n) y\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n (x + y) = f n x + f n y
[PROOF STEP]
using \<open>\<And> n.  linear (f n)\<close>
[PROOF STATE]
proof (prove)
using this:
linear (f ?n)

goal (1 subgoal):
 1. f n (x + y) = f n x + f n y
[PROOF STEP]
unfolding linear_def
[PROOF STATE]
proof (prove)
using this:
Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) (f ?n)

goal (1 subgoal):
 1. f n (x + y) = f n x + f n y
[PROOF STEP]
using Real_Vector_Spaces.linear_iff assms(1)
[PROOF STATE]
proof (prove)
using this:
Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) (f ?n)
linear ?f = ((\<forall>x y. ?f (x + y) = ?f x + ?f y) \<and> (\<forall>c x. ?f (c *\<^sub>R x) = c *\<^sub>R ?f x))
linear (f ?n)

goal (1 subgoal):
 1. f n (x + y) = f n x + f n y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ?n (x + y) = f ?n x + f ?n y

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
hence \<open>lim (\<lambda> n. (f n) (x + y)) = lim (\<lambda> n. (f n) x + (f n) y)\<close>
[PROOF STATE]
proof (prove)
using this:
f ?n (x + y) = f ?n x + f ?n y

goal (1 subgoal):
 1. lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x + f n y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x + f n y)

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
hence \<open>lim (\<lambda> n. (f n) (x + y)) = lim (\<lambda> n. (f n) x) + lim (\<lambda> n. (f n) y)\<close>
[PROOF STATE]
proof (prove)
using this:
lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x + f n y)

goal (1 subgoal):
 1. lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x) + lim (\<lambda>n. f n y)
[PROOF STEP]
using lim_sum
[PROOF STATE]
proof (prove)
using this:
lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x + f n y)
lim (\<lambda>n. f n x + f n y) = lim (\<lambda>n. f n x) + lim (\<lambda>n. f n y)

goal (1 subgoal):
 1. lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x) + lim (\<lambda>n. f n y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x) + lim (\<lambda>n. f n y)

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x) + lim (\<lambda>n. f n y)

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
have \<open>(\<lambda> n. (f n) (x + y)) \<longlonglongrightarrow> F (x + y)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n (x + y)) \<longlonglongrightarrow> F (x + y)
[PROOF STEP]
using \<open>f \<midarrow>pointwise\<rightarrow> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<midarrow>pointwise\<rightarrow> F

goal (1 subgoal):
 1. (\<lambda>n. f n (x + y)) \<longlonglongrightarrow> F (x + y)
[PROOF STEP]
unfolding pointwise_convergent_to_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t. (\<lambda>n. f n t) \<longlonglongrightarrow> F t

goal (1 subgoal):
 1. (\<lambda>n. f n (x + y)) \<longlonglongrightarrow> F (x + y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n (x + y)) \<longlonglongrightarrow> F (x + y)

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n (x + y)) \<longlonglongrightarrow> F (x + y)

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
have \<open>(\<lambda> n. (f n) x) \<longlonglongrightarrow> F x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n x) \<longlonglongrightarrow> F x
[PROOF STEP]
using \<open>f \<midarrow>pointwise\<rightarrow> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<midarrow>pointwise\<rightarrow> F

goal (1 subgoal):
 1. (\<lambda>n. f n x) \<longlonglongrightarrow> F x
[PROOF STEP]
unfolding pointwise_convergent_to_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t. (\<lambda>n. f n t) \<longlonglongrightarrow> F t

goal (1 subgoal):
 1. (\<lambda>n. f n x) \<longlonglongrightarrow> F x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n x) \<longlonglongrightarrow> F x

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n x) \<longlonglongrightarrow> F x

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
have \<open>(\<lambda> n. (f n) y) \<longlonglongrightarrow> F y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n y) \<longlonglongrightarrow> F y
[PROOF STEP]
using \<open>f \<midarrow>pointwise\<rightarrow> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<midarrow>pointwise\<rightarrow> F

goal (1 subgoal):
 1. (\<lambda>n. f n y) \<longlonglongrightarrow> F y
[PROOF STEP]
unfolding pointwise_convergent_to_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t. (\<lambda>n. f n t) \<longlonglongrightarrow> F t

goal (1 subgoal):
 1. (\<lambda>n. f n y) \<longlonglongrightarrow> F y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n y) \<longlonglongrightarrow> F y

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x) + lim (\<lambda>n. f n y)
(\<lambda>n. f n (x + y)) \<longlonglongrightarrow> F (x + y)
(\<lambda>n. f n x) \<longlonglongrightarrow> F x
(\<lambda>n. f n y) \<longlonglongrightarrow> F y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lim (\<lambda>n. f n (x + y)) = lim (\<lambda>n. f n x) + lim (\<lambda>n. f n y)
(\<lambda>n. f n (x + y)) \<longlonglongrightarrow> F (x + y)
(\<lambda>n. f n x) \<longlonglongrightarrow> F x
(\<lambda>n. f n y) \<longlonglongrightarrow> F y

goal (1 subgoal):
 1. F (x + y) = F x + F y
[PROOF STEP]
by (metis limI)
[PROOF STATE]
proof (state)
this:
F (x + y) = F x + F y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
F (?x + ?y) = F ?x + F ?y

goal (1 subgoal):
 1. \<And>r b. F (r *\<^sub>R b) = r *\<^sub>R F b
[PROOF STEP]
show "F (r *\<^sub>R x) = r *\<^sub>R F x" for r and x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
have \<open>(f n) (r *\<^sub>R x) = r *\<^sub>R (f n) x\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n (r *\<^sub>R x) = r *\<^sub>R f n x
[PROOF STEP]
using  \<open>\<And> n.  linear (f n)\<close>
[PROOF STATE]
proof (prove)
using this:
linear (f ?n)

goal (1 subgoal):
 1. f n (r *\<^sub>R x) = r *\<^sub>R f n x
[PROOF STEP]
by (simp add: Real_Vector_Spaces.linear_def real_vector.linear_scale)
[PROOF STATE]
proof (state)
this:
f ?n (r *\<^sub>R x) = r *\<^sub>R f ?n x

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
hence \<open>lim (\<lambda> n. (f n) (r *\<^sub>R x)) = lim (\<lambda> n. r *\<^sub>R (f n) x)\<close>
[PROOF STATE]
proof (prove)
using this:
f ?n (r *\<^sub>R x) = r *\<^sub>R f ?n x

goal (1 subgoal):
 1. lim (\<lambda>n. f n (r *\<^sub>R x)) = lim (\<lambda>n. r *\<^sub>R f n x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lim (\<lambda>n. f n (r *\<^sub>R x)) = lim (\<lambda>n. r *\<^sub>R f n x)

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
have \<open>convergent (\<lambda> n. (f n) x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent (\<lambda>n. f n x)
[PROOF STEP]
by (metis assms(2) convergentI pointwise_convergent_to_def)
[PROOF STATE]
proof (state)
this:
convergent (\<lambda>n. f n x)

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
convergent (\<lambda>n. f n x)

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
have \<open>isCont (\<lambda> t::'b. r *\<^sub>R t) tt\<close> for tt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCont ((*\<^sub>R) r) tt
[PROOF STEP]
by (simp add: bounded_linear_scaleR_right)
[PROOF STATE]
proof (state)
this:
isCont ((*\<^sub>R) r) ?tt

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
convergent (\<lambda>n. f n x)
isCont ((*\<^sub>R) r) ?tt
[PROOF STEP]
have \<open>lim (\<lambda> n. r *\<^sub>R ((f n) x)) =  r *\<^sub>R lim (\<lambda> n. (f n) x)\<close>
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>n. f n x)
isCont ((*\<^sub>R) r) ?tt

goal (1 subgoal):
 1. lim (\<lambda>n. r *\<^sub>R f n x) = r *\<^sub>R lim (\<lambda>n. f n x)
[PROOF STEP]
using \<open>f \<midarrow>pointwise\<rightarrow> F\<close>
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>n. f n x)
isCont ((*\<^sub>R) r) ?tt
f \<midarrow>pointwise\<rightarrow> F

goal (1 subgoal):
 1. lim (\<lambda>n. r *\<^sub>R f n x) = r *\<^sub>R lim (\<lambda>n. f n x)
[PROOF STEP]
unfolding pointwise_convergent_to_def
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>n. f n x)
isCont ((*\<^sub>R) r) ?tt
\<forall>t. (\<lambda>n. f n t) \<longlonglongrightarrow> F t

goal (1 subgoal):
 1. lim (\<lambda>n. r *\<^sub>R f n x) = r *\<^sub>R lim (\<lambda>n. f n x)
[PROOF STEP]
by (metis (mono_tags) isCont_tendsto_compose limI)
[PROOF STATE]
proof (state)
this:
lim (\<lambda>n. r *\<^sub>R f n x) = r *\<^sub>R lim (\<lambda>n. f n x)

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
hence \<open>lim (\<lambda> n.  (f n) (r *\<^sub>R x)) = r *\<^sub>R lim (\<lambda> n. (f n) x)\<close>
[PROOF STATE]
proof (prove)
using this:
lim (\<lambda>n. r *\<^sub>R f n x) = r *\<^sub>R lim (\<lambda>n. f n x)

goal (1 subgoal):
 1. lim (\<lambda>n. f n (r *\<^sub>R x)) = r *\<^sub>R lim (\<lambda>n. f n x)
[PROOF STEP]
using \<open>lim (\<lambda> n. (f n) (r *\<^sub>R x)) = lim (\<lambda> n. r *\<^sub>R (f n) x)\<close>
[PROOF STATE]
proof (prove)
using this:
lim (\<lambda>n. r *\<^sub>R f n x) = r *\<^sub>R lim (\<lambda>n. f n x)
lim (\<lambda>n. f n (r *\<^sub>R x)) = lim (\<lambda>n. r *\<^sub>R f n x)

goal (1 subgoal):
 1. lim (\<lambda>n. f n (r *\<^sub>R x)) = r *\<^sub>R lim (\<lambda>n. f n x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lim (\<lambda>n. f n (r *\<^sub>R x)) = r *\<^sub>R lim (\<lambda>n. f n x)

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lim (\<lambda>n. f n (r *\<^sub>R x)) = r *\<^sub>R lim (\<lambda>n. f n x)

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
have \<open>(\<lambda> n. (f n) x) \<longlonglongrightarrow> F x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n x) \<longlonglongrightarrow> F x
[PROOF STEP]
using \<open>f \<midarrow>pointwise\<rightarrow> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<midarrow>pointwise\<rightarrow> F

goal (1 subgoal):
 1. (\<lambda>n. f n x) \<longlonglongrightarrow> F x
[PROOF STEP]
unfolding pointwise_convergent_to_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t. (\<lambda>n. f n t) \<longlonglongrightarrow> F t

goal (1 subgoal):
 1. (\<lambda>n. f n x) \<longlonglongrightarrow> F x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n x) \<longlonglongrightarrow> F x

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n x) \<longlonglongrightarrow> F x

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
have \<open>(\<lambda> n.  (f n) (r *\<^sub>R x)) \<longlonglongrightarrow> F (r *\<^sub>R x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n (r *\<^sub>R x)) \<longlonglongrightarrow> F (r *\<^sub>R x)
[PROOF STEP]
using \<open>f \<midarrow>pointwise\<rightarrow> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<midarrow>pointwise\<rightarrow> F

goal (1 subgoal):
 1. (\<lambda>n. f n (r *\<^sub>R x)) \<longlonglongrightarrow> F (r *\<^sub>R x)
[PROOF STEP]
unfolding pointwise_convergent_to_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t. (\<lambda>n. f n t) \<longlonglongrightarrow> F t

goal (1 subgoal):
 1. (\<lambda>n. f n (r *\<^sub>R x)) \<longlonglongrightarrow> F (r *\<^sub>R x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n (r *\<^sub>R x)) \<longlonglongrightarrow> F (r *\<^sub>R x)

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lim (\<lambda>n. f n (r *\<^sub>R x)) = r *\<^sub>R lim (\<lambda>n. f n x)
(\<lambda>n. f n x) \<longlonglongrightarrow> F x
(\<lambda>n. f n (r *\<^sub>R x)) \<longlonglongrightarrow> F (r *\<^sub>R x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lim (\<lambda>n. f n (r *\<^sub>R x)) = r *\<^sub>R lim (\<lambda>n. f n x)
(\<lambda>n. f n x) \<longlonglongrightarrow> F x
(\<lambda>n. f n (r *\<^sub>R x)) \<longlonglongrightarrow> F (r *\<^sub>R x)

goal (1 subgoal):
 1. F (r *\<^sub>R x) = r *\<^sub>R F x
[PROOF STEP]
by (metis limI)
[PROOF STATE]
proof (state)
this:
F (r *\<^sub>R x) = r *\<^sub>R F x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
F (?r *\<^sub>R ?x) = ?r *\<^sub>R F ?x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hnr_is_empty_aux: "(is_empty, RETURN o op_set_is_empty)\<in>is_set\<^sup>k \<rightarrow>\<^sub>a bool_assn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_empty, RETURN \<circ> op_set_is_empty) \<in> is_set\<^sup>k \<rightarrow>\<^sub>a bool_assn
[PROOF STEP]
by solve_sepl_binding


[STATEMENT]
lemma [def_pat_rules]: "op_iam_empty_sz$N \<equiv> UNPROTECT (op_iam_empty_sz N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_iam_empty_sz $ N \<equiv> UNPROTECT (op_iam_empty_sz N)
[PROOF STEP]
by simp


[STATEMENT]
lemma row_map_mat[simp]:
  assumes "i < dim_row A" shows "row (map_mat f A) i = map_vec f (row A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (map_mat f A) i = map_vec f (row A i)
[PROOF STEP]
unfolding map_mat_def map_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (mat (dim_row A) (dim_col A) (\<lambda>ij. f (A $$ ij))) i = vec (dim_vec (row A i)) (\<lambda>ia. f (row A i $ ia))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < dim_row A

goal (1 subgoal):
 1. row (mat (dim_row A) (dim_col A) (\<lambda>ij. f (A $$ ij))) i = vec (dim_vec (row A i)) (\<lambda>ia. f (row A i $ ia))
[PROOF STEP]
by auto


[STATEMENT]
lemma game_sem_loop_fixpoint_mono: "mono (\<lambda>Z. X \<union> game_sem I \<alpha> Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>Z. X \<union> game_sem I \<alpha> Z)
[PROOF STEP]
using game_sem_mono
[PROOF STATE]
proof (prove)
using this:
mono (game_sem ?I ?\<alpha>)

goal (1 subgoal):
 1. mono (\<lambda>Z. X \<union> game_sem I \<alpha> Z)
[PROOF STEP]
by (metis Un_mono mon_mono order_refl)


[STATEMENT]
lemma normal_exponent_bounds_real:
  "2 - 2 ^ (LENGTH('e) - 1) - real LENGTH('f) \<le> normal_exponent x"
  "normal_exponent x \<le> 2 ^ (LENGTH('e) - 1) - real LENGTH('f) - 1"
  if "is_normal x"
  for x::"('e, 'f)float"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 - 2 ^ (LENGTH('e) - 1) - real LENGTH('f) \<le> real_of_int (normal_exponent x) &&& real_of_int (normal_exponent x) \<le> 2 ^ (LENGTH('e) - 1) - real LENGTH('f) - 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 - 2 ^ (LENGTH('e) - 1) - real LENGTH('f) \<le> real_of_int (normal_exponent x)
[PROOF STEP]
by (rule order_trans[OF _ of_int_leI[OF normal_exponent_bounds_int(1)[OF that]]]) auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (normal_exponent x) \<le> 2 ^ (LENGTH('e) - 1) - real LENGTH('f) - 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (normal_exponent x) \<le> 2 ^ (LENGTH('e) - 1) - real LENGTH('f) - 1
[PROOF STEP]
by (rule order_trans[OF of_int_leI[OF normal_exponent_bounds_int(2)[OF that]]]) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma dual_top [simp]: "\<top> ^ o = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<top> ^ o = \<bottom>
[PROOF STEP]
apply (rule order.antisym, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<top> ^ o \<le> \<bottom>
[PROOF STEP]
by (subst dual_le, simp)


[STATEMENT]
lemma le_comp_left_right: "x \<le> y \<Longrightarrow> u \<le> v \<Longrightarrow> x * u \<le> y * v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; u \<le> v\<rbrakk> \<Longrightarrow> x * u \<le> y * v
[PROOF STEP]
apply (rule_tac y = "x * v" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> y; u \<le> v\<rbrakk> \<Longrightarrow> x * u \<le> x * v
 2. \<lbrakk>x \<le> y; u \<le> v\<rbrakk> \<Longrightarrow> x * v \<le> y * v
[PROOF STEP]
apply (rule le_comp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; u \<le> v\<rbrakk> \<Longrightarrow> x * v \<le> y * v
[PROOF STEP]
by (rule le_comp_right, simp)