[STATEMENT]
lemma num_ni_nz_if[simp]: "\<lbrakk>t < N; ts t \<noteq> INIT\<rbrakk> \<Longrightarrow> num_ni ts \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t < N; ts t \<noteq> INIT\<rbrakk> \<Longrightarrow> num_ni ts \<noteq> 0
[PROOF STEP]
apply (cases "ts t")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t < N; ts t \<noteq> INIT; ts t = INIT\<rbrakk> \<Longrightarrow> num_ni ts \<noteq> 0
 2. \<And>x2. \<lbrakk>t < N; ts t \<noteq> INIT; ts t = WAIT x2\<rbrakk> \<Longrightarrow> num_ni ts \<noteq> 0
 3. \<And>x3. \<lbrakk>t < N; ts t \<noteq> INIT; ts t = HOLD x3\<rbrakk> \<Longrightarrow> num_ni ts \<noteq> 0
 4. \<And>x4. \<lbrakk>t < N; ts t \<noteq> INIT; ts t = REL x4\<rbrakk> \<Longrightarrow> num_ni ts \<noteq> 0
[PROOF STEP]
by (simp_all add: num_ni_def) force+


[STATEMENT]
lemma num_ni_leN: "num_ni ts \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_ni ts \<le> N
[PROOF STEP]
apply (clarsimp simp: num_ni_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<N. ni_weight (ts i)) \<le> N
[PROOF STEP]
apply (rule order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<Sum>i = 0..<N. ni_weight (ts i)) \<le> ?y
 2. ?y \<le> N
[PROOF STEP]
apply (rule sum_bounded_above[where K=1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<in> {0..<N} \<Longrightarrow> ni_weight (ts i) \<le> 1
 2. of_nat (card {0..<N}) * 1 \<le> N
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_invar3: "A.is_invar invar3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.is_invar invar3
[PROOF STEP]
apply (rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. invar3 as\<^sub>0
 2. \<And>s s'. \<lbrakk>A.reachable s; invar3 s; A.step s s'\<rbrakk> \<Longrightarrow> invar3 s'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar3 as\<^sub>0
[PROOF STEP]
by (auto simp: invar3_def as\<^sub>0_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>A.reachable s; invar3 s; A.step s s'\<rbrakk> \<Longrightarrow> invar3 s'
[PROOF STEP]
subgoal for s s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable s; invar3 s; A.step s s'\<rbrakk> \<Longrightarrow> invar3 s'
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>A.reachable s; invar3 s; alstep l s s'\<rbrakk> \<Longrightarrow> invar3 s'
[PROOF STEP]
apply (erule alstep.cases, erule astep_sng.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>l c n ts c' n' s'a ca na. \<lbrakk>A.reachable s; invar3 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, INIT); (c', n', s'a) = (ca, na + 1, WAIT na)\<rbrakk> \<Longrightarrow> invar3 s'
 2. \<And>l c n ts c' n' s'a ca k na. \<lbrakk>A.reachable s; invar3 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, WAIT k); (c', n', s'a) = (ca, na, WAIT k); ca \<noteq> k\<rbrakk> \<Longrightarrow> invar3 s'
 3. \<And>l c n ts c' n' s'a ca na. \<lbrakk>A.reachable s; invar3 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, WAIT ca); (c', n', s'a) = (ca, na, HOLD ca)\<rbrakk> \<Longrightarrow> invar3 s'
 4. \<And>l c n ts c' n' s'a ca na k. \<lbrakk>A.reachable s; invar3 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, HOLD k); (c', n', s'a) = (ca, na, REL k)\<rbrakk> \<Longrightarrow> invar3 s'
 5. \<And>l c n ts c' n' s'a ca na k. \<lbrakk>A.reachable s; invar3 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, REL k); (c', n', s'a) = (k + 1, na, INIT)\<rbrakk> \<Longrightarrow> invar3 s'
[PROOF STEP]
apply (auto simp: invar3_def num_ni_upd)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l c ts k. \<lbrakk>A.reachable (c, c + num_ni ts, ts); s = (c, c + num_ni ts, ts); s' = (Suc k, c + num_ni ts, ts(l := INIT)); l < N; ts l = REL k\<rbrakk> \<Longrightarrow> c + num_ni ts = Suc (k + (num_ni ts - Suc 0))
[PROOF STEP]
using holds_only_current
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>A.reachable (?c, ?n, ?ts); ?t < N; locks_ticket (?ts ?t) ?k\<rbrakk> \<Longrightarrow> ?k = ?c

goal (1 subgoal):
 1. \<And>l c ts k. \<lbrakk>A.reachable (c, c + num_ni ts, ts); s = (c, c + num_ni ts, ts); s' = (Suc k, c + num_ni ts, ts(l := INIT)); l < N; ts l = REL k\<rbrakk> \<Longrightarrow> c + num_ni ts = Suc (k + (num_ni ts - Suc 0))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sraux:
    "sim_rel1 (c,n,ts) (ci,ni,tsi) \<Longrightarrow> ci = c mod N \<and> ni = n mod (k*N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_rel1 (c, n, ts) (ci, ni, tsi) \<Longrightarrow> ci = c mod N \<and> ni = n mod (k * N)
[PROOF STEP]
by (auto simp: sim_rel1_def Let_def)


