[STATEMENT]
lemma wp2_aux[rule_format]: "wellformed_policy2 (xs @ [x]) \<longrightarrow>
                             wellformed_policy2 xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_policy2 (xs @ [x]) \<longrightarrow> wellformed_policy2 xs
[PROOF STEP]
apply (induct xs, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. wellformed_policy2 (xs @ [x]) \<longrightarrow> wellformed_policy2 xs \<Longrightarrow> wellformed_policy2 (a # xs @ [x]) \<longrightarrow> wellformed_policy2 (a # xs)
[PROOF STEP]
subgoal for a xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_policy2 (xs @ [x]) \<longrightarrow> wellformed_policy2 xs \<Longrightarrow> wellformed_policy2 (a # xs @ [x]) \<longrightarrow> wellformed_policy2 (a # xs)
[PROOF STEP]
apply (case_tac "a", simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma DA_is_deny:
  "x \<in> dom (C (DenyAllFromTo a b \<oplus> DenyAllFromTo b a \<oplus> DenyAllFromTo a b)) \<Longrightarrow>
   C (DenyAllFromTo a b\<oplus>DenyAllFromTo b a \<oplus> DenyAllFromTo a b) x = Some (deny ())"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> dom (C (DenyAllFromTo a b \<oplus> DenyAllFromTo b a \<oplus> DenyAllFromTo a b)) \<Longrightarrow> C (DenyAllFromTo a b \<oplus> DenyAllFromTo b a \<oplus> DenyAllFromTo a b) x = \<lfloor>deny ()\<rfloor>
[PROOF STEP]
apply (case_tac "x \<in> dom (C (DenyAllFromTo a b))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> dom (C (DenyAllFromTo a b \<oplus> DenyAllFromTo b a \<oplus> DenyAllFromTo a b)); x \<in> dom (C (DenyAllFromTo a b))\<rbrakk> \<Longrightarrow> C (DenyAllFromTo a b \<oplus> DenyAllFromTo b a \<oplus> DenyAllFromTo a b) x = \<lfloor>deny ()\<rfloor>
 2. \<lbrakk>x \<in> dom (C (DenyAllFromTo a b \<oplus> DenyAllFromTo b a \<oplus> DenyAllFromTo a b)); x \<notin> dom (C (DenyAllFromTo a b))\<rbrakk> \<Longrightarrow> C (DenyAllFromTo a b \<oplus> DenyAllFromTo b a \<oplus> DenyAllFromTo a b) x = \<lfloor>deny ()\<rfloor>
[PROOF STEP]
apply (simp_all add: PLemmas)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<exists>y. (case case if (\<exists>xa\<in>a. fst (snd x) \<in> xa) \<and> (\<exists>xa\<in>b. fst (snd (snd x)) \<in> xa) then D\<^sub>U x else \<bottom> of \<bottom> \<Rightarrow> if Bex b ((\<in>) (fst (snd x))) \<and> Bex a ((\<in>) (fst (snd (snd x)))) then D\<^sub>U x else \<bottom> | \<lfloor>x\<rfloor> \<Rightarrow> \<lfloor>x\<rfloor> of \<bottom> \<Rightarrow> if Bex a ((\<in>) (fst (snd x))) \<and> Bex b ((\<in>) (fst (snd (snd x)))) then D\<^sub>U x else \<bottom> | \<lfloor>x\<rfloor> \<Rightarrow> \<lfloor>x\<rfloor>) = \<lfloor>y\<rfloor>; \<exists>y. (if (\<exists>xa\<in>a. fst (snd x) \<in> xa) \<and> (\<exists>xa\<in>b. fst (snd (snd x)) \<in> xa) then D\<^sub>U x else \<bottom>) = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> ((\<forall>xa\<in>b. fst (snd x) \<notin> xa) \<longrightarrow> Bex a ((\<in>) (fst (snd x))) \<and> Bex b ((\<in>) (fst (snd (snd x))))) \<and> ((\<forall>xa\<in>a. fst (snd (snd x)) \<notin> xa) \<longrightarrow> Bex a ((\<in>) (fst (snd x))) \<and> Bex b ((\<in>) (fst (snd (snd x)))))
 2. \<lbrakk>\<exists>y. (case if (\<exists>xa\<in>b. fst (snd x) \<in> xa) \<and> (\<exists>xa\<in>a. fst (snd (snd x)) \<in> xa) then D\<^sub>U x else \<bottom> of \<bottom> \<Rightarrow> if Bex a ((\<in>) (fst (snd x))) \<and> Bex b ((\<in>) (fst (snd (snd x)))) then D\<^sub>U x else \<bottom> | \<lfloor>x\<rfloor> \<Rightarrow> \<lfloor>x\<rfloor>) = \<lfloor>y\<rfloor>; (if (\<exists>xa\<in>a. fst (snd x) \<in> xa) \<and> (\<exists>xa\<in>b. fst (snd (snd x)) \<in> xa) then D\<^sub>U x else \<bottom>) = \<bottom>\<rbrakk> \<Longrightarrow> Bex b ((\<in>) (fst (snd x))) \<and> Bex a ((\<in>) (fst (snd (snd x))))
[PROOF STEP]
apply (simp_all split: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma after_is_state_is_in_language :
  assumes "q \<in> states M"
  and     "is_in_language M q io"
  shows "FSM.after M q io \<in> states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. after M q io \<in> FSM.states M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> FSM.states M
is_in_language M q io

goal (1 subgoal):
 1. after M q io \<in> FSM.states M
[PROOF STEP]
proof (induction io arbitrary: q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>q \<in> FSM.states M; is_in_language M q []\<rbrakk> \<Longrightarrow> after M q [] \<in> FSM.states M
 2. \<And>a io q. \<lbrakk>\<And>q. \<lbrakk>q \<in> FSM.states M; is_in_language M q io\<rbrakk> \<Longrightarrow> after M q io \<in> FSM.states M; q \<in> FSM.states M; is_in_language M q (a # io)\<rbrakk> \<Longrightarrow> after M q (a # io) \<in> FSM.states M
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
q \<in> FSM.states M
is_in_language M q []

goal (2 subgoals):
 1. \<And>q. \<lbrakk>q \<in> FSM.states M; is_in_language M q []\<rbrakk> \<Longrightarrow> after M q [] \<in> FSM.states M
 2. \<And>a io q. \<lbrakk>\<And>q. \<lbrakk>q \<in> FSM.states M; is_in_language M q io\<rbrakk> \<Longrightarrow> after M q io \<in> FSM.states M; q \<in> FSM.states M; is_in_language M q (a # io)\<rbrakk> \<Longrightarrow> after M q (a # io) \<in> FSM.states M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> FSM.states M
is_in_language M q []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q \<in> FSM.states M
is_in_language M q []

goal (1 subgoal):
 1. after M q [] \<in> FSM.states M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
after M q [] \<in> FSM.states M

goal (1 subgoal):
 1. \<And>a io q. \<lbrakk>\<And>q. \<lbrakk>q \<in> FSM.states M; is_in_language M q io\<rbrakk> \<Longrightarrow> after M q io \<in> FSM.states M; q \<in> FSM.states M; is_in_language M q (a # io)\<rbrakk> \<Longrightarrow> after M q (a # io) \<in> FSM.states M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a io q. \<lbrakk>\<And>q. \<lbrakk>q \<in> FSM.states M; is_in_language M q io\<rbrakk> \<Longrightarrow> after M q io \<in> FSM.states M; q \<in> FSM.states M; is_in_language M q (a # io)\<rbrakk> \<Longrightarrow> after M q (a # io) \<in> FSM.states M
[PROOF STEP]
case (Cons a io)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<in> FSM.states M; is_in_language M ?q io\<rbrakk> \<Longrightarrow> after M ?q io \<in> FSM.states M
q \<in> FSM.states M
is_in_language M q (a # io)

goal (1 subgoal):
 1. \<And>a io q. \<lbrakk>\<And>q. \<lbrakk>q \<in> FSM.states M; is_in_language M q io\<rbrakk> \<Longrightarrow> after M q io \<in> FSM.states M; q \<in> FSM.states M; is_in_language M q (a # io)\<rbrakk> \<Longrightarrow> after M q (a # io) \<in> FSM.states M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?q \<in> FSM.states M; is_in_language M ?q io\<rbrakk> \<Longrightarrow> after M ?q io \<in> FSM.states M
q \<in> FSM.states M
is_in_language M q (a # io)
[PROOF STEP]
obtain x y where "a = (x,y)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> FSM.states M; is_in_language M ?q io\<rbrakk> \<Longrightarrow> after M ?q io \<in> FSM.states M
q \<in> FSM.states M
is_in_language M q (a # io)

goal (1 subgoal):
 1. (\<And>x y. a = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> FSM.states M; is_in_language M ?q io\<rbrakk> \<Longrightarrow> after M ?q io \<in> FSM.states M
q \<in> FSM.states M
is_in_language M q (a # io)
(\<And>x1 x2. ?y = (x1, x2) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>x y. a = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a = (x, y)

goal (1 subgoal):
 1. \<And>a io q. \<lbrakk>\<And>q. \<lbrakk>q \<in> FSM.states M; is_in_language M q io\<rbrakk> \<Longrightarrow> after M q io \<in> FSM.states M; q \<in> FSM.states M; is_in_language M q (a # io)\<rbrakk> \<Longrightarrow> after M q (a # io) \<in> FSM.states M
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. after M q (a # io) \<in> FSM.states M
[PROOF STEP]
using \<open>is_in_language M q (a # io)\<close> Cons.IH[OF h_obs_state[of M q x y]]
[PROOF STATE]
proof (prove)
using this:
is_in_language M q (a # io)
\<lbrakk>FSM.h_obs M q x y = Some ?q; is_in_language M ?q io\<rbrakk> \<Longrightarrow> after M ?q io \<in> FSM.states M

goal (1 subgoal):
 1. after M q (a # io) \<in> FSM.states M
[PROOF STEP]
unfolding \<open>a = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
is_in_language M q ((x, y) # io)
\<lbrakk>FSM.h_obs M q x y = Some ?q; is_in_language M ?q io\<rbrakk> \<Longrightarrow> after M ?q io \<in> FSM.states M

goal (1 subgoal):
 1. after M q ((x, y) # io) \<in> FSM.states M
[PROOF STEP]
unfolding after.simps is_in_language.simps
[PROOF STATE]
proof (prove)
using this:
case FSM.h_obs M q x y of None \<Rightarrow> False | Some q' \<Rightarrow> is_in_language M q' io
\<lbrakk>FSM.h_obs M q x y = Some ?q; is_in_language M ?q io\<rbrakk> \<Longrightarrow> after M ?q io \<in> FSM.states M

goal (1 subgoal):
 1. after M (the (FSM.h_obs M q x y)) io \<in> FSM.states M
[PROOF STEP]
by (metis option.case_eq_if option.exhaust_sel)
[PROOF STATE]
proof (state)
this:
after M q (a # io) \<in> FSM.states M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prm_set_unit_action:
  assumes "a \<in> S" and "b \<notin> S"
  shows "[a \<leftrightarrow> b] {$} S = S - {a} \<union> {b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a \<leftrightarrow> b] {$} S = S - {a} \<union> {b}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [a \<leftrightarrow> b] {$} S \<subseteq> S - {a} \<union> {b}
 2. S - {a} \<union> {b} \<subseteq> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
show "[a \<leftrightarrow> b] {$} S \<subseteq> S - {a} \<union> {b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a \<leftrightarrow> b] {$} S \<subseteq> S - {a} \<union> {b}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> [a \<leftrightarrow> b] {$} S \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> [a \<leftrightarrow> b] {$} S \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
assume H: "x \<in> [a \<leftrightarrow> b] {$} S"
[PROOF STATE]
proof (state)
this:
x \<in> [a \<leftrightarrow> b] {$} S

goal (1 subgoal):
 1. \<And>x. x \<in> [a \<leftrightarrow> b] {$} S \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
obtain y where "x = [a \<leftrightarrow> b] $ y"
[PROOF STATE]
proof (prove)
using this:
x \<in> [a \<leftrightarrow> b] {$} S

goal (1 subgoal):
 1. (\<And>y. x = [a \<leftrightarrow> b] $ y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding prm_set_def
[PROOF STATE]
proof (prove)
using this:
x \<in> ($) [a \<leftrightarrow> b] ` S

goal (1 subgoal):
 1. (\<And>y. x = [a \<leftrightarrow> b] $ y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using imageE
[PROOF STATE]
proof (prove)
using this:
x \<in> ($) [a \<leftrightarrow> b] ` S
\<lbrakk>?b \<in> ?f ` ?A; \<And>x. \<lbrakk>?b = ?f x; x \<in> ?A\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>y. x = [a \<leftrightarrow> b] $ y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x = [a \<leftrightarrow> b] $ y

goal (1 subgoal):
 1. \<And>x. x \<in> [a \<leftrightarrow> b] {$} S \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
hence "y \<in> S"
[PROOF STATE]
proof (prove)
using this:
x = [a \<leftrightarrow> b] $ y

goal (1 subgoal):
 1. y \<in> S
[PROOF STEP]
using H inj_image_mem_iff prm_apply_injective prm_set_def
[PROOF STATE]
proof (prove)
using this:
x = [a \<leftrightarrow> b] $ y
x \<in> [a \<leftrightarrow> b] {$} S
inj ?f \<Longrightarrow> (?f ?a \<in> ?f ` ?A) = (?a \<in> ?A)
inj (($) ?\<pi>)
?\<pi> {$} ?S \<equiv> ($) ?\<pi> ` ?S

goal (1 subgoal):
 1. y \<in> S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
y \<in> S

goal (1 subgoal):
 1. \<And>x. x \<in> [a \<leftrightarrow> b] {$} S \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
hence "y \<noteq> b"
[PROOF STATE]
proof (prove)
using this:
y \<in> S

goal (1 subgoal):
 1. y \<noteq> b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> S
a \<in> S
b \<notin> S

goal (1 subgoal):
 1. y \<noteq> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<noteq> b

goal (1 subgoal):
 1. \<And>x. x \<in> [a \<leftrightarrow> b] {$} S \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
consider "y = a" | "y \<noteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y = a \<Longrightarrow> thesis; y \<noteq> a \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>y = a \<Longrightarrow> ?thesis; y \<noteq> a \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x. x \<in> [a \<leftrightarrow> b] {$} S \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
thus "x \<in> S - {a} \<union> {b}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>y = a \<Longrightarrow> ?thesis; y \<noteq> a \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. x \<in> S - {a} \<union> {b}
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = a \<Longrightarrow> x \<in> S - {a} \<union> {b}
 2. y \<noteq> a \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
y = a

goal (2 subgoals):
 1. y = a \<Longrightarrow> x \<in> S - {a} \<union> {b}
 2. y \<noteq> a \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
hence "x = b"
[PROOF STATE]
proof (prove)
using this:
y = a

goal (1 subgoal):
 1. x = b
[PROOF STEP]
using \<open>x = [a \<leftrightarrow> b] $ y\<close>
[PROOF STATE]
proof (prove)
using this:
y = a
x = [a \<leftrightarrow> b] $ y

goal (1 subgoal):
 1. x = b
[PROOF STEP]
using prm_unit_action
[PROOF STATE]
proof (prove)
using this:
y = a
x = [a \<leftrightarrow> b] $ y
[?a \<leftrightarrow> ?b] $ ?a = ?b

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

goal (2 subgoals):
 1. y = a \<Longrightarrow> x \<in> S - {a} \<union> {b}
 2. y \<noteq> a \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = b

goal (1 subgoal):
 1. x \<in> S - {a} \<union> {b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> S - {a} \<union> {b}

goal (1 subgoal):
 1. y \<noteq> a \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> a \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
y \<noteq> a

goal (1 subgoal):
 1. y \<noteq> a \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
hence "x = y"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> a

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using \<open>x = [a \<leftrightarrow> b] $ y\<close>
[PROOF STATE]
proof (prove)
using this:
y \<noteq> a
x = [a \<leftrightarrow> b] $ y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using prm_unit_inaction \<open>y \<noteq> b\<close>
[PROOF STATE]
proof (prove)
using this:
y \<noteq> a
x = [a \<leftrightarrow> b] $ y
\<lbrakk>?x \<noteq> ?a; ?x \<noteq> ?b\<rbrakk> \<Longrightarrow> [?a \<leftrightarrow> ?b] $ ?x = ?x
y \<noteq> b

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

goal (1 subgoal):
 1. y \<noteq> a \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
hence "x \<in> S" and "x \<noteq> a"
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. x \<in> S &&& x \<noteq> a
[PROOF STEP]
using \<open>y \<in> S\<close> \<open>y \<noteq> a\<close>
[PROOF STATE]
proof (prove)
using this:
x = y
y \<in> S
y \<noteq> a

goal (1 subgoal):
 1. x \<in> S &&& x \<noteq> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> S
x \<noteq> a

goal (1 subgoal):
 1. y \<noteq> a \<Longrightarrow> x \<in> S - {a} \<union> {b}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> S
x \<noteq> a

goal (1 subgoal):
 1. x \<in> S - {a} \<union> {b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> S - {a} \<union> {b}

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> S - {a} \<union> {b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[a \<leftrightarrow> b] {$} S \<subseteq> S - {a} \<union> {b}

goal (1 subgoal):
 1. S - {a} \<union> {b} \<subseteq> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
show "S - {a} \<union> {b} \<subseteq> [a \<leftrightarrow> b] {$} S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - {a} \<union> {b} \<subseteq> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S - {a} \<union> {b} \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S - {a} \<union> {b} \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
assume H: "x \<in> S - {a} \<union> {b}"
[PROOF STATE]
proof (state)
this:
x \<in> S - {a} \<union> {b}

goal (1 subgoal):
 1. \<And>x. x \<in> S - {a} \<union> {b} \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
hence "x \<noteq> a"
[PROOF STATE]
proof (prove)
using this:
x \<in> S - {a} \<union> {b}

goal (1 subgoal):
 1. x \<noteq> a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> S - {a} \<union> {b}
a \<in> S
b \<notin> S

goal (1 subgoal):
 1. x \<noteq> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> a

goal (1 subgoal):
 1. \<And>x. x \<in> S - {a} \<union> {b} \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
consider "x = b" | "x \<noteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = b \<Longrightarrow> thesis; x \<noteq> b \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = b \<Longrightarrow> ?thesis; x \<noteq> b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x. x \<in> S - {a} \<union> {b} \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
thus "x \<in> [a \<leftrightarrow> b] {$} S"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = b \<Longrightarrow> ?thesis; x \<noteq> b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
 2. x \<noteq> b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x = b

goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
 2. x \<noteq> b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
hence "x = [a \<leftrightarrow> b] $ a"
[PROOF STATE]
proof (prove)
using this:
x = b

goal (1 subgoal):
 1. x = [a \<leftrightarrow> b] $ a
[PROOF STEP]
using prm_unit_action
[PROOF STATE]
proof (prove)
using this:
x = b
[?a \<leftrightarrow> ?b] $ ?a = ?b

goal (1 subgoal):
 1. x = [a \<leftrightarrow> b] $ a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x = [a \<leftrightarrow> b] $ a

goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
 2. x \<noteq> b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = [a \<leftrightarrow> b] $ a

goal (1 subgoal):
 1. x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
using \<open>a \<in> S\<close> prm_set_membership
[PROOF STATE]
proof (prove)
using this:
x = [a \<leftrightarrow> b] $ a
a \<in> S
?x \<in> ?S \<Longrightarrow> ?\<pi> $ ?x \<in> ?\<pi> {$} ?S

goal (1 subgoal):
 1. x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x \<in> [a \<leftrightarrow> b] {$} S

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
x \<noteq> b

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
hence "x \<in> S"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> b

goal (1 subgoal):
 1. x \<in> S
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
x \<noteq> b
x \<in> S - {a} \<union> {b}

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

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> S

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
have "x = [a \<leftrightarrow> b] $ x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = [a \<leftrightarrow> b] $ x
[PROOF STEP]
using prm_unit_inaction \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<noteq> ?a; ?x \<noteq> ?b\<rbrakk> \<Longrightarrow> [?a \<leftrightarrow> ?b] $ ?x = ?x
x \<noteq> a
x \<noteq> b

goal (1 subgoal):
 1. x = [a \<leftrightarrow> b] $ x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x = [a \<leftrightarrow> b] $ x

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> S
x = [a \<leftrightarrow> b] $ x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> S
x = [a \<leftrightarrow> b] $ x

goal (1 subgoal):
 1. x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
using prm_set_membership
[PROOF STATE]
proof (prove)
using this:
x \<in> S
x = [a \<leftrightarrow> b] $ x
?x \<in> ?S \<Longrightarrow> ?\<pi> $ ?x \<in> ?\<pi> {$} ?S

goal (1 subgoal):
 1. x \<in> [a \<leftrightarrow> b] {$} S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x \<in> [a \<leftrightarrow> b] {$} S

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> [a \<leftrightarrow> b] {$} S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S - {a} \<union> {b} \<subseteq> [a \<leftrightarrow> b] {$} S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma may_acquire_all_has_locks_acquire_locks [simp]:
  fixes ln
  shows "\<lbrakk> may_acquire_all ls t ln; t \<noteq> t' \<rbrakk> \<Longrightarrow> has_locks (acquire_locks (ls $ l) t (ln $ l)) t' = has_locks (ls $ l) t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>may_acquire_all ls t ln; t \<noteq> t'\<rbrakk> \<Longrightarrow> has_locks (acquire_locks (ls $ l) t (ln $ l)) t' = has_locks (ls $ l) t'
[PROOF STEP]
by(cases "ln $ l > 0")(auto dest: may_acquire_allD)


[STATEMENT]
lemma Keys_to_list_map_key_PP:
  "pp_pm.punit.Keys_to_list (map (Poly_Mapping.map_key PP) fs) = map mapping_of (punit.Keys_to_list fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pp_pm.punit.Keys_to_list (map (Poly_Mapping.map_key PP) fs) = map pp.mapping_of (punit.Keys_to_list fs)
[PROOF STEP]
by (simp add: punit.Keys_to_list_eq_pps_to_list pp_pm.punit.Keys_to_list_eq_pps_to_list
          map_mapping_of_pps_to_list Keys_def image_UN keys_map_key_PP)


[STATEMENT]
lemma (in is_cat_obj_coprod) is_cat_obj_prod_op:
  "op_ntcf \<pi> : U <\<^sub>C\<^sub>F\<^sub>.\<^sub>\<Prod> A : I \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<pi> : U <\<^sub>C\<^sub>F\<^sub>.\<^sub>\<Prod> A : I \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<CC>
[PROOF STEP]
using cf_discrete_vdomain_vsubset_Vset
[PROOF STATE]
proof (prove)
using this:
I \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. op_ntcf \<pi> : U <\<^sub>C\<^sub>F\<^sub>.\<^sub>\<Prod> A : I \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<CC>
[PROOF STEP]
by (intro is_cat_obj_prodI)
    (
      cs_concl cs_shallow
        cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros
    )


[STATEMENT]
lemma (in is_cat_obj_coprod_2) is_cat_obj_prod_2_op:
  "op_ntcf \<pi> : P <\<^sub>C\<^sub>F\<^sub>.\<^sub>\<times> {a,b} : 2\<^sub>C \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<pi> : P <\<^sub>C\<^sub>F\<^sub>.\<^sub>\<times> {a,b} : 2\<^sub>C \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<CC>
[PROOF STEP]
by (rule is_cat_obj_prod_2I[OF is_cat_obj_prod_op])


[STATEMENT]
lemma zeta_tail_bigo:
  fixes s :: real
  assumes s: "s > 1"
  shows   "(\<lambda>n. Re (hurwitz_zeta (real n + 1) s)) \<in> O(\<lambda>x. real x powr (1 - s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. Re (hurwitz_zeta (real n + 1) (complex_of_real s))) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. Re (hurwitz_zeta (real n + 1) (complex_of_real s))) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
have [simp]: "complex_of_real (Re (zeta s)) = zeta s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real (Re (zeta (complex_of_real s))) = zeta (complex_of_real s)
[PROOF STEP]
using zeta_real[of s]
[PROOF STATE]
proof (prove)
using this:
zeta (complex_of_real s) \<in> \<real>

goal (1 subgoal):
 1. complex_of_real (Re (zeta (complex_of_real s))) = zeta (complex_of_real s)
[PROOF STEP]
by (auto elim!: Reals_cases)
[PROOF STATE]
proof (state)
this:
complex_of_real (Re (zeta (complex_of_real s))) = zeta (complex_of_real s)

goal (1 subgoal):
 1. (\<lambda>n. Re (hurwitz_zeta (real n + 1) (complex_of_real s))) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
1 < s
[PROOF STEP]
have s': "s > 0" "s \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
1 < s

goal (1 subgoal):
 1. 0 < s &&& s \<noteq> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < s
s \<noteq> 1

goal (1 subgoal):
 1. (\<lambda>n. Re (hurwitz_zeta (real n + 1) (complex_of_real s))) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
have "(\<lambda>n. -Re (hurwitz_zeta (real n + 1) s) - real n powr (1 - s) / (1 - s)
              + real n powr (1 - s) / (1 - s))
          \<in> O(\<lambda>x. real x powr (1 - s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) + real n powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
proof (rule sum_in_bigo)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. - Re (hurwitz_zeta (real x + 1) (complex_of_real s)) - real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
 2. (\<lambda>x. real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
have "(\<lambda>n. -Re (hurwitz_zeta (real n + 1) s) - real n powr (1 - s) / (1 - s)) =
            (\<lambda>n. (\<Sum>k=1..n. real k powr -s) - real n powr (1 - s) / (1 - s) - Re (zeta s))"
      (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s)) = (\<lambda>n. (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) = (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) = (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))
[PROOF STEP]
have "hurwitz_zeta (1 + real n) s = zeta s - (\<Sum>k<n. real (Suc k) powr -s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hurwitz_zeta (1 + real n) (complex_of_real s) = zeta (complex_of_real s) - complex_of_real (\<Sum>k<n. real (Suc k) powr - s)
[PROOF STEP]
by (subst hurwitz_zeta_shift) (use assms in \<open>auto simp: zeta_def powr_Reals_eq\<close>)
[PROOF STATE]
proof (state)
this:
hurwitz_zeta (1 + real n) (complex_of_real s) = zeta (complex_of_real s) - complex_of_real (\<Sum>k<n. real (Suc k) powr - s)

goal (1 subgoal):
 1. \<And>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) = (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hurwitz_zeta (1 + real n) (complex_of_real s) = zeta (complex_of_real s) - complex_of_real (\<Sum>k<n. real (Suc k) powr - s)

goal (1 subgoal):
 1. \<And>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) = (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))
[PROOF STEP]
have "(\<Sum>k<n. real (Suc k) powr -s) = (\<Sum>k=1..n. real k powr -s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k<n. real (Suc k) powr - s) = (\<Sum>k = 1..n. real k powr - s)
[PROOF STEP]
by (rule sum.reindex_bij_witness[of _ "\<lambda>k. k - 1" Suc]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>k<n. real (Suc k) powr - s) = (\<Sum>k = 1..n. real k powr - s)

goal (1 subgoal):
 1. \<And>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) = (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
hurwitz_zeta (1 + real n) (complex_of_real s) = zeta (complex_of_real s) - complex_of_real (\<Sum>k = 1..n. real k powr - s)
[PROOF STEP]
show "?lhs n = ?rhs n"
[PROOF STATE]
proof (prove)
using this:
hurwitz_zeta (1 + real n) (complex_of_real s) = zeta (complex_of_real s) - complex_of_real (\<Sum>k = 1..n. real k powr - s)

goal (1 subgoal):
 1. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) = (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))
[PROOF STEP]
by (simp add: add_ac)
[PROOF STATE]
proof (state)
this:
- Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) = (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s)) = (\<lambda>n. (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s)))

goal (2 subgoals):
 1. (\<lambda>x. - Re (hurwitz_zeta (real x + 1) (complex_of_real s)) - real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
 2. (\<lambda>x. real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s)) = (\<lambda>n. (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s)))

goal (2 subgoals):
 1. (\<lambda>x. - Re (hurwitz_zeta (real x + 1) (complex_of_real s)) - real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
 2. (\<lambda>x. real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
have "\<dots> \<in> O(\<lambda>x. real x powr (-s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))) \<in> O(\<lambda>x. real x powr - s)
[PROOF STEP]
by (rule zeta_partial_sum_bigo_pos) (use s in auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))) \<in> O(\<lambda>x. real x powr - s)

goal (2 subgoals):
 1. (\<lambda>x. - Re (hurwitz_zeta (real x + 1) (complex_of_real s)) - real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
 2. (\<lambda>x. real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (\<Sum>k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - Re (zeta (complex_of_real s))) \<in> O(\<lambda>x. real x powr - s)

goal (2 subgoals):
 1. (\<lambda>x. - Re (hurwitz_zeta (real x + 1) (complex_of_real s)) - real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
 2. (\<lambda>x. real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
have "(\<lambda>x. real x powr (-s)) \<in> O(\<lambda>x. real x powr (1-s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real x powr - s) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real x powr - s) \<in> O(\<lambda>x. real x powr (1 - s))

goal (2 subgoals):
 1. (\<lambda>x. - Re (hurwitz_zeta (real x + 1) (complex_of_real s)) - real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
 2. (\<lambda>x. real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
show "(\<lambda>n. -Re (hurwitz_zeta (real n + 1) s) - real n powr (1 - s) / (1 - s)) \<in> \<dots>"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))

goal (1 subgoal):
 1. (\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))

goal (1 subgoal):
 1. (\<lambda>x. real x powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
qed (use s in real_asymp)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) + real n powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))

goal (1 subgoal):
 1. (\<lambda>n. Re (hurwitz_zeta (real n + 1) (complex_of_real s))) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. - Re (hurwitz_zeta (real n + 1) (complex_of_real s)) - real n powr (1 - s) / (1 - s) + real n powr (1 - s) / (1 - s)) \<in> O(\<lambda>x. real x powr (1 - s))

goal (1 subgoal):
 1. (\<lambda>n. Re (hurwitz_zeta (real n + 1) (complex_of_real s))) \<in> O(\<lambda>x. real x powr (1 - s))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. Re (hurwitz_zeta (real n + 1) (complex_of_real s))) \<in> O(\<lambda>x. real x powr (1 - s))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zig_zig: fixes lx x rx lb b rb a ra u lb1 lb2
defines [simp]: "X == Node lx (x) rx" defines[simp]: "B == Node lb b rb"
defines [simp]: "t == Node B a ra" defines [simp]: "A' == Node rb a ra"
defines [simp]: "t' == Node lb1 u (Node lb2 b A')"
assumes hyps: "lb \<noteq> \<langle>\<rangle>" and IH: "T_splay x lb + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb \<le> 2 * \<phi> lb - 3 * \<phi> X + 1" and
 prems: "size lb = size lb1 + size lb2 + 1" "X \<in> subtrees lb"
shows "T_splay x lb + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
define B' where [simp]: "B' = Node lb2 b A'"
[PROOF STATE]
proof (state)
this:
B' = \<langle>lb2, b, A'\<rangle>

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
have "T_splay x lb + \<Phi> t' - \<Phi> t = T_splay x lb + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t = real (T_splay x lb) + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
size lb = size lb1 + size lb2 + 1
X \<in> subtrees lb

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t = real (T_splay x lb) + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B
[PROOF STEP]
by(auto simp: A_splay_def size_if_splay algebra_simps in_set_tree_if split: tree.split)
[PROOF STATE]
proof (state)
this:
real (T_splay x lb) + \<Phi> t' - \<Phi> t = real (T_splay x lb) + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (T_splay x lb) + \<Phi> t' - \<Phi> t = real (T_splay x lb) + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
have "\<dots> \<le> 2 * \<phi> lb + \<phi> B' + \<phi> A' - \<phi> B - 3 * \<phi> X + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B \<le> 2 * \<phi> lb + \<phi> B' + \<phi> A' - \<phi> B - 3 * \<phi> X + 1
[PROOF STEP]
using IH prems(2)
[PROOF STATE]
proof (prove)
using this:
real (T_splay x lb) + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb \<le> 2 * \<phi> lb - 3 * \<phi> X + 1
X \<in> subtrees lb

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B \<le> 2 * \<phi> lb + \<phi> B' + \<phi> A' - \<phi> B - 3 * \<phi> X + 1
[PROOF STEP]
by(auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
real (T_splay x lb) + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B \<le> 2 * \<phi> lb + \<phi> B' + \<phi> A' - \<phi> B - 3 * \<phi> X + 1

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (T_splay x lb) + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B \<le> 2 * \<phi> lb + \<phi> B' + \<phi> A' - \<phi> B - 3 * \<phi> X + 1

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
have "\<dots> \<le> \<phi> lb + \<phi> B' + \<phi> A' - 3 * \<phi> X + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * \<phi> lb + \<phi> B' + \<phi> A' - \<phi> B - 3 * \<phi> X + 1 \<le> \<phi> lb + \<phi> B' + \<phi> A' - 3 * \<phi> X + 1
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
2 * \<phi> lb + \<phi> B' + \<phi> A' - \<phi> B - 3 * \<phi> X + 1 \<le> \<phi> lb + \<phi> B' + \<phi> A' - 3 * \<phi> X + 1

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * \<phi> lb + \<phi> B' + \<phi> A' - \<phi> B - 3 * \<phi> X + 1 \<le> \<phi> lb + \<phi> B' + \<phi> A' - 3 * \<phi> X + 1

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
have "\<dots> \<le> \<phi> B' + 2 * \<phi> t - 3 * \<phi> X "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> lb + \<phi> B' + \<phi> A' - 3 * \<phi> X + 1 \<le> \<phi> B' + 2 * \<phi> t - 3 * \<phi> X
[PROOF STEP]
using prems ld_ld_1_less[of "size1 lb" "size1 A'"]
[PROOF STATE]
proof (prove)
using this:
size lb = size lb1 + size lb2 + 1
X \<in> subtrees lb
\<lbrakk>0 < real (size1 lb); 0 < real (size1 A')\<rbrakk> \<Longrightarrow> 1 + \<phi> lb + \<phi> A' < 2 * log 2 (real (size1 lb) + real (size1 A'))

goal (1 subgoal):
 1. \<phi> lb + \<phi> B' + \<phi> A' - 3 * \<phi> X + 1 \<le> \<phi> B' + 2 * \<phi> t - 3 * \<phi> X
[PROOF STEP]
by(simp add: size_if_splay)
[PROOF STATE]
proof (state)
this:
\<phi> lb + \<phi> B' + \<phi> A' - 3 * \<phi> X + 1 \<le> \<phi> B' + 2 * \<phi> t - 3 * \<phi> X

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> lb + \<phi> B' + \<phi> A' - 3 * \<phi> X + 1 \<le> \<phi> B' + 2 * \<phi> t - 3 * \<phi> X

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
have "\<dots> \<le> 3 * \<phi> t - 3 * \<phi> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> B' + 2 * \<phi> t - 3 * \<phi> X \<le> 3 * \<phi> t - 3 * \<phi> X
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
size lb = size lb1 + size lb2 + 1
X \<in> subtrees lb

goal (1 subgoal):
 1. \<phi> B' + 2 * \<phi> t - 3 * \<phi> X \<le> 3 * \<phi> t - 3 * \<phi> X
[PROOF STEP]
by(simp add: size_if_splay)
[PROOF STATE]
proof (state)
this:
\<phi> B' + 2 * \<phi> t - 3 * \<phi> X \<le> 3 * \<phi> t - 3 * \<phi> X

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * \<phi> t - 3 * \<phi> X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * \<phi> t - 3 * \<phi> X

goal (1 subgoal):
 1. real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (T_splay x lb) + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)

goal:
No subgoals!
[PROOF STEP]
qed