[STATEMENT]
lemma sraux2: "\<lbrakk>sim_rel1 (c,n,ts) (ci,ni,tsi); t<N\<rbrakk>
    \<Longrightarrow> tsi t = map_ticket (\<lambda>x. x mod N) (ts t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sim_rel1 (c, n, ts) (ci, ni, tsi); t < N\<rbrakk> \<Longrightarrow> tsi t = map_ticket (\<lambda>x. x mod N) (ts t)
[PROOF STEP]
by (auto simp: sim_rel1_def Let_def)


[STATEMENT]
lemma xfer_locks_ticket:
    assumes "locks_ticket (map_ticket (\<lambda>t. t mod N) (ts t)) tki"
    obtains tk where "tki=tk mod N" "locks_ticket (ts t) tk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tk. \<lbrakk>tki = tk mod N; locks_ticket (ts t) tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
locks_ticket (map_ticket (\<lambda>t. t mod N) (ts t)) tki

goal (1 subgoal):
 1. (\<And>tk. \<lbrakk>tki = tk mod N; locks_ticket (ts t) tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding locks_ticket_def
[PROOF STATE]
proof (prove)
using this:
map_ticket (\<lambda>t. t mod N) (ts t) = HOLD tki \<or> map_ticket (\<lambda>t. t mod N) (ts t) = REL tki

goal (1 subgoal):
 1. (\<And>tk. \<lbrakk>tki = tk mod N; ts t = HOLD tk \<or> ts t = REL tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma b_holds_only_current:
    "\<lbrakk>B.reachable (c, n, ts); t < N; locks_ticket (ts t) tk\<rbrakk> \<Longrightarrow> tk = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable (c, n, ts); t < N; locks_ticket (ts t) tk\<rbrakk> \<Longrightarrow> tk = c
[PROOF STEP]
apply (rule sim1.xfer_reachable, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>B.reachable (c, n, ts); t < N; locks_ticket (ts t) tk; sim_rel1 as (c, n, ts); A.reachable as\<rbrakk> \<Longrightarrow> tk = c
[PROOF STEP]
apply (clarsimp simp: sim_rel1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>B.reachable (a mod N, aa mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> b); t < N; locks_ticket (map_ticket (\<lambda>t. t mod N) (b t)) tk; A.reachable (a, aa, b); c = a mod N; ts = map_ticket (\<lambda>t. t mod N) \<circ> b; n = aa mod (k * N)\<rbrakk> \<Longrightarrow> tk = a mod N
[PROOF STEP]
apply (erule xfer_locks_ticket)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b tka. \<lbrakk>B.reachable (a mod N, aa mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> b); t < N; A.reachable (a, aa, b); c = a mod N; ts = map_ticket (\<lambda>t. t mod N) \<circ> b; n = aa mod (k * N); tk = tka mod N; locks_ticket (b t) tka\<rbrakk> \<Longrightarrow> tk = a mod N
[PROOF STEP]
using holds_only_current
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>A.reachable (?c, ?n, ?ts); ?t < N; locks_ticket (?ts ?t) ?k\<rbrakk> \<Longrightarrow> ?k = ?c

goal (1 subgoal):
 1. \<And>a aa b tka. \<lbrakk>B.reachable (a mod N, aa mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> b); t < N; A.reachable (a, aa, b); c = a mod N; ts = map_ticket (\<lambda>t. t mod N) \<circ> b; n = aa mod (k * N); tk = tka mod N; locks_ticket (b t) tka\<rbrakk> \<Longrightarrow> tk = a mod N
[PROOF STEP]
by blast


[STATEMENT]
lemma b_mutual_exclusion': "\<lbrakk>B.reachable s;
      t<N; t'<N; t\<noteq>t'; locks_ticket (tts s t) tk; locks_ticket (tts s t') tk'
    \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable s; t < N; t' < N; t \<noteq> t'; locks_ticket (tts s t) tk; locks_ticket (tts s t') tk'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rule sim1.xfer_reachable, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>B.reachable s; t < N; t' < N; t \<noteq> t'; locks_ticket (tts s t) tk; locks_ticket (tts s t') tk'; sim_rel1 as s; A.reachable as\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp simp: sim_rel1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>B.reachable (a mod N, aa mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> b); t < N; t' < N; t \<noteq> t'; locks_ticket (map_ticket (\<lambda>t. t mod N) (b t)) tk; locks_ticket (map_ticket (\<lambda>t. t mod N) (b t')) tk'; A.reachable (a, aa, b); s = (a mod N, aa mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> b)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule xfer_locks_ticket)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b tka tkaa. \<lbrakk>B.reachable (a mod N, aa mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> b); t < N; t' < N; t \<noteq> t'; A.reachable (a, aa, b); s = (a mod N, aa mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> b); tk = tka mod N; locks_ticket (b t) tka; tk' = tkaa mod N; locks_ticket (b t') tkaa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule (3) mutual_exclusion'; simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma xfer_has_ticket:
    assumes "has_ticket (map_ticket (\<lambda>t. t mod N) (ts t)) tki"
    obtains tk where "tki=tk mod N" "has_ticket (ts t) tk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tk. \<lbrakk>tki = tk mod N; has_ticket (ts t) tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
has_ticket (map_ticket (\<lambda>t. t mod N) (ts t)) tki

goal (1 subgoal):
 1. (\<And>tk. \<lbrakk>tki = tk mod N; has_ticket (ts t) tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding has_ticket_def
[PROOF STATE]
proof (prove)
using this:
map_ticket (\<lambda>t. t mod N) (ts t) = WAIT tki \<or> map_ticket (\<lambda>t. t mod N) (ts t) = HOLD tki \<or> map_ticket (\<lambda>t. t mod N) (ts t) = REL tki

goal (1 subgoal):
 1. (\<And>tk. \<lbrakk>tki = tk mod N; ts t = WAIT tk \<or> ts t = HOLD tk \<or> ts t = REL tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma has_ticket_in_range:
    assumes Ra: "A.reachable (c,n,ts)" and "t<N" and U: "has_ticket (ts t) tk"
    shows "c\<le>tk \<and> tk<c+N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<le> tk \<and> tk < c + N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<le> tk \<and> tk < c + N
[PROOF STEP]
have [simp]: "n=c + num_ni ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = c + num_ni ts
[PROOF STEP]
using A.invar_reachable[OF is_invar3 Ra, unfolded invar3_def]
[PROOF STATE]
proof (prove)
using this:
case (c, n, ts) of (c, n, ts) \<Rightarrow> n = c + num_ni ts

goal (1 subgoal):
 1. n = c + num_ni ts
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = c + num_ni ts

goal (1 subgoal):
 1. c \<le> tk \<and> tk < c + N
[PROOF STEP]
show "c\<le>tk \<and> tk<c+N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<le> tk \<and> tk < c + N
[PROOF STEP]
using A.invar_reachable[OF is_invar1 Ra] U
[PROOF STATE]
proof (prove)
using this:
invar1 (c, n, ts)
has_ticket (ts t) tk

goal (1 subgoal):
 1. c \<le> tk \<and> tk < c + N
[PROOF STEP]
apply (auto simp: invar1_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < c + num_ni ts \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k); has_ticket (ts t) tk\<rbrakk> \<Longrightarrow> c \<le> tk
 2. \<lbrakk>\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < c + num_ni ts \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k); has_ticket (ts t) tk\<rbrakk> \<Longrightarrow> tk < c + N
[PROOF STEP]
using \<open>t<N\<close>
[PROOF STATE]
proof (prove)
using this:
t < N

goal (2 subgoals):
 1. \<lbrakk>\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < c + num_ni ts \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k); has_ticket (ts t) tk\<rbrakk> \<Longrightarrow> c \<le> tk
 2. \<lbrakk>\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < c + num_ni ts \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k); has_ticket (ts t) tk\<rbrakk> \<Longrightarrow> tk < c + N
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < c + num_ni ts \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k); has_ticket (ts t) tk\<rbrakk> \<Longrightarrow> tk < c + N
[PROOF STEP]
using \<open>t<N\<close> num_ni_leN[of ts]
[PROOF STATE]
proof (prove)
using this:
t < N
num_ni ts \<le> N

goal (1 subgoal):
 1. \<lbrakk>\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < c + num_ni ts \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k); has_ticket (ts t) tk\<rbrakk> \<Longrightarrow> tk < c + N
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
c \<le> tk \<and> tk < c + N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma b_has_ticket_unique: "\<lbrakk>B.reachable (ci,ni,tsi);
      t<N; has_ticket (tsi t) tki; t'<N; has_ticket (tsi t') tki
    \<rbrakk> \<Longrightarrow> t'=t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable (ci, ni, tsi); t < N; has_ticket (tsi t) tki; t' < N; has_ticket (tsi t') tki\<rbrakk> \<Longrightarrow> t' = t
[PROOF STEP]
apply (rule sim1.xfer_reachable, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>B.reachable (ci, ni, tsi); t < N; has_ticket (tsi t) tki; t' < N; has_ticket (tsi t') tki; sim_rel1 as (ci, ni, tsi); A.reachable as\<rbrakk> \<Longrightarrow> t' = t
[PROOF STEP]
apply (auto simp: sim_rel1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>B.reachable (a mod N, aa mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> b); t < N; has_ticket (map_ticket (\<lambda>t. t mod N) (b t)) tki; t' < N; has_ticket (map_ticket (\<lambda>t. t mod N) (b t')) tki; A.reachable (a, aa, b); ci = a mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> b; ni = aa mod (k * N)\<rbrakk> \<Longrightarrow> t' = t
[PROOF STEP]
subgoal for c n ts
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; has_ticket (map_ticket (\<lambda>t. t mod N) (ts t)) tki; t' < N; has_ticket (map_ticket (\<lambda>t. t mod N) (ts t')) tki; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N)\<rbrakk> \<Longrightarrow> t' = t
[PROOF STEP]
apply (erule xfer_has_ticket)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tk tka. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tki = tk mod N; has_ticket (ts t) tk; tki = tka mod N; has_ticket (ts t') tka\<rbrakk> \<Longrightarrow> t' = t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tk tka. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tka mod N = tk mod N; has_ticket (ts t) tk; tki = tk mod N; has_ticket (ts t') tka\<rbrakk> \<Longrightarrow> t' = t
[PROOF STEP]
subgoal for tk tk'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tk' mod N = tk mod N; has_ticket (ts t) tk; tki = tk mod N; has_ticket (ts t') tk'\<rbrakk> \<Longrightarrow> t' = t
[PROOF STEP]
apply (subgoal_tac "tk=tk'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tk' mod N = tk mod N; has_ticket (ts t) tk; tki = tk mod N; has_ticket (ts t') tk'; tk = tk'\<rbrakk> \<Longrightarrow> t' = t
 2. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tk' mod N = tk mod N; has_ticket (ts t) tk; tki = tk mod N; has_ticket (ts t') tk'\<rbrakk> \<Longrightarrow> tk = tk'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); has_ticket (ts t) tk'; tki = tk' mod N; has_ticket (ts t') tk'; tk = tk'\<rbrakk> \<Longrightarrow> t' = t
 2. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tk' mod N = tk mod N; has_ticket (ts t) tk; tki = tk mod N; has_ticket (ts t') tk'\<rbrakk> \<Longrightarrow> tk = tk'
[PROOF STEP]
apply (frule (4) has_ticket_unique, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tk' mod N = tk mod N; has_ticket (ts t) tk; tki = tk mod N; has_ticket (ts t') tk'\<rbrakk> \<Longrightarrow> tk = tk'
[PROOF STEP]
apply (frule (2) has_ticket_in_range[where tk=tk])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tk' mod N = tk mod N; has_ticket (ts t) tk; tki = tk mod N; has_ticket (ts t') tk'; c \<le> tk \<and> tk < c + N\<rbrakk> \<Longrightarrow> tk = tk'
[PROOF STEP]
apply (frule (2) has_ticket_in_range[where tk=tk'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tk' mod N = tk mod N; has_ticket (ts t) tk; tki = tk mod N; has_ticket (ts t') tk'; c \<le> tk \<and> tk < c + N; c \<le> tk' \<and> tk' < c + N\<rbrakk> \<Longrightarrow> tk = tk'
[PROOF STEP]
apply (auto simp: mod_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable (c mod N, n mod (k * N), map_ticket (\<lambda>t. t mod N) \<circ> ts); t < N; t' < N; A.reachable (c, n, ts); ci = c mod N; tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts; ni = n mod (k * N); tk' mod N = tk mod N; has_ticket (ts t) tk; tki = tk mod N; has_ticket (ts t') tk'; c \<le> tk; tk < c + N; c \<le> tk'; tk' < c + N\<rbrakk> \<Longrightarrow> tk = tk'
[PROOF STEP]
apply (rule mod_eq_imp_eq; (assumption|simp))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma c_never_blocked: "C.can_step l s \<longleftrightarrow> l<N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.can_step l s = (l < N)
[PROOF STEP]
apply (cases s; cases "tts s l"; simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>s = (a, b, c); c l = INIT\<rbrakk> \<Longrightarrow> C.can_step l (a, b, c) = (l < N)
 2. \<And>a b c x2. \<lbrakk>s = (a, b, c); c l = WAIT x2\<rbrakk> \<Longrightarrow> C.can_step l (a, b, c) = (l < N)
 3. \<And>a b c x3. \<lbrakk>s = (a, b, c); c l = HOLD x3\<rbrakk> \<Longrightarrow> C.can_step l (a, b, c) = (l < N)
 4. \<And>a b c x4. \<lbrakk>s = (a, b, c); c l = REL x4\<rbrakk> \<Longrightarrow> C.can_step l (a, b, c) = (l < N)
[PROOF STEP]
unfolding C.can_step_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>s = (a, b, c); c l = INIT\<rbrakk> \<Longrightarrow> (\<exists>s'. clstep l (a, b, c) s') = (l < N)
 2. \<And>a b c x2. \<lbrakk>s = (a, b, c); c l = WAIT x2\<rbrakk> \<Longrightarrow> (\<exists>s'. clstep l (a, b, c) s') = (l < N)
 3. \<And>a b c x3. \<lbrakk>s = (a, b, c); c l = HOLD x3\<rbrakk> \<Longrightarrow> (\<exists>s'. clstep l (a, b, c) s') = (l < N)
 4. \<And>a b c x4. \<lbrakk>s = (a, b, c); c l = REL x4\<rbrakk> \<Longrightarrow> (\<exists>s'. clstep l (a, b, c) s') = (l < N)
[PROOF STEP]
apply (clarsimp_all simp: clstep.simps cstep_sng.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c x2. \<lbrakk>s = (a, b, c); c l = WAIT x2\<rbrakk> \<Longrightarrow> (l < N \<and> (\<exists>aa ab s'. aa = a \<and> ab = b \<and> s' = WAIT x2 \<and> \<not> a ! x2 \<or> aa = a \<and> ab = b \<and> s' = HOLD x2 \<and> a ! x2)) = (l < N)
[PROOF STEP]
by metis


[STATEMENT]
lemma is_invar4: "B.is_invar invar4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B.is_invar invar4
[PROOF STEP]
apply (rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. invar4 bs\<^sub>0
 2. \<And>s s'. \<lbrakk>B.reachable s; invar4 s; B.step s s'\<rbrakk> \<Longrightarrow> invar4 s'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar4 bs\<^sub>0
[PROOF STEP]
by (auto simp: invar4_def bs\<^sub>0_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>B.reachable s; invar4 s; B.step s s'\<rbrakk> \<Longrightarrow> invar4 s'
[PROOF STEP]
subgoal for s s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B.reachable s; invar4 s; B.step s s'\<rbrakk> \<Longrightarrow> invar4 s'
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>B.reachable s; invar4 s; blstep l s s'\<rbrakk> \<Longrightarrow> invar4 s'
[PROOF STEP]
apply (erule blstep.cases, erule bstep_sng.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>l c n ts c' n' s'a ca na. \<lbrakk>B.reachable s; invar4 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, INIT); (c', n', s'a) = (ca, (na + 1) mod (k * N), WAIT (na mod N))\<rbrakk> \<Longrightarrow> invar4 s'
 2. \<And>l c n ts c' n' s'a ca tk na. \<lbrakk>B.reachable s; invar4 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, WAIT tk); (c', n', s'a) = (ca, na, WAIT tk); ca \<noteq> tk\<rbrakk> \<Longrightarrow> invar4 s'
 3. \<And>l c n ts c' n' s'a ca na. \<lbrakk>B.reachable s; invar4 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, WAIT ca); (c', n', s'a) = (ca, na, HOLD ca)\<rbrakk> \<Longrightarrow> invar4 s'
 4. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable s; invar4 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, HOLD tk); (c', n', s'a) = (ca, na, REL tk)\<rbrakk> \<Longrightarrow> invar4 s'
 5. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable s; invar4 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, REL tk); (c', n', s'a) = ((tk + 1) mod N, na, INIT)\<rbrakk> \<Longrightarrow> invar4 s'
[PROOF STEP]
unfolding invar4_def
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>l c n ts c' n' s'a ca na. \<lbrakk>B.reachable s; case s of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N); s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, INIT); (c', n', s'a) = (ca, (na + 1) mod (k * N), WAIT (na mod N))\<rbrakk> \<Longrightarrow> case s' of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N)
 2. \<And>l c n ts c' n' s'a ca tk na. \<lbrakk>B.reachable s; case s of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N); s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, WAIT tk); (c', n', s'a) = (ca, na, WAIT tk); ca \<noteq> tk\<rbrakk> \<Longrightarrow> case s' of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N)
 3. \<And>l c n ts c' n' s'a ca na. \<lbrakk>B.reachable s; case s of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N); s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, WAIT ca); (c', n', s'a) = (ca, na, HOLD ca)\<rbrakk> \<Longrightarrow> case s' of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N)
 4. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable s; case s of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N); s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, HOLD tk); (c', n', s'a) = (ca, na, REL tk)\<rbrakk> \<Longrightarrow> case s' of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N)
 5. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable s; case s of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N); s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, REL tk); (c', n', s'a) = ((tk + 1) mod N, na, INIT)\<rbrakk> \<Longrightarrow> case s' of (c, n, ts) \<Rightarrow> c < N \<and> (\<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>l c n ts c' n' s'a ca na t tk. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, (na + 1) mod (k * N), ts(l := WAIT (na mod N))); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = INIT; t < N; has_ticket ((ts(l := WAIT (na mod N))) t) tk\<rbrakk> \<Longrightarrow> tk < N
 2. \<And>l c n ts c' n' s'a ca tk na t tka. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, na, ts(l := WAIT tk)); l < N; ca \<noteq> tk; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = WAIT tk; t < N; has_ticket ((ts(l := WAIT tk)) t) tka\<rbrakk> \<Longrightarrow> tka < N
 3. \<And>l c n ts c' n' s'a ca na t tk. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, na, ts(l := HOLD ca)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = WAIT ca; t < N; has_ticket ((ts(l := HOLD ca)) t) tk\<rbrakk> \<Longrightarrow> tk < N
 4. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, na, ts(l := REL tk)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = HOLD tk; t < N; has_ticket ((ts(l := REL tk)) t) tka\<rbrakk> \<Longrightarrow> tka < N
 5. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk\<rbrakk> \<Longrightarrow> (tk + 1) mod N < N
 6. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk; t < N; has_ticket ((ts(l := INIT)) t) tka\<rbrakk> \<Longrightarrow> tka < N
[PROOF STEP]
apply (metis N_gt0 fun_upd_apply has_ticket_simps(2) mod_less_divisor)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>l c n ts c' n' s'a ca tk na t tka. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, na, ts(l := WAIT tk)); l < N; ca \<noteq> tk; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = WAIT tk; t < N; has_ticket ((ts(l := WAIT tk)) t) tka\<rbrakk> \<Longrightarrow> tka < N
 2. \<And>l c n ts c' n' s'a ca na t tk. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, na, ts(l := HOLD ca)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = WAIT ca; t < N; has_ticket ((ts(l := HOLD ca)) t) tk\<rbrakk> \<Longrightarrow> tk < N
 3. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, na, ts(l := REL tk)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = HOLD tk; t < N; has_ticket ((ts(l := REL tk)) t) tka\<rbrakk> \<Longrightarrow> tka < N
 4. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk\<rbrakk> \<Longrightarrow> (tk + 1) mod N < N
 5. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk; t < N; has_ticket ((ts(l := INIT)) t) tka\<rbrakk> \<Longrightarrow> tka < N
[PROOF STEP]
apply (metis fun_upd_triv)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>l c n ts c' n' s'a ca na t tk. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, na, ts(l := HOLD ca)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = WAIT ca; t < N; has_ticket ((ts(l := HOLD ca)) t) tk\<rbrakk> \<Longrightarrow> tk < N
 2. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, na, ts(l := REL tk)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = HOLD tk; t < N; has_ticket ((ts(l := REL tk)) t) tka\<rbrakk> \<Longrightarrow> tka < N
 3. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk\<rbrakk> \<Longrightarrow> (tk + 1) mod N < N
 4. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk; t < N; has_ticket ((ts(l := INIT)) t) tka\<rbrakk> \<Longrightarrow> tka < N
[PROOF STEP]
apply (metis fun_upd_other fun_upd_same has_ticket_simps(3))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = (ca, na, ts(l := REL tk)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = HOLD tk; t < N; has_ticket ((ts(l := REL tk)) t) tka\<rbrakk> \<Longrightarrow> tka < N
 2. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk\<rbrakk> \<Longrightarrow> (tk + 1) mod N < N
 3. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk; t < N; has_ticket ((ts(l := INIT)) t) tka\<rbrakk> \<Longrightarrow> tka < N
[PROOF STEP]
apply (metis fun_upd_other fun_upd_same has_ticket_def has_ticket_simps(4))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk\<rbrakk> \<Longrightarrow> (tk + 1) mod N < N
 2. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk; t < N; has_ticket ((ts(l := INIT)) t) tka\<rbrakk> \<Longrightarrow> tka < N
[PROOF STEP]
using mod_less_divisor
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> ?m mod ?n < ?n

goal (2 subgoals):
 1. \<And>l c n ts c' n' s'a ca na tk. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk\<rbrakk> \<Longrightarrow> (tk + 1) mod N < N
 2. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk; t < N; has_ticket ((ts(l := INIT)) t) tka\<rbrakk> \<Longrightarrow> tka < N
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l c n ts c' n' s'a ca na tk t tka. \<lbrakk>B.reachable (ca, na, ts); s' = ((tk + 1) mod N, na, ts(l := INIT)); l < N; s = (ca, na, ts); ca < N; \<forall>t<N. \<forall>tk. has_ticket (ts t) tk \<longrightarrow> tk < N; ts l = REL tk; t < N; has_ticket ((ts(l := INIT)) t) tka\<rbrakk> \<Longrightarrow> tka < N
[PROOF STEP]
apply (metis fun_upd_apply thread.distinct(1) thread.distinct(3)
          thread.distinct(5) has_ticket_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_REL_state_simps[simp]:
    "t<N \<Longrightarrow> is_REL_state (ts(t:=REL tk))"
    "t<N \<Longrightarrow> \<not>is_REL (ts t) \<Longrightarrow> \<not>is_REL s'
      \<Longrightarrow> is_REL_state (ts(t:=s')) \<longleftrightarrow> is_REL_state ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t < N \<Longrightarrow> is_REL_state (ts(t := REL tk))) &&& (\<lbrakk>t < N; \<not> is_REL (ts t); \<not> is_REL s'\<rbrakk> \<Longrightarrow> is_REL_state (ts(t := s')) = is_REL_state ts)
[PROOF STEP]
unfolding is_REL_state_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t < N \<Longrightarrow> \<exists>ta<N. \<exists>tka. (ts(t := REL tk)) ta = REL tka) &&& (\<lbrakk>t < N; \<not> is_REL (ts t); \<not> is_REL s'\<rbrakk> \<Longrightarrow> (\<exists>ta<N. \<exists>tk. (ts(t := s')) ta = REL tk) = (\<exists>t<N. \<exists>tk. ts t = REL tk))
[PROOF STEP]
apply (auto; fail) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t < N; \<not> is_REL (ts t); \<not> is_REL s'\<rbrakk> \<Longrightarrow> (\<exists>ta<N. \<exists>tk. (ts(t := s')) ta = REL tk) = (\<exists>t<N. \<exists>tk. ts t = REL tk)
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ta tk. \<lbrakk>t < N; \<not> is_REL (ts t); \<not> is_REL s'; ta < N; ts ta = REL tk\<rbrakk> \<Longrightarrow> \<exists>ta. (ta = t \<longrightarrow> (\<exists>tk. s' = REL tk)) \<and> (ta \<noteq> t \<longrightarrow> ta < N \<and> (\<exists>tk. ts ta = REL tk))
[PROOF STEP]
by (metis thread.disc(12))


[STATEMENT]
lemma is_REL_state_aux1:
    assumes R: "B.reachable (c,n,ts)"
    assumes REL: "is_REL_state ts"
    assumes "t<N" and [simp]: "ts t = WAIT tk"
    shows "tk\<noteq>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tk \<noteq> c
[PROOF STEP]
using REL
[PROOF STATE]
proof (prove)
using this:
is_REL_state ts

goal (1 subgoal):
 1. tk \<noteq> c
[PROOF STEP]
unfolding is_REL_state_def
[PROOF STATE]
proof (prove)
using this:
\<exists>t<N. \<exists>tk. ts t = REL tk

goal (1 subgoal):
 1. tk \<noteq> c
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t tka. \<lbrakk>t < N; ts t = REL tka; tk = c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for t' tk'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' < N; ts t' = REL tk'; tk = c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using b_has_ticket_unique[OF R \<open>t<N\<close>, of tk t']
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>has_ticket (ts t) tk; t' < N; has_ticket (ts t') tk\<rbrakk> \<Longrightarrow> t' = t

goal (1 subgoal):
 1. \<lbrakk>t' < N; ts t' = REL tk'; tk = c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using b_holds_only_current[OF R, of t' tk']
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>has_ticket (ts t) tk; t' < N; has_ticket (ts t') tk\<rbrakk> \<Longrightarrow> t' = t
\<lbrakk>t' < N; locks_ticket (ts t') tk'\<rbrakk> \<Longrightarrow> tk' = c

goal (1 subgoal):
 1. \<lbrakk>t' < N; ts t' = REL tk'; tk = c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_REL_state_aux2:
    assumes R: "B.reachable (c,n,ts)"
    assumes A: "t<N" "ts t = REL tk"
    shows "\<not>is_REL_state (ts(t:=INIT))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_REL_state (ts(t := INIT))
[PROOF STEP]
using b_holds_only_current[OF R] A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t < N; locks_ticket (ts ?t) ?tk\<rbrakk> \<Longrightarrow> ?tk = c
t < N
ts t = REL tk

goal (1 subgoal):
 1. \<not> is_REL_state (ts(t := INIT))
[PROOF STEP]
using b_mutual_exclusion'[OF R]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t < N; locks_ticket (ts ?t) ?tk\<rbrakk> \<Longrightarrow> ?tk = c
t < N
ts t = REL tk
\<lbrakk>?t < N; ?t' < N; ?t \<noteq> ?t'; locks_ticket (tts (c, n, ts) ?t) ?tk; locks_ticket (tts (c, n, ts) ?t') ?tk'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> is_REL_state (ts(t := INIT))
[PROOF STEP]
apply (clarsimp simp: is_REL_state_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ta tka. \<lbrakk>\<And>t tk. \<lbrakk>t < N; locks_ticket (ts t) tk\<rbrakk> \<Longrightarrow> tk = c; t < N; ts t = REL tk; \<And>t t' tk tk'. \<lbrakk>t < N; t' < N; t \<noteq> t'; locks_ticket (ts t) tk; locks_ticket (ts t') tk'\<rbrakk> \<Longrightarrow> False; ta \<noteq> t; ta < N; ts ta = REL tka\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by fastforce


[STATEMENT]
lemma xfer_holds:
    assumes "sim_rel s cs"
    shows "is_HOLD (tts cs t) \<longleftrightarrow> is_HOLD (tts s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_HOLD (tts cs t) = is_HOLD (tts s t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sim_rel s cs

goal (1 subgoal):
 1. is_HOLD (tts cs t) = is_HOLD (tts s t)
[PROOF STEP]
unfolding sim_rel_def sim_rel1_def sim_rel2_def
[PROOF STATE]
proof (prove)
using this:
((\<lambda>(c, n, ts) (ci, ni, tsi). ci = c mod N \<and> ni = n mod (k * N) \<and> tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts) OO (\<lambda>(c, n, ts) (ci, ni, tsi). (if is_REL_state ts then ci = replicate N False else ci = (replicate N False)[c := True]) \<and> ni = n \<and> tsi = ts)) s cs

goal (1 subgoal):
 1. is_HOLD (tts cs t) = is_HOLD (tts s t)
[PROOF STEP]
by (cases "tts cs t") auto


[STATEMENT]
lemma xfer_waits:
    assumes "sim_rel s cs"
    shows "is_WAIT (tts cs t) \<longleftrightarrow> is_WAIT (tts s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_WAIT (tts cs t) = is_WAIT (tts s t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sim_rel s cs

goal (1 subgoal):
 1. is_WAIT (tts cs t) = is_WAIT (tts s t)
[PROOF STEP]
unfolding sim_rel_def sim_rel1_def sim_rel2_def
[PROOF STATE]
proof (prove)
using this:
((\<lambda>(c, n, ts) (ci, ni, tsi). ci = c mod N \<and> ni = n mod (k * N) \<and> tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts) OO (\<lambda>(c, n, ts) (ci, ni, tsi). (if is_REL_state ts then ci = replicate N False else ci = (replicate N False)[c := True]) \<and> ni = n \<and> tsi = ts)) s cs

goal (1 subgoal):
 1. is_WAIT (tts cs t) = is_WAIT (tts s t)
[PROOF STEP]
by (cases "tts cs t") auto


[STATEMENT]
lemma xfer_init:
    assumes "sim_rel s cs"
    shows "tts cs t = INIT \<longleftrightarrow> tts s t = INIT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (tts cs t = INIT) = (tts s t = INIT)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sim_rel s cs

goal (1 subgoal):
 1. (tts cs t = INIT) = (tts s t = INIT)
[PROOF STEP]
unfolding sim_rel_def sim_rel1_def sim_rel2_def
[PROOF STATE]
proof (prove)
using this:
((\<lambda>(c, n, ts) (ci, ni, tsi). ci = c mod N \<and> ni = n mod (k * N) \<and> tsi = map_ticket (\<lambda>t. t mod N) \<circ> ts) OO (\<lambda>(c, n, ts) (ci, ni, tsi). (if is_REL_state ts then ci = replicate N False else ci = (replicate N False)[c := True]) \<and> ni = n \<and> tsi = ts)) s cs

goal (1 subgoal):
 1. (tts cs t = INIT) = (tts s t = INIT)
[PROOF STEP]
by auto


[STATEMENT]
theorem final_mutual_exclusion: "\<lbrakk>C.reachable s;
      t<N; t'<N; t\<noteq>t'; is_HOLD (tts s t); is_HOLD (tts s t')
    \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C.reachable s; t < N; t' < N; t \<noteq> t'; is_HOLD (tts s t); is_HOLD (tts s t')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule sim.xfer_reachable)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>t < N; t' < N; t \<noteq> t'; is_HOLD (tts s t); is_HOLD (tts s t'); sim_rel as s; A.reachable as\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: xfer_holds)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>t < N; t' < N; t \<noteq> t'; is_HOLD (tts as t); is_HOLD (tts as t'); sim_rel as s; A.reachable as\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (erule (5) mutual_exclusion)


[STATEMENT]
theorem final_fair:
    assumes RUN: "C.is_run s"
    assumes ACQ: "t<N" and "tts (s i) t=INIT" and "is_WAIT (tts (s (Suc i)) t)"
      \<comment> \<open>Thread \<open>t\<close> draws ticket in step \<open>i\<close>\<close>
    assumes HOLD: "i<j" and "is_HOLD (tts (s j) t)"
      \<comment> \<open>Thread \<open>t\<close> holds lock in step \<open>j\<close>\<close>
    assumes WAIT: "t'<N" and "is_WAIT (tts (s i) t')"
      \<comment> \<open>Thread \<open>t'\<close> waits for lock at step \<open>i\<close>\<close>
    obtains l where "i<l" and "l<j" and "is_HOLD (tts (s l) t')"
      \<comment> \<open>Then, \<open>t'\<close> gets lock earlier\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using RUN
[PROOF STATE]
proof (prove)
using this:
C.is_run s

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule sim.xfer_run)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis; A.is_run as; \<forall>i. sim_rel (as i) (s i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix as
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis; A.is_run as; \<forall>i. sim_rel (as i) (s i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume Ra: "A.is_run as" and SIM[rule_format]: "\<forall>i. sim_rel (as i) (s i)"
[PROOF STATE]
proof (state)
this:
A.is_run as
sim_rel (as ?i) (s ?i)

goal (1 subgoal):
 1. \<And>as. \<lbrakk>\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis; A.is_run as; \<forall>i. sim_rel (as i) (s i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note XFER = xfer_init[OF SIM] xfer_holds[OF SIM] xfer_waits[OF SIM]
[PROOF STATE]
proof (state)
this:
(tts (s ?i1) ?t = INIT) = (tts (as ?i1) ?t = INIT)
is_HOLD (tts (s ?i1) ?t) = is_HOLD (tts (as ?i1) ?t)
is_WAIT (tts (s ?i1) ?t) = is_WAIT (tts (as ?i1) ?t)

goal (1 subgoal):
 1. \<And>as. \<lbrakk>\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis; A.is_run as; \<forall>i. sim_rel (as i) (s i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C.is_run s
t < N
tts (s i) t = INIT
is_WAIT (tts (s (Suc i)) t)
i < j
is_HOLD (tts (s j) t)
t' < N
is_WAIT (tts (s i) t')

goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (simp add: XFER)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C.is_run s; t < N; tts (as i) t = INIT; is_WAIT (tts (as (Suc i)) t); i < j; is_HOLD (tts (as j) t); t' < N; is_WAIT (tts (as i) t')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule (6) fair[OF Ra])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>C.is_run s; tts (as i) t = INIT; is_WAIT (tts (as (Suc i)) t); i < j; is_HOLD (tts (as j) t); t' < N; is_WAIT (tts (as i) t'); i < l; l < j; is_HOLD (tts (as l) t')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule (1) that)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>C.is_run s; tts (as i) t = INIT; is_WAIT (tts (as (Suc i)) t); i < j; is_HOLD (tts (as j) t); t' < N; is_WAIT (tts (as i) t'); l < j; is_HOLD (tts (as l) t')\<rbrakk> \<Longrightarrow> is_HOLD (tts (s l) t')
[PROOF STEP]
apply (simp add: XFER)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem final_progress:
    assumes FRUN: "C.is_fair_run s"
    assumes WAIT: "t<N" and "is_WAIT (tts (s i) t)"
    shows "\<exists>j>i. is_HOLD (tts (s j) t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
using FRUN
[PROOF STATE]
proof (prove)
using this:
C.is_fair_run s

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
proof (rule sim.xfer_fair_run)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>A.is_fair_run as; \<forall>i. sim_rel (as i) (s i)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
fix as
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>A.is_fair_run as; \<forall>i. sim_rel (as i) (s i)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
assume Ra: "A.is_fair_run as"
       and SIM[rule_format]: "\<forall>i. sim_rel (as i) (s i)"
[PROOF STATE]
proof (state)
this:
A.is_fair_run as
sim_rel (as ?i) (s ?i)

goal (1 subgoal):
 1. \<And>as. \<lbrakk>A.is_fair_run as; \<forall>i. sim_rel (as i) (s i)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
note XFER = xfer_init[OF SIM] xfer_holds[OF SIM] xfer_waits[OF SIM]
[PROOF STATE]
proof (state)
this:
(tts (s ?i1) ?t = INIT) = (tts (as ?i1) ?t = INIT)
is_HOLD (tts (s ?i1) ?t) = is_HOLD (tts (as ?i1) ?t)
is_WAIT (tts (s ?i1) ?t) = is_WAIT (tts (as ?i1) ?t)

goal (1 subgoal):
 1. \<And>as. \<lbrakk>A.is_fair_run as; \<forall>i. sim_rel (as i) (s i)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C.is_fair_run s
t < N
is_WAIT (tts (s i) t)

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
apply (simp add: XFER)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C.is_fair_run s; t < N; is_WAIT (tts (as i) t)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (as j) t)
[PROOF STEP]
apply (erule (1) progress[OF Ra])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>j>i. is_HOLD (tts (s j) t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma asymp_equivD_strong:
  assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<noteq> 0 \<or> g x \<noteq> 0) F"
  shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
f \<sim>[F] g
[PROOF STEP]
have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
[PROOF STATE]
proof (prove)
using this:
f \<sim>[F] g

goal (1 subgoal):
 1. ((\<lambda>x. if f x = (0::'b) \<and> g x = (0::'b) then 1::'b else f x / g x) \<longlongrightarrow> (1::'b)) F
[PROOF STEP]
by (rule asymp_equivD)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. if f x = (0::'b) \<and> g x = (0::'b) then 1::'b else f x / g x) \<longlongrightarrow> (1::'b)) F

goal (1 subgoal):
 1. ((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. if f x = (0::'b) \<and> g x = (0::'b) then 1::'b else f x / g x) \<longlongrightarrow> (1::'b)) F

goal (1 subgoal):
 1. ((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F
[PROOF STEP]
have "?this \<longleftrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. if f x = (0::'b) \<and> g x = (0::'b) then 1::'b else f x / g x) \<longlongrightarrow> (1::'b)) F = ((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F
[PROOF STEP]
by (intro filterlim_cong eventually_mono[OF assms(2)]) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. if f x = (0::'b) \<and> g x = (0::'b) then 1::'b else f x / g x) \<longlongrightarrow> (1::'b)) F = ((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F

goal (1 subgoal):
 1. ((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F

goal (1 subgoal):
 1. ((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f x / g x) \<longlongrightarrow> (1::'b)) F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frontier_real_Ici [simp]:
  fixes a :: real
  shows "frontier {a..} = {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frontier {a..} = {a}
[PROOF STEP]
unfolding frontier_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure {a..} - interior {a..} = {a}
[PROOF STEP]
by (auto simp: interior_real_atLeast)


[STATEMENT]
lemma sum_upto_ln_conv_sum_upto_mangoldt:
  "sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * nat \<lfloor>x / real n\<rfloor>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
have "sum_upto (\<lambda>n. ln (real n)) x =
          sum_upto (\<lambda>n. \<Sum>d | d dvd n. mangoldt d) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. \<Sum>d | d dvd n. mangoldt d) x
[PROOF STEP]
by (intro sum_upto_cong) (simp_all add: mangoldt_sum)
[PROOF STATE]
proof (state)
this:
sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. \<Sum>d | d dvd n. mangoldt d) x

goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. \<Sum>d | d dvd n. mangoldt d) x

goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
have "\<dots> = sum_upto (\<lambda>k. sum_upto (\<lambda>d. mangoldt k) (x / real k)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto (\<lambda>n. \<Sum>d | d dvd n. mangoldt d) x = sum_upto (\<lambda>k. sum_upto (\<lambda>d. mangoldt k) (x / real k)) x
[PROOF STEP]
by (rule sum_upto_sum_divisors)
[PROOF STATE]
proof (state)
this:
sum_upto (\<lambda>n. \<Sum>d | d dvd n. mangoldt d) x = sum_upto (\<lambda>k. sum_upto (\<lambda>d. mangoldt k) (x / real k)) x

goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_upto (\<lambda>n. \<Sum>d | d dvd n. mangoldt d) x = sum_upto (\<lambda>k. sum_upto (\<lambda>d. mangoldt k) (x / real k)) x

goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
have "\<dots> = sum_upto (\<lambda>n. mangoldt n * nat \<lfloor>x / real n\<rfloor>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto (\<lambda>k. sum_upto (\<lambda>d. mangoldt k) (x / real k)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
unfolding sum_upto_altdef
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<in>{0<..nat \<lfloor>x\<rfloor>}. \<Sum>d\<in>{0<..nat \<lfloor>x / real k\<rfloor>}. mangoldt k) = (\<Sum>n\<in>{0<..nat \<lfloor>x\<rfloor>}. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>))
[PROOF STEP]
by (simp add: mult_ac)
[PROOF STATE]
proof (state)
this:
sum_upto (\<lambda>k. sum_upto (\<lambda>d. mangoldt k) (x / real k)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x

goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x

goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum_upto (\<lambda>n. ln (real n)) x = sum_upto (\<lambda>n. mangoldt n * real (nat \<lfloor>x / real n\<rfloor>)) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ln_fact_conv_sum_upto_mangoldt:
  "ln (fact n) = sum_upto (\<lambda>k. mangoldt k * (n div k)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
have [simp]: "{0<..Suc n} = insert (Suc n) {0<..n}" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0<..Suc n} = insert (Suc n) {0<..n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0<..Suc ?n} = insert (Suc ?n) {0<..?n}

goal (1 subgoal):
 1. ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
have "ln (fact n) = sum_upto (\<lambda>n. ln (real n)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (fact n) = sum_upto (\<lambda>n. ln (real n)) (real n)
[PROOF STEP]
by (induction n) (auto simp: sum_upto_altdef nat_add_distrib ln_mult)
[PROOF STATE]
proof (state)
this:
ln (fact n) = sum_upto (\<lambda>n. ln (real n)) (real n)

goal (1 subgoal):
 1. ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ln (fact n) = sum_upto (\<lambda>n. ln (real n)) (real n)

goal (1 subgoal):
 1. ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
have "\<dots> = sum_upto (\<lambda>k. mangoldt k * (n div k)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto (\<lambda>n. ln (real n)) (real n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
unfolding sum_upto_ln_conv_sum_upto_mangoldt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto (\<lambda>na. mangoldt na * real (nat \<lfloor>real n / real na\<rfloor>)) (real n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
by (intro sum_upto_cong) (auto simp: floor_divide_of_nat_eq)
[PROOF STATE]
proof (state)
this:
sum_upto (\<lambda>n. ln (real n)) (real n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)

goal (1 subgoal):
 1. ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)

goal (1 subgoal):
 1. ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ln (fact n) = sum_upto (\<lambda>k. mangoldt k * real (n div k)) (real n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma powr_sum: "x \<noteq> 0 \<Longrightarrow> finite A \<Longrightarrow> x powr sum f A = (\<Prod>y\<in>A. x powr f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> (0::'a); finite A\<rbrakk> \<Longrightarrow> x powr sum f A = (\<Prod>y\<in>A. x powr f y)
[PROOF STEP]
by (simp add: powr_def exp_sum sum_distrib_right)


[STATEMENT]
lemma fds_abs_converges_comparison_test:
  fixes s :: "'a :: dirichlet_series"
  assumes "eventually (\<lambda>n. norm (fds_nth f n) \<le> fds_nth g n) at_top" and "fds_converges g (s \<bullet> 1)"
  shows   "fds_abs_converges f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
unfolding fds_abs_converges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. norm (fds_nth f n / nat_power n s))
[PROOF STEP]
proof (rule summable_comparison_test_ev)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<^sub>F n in sequentially. norm (norm (fds_nth f n / nat_power n s)) \<le> ?g n
 2. summable ?g
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
fds_converges g (s \<bullet> (1::'a))
[PROOF STEP]
show "summable (\<lambda>n. fds_nth g n / n powr (s \<bullet> 1))"
[PROOF STATE]
proof (prove)
using this:
fds_converges g (s \<bullet> (1::'a))

goal (1 subgoal):
 1. summable (\<lambda>n. fds_nth g n / real n powr (s \<bullet> (1::'a)))
[PROOF STEP]
by (auto simp: fds_converges_def)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. fds_nth g n / real n powr (s \<bullet> (1::'a)))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (norm (fds_nth f n / nat_power n s)) \<le> fds_nth g n / real n powr (s \<bullet> (1::'a))
[PROOF STEP]
from assms(1) eventually_gt_at_top[of 0]
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. norm (fds_nth f n) \<le> fds_nth g n
eventually ((<) (0::?'b1)) at_top
[PROOF STEP]
show "eventually (\<lambda>n. norm (norm (fds_nth f n / nat_power n s)) \<le>
                            fds_nth g n / real n powr (s \<bullet> 1)) at_top"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. norm (fds_nth f n) \<le> fds_nth g n
eventually ((<) (0::?'b1)) at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (norm (fds_nth f n / nat_power n s)) \<le> fds_nth g n / real n powr (s \<bullet> (1::'a))
[PROOF STEP]
by eventually_elim (auto simp: norm_divide norm_nat_power intro!: divide_right_mono)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. norm (norm (fds_nth f n / nat_power n s)) \<le> fds_nth g n / real n powr (s \<bullet> (1::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fds_converges_scaleR [intro]:
  assumes "fds_converges f s"
  shows   "fds_converges (c *\<^sub>R f) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_converges (c *\<^sub>R f) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fds_converges (c *\<^sub>R f) s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
fds_converges f s
[PROOF STEP]
have "summable (\<lambda>n. c *\<^sub>R (fds_nth f n / nat_power n s))"
[PROOF STATE]
proof (prove)
using this:
fds_converges f s

goal (1 subgoal):
 1. summable (\<lambda>n. c *\<^sub>R (fds_nth f n / nat_power n s))
[PROOF STEP]
by (intro summable_scaleR_right) (auto simp: fds_converges_def)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. c *\<^sub>R (fds_nth f n / nat_power n s))

goal (1 subgoal):
 1. fds_converges (c *\<^sub>R f) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. c *\<^sub>R (fds_nth f n / nat_power n s))

goal (1 subgoal):
 1. fds_converges (c *\<^sub>R f) s
[PROOF STEP]
have "(\<lambda>n. c *\<^sub>R (fds_nth f n / nat_power n s)) = (\<lambda>n. (c *\<^sub>R fds_nth f n / nat_power n s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. c *\<^sub>R (fds_nth f n / nat_power n s)) = (\<lambda>n. c *\<^sub>R fds_nth f n / nat_power n s)
[PROOF STEP]
by (simp add: scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. c *\<^sub>R (fds_nth f n / nat_power n s)) = (\<lambda>n. c *\<^sub>R fds_nth f n / nat_power n s)

goal (1 subgoal):
 1. fds_converges (c *\<^sub>R f) s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. c *\<^sub>R fds_nth f n / nat_power n s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. c *\<^sub>R fds_nth f n / nat_power n s)

goal (1 subgoal):
 1. fds_converges (c *\<^sub>R f) s
[PROOF STEP]
by (simp add: fds_converges_def)
[PROOF STATE]
proof (state)
this:
fds_converges (c *\<^sub>R f) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fds_abs_converges_scaleR [intro]:
  assumes "fds_abs_converges f s"
  shows   "fds_abs_converges (c *\<^sub>R f) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges (c *\<^sub>R f) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fds_abs_converges (c *\<^sub>R f) s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
fds_abs_converges f s
[PROOF STEP]
have "summable (\<lambda>n. abs c * norm (fds_nth f n / nat_power n s))"
[PROOF STATE]
proof (prove)
using this:
fds_abs_converges f s

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>c\<bar> * norm (fds_nth f n / nat_power n s))
[PROOF STEP]
by (intro summable_mult) (auto simp: fds_abs_converges_def)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. \<bar>c\<bar> * norm (fds_nth f n / nat_power n s))

goal (1 subgoal):
 1. fds_abs_converges (c *\<^sub>R f) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. \<bar>c\<bar> * norm (fds_nth f n / nat_power n s))

goal (1 subgoal):
 1. fds_abs_converges (c *\<^sub>R f) s
[PROOF STEP]
have "(\<lambda>n. abs c * norm (fds_nth f n / nat_power n s)) =
               (\<lambda>n. norm ((c *\<^sub>R fds_nth f n) / nat_power n s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<bar>c\<bar> * norm (fds_nth f n / nat_power n s)) = (\<lambda>n. norm (c *\<^sub>R fds_nth f n / nat_power n s))
[PROOF STEP]
by (simp add: norm_divide)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<bar>c\<bar> * norm (fds_nth f n / nat_power n s)) = (\<lambda>n. norm (c *\<^sub>R fds_nth f n / nat_power n s))

goal (1 subgoal):
 1. fds_abs_converges (c *\<^sub>R f) s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. norm (c *\<^sub>R fds_nth f n / nat_power n s))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. norm (c *\<^sub>R fds_nth f n / nat_power n s))

goal (1 subgoal):
 1. fds_abs_converges (c *\<^sub>R f) s
[PROOF STEP]
by (simp add: fds_abs_converges_def)
[PROOF STATE]
proof (state)
this:
fds_abs_converges (c *\<^sub>R f) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma conv_abscissa_scaleR: "conv_abscissa (scaleR c f) \<le> conv_abscissa f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conv_abscissa (c *\<^sub>R f) \<le> conv_abscissa f
[PROOF STEP]
by (rule conv_abscissa_mono) auto


[STATEMENT]
lemma abs_conv_abscissa_scaleR: "abs_conv_abscissa (scaleR c f) \<le> abs_conv_abscissa f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_conv_abscissa (c *\<^sub>R f) \<le> abs_conv_abscissa f
[PROOF STEP]
by (rule abs_conv_abscissa_mono) auto


[STATEMENT]
lemma fds_converges_mult_const_left [intro]:
  "fds_converges f s \<Longrightarrow> fds_converges (fds_const c * f) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> fds_converges (fds_const c * f) s
[PROOF STEP]
by (auto simp: fds_converges_def dest: summable_mult[of _ c])


[STATEMENT]
lemma fds_abs_converges_mult_const_left [intro]:
  "fds_abs_converges f s \<Longrightarrow> fds_abs_converges (fds_const c * f) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges f s \<Longrightarrow> fds_abs_converges (fds_const c * f) s
[PROOF STEP]
by (auto simp: fds_abs_converges_def norm_mult norm_divide dest: summable_mult[of _ "norm c"])


[STATEMENT]
lemma conv_abscissa_mult_const_left:
  "conv_abscissa (fds_const c * f) \<le> conv_abscissa f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conv_abscissa (fds_const c * f) \<le> conv_abscissa f
[PROOF STEP]
by (intro conv_abscissa_mono) auto


[STATEMENT]
lemma abs_conv_abscissa_mult_const_left:
  "abs_conv_abscissa (fds_const c * f) \<le> abs_conv_abscissa f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_conv_abscissa (fds_const c * f) \<le> abs_conv_abscissa f
[PROOF STEP]
by (intro abs_conv_abscissa_mono) auto


[STATEMENT]
lemma fds_converges_mult_const_right [intro]:
  "fds_converges f s \<Longrightarrow> fds_converges (f * fds_const c) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> fds_converges (f * fds_const c) s
[PROOF STEP]
by (auto simp: fds_converges_def dest: summable_mult2[of _ c])


[STATEMENT]
lemma fds_abs_converges_mult_const_right [intro]:
  "fds_abs_converges f s \<Longrightarrow> fds_abs_converges (f * fds_const c) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges f s \<Longrightarrow> fds_abs_converges (f * fds_const c) s
[PROOF STEP]
by (auto simp: fds_abs_converges_def norm_mult norm_divide dest: summable_mult2[of _ "norm c"])


[STATEMENT]
lemma conv_abscissa_mult_const_right:
  "conv_abscissa (f * fds_const c) \<le> conv_abscissa f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conv_abscissa (f * fds_const c) \<le> conv_abscissa f
[PROOF STEP]
by (intro conv_abscissa_mono) auto


[STATEMENT]
lemma abs_conv_abscissa_mult_const_right:
  "abs_conv_abscissa (f * fds_const c) \<le> abs_conv_abscissa f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_conv_abscissa (f * fds_const c) \<le> abs_conv_abscissa f
[PROOF STEP]
by (intro abs_conv_abscissa_mono) auto


[STATEMENT]
lemma bounded_coeffs_imp_fds_abs_converges:
  fixes s :: "'a :: dirichlet_series" and f :: "'a fds"
  assumes "Bseq (fds_nth f)" "s \<bullet> 1 > 1"
  shows   "fds_abs_converges f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bseq (fds_nth f)
1 < s \<bullet> (1::'a)
[PROOF STEP]
obtain C where C: "\<And>n. norm (fds_nth f n) \<le> C"
[PROOF STATE]
proof (prove)
using this:
Bseq (fds_nth f)
1 < s \<bullet> (1::'a)

goal (1 subgoal):
 1. (\<And>C. (\<And>n. norm (fds_nth f n) \<le> C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Bseq_def)
[PROOF STATE]
proof (state)
this:
norm (fds_nth f ?n) \<le> C

goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
proof (rule fds_abs_converges_comparison_test)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<^sub>F n in sequentially. norm (fds_nth f n) \<le> fds_nth ?g n
 2. fds_converges ?g (s \<bullet> (1::'a))
[PROOF STEP]
from \<open>s \<bullet> 1 > 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 < s \<bullet> (1::'a)
[PROOF STEP]
show "fds_converges (C *\<^sub>R fds_zeta) (s \<bullet> 1)"
[PROOF STATE]
proof (prove)
using this:
1 < s \<bullet> (1::'a)

goal (1 subgoal):
 1. fds_converges (C *\<^sub>R fds_zeta) (s \<bullet> (1::'a))
[PROOF STEP]
by (intro fds_abs_converges_imp_converges) auto
[PROOF STATE]
proof (state)
this:
fds_converges (C *\<^sub>R fds_zeta) (s \<bullet> (1::'a))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (fds_nth f n) \<le> fds_nth (C *\<^sub>R fds_zeta) n
[PROOF STEP]
from C
[PROOF STATE]
proof (chain)
picking this:
norm (fds_nth f ?n) \<le> C
[PROOF STEP]
show "eventually (\<lambda>n. norm (fds_nth f n) \<le> fds_nth (C *\<^sub>R fds_zeta) n) at_top"
[PROOF STATE]
proof (prove)
using this:
norm (fds_nth f ?n) \<le> C

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (fds_nth f n) \<le> fds_nth (C *\<^sub>R fds_zeta) n
[PROOF STEP]
by (intro always_eventually) (auto simp: fds_nth_zeta)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. norm (fds_nth f n) \<le> fds_nth (C *\<^sub>R fds_zeta) n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_coeffs_imp_fds_abs_converges':
  fixes s :: "'a :: dirichlet_series" and f :: "'a fds"
  assumes "Bseq (\<lambda>n. fds_nth f n * nat_power n s0)" "s \<bullet> 1 > 1 - s0 \<bullet> 1"
  shows   "fds_abs_converges f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
have "fds_nth (fds_shift s0 f) = (\<lambda>n. fds_nth f n * nat_power n s0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_nth (fds_shift s0 f) = (\<lambda>n. fds_nth f n * nat_power n s0)
[PROOF STEP]
by (auto simp: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
fds_nth (fds_shift s0 f) = (\<lambda>n. fds_nth f n * nat_power n s0)

goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Bseq (\<lambda>n. fds_nth f n * nat_power n s0)
1 - s0 \<bullet> (1::'a) < s \<bullet> (1::'a)
fds_nth (fds_shift s0 f) = (\<lambda>n. fds_nth f n * nat_power n s0)
[PROOF STEP]
have "Bseq (fds_nth (fds_shift s0 f))"
[PROOF STATE]
proof (prove)
using this:
Bseq (\<lambda>n. fds_nth f n * nat_power n s0)
1 - s0 \<bullet> (1::'a) < s \<bullet> (1::'a)
fds_nth (fds_shift s0 f) = (\<lambda>n. fds_nth f n * nat_power n s0)

goal (1 subgoal):
 1. Bseq (fds_nth (fds_shift s0 f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bseq (fds_nth (fds_shift s0 f))

goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
1 - s0 \<bullet> (1::'a) < s \<bullet> (1::'a)
Bseq (fds_nth (fds_shift s0 f))
[PROOF STEP]
have "fds_abs_converges (fds_shift s0 f) (s + s0)"
[PROOF STATE]
proof (prove)
using this:
1 - s0 \<bullet> (1::'a) < s \<bullet> (1::'a)
Bseq (fds_nth (fds_shift s0 f))

goal (1 subgoal):
 1. fds_abs_converges (fds_shift s0 f) (s + s0)
[PROOF STEP]
by (intro bounded_coeffs_imp_fds_abs_converges) (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
fds_abs_converges (fds_shift s0 f) (s + s0)

goal (1 subgoal):
 1. fds_abs_converges f s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fds_abs_converges (fds_shift s0 f) (s + s0)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_coeffs_imp_abs_conv_abscissa_le:
  fixes s :: "'a :: dirichlet_series" and f :: "'a fds" and c :: ereal
  assumes "Bseq (\<lambda>n. fds_nth f n * nat_power n s)" "1 - s \<bullet> 1 \<le> c"
  shows   "abs_conv_abscissa f \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_conv_abscissa f \<le> c
[PROOF STEP]
proof (rule abs_conv_abscissa_leI_weak)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. c < ereal x \<Longrightarrow> fds_abs_converges f (of_real x)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. c < ereal x \<Longrightarrow> fds_abs_converges f (of_real x)
[PROOF STEP]
assume "c < ereal x"
[PROOF STATE]
proof (state)
this:
c < ereal x

goal (1 subgoal):
 1. \<And>x. c < ereal x \<Longrightarrow> fds_abs_converges f (of_real x)
[PROOF STEP]
have "ereal (1 - s \<bullet> 1) \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ereal (1 - s \<bullet> (1::'a)) \<le> c
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
ereal (1 - s \<bullet> (1::'a)) \<le> c

goal (1 subgoal):
 1. \<And>x. c < ereal x \<Longrightarrow> fds_abs_converges f (of_real x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ereal (1 - s \<bullet> (1::'a)) \<le> c

goal (1 subgoal):
 1. \<And>x. c < ereal x \<Longrightarrow> fds_abs_converges f (of_real x)
[PROOF STEP]
have "\<dots> < ereal x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < ereal x
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
c < ereal x

goal (1 subgoal):
 1. \<And>x. c < ereal x \<Longrightarrow> fds_abs_converges f (of_real x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ereal (1 - s \<bullet> (1::'a)) < ereal x
[PROOF STEP]
have "1 - s \<bullet> 1 < ereal x"
[PROOF STATE]
proof (prove)
using this:
ereal (1 - s \<bullet> (1::'a)) < ereal x

goal (1 subgoal):
 1. ereal (1 - s \<bullet> (1::'a)) < ereal x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ereal (1 - s \<bullet> (1::'a)) < ereal x

goal (1 subgoal):
 1. \<And>x. c < ereal x \<Longrightarrow> fds_abs_converges f (of_real x)
[PROOF STEP]
thus "fds_abs_converges f (of_real x)"
[PROOF STATE]
proof (prove)
using this:
ereal (1 - s \<bullet> (1::'a)) < ereal x

goal (1 subgoal):
 1. fds_abs_converges f (of_real x)
[PROOF STEP]
by (intro bounded_coeffs_imp_fds_abs_converges'[OF assms(1)]) auto
[PROOF STATE]
proof (state)
this:
fds_abs_converges f (of_real x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_coeffs_imp_abs_conv_abscissa_le_1:
  fixes s :: "'a :: dirichlet_series" and f :: "'a fds"
  assumes "Bseq (\<lambda>n. fds_nth f n)"
  shows   "abs_conv_abscissa f \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_conv_abscissa f \<le> 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. abs_conv_abscissa f \<le> 1
[PROOF STEP]
have [simp]: "fds_nth f n * nat_power n 0 = fds_nth f n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_nth f n * nat_power n (0::'a) = fds_nth f n
[PROOF STEP]
by (cases "n = 0") auto
[PROOF STATE]
proof (state)
this:
fds_nth f ?n * nat_power ?n (0::'a) = fds_nth f ?n

goal (1 subgoal):
 1. abs_conv_abscissa f \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_conv_abscissa f \<le> 1
[PROOF STEP]
by (rule bounded_coeffs_imp_abs_conv_abscissa_le[where s = 0]) (insert assms, auto simp:)
[PROOF STATE]
proof (state)
this:
abs_conv_abscissa f \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fds_converges_altdef2:
  "fds_converges f s \<longleftrightarrow> convergent (\<lambda>N. eval_fds (fds_truncate N f) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_converges f s = convergent (\<lambda>N. eval_fds (fds_truncate N f) s)
[PROOF STEP]
unfolding fds_converges_def summable_iff_convergent' eval_fds_truncate
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent (\<lambda>n. \<Sum>n\<le>n. fds_nth f n / nat_power n s) = convergent (\<lambda>N. \<Sum>k = 1..N. fds_nth f k / nat_power k s)
[PROOF STEP]
by (auto simp: not_le intro!: convergent_cong always_eventually sum.mono_neutral_right)


[STATEMENT]
lemma tendsto_eval_fds_truncate:
  assumes "fds_converges f s"
  shows   "(\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
have "(\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s \<longleftrightarrow>
          (\<lambda>N. \<Sum>i\<le>N. fds_nth f i / nat_power i s) \<longlonglongrightarrow> eval_fds f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s = (\<lambda>N. \<Sum>i\<le>N. fds_nth f i / nat_power i s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
unfolding eval_fds_truncate
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>N. \<Sum>k = 1..N. fds_nth f k / nat_power k s) \<longlonglongrightarrow> eval_fds f s = (\<lambda>N. \<Sum>i\<le>N. fds_nth f i / nat_power i s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
by (intro filterlim_cong always_eventually allI sum.mono_neutral_left) (auto simp: not_le)
[PROOF STATE]
proof (state)
this:
(\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s = (\<lambda>N. \<Sum>i\<le>N. fds_nth f i / nat_power i s) \<longlonglongrightarrow> eval_fds f s

goal (1 subgoal):
 1. (\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s = (\<lambda>N. \<Sum>i\<le>N. fds_nth f i / nat_power i s) \<longlonglongrightarrow> eval_fds f s

goal (1 subgoal):
 1. (\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
have \<dots>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>N. \<Sum>i\<le>N. fds_nth f i / nat_power i s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fds_converges f s

goal (1 subgoal):
 1. (\<lambda>N. \<Sum>i\<le>N. fds_nth f i / nat_power i s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
by (simp add: fds_converges_iff sums_def' atLeast0AtMost)
[PROOF STATE]
proof (state)
this:
(\<lambda>N. \<Sum>i\<le>N. fds_nth f i / nat_power i s) \<longlonglongrightarrow> eval_fds f s

goal (1 subgoal):
 1. (\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s

goal (1 subgoal):
 1. (\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>N. eval_fds (fds_truncate N f) s) \<longlonglongrightarrow> eval_fds f s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linepath_translate_left: "linepath (c + a) (c + a) = (\<lambda>x. c + a) \<circ> linepath a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linepath (c + a) (c + a) = (\<lambda>x. c + a) \<circ> linepath a b
[PROOF STEP]
by (auto simp: fun_eq_iff linepath_def algebra_simps)


[STATEMENT]
lemma integrable_on_affinity:
  assumes "m \<noteq> 0" "f integrable_on (cbox a b)"
  shows   "(\<lambda>x. f (m *\<^sub>R x + c)) integrable_on ((\<lambda>x. (1 / m) *\<^sub>R x - ((1 / m) *\<^sub>R c)) ` cbox a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f (m *\<^sub>R x + c)) integrable_on (\<lambda>x. (1 / m) *\<^sub>R x - (1 / m) *\<^sub>R c) ` cbox a b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. f (m *\<^sub>R x + c)) integrable_on (\<lambda>x. (1 / m) *\<^sub>R x - (1 / m) *\<^sub>R c) ` cbox a b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
m \<noteq> 0
f integrable_on cbox a b
[PROOF STEP]
obtain I where "(f has_integral I) (cbox a b)"
[PROOF STATE]
proof (prove)
using this:
m \<noteq> 0
f integrable_on cbox a b

goal (1 subgoal):
 1. (\<And>I. (f has_integral I) (cbox a b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: integrable_on_def)
[PROOF STATE]
proof (state)
this:
(f has_integral I) (cbox a b)

goal (1 subgoal):
 1. (\<lambda>x. f (m *\<^sub>R x + c)) integrable_on (\<lambda>x. (1 / m) *\<^sub>R x - (1 / m) *\<^sub>R c) ` cbox a b
[PROOF STEP]
from has_integral_affinity[OF this assms(1), of c]
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R I) ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R I) ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)

goal (1 subgoal):
 1. (\<lambda>x. f (m *\<^sub>R x + c)) integrable_on (\<lambda>x. (1 / m) *\<^sub>R x - (1 / m) *\<^sub>R c) ` cbox a b
[PROOF STEP]
by (auto simp: integrable_on_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f (m *\<^sub>R x + c)) integrable_on (\<lambda>x. (1 / m) *\<^sub>R x - (1 / m) *\<^sub>R c) ` cbox a b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_integral_cmul_iff:
  assumes "c \<noteq> 0"
  shows   "((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R I)) A \<longleftrightarrow> (f has_integral I) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. c *\<^sub>R f x) has_integral c *\<^sub>R I) A = (f has_integral I) A
[PROOF STEP]
using assms has_integral_cmul[of f I A c]
        has_integral_cmul[of "\<lambda>x. c *\<^sub>R f x" "c *\<^sub>R I" A "inverse c"]
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
(f has_integral I) A \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral c *\<^sub>R I) A
((\<lambda>x. c *\<^sub>R f x) has_integral c *\<^sub>R I) A \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x /\<^sub>R c) has_integral c *\<^sub>R I /\<^sub>R c) A

goal (1 subgoal):
 1. ((\<lambda>x. c *\<^sub>R f x) has_integral c *\<^sub>R I) A = (f has_integral I) A
[PROOF STEP]
by (auto simp: field_simps)


[STATEMENT]
lemma has_integral_affinity':
  fixes a :: "'a::euclidean_space"
  assumes "(f has_integral i) (cbox a b)" and "m > 0"
  shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral (i /\<^sub>R m ^ DIM('a)))
           (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
proof (cases "cbox a b = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cbox a b = {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
 2. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
cbox a b = {}

goal (2 subgoals):
 1. cbox a b = {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
 2. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
hence "(cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) = {}"
[PROOF STATE]
proof (prove)
using this:
cbox a b = {}

goal (1 subgoal):
 1. cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m) = {}
[PROOF STEP]
using \<open>m > 0\<close>
[PROOF STATE]
proof (prove)
using this:
cbox a b = {}
0 < m

goal (1 subgoal):
 1. cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m) = {}
[PROOF STEP]
unfolding box_eq_empty
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>Basis. b \<bullet> i < a \<bullet> i
0 < m

goal (1 subgoal):
 1. \<exists>i\<in>Basis. ((b - c) /\<^sub>R m) \<bullet> i < ((a - c) /\<^sub>R m) \<bullet> i
[PROOF STEP]
by (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m) = {}

goal (2 subgoals):
 1. cbox a b = {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
 2. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
with True and assms
[PROOF STATE]
proof (chain)
picking this:
cbox a b = {}
(f has_integral i) (cbox a b)
0 < m
cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cbox a b = {}
(f has_integral i) (cbox a b)
0 < m
cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m) = {}

goal (1 subgoal):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))

goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
cbox a b \<noteq> {}

goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
have "((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i)
          ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i) ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f has_integral i) (cbox a b)
0 < m

goal (1 subgoal):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i) ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)
[PROOF STEP]
by (intro has_integral_affinity) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i) ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)

goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i) ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)

goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
have "((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b) =
               ((\<lambda>x.  - ((1 / m) *\<^sub>R c) + x) ` (\<lambda>x. (1 / m) *\<^sub>R x) ` cbox a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b = (+) (- ((1 / m) *\<^sub>R c)) ` (*\<^sub>R) (1 / m) ` cbox a b
[PROOF STEP]
by (simp add: image_image algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b = (+) (- ((1 / m) *\<^sub>R c)) ` (*\<^sub>R) (1 / m) ` cbox a b

goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b = (+) (- ((1 / m) *\<^sub>R c)) ` (*\<^sub>R) (1 / m) ` cbox a b

goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
have "(\<lambda>x. (1 / m) *\<^sub>R x) ` cbox a b = cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*\<^sub>R) (1 / m) ` cbox a b = cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b)
[PROOF STEP]
using \<open>m > 0\<close> False
[PROOF STATE]
proof (prove)
using this:
0 < m
cbox a b \<noteq> {}

goal (1 subgoal):
 1. (*\<^sub>R) (1 / m) ` cbox a b = cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b)
[PROOF STEP]
by (subst image_smult_cbox) simp_all
[PROOF STATE]
proof (state)
this:
(*\<^sub>R) (1 / m) ` cbox a b = cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b)

goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(*\<^sub>R) (1 / m) ` cbox a b = cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b)

goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
have "(\<lambda>x. - ((1 / m) *\<^sub>R c) + x) ` \<dots> = cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (+) (- ((1 / m) *\<^sub>R c)) ` cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b) = cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)
[PROOF STEP]
by (subst cbox_translation [symmetric]) (simp add: field_simps vector_add_divide_simps)
[PROOF STATE]
proof (state)
this:
(+) (- ((1 / m) *\<^sub>R c)) ` cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b) = cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)

goal (1 subgoal):
 1. cbox a b \<noteq> {} \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))

goal (1 subgoal):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
using \<open>m > 0\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
0 < m

goal (1 subgoal):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral i /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_integral_affinity_iff:
  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: real_normed_vector"
  assumes "m > 0"
  shows   "((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (I /\<^sub>R m ^ DIM('a)))
               (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) \<longleftrightarrow>
           (f has_integral I) (cbox a b)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) = (f has_integral I) (cbox a b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) \<Longrightarrow> (f has_integral I) (cbox a b)
 2. (f has_integral I) (cbox a b) \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))

goal (2 subgoals):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) \<Longrightarrow> (f has_integral I) (cbox a b)
 2. (f has_integral I) (cbox a b) \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
from has_integral_affinity'[OF this, of "1 / m" "-c /\<^sub>R m"] and \<open>m > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < 1 / m \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R ((1 / m) *\<^sub>R x + - c /\<^sub>R m) + c)) has_integral I /\<^sub>R m ^ DIM('a) /\<^sub>R (1 / m) ^ DIM('a)) (cbox (((a - c) /\<^sub>R m - - c /\<^sub>R m) /\<^sub>R (1 / m)) (((b - c) /\<^sub>R m - - c /\<^sub>R m) /\<^sub>R (1 / m)))
0 < m
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
0 < 1 / m \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R ((1 / m) *\<^sub>R x + - c /\<^sub>R m) + c)) has_integral I /\<^sub>R m ^ DIM('a) /\<^sub>R (1 / m) ^ DIM('a)) (cbox (((a - c) /\<^sub>R m - - c /\<^sub>R m) /\<^sub>R (1 / m)) (((b - c) /\<^sub>R m - - c /\<^sub>R m) /\<^sub>R (1 / m)))
0 < m

goal (1 subgoal):
 1. (f has_integral I) (cbox a b)
[PROOF STEP]
by (simp add: vector_add_divide_simps) (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(f has_integral I) (cbox a b)

goal (1 subgoal):
 1. (f has_integral I) (cbox a b) \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f has_integral I) (cbox a b) \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
(f has_integral I) (cbox a b)

goal (1 subgoal):
 1. (f has_integral I) (cbox a b) \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
from has_integral_affinity'[OF this, of m c] and \<open>m > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < m \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
0 < m
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
0 < m \<Longrightarrow> ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
0 < m

goal (1 subgoal):
 1. ((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (m *\<^sub>R x + c)) has_integral I /\<^sub>R m ^ DIM('a)) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))

goal:
No subgoals!
[PROOF STEP]
qed