[STATEMENT]
theorem (in snd_sylow) p_sylow_mod_p:
  shows "card (subgroups_of_size (p ^ a)) mod p = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
obtain P where PG:"subgroup P G" and cardP:"card P = p ^ a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrakk>subgroup P G; card P = p ^ a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis sylow_thm)
[PROOF STATE]
proof (state)
this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
hence orderP:"order (G\<lparr>carrier := P\<rparr>) = p ^ a"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. order (G\<lparr>carrier := P\<rparr>) = p ^ a
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. card (carrier (G\<lparr>carrier := P\<rparr>)) = p ^ a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
order (G\<lparr>carrier := P\<rparr>) = p ^ a

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
from PG
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
[PROOF STEP]
have PsubG:"P \<subseteq> carrier G"
[PROOF STATE]
proof (prove)
using this:
subgroup P G

goal (1 subgoal):
 1. P \<subseteq> carrier G
[PROOF STEP]
by (metis subgroup.subset)
[PROOF STATE]
proof (state)
this:
P \<subseteq> carrier G

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
from PG cardP
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
card P = p ^ a
[PROOF STEP]
have PSize:"P \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. P \<in> {H. subgroup H G \<and> card H = p ^ a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
from PG
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
[PROOF STEP]
interpret groupP:group "(G\<lparr>carrier := P\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
subgroup P G

goal (1 subgoal):
 1. Group.group (G\<lparr>carrier := P\<rparr>)
[PROOF STEP]
by (rule subgroup_imp_group)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
from cardP
[PROOF STATE]
proof (chain)
picking this:
card P = p ^ a
[PROOF STEP]
have PSize2:"P \<in> groupP.subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a

goal (1 subgoal):
 1. P \<in> groupP.subgroups_of_size (p ^ a)
[PROOF STEP]
using groupP.subgroups_of_size_def groupP.subgroup_self
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a
groupP.subgroups_of_size ?p = {H. subgroup H (G\<lparr>carrier := P\<rparr>) \<and> card H = ?p}
subgroup (carrier (G\<lparr>carrier := P\<rparr>)) (G\<lparr>carrier := P\<rparr>)

goal (1 subgoal):
 1. P \<in> groupP.subgroups_of_size (p ^ a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> groupP.subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
from finite_G
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
[PROOF STEP]
interpret conjG: group_action G "conjugation_action (p ^ a)" "subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. group_action G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a))
[PROOF STEP]
by (rule acts_on_subsets)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
from PG
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
[PROOF STEP]
interpret conjP: group_action "G\<lparr>carrier := P\<rparr>" "conjugation_action (p ^ a)" "subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
subgroup P G

goal (1 subgoal):
 1. group_action (G\<lparr>carrier := P\<rparr>) (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a))
[PROOF STEP]
by (rule conjG.subgroup_action)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
from finite_G
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
[PROOF STEP]
have "finite (subgroups_of_size (p ^ a))"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. finite (subgroups_of_size (p ^ a))
[PROOF STEP]
unfolding subgroups_of_size_def subgroup_def
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. finite {H. ((H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> H \<longrightarrow> y \<in> H \<longrightarrow> x \<otimes> y \<in> H)) \<and> \<one> \<in> H \<and> (\<forall>x. x \<in> H \<longrightarrow> inv x \<in> H)) \<and> card H = p ^ a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (subgroups_of_size (p ^ a))

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
with orderP prime_p
[PROOF STATE]
proof (chain)
picking this:
order (G\<lparr>carrier := P\<rparr>) = p ^ a
prime p
finite (subgroups_of_size (p ^ a))
[PROOF STEP]
have "card (subgroups_of_size (p ^ a)) mod p = card conjP.fixed_points mod p"
[PROOF STATE]
proof (prove)
using this:
order (G\<lparr>carrier := P\<rparr>) = p ^ a
prime p
finite (subgroups_of_size (p ^ a))

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = card conjP.fixed_points mod p
[PROOF STEP]
by (rule conjP.fixed_point_congruence)
[PROOF STATE]
proof (state)
this:
card (subgroups_of_size (p ^ a)) mod p = card conjP.fixed_points mod p

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (subgroups_of_size (p ^ a)) mod p = card conjP.fixed_points mod p

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
have "... = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
have "\<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
fix Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
assume Qfixed:"Q \<in> conjP.fixed_points"
[PROOF STATE]
proof (state)
this:
Q \<in> conjP.fixed_points

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
hence Qsize:"Q \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
Q \<in> conjP.fixed_points

goal (1 subgoal):
 1. Q \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
unfolding conjP.fixed_points_def
[PROOF STATE]
proof (prove)
using this:
Q \<in> {m \<in> subgroups_of_size (p ^ a). carrier (G\<lparr>carrier := P\<rparr>) \<subseteq> conjP.stabilizer m}

goal (1 subgoal):
 1. Q \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Q \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
hence cardQ:"card Q = p ^ a"
[PROOF STATE]
proof (prove)
using this:
Q \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. card Q = p ^ a
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
Q \<in> {H. subgroup H G \<and> card H = p ^ a}

goal (1 subgoal):
 1. card Q = p ^ a
[PROOF STEP]
by simp
      \<comment> \<open>The normalizer of @{term Q} in @{term G}\<close>
      \<comment> \<open>Let's first show some basic propertiers of @{text N}\<close>
[PROOF STATE]
proof (state)
this:
card Q = p ^ a

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
define N where "N = conjG.stabilizer Q"
[PROOF STATE]
proof (state)
this:
N = conjG.stabilizer Q

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
define k where "k = (card N) div (p ^ a)"
[PROOF STATE]
proof (state)
this:
k = card N div p ^ a

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
from N_def Qsize
[PROOF STATE]
proof (chain)
picking this:
N = conjG.stabilizer Q
Q \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have NG:"subgroup N G"
[PROOF STATE]
proof (prove)
using this:
N = conjG.stabilizer Q
Q \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. subgroup N G
[PROOF STEP]
by (metis conjG.stabilizer_is_subgroup)
[PROOF STATE]
proof (state)
this:
subgroup N G

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subgroup N G
[PROOF STEP]
interpret groupN: group "G\<lparr>carrier := N\<rparr>"
[PROOF STATE]
proof (prove)
using this:
subgroup N G

goal (1 subgoal):
 1. Group.group (G\<lparr>carrier := N\<rparr>)
[PROOF STEP]
by (metis subgroup_imp_group)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
from Qsize N_def
[PROOF STATE]
proof (chain)
picking this:
Q \<in> subgroups_of_size (p ^ a)
N = conjG.stabilizer Q
[PROOF STEP]
have QN:"subgroup Q (G\<lparr>carrier := N\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
Q \<in> subgroups_of_size (p ^ a)
N = conjG.stabilizer Q

goal (1 subgoal):
 1. subgroup Q (G\<lparr>carrier := N\<rparr>)
[PROOF STEP]
using stabilizer_supergrp_P
[PROOF STATE]
proof (prove)
using this:
Q \<in> subgroups_of_size (p ^ a)
N = conjG.stabilizer Q
\<lbrakk>finite (carrier G); ?P \<in> subgroups_of_size ?p\<rbrakk> \<Longrightarrow> subgroup ?P (G\<lparr>carrier := group_action.stabilizer G (conjugation_action ?p) ?P\<rparr>)

goal (1 subgoal):
 1. subgroup Q (G\<lparr>carrier := N\<rparr>)
[PROOF STEP]
by auto
      \<comment> \<open>The following proposition is used to show that $P = Q$ later\<close>
[PROOF STATE]
proof (state)
this:
subgroup Q (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
from Qsize
[PROOF STATE]
proof (chain)
picking this:
Q \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have NfixesQ:"\<forall>g\<in>N. conjugation_action (p ^ a) g Q = Q"
[PROOF STATE]
proof (prove)
using this:
Q \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. \<forall>g\<in>N. conjugation_action (p ^ a) g Q = Q
[PROOF STEP]
unfolding N_def conjG.stabilizer_def
[PROOF STATE]
proof (prove)
using this:
Q \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. \<forall>g\<in>{g \<in> carrier G. conjugation_action (p ^ a) g Q = Q}. conjugation_action (p ^ a) g Q = Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>g\<in>N. conjugation_action (p ^ a) g Q = Q

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
from Qfixed
[PROOF STATE]
proof (chain)
picking this:
Q \<in> conjP.fixed_points
[PROOF STEP]
have PfixesQ:"\<forall>g\<in>P. conjugation_action (p ^ a) g Q = Q"
[PROOF STATE]
proof (prove)
using this:
Q \<in> conjP.fixed_points

goal (1 subgoal):
 1. \<forall>g\<in>P. conjugation_action (p ^ a) g Q = Q
[PROOF STEP]
unfolding conjP.fixed_points_def conjP.stabilizer_def
[PROOF STATE]
proof (prove)
using this:
Q \<in> {m \<in> subgroups_of_size (p ^ a). carrier (G\<lparr>carrier := P\<rparr>) \<subseteq> {g \<in> carrier (G\<lparr>carrier := P\<rparr>). conjugation_action (p ^ a) g m = m}}

goal (1 subgoal):
 1. \<forall>g\<in>P. conjugation_action (p ^ a) g Q = Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>g\<in>P. conjugation_action (p ^ a) g Q = Q

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
with PsubG
[PROOF STATE]
proof (chain)
picking this:
P \<subseteq> carrier G
\<forall>g\<in>P. conjugation_action (p ^ a) g Q = Q
[PROOF STEP]
have  "P \<subseteq> N"
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> carrier G
\<forall>g\<in>P. conjugation_action (p ^ a) g Q = Q

goal (1 subgoal):
 1. P \<subseteq> N
[PROOF STEP]
unfolding N_def conjG.stabilizer_def
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> carrier G
\<forall>g\<in>P. conjugation_action (p ^ a) g Q = Q

goal (1 subgoal):
 1. P \<subseteq> {g \<in> carrier G. conjugation_action (p ^ a) g Q = Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<subseteq> N

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
with PG N_def Qsize
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
N = conjG.stabilizer Q
Q \<in> subgroups_of_size (p ^ a)
P \<subseteq> N
[PROOF STEP]
have PN:"subgroup P (G\<lparr>carrier := N\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
N = conjG.stabilizer Q
Q \<in> subgroups_of_size (p ^ a)
P \<subseteq> N

goal (1 subgoal):
 1. subgroup P (G\<lparr>carrier := N\<rparr>)
[PROOF STEP]
by (metis conjG.stabilizer_is_subgroup is_group subgroup.subgroup_of_subset)
[PROOF STATE]
proof (state)
this:
subgroup P (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
with cardP
[PROOF STATE]
proof (chain)
picking this:
card P = p ^ a
subgroup P (G\<lparr>carrier := N\<rparr>)
[PROOF STEP]
have "p ^ a dvd order (G\<lparr>carrier := N\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a
subgroup P (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. p ^ a dvd order (G\<lparr>carrier := N\<rparr>)
[PROOF STEP]
using groupN.card_subgrp_dvd
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a
subgroup P (G\<lparr>carrier := N\<rparr>)
subgroup ?H (G\<lparr>carrier := N\<rparr>) \<Longrightarrow> card ?H dvd order (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. p ^ a dvd order (G\<lparr>carrier := N\<rparr>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
p ^ a dvd order (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
hence "p ^ a dvd card N"
[PROOF STATE]
proof (prove)
using this:
p ^ a dvd order (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. p ^ a dvd card N
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
p ^ a dvd card (carrier (G\<lparr>carrier := N\<rparr>))

goal (1 subgoal):
 1. p ^ a dvd card N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p ^ a dvd card N

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
with NG
[PROOF STATE]
proof (chain)
picking this:
subgroup N G
p ^ a dvd card N
[PROOF STEP]
have smaller_sylow:"snd_sylow (G\<lparr>carrier := N\<rparr>) p a k"
[PROOF STATE]
proof (prove)
using this:
subgroup N G
p ^ a dvd card N

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := N\<rparr>) p a k
[PROOF STEP]
unfolding k_def
[PROOF STATE]
proof (prove)
using this:
subgroup N G
p ^ a dvd card N

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := N\<rparr>) p a (card N div p ^ a)
[PROOF STEP]
by (rule restrict_locale)
      \<comment> \<open>Instantiate the @{term snd_sylow} Locale a second time for the normalizer of @{term Q}\<close>
[PROOF STATE]
proof (state)
this:
snd_sylow (G\<lparr>carrier := N\<rparr>) p a k

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
define NcalM where "NcalM = {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a}"
[PROOF STATE]
proof (state)
this:
NcalM = {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a}

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
define NRelM where "NRelM = {(N1, N2). N1 \<in> NcalM \<and> N2 \<in> NcalM \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := N\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)}"
[PROOF STATE]
proof (state)
this:
NRelM = {(N1, N2). N1 \<in> NcalM \<and> N2 \<in> NcalM \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := N\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)}

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
interpret Nsylow: snd_sylow "G\<lparr>carrier := N\<rparr>" p a k NcalM NRelM
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := N\<rparr>) p a k &&& (NcalM \<equiv> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a}) &&& NRelM \<equiv> {(N1, N2). N1 \<in> NcalM \<and> N2 \<in> NcalM \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := N\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)}
[PROOF STEP]
unfolding NcalM_def NRelM_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := N\<rparr>) p a k &&& ({s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<equiv> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a}) &&& {(N1, N2). N1 \<in> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<and> N2 \<in> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := N\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)} \<equiv> {(N1, N2). N1 \<in> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<and> N2 \<in> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := N\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)}
[PROOF STEP]
using smaller_sylow
[PROOF STATE]
proof (prove)
using this:
snd_sylow (G\<lparr>carrier := N\<rparr>) p a k

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := N\<rparr>) p a k &&& ({s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<equiv> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a}) &&& {(N1, N2). N1 \<in> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<and> N2 \<in> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := N\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)} \<equiv> {(N1, N2). N1 \<in> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<and> N2 \<in> {s. s \<subseteq> carrier (G\<lparr>carrier := N\<rparr>) \<and> card s = p ^ a} \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := N\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)}
[PROOF STEP]
.
      \<comment> \<open>@{term P} and @{term Q} are conjugate in @{term N}:\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
from cardP PN
[PROOF STATE]
proof (chain)
picking this:
card P = p ^ a
subgroup P (G\<lparr>carrier := N\<rparr>)
[PROOF STEP]
have PsizeN:"P \<in> groupN.subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a
subgroup P (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. P \<in> groupN.subgroups_of_size (p ^ a)
[PROOF STEP]
unfolding groupN.subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a
subgroup P (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. P \<in> {H. subgroup H (G\<lparr>carrier := N\<rparr>) \<and> card H = p ^ a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> groupN.subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
from cardQ QN
[PROOF STATE]
proof (chain)
picking this:
card Q = p ^ a
subgroup Q (G\<lparr>carrier := N\<rparr>)
[PROOF STEP]
have QsizeN:"Q \<in> groupN.subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
card Q = p ^ a
subgroup Q (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. Q \<in> groupN.subgroups_of_size (p ^ a)
[PROOF STEP]
unfolding groupN.subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
card Q = p ^ a
subgroup Q (G\<lparr>carrier := N\<rparr>)

goal (1 subgoal):
 1. Q \<in> {H. subgroup H (G\<lparr>carrier := N\<rparr>) \<and> card H = p ^ a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q \<in> groupN.subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
from QsizeN PsizeN
[PROOF STATE]
proof (chain)
picking this:
Q \<in> groupN.subgroups_of_size (p ^ a)
P \<in> groupN.subgroups_of_size (p ^ a)
[PROOF STEP]
obtain g where g:"g \<in> carrier (G\<lparr>carrier := N\<rparr>)" "P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)"
[PROOF STATE]
proof (prove)
using this:
Q \<in> groupN.subgroups_of_size (p ^ a)
P \<in> groupN.subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier (G\<lparr>carrier := N\<rparr>); P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Nsylow.sylow_conjugate)
[PROOF STATE]
proof (state)
this:
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
with NG
[PROOF STATE]
proof (chain)
picking this:
subgroup N G
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)
[PROOF STEP]
have "P = g <# (Q #> inv g)"
[PROOF STATE]
proof (prove)
using this:
subgroup N G
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)

goal (1 subgoal):
 1. P = g <# (Q #> inv g)
[PROOF STEP]
unfolding r_coset_def l_coset_def
[PROOF STATE]
proof (prove)
using this:
subgroup N G
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = (\<Union>h\<in>\<Union>h\<in>Q. {h \<otimes>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g}. {g \<otimes>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> h})

goal (1 subgoal):
 1. P = (\<Union>h\<in>\<Union>h\<in>Q. {h \<otimes> inv g}. {g \<otimes> h})
[PROOF STEP]
by (auto simp:m_inv_consistent)
[PROOF STATE]
proof (state)
this:
P = g <# (Q #> inv g)

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
with NG g Qsize
[PROOF STATE]
proof (chain)
picking this:
subgroup N G
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)
Q \<in> subgroups_of_size (p ^ a)
P = g <# (Q #> inv g)
[PROOF STEP]
have "conjugation_action (p ^ a) g Q = P"
[PROOF STATE]
proof (prove)
using this:
subgroup N G
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)
Q \<in> subgroups_of_size (p ^ a)
P = g <# (Q #> inv g)

goal (1 subgoal):
 1. conjugation_action (p ^ a) g Q = P
[PROOF STEP]
unfolding conjugation_action_def
[PROOF STATE]
proof (prove)
using this:
subgroup N G
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)
Q \<in> subgroups_of_size (p ^ a)
P = g <# (Q #> inv g)

goal (1 subgoal):
 1. (\<lambda>g\<in>carrier G. \<lambda>P\<in>subgroups_of_size (p ^ a). g <# (P #> inv g)) g Q = P
[PROOF STEP]
using subgroup.subset
[PROOF STATE]
proof (prove)
using this:
subgroup N G
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)
Q \<in> subgroups_of_size (p ^ a)
P = g <# (Q #> inv g)
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

goal (1 subgoal):
 1. (\<lambda>g\<in>carrier G. \<lambda>P\<in>subgroups_of_size (p ^ a). g <# (P #> inv g)) g Q = P
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
conjugation_action (p ^ a) g Q = P

goal (1 subgoal):
 1. \<And>Q. Q \<in> conjP.fixed_points \<Longrightarrow> Q = P
[PROOF STEP]
with g NfixesQ
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)
\<forall>g\<in>N. conjugation_action (p ^ a) g Q = Q
conjugation_action (p ^ a) g Q = P
[PROOF STEP]
show "Q = P"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier (G\<lparr>carrier := N\<rparr>)
P = g <#\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> (Q #>\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := N\<rparr>\<^esub> g)
\<forall>g\<in>N. conjugation_action (p ^ a) g Q = Q
conjugation_action (p ^ a) g Q = P

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?Q \<in> conjP.fixed_points \<Longrightarrow> ?Q = P

goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?Q \<in> conjP.fixed_points \<Longrightarrow> ?Q = P

goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
from finite_G PSize
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have "P \<in> conjP.fixed_points"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. P \<in> conjP.fixed_points
[PROOF STEP]
using P_fixed_point_of_P_conj
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)
\<lbrakk>finite (carrier G); ?P \<in> subgroups_of_size ?p\<rbrakk> \<Longrightarrow> ?P \<in> group_action.fixed_points (G\<lparr>carrier := ?P\<rparr>) (conjugation_action ?p) (subgroups_of_size ?p)

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

goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?Q \<in> conjP.fixed_points \<Longrightarrow> ?Q = P
P \<in> conjP.fixed_points
[PROOF STEP]
have "conjP.fixed_points = {P}"
[PROOF STATE]
proof (prove)
using this:
?Q \<in> conjP.fixed_points \<Longrightarrow> ?Q = P
P \<in> conjP.fixed_points

goal (1 subgoal):
 1. conjP.fixed_points = {P}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
conjP.fixed_points = {P}

goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
hence one:"card conjP.fixed_points = 1"
[PROOF STATE]
proof (prove)
using this:
conjP.fixed_points = {P}

goal (1 subgoal):
 1. card conjP.fixed_points = 1
[PROOF STEP]
by (auto simp: card_Suc_eq)
[PROOF STATE]
proof (state)
this:
card conjP.fixed_points = 1

goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
with prime_p
[PROOF STATE]
proof (chain)
picking this:
prime p
card conjP.fixed_points = 1
[PROOF STEP]
have "card conjP.fixed_points < p"
[PROOF STATE]
proof (prove)
using this:
prime p
card conjP.fixed_points = 1

goal (1 subgoal):
 1. card conjP.fixed_points < p
[PROOF STEP]
unfolding prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)
card conjP.fixed_points = 1

goal (1 subgoal):
 1. card conjP.fixed_points < p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card conjP.fixed_points < p

goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
with one
[PROOF STATE]
proof (chain)
picking this:
card conjP.fixed_points = 1
card conjP.fixed_points < p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card conjP.fixed_points = 1
card conjP.fixed_points < p

goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
using mod_pos_pos_trivial
[PROOF STATE]
proof (prove)
using this:
card conjP.fixed_points = 1
card conjP.fixed_points < p
\<lbrakk>0 \<le> ?k; ?k < ?l\<rbrakk> \<Longrightarrow> ?k mod ?l = ?k

goal (1 subgoal):
 1. card conjP.fixed_points mod p = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card conjP.fixed_points mod p = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card conjP.fixed_points mod p = 1

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (subgroups_of_size (p ^ a)) mod p = 1

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) mod p = 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card (subgroups_of_size (p ^ a)) mod p = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "exp_count_up1 = exp_count_up2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp_count_up1 = exp_count_up2
[PROOF STEP]
unfolding exp_count_up1_def exp_count_up2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ''a'' ::= N 1;; ''c'' ::= N 0;; WHILE Cmpop (<) (V ''c'') (V ''n'') DO (''a'' ::= Binop (*) (N 2) (V ''a'');; ''c'' ::= Binop (+) (V ''c'') (N 1)) = ''a'' ::= N 1;; ''c'' ::= N 0;; WHILE Cmpop (<) (V ''c'') (V ''n'') DO (''a'' ::= Binop (*) (N 2) (V ''a'');; ''c'' ::= Binop (+) (V ''c'') (N 1))
[PROOF STEP]
..


[STATEMENT]
lemma "V ''x'' = Vidx ''x'' (N 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ''x'' = V ''x''
[PROOF STEP]
.. \<comment> \<open>Shortcut for access at index \<open>0\<close>\<close>


[STATEMENT]
lemma \<open>Assign ''x'' v = AssignIdx ''x'' (N 0) v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ''x'' ::= v = ''x'' ::= v
[PROOF STEP]
.. \<comment> \<open>Shortcut for assignment to index \<open>0\<close>\<close>


[STATEMENT]
lemma "s\<^sub>0 ''n'' 0 \<ge> 0 \<Longrightarrow> wlp \<pi> exp_count_up1 (\<lambda>s. s ''a'' 0 = 2^nat (s\<^sub>0 ''n'' 0)) s\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> s\<^sub>0 ''n'' 0 \<Longrightarrow> wlp \<pi> exp_count_up1 (\<lambda>s. s ''a'' 0 = 2 ^ nat (s\<^sub>0 ''n'' 0)) s\<^sub>0
[PROOF STEP]
unfolding exp_count_up1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> s\<^sub>0 ''n'' 0 \<Longrightarrow> wlp \<pi> (''a'' ::= N 1;; ''c'' ::= N 0;; WHILE Cmpop (<) (V ''c'') (V ''n'') DO (''a'' ::= Binop (*) (N 2) (V ''a'');; ''c'' ::= Binop (+) (V ''c'') (N 1))) (\<lambda>s. s ''a'' 0 = 2 ^ nat (s\<^sub>0 ''n'' 0)) s\<^sub>0
[PROOF STEP]
apply (subst annotate_whileI[where
          I="\<lambda>s. s ''n'' 0 = s\<^sub>0 ''n'' 0 \<and>  s ''a'' 0 = 2 ^ nat (s ''c'' 0) \<and> 0 \<le> s ''c'' 0 \<and> s ''c'' 0 \<le> s\<^sub>0 ''n'' 0"
        ])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> s\<^sub>0 ''n'' 0 \<Longrightarrow> wlp \<pi> (''a'' ::= N 1;; ''c'' ::= N 0;; WHILE {\<lambda>s. s ''n'' 0 = s\<^sub>0 ''n'' 0 \<and> s ''a'' 0 = 2 ^ nat (s ''c'' 0) \<and> 0 \<le> s ''c'' 0 \<and> s ''c'' 0 \<le> s\<^sub>0 ''n'' 0} Cmpop (<) (V ''c'') (V ''n'') DO (''a'' ::= Binop (*) (N 2) (V ''a'');; ''c'' ::= Binop (+) (V ''c'') (N 1))) (\<lambda>s. s ''a'' 0 = 2 ^ nat (s\<^sub>0 ''n'' 0)) s\<^sub>0
[PROOF STEP]
apply (i_vcg_preprocess; i_vcg_gen; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<paragraph>''invar-pres''; modifies {''a'', ''c''} s (s\<^sub>0(''c'' := (s\<^sub>0 ''c'')(0 := 0), ''a'' := (s\<^sub>0 ''a'')(0 := 1))); s ''c'' 0 < s\<^sub>0 ''n'' 0; s ''n'' 0 = s\<^sub>0 ''n'' 0; s ''a'' 0 = 2 ^ nat (s ''c'' 0); 0 \<le> s ''c'' 0\<rbrakk> \<Longrightarrow> 2 * 2 ^ nat (s ''c'' 0) = 2 ^ nat (s ''c'' 0 + 1)
[PROOF STEP]
text \<open>The postprocessor converts from states applied to string names to actual variables\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<paragraph>''invar-pres''; modifies {''a'', ''c''} s (s\<^sub>0(''c'' := (s\<^sub>0 ''c'')(0 := 0), ''a'' := (s\<^sub>0 ''a'')(0 := 1))); s ''c'' 0 < s\<^sub>0 ''n'' 0; s ''n'' 0 = s\<^sub>0 ''n'' 0; s ''a'' 0 = 2 ^ nat (s ''c'' 0); 0 \<le> s ''c'' 0\<rbrakk> \<Longrightarrow> 2 * 2 ^ nat (s ''c'' 0) = 2 ^ nat (s ''c'' 0 + 1)
[PROOF STEP]
apply i_vcg_postprocess
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a n\<^sub>0. \<lbrakk>\<paragraph>''invar-pres''; c < n\<^sub>0; n\<^sub>0 = n\<^sub>0; a = 2 ^ nat c; 0 \<le> c\<rbrakk> \<Longrightarrow> 2 * 2 ^ nat c = 2 ^ nat (c + 1)
[PROOF STEP]
by (auto simp: algebra_simps nat_distribs)


[STATEMENT]
lemma "s\<^sub>0 ''n'' 0 \<ge> 0 \<Longrightarrow> wlp \<pi> exp_count_up1 (\<lambda>s. s ''a'' 0 = 2^nat (s\<^sub>0 ''n'' 0)) s\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> s\<^sub>0 ''n'' 0 \<Longrightarrow> wlp \<pi> exp_count_up1 (\<lambda>s. s ''a'' 0 = 2 ^ nat (s\<^sub>0 ''n'' 0)) s\<^sub>0
[PROOF STEP]
unfolding exp_count_up1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> s\<^sub>0 ''n'' 0 \<Longrightarrow> wlp \<pi> (''a'' ::= N 1;; ''c'' ::= N 0;; WHILE Cmpop (<) (V ''c'') (V ''n'') DO (''a'' ::= Binop (*) (N 2) (V ''a'');; ''c'' ::= Binop (+) (V ''c'') (N 1))) (\<lambda>s. s ''a'' 0 = 2 ^ nat (s\<^sub>0 ''n'' 0)) s\<^sub>0
[PROOF STEP]
apply (subst annotate_whileI[where
          I="\<lambda>s. s ''n'' 0 = s\<^sub>0 ''n'' 0 \<and>  s ''a'' 0 = 2 ^ nat (s ''c'' 0) \<and> 0 \<le> s ''c'' 0 \<and> s ''c'' 0 \<le> s\<^sub>0 ''n'' 0"
        ])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> s\<^sub>0 ''n'' 0 \<Longrightarrow> wlp \<pi> (''a'' ::= N 1;; ''c'' ::= N 0;; WHILE {\<lambda>s. s ''n'' 0 = s\<^sub>0 ''n'' 0 \<and> s ''a'' 0 = 2 ^ nat (s ''c'' 0) \<and> 0 \<le> s ''c'' 0 \<and> s ''c'' 0 \<le> s\<^sub>0 ''n'' 0} Cmpop (<) (V ''c'') (V ''n'') DO (''a'' ::= Binop (*) (N 2) (V ''a'');; ''c'' ::= Binop (+) (V ''c'') (N 1))) (\<lambda>s. s ''a'' 0 = 2 ^ nat (s\<^sub>0 ''n'' 0)) s\<^sub>0
[PROOF STEP]
text \<open>The postprocessor is invoked by default\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> s\<^sub>0 ''n'' 0 \<Longrightarrow> wlp \<pi> (''a'' ::= N 1;; ''c'' ::= N 0;; WHILE {\<lambda>s. s ''n'' 0 = s\<^sub>0 ''n'' 0 \<and> s ''a'' 0 = 2 ^ nat (s ''c'' 0) \<and> 0 \<le> s ''c'' 0 \<and> s ''c'' 0 \<le> s\<^sub>0 ''n'' 0} Cmpop (<) (V ''c'') (V ''n'') DO (''a'' ::= Binop (*) (N 2) (V ''a'');; ''c'' ::= Binop (+) (V ''c'') (N 1))) (\<lambda>s. s ''a'' 0 = 2 ^ nat (s\<^sub>0 ''n'' 0)) s\<^sub>0
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n\<^sub>0. \<lbrakk>\<paragraph>''invar-initial''; 0 \<le> n\<^sub>0\<rbrakk> \<Longrightarrow> 1 = 2 ^ nat 0 \<and> 0 \<le> 0
 2. \<And>c a n\<^sub>0. \<lbrakk>\<paragraph>''invar-pres''; 0 \<le> n\<^sub>0; n\<^sub>0 = n\<^sub>0 \<and> a = 2 ^ nat c \<and> 0 \<le> c \<and> c \<le> n\<^sub>0; c < n\<^sub>0\<rbrakk> \<Longrightarrow> 2 * 2 ^ nat c = 2 ^ nat (c + 1) \<and> 0 \<le> c + 1 \<and> c + 1 \<le> n\<^sub>0
 3. \<And>c a n\<^sub>0. \<lbrakk>\<paragraph>''invar-post''; 0 \<le> n\<^sub>0; n\<^sub>0 = n\<^sub>0 \<and> a = 2 ^ nat c \<and> 0 \<le> c \<and> c \<le> n\<^sub>0; \<not> c < n\<^sub>0\<rbrakk> \<Longrightarrow> 2 ^ nat c = 2 ^ nat n\<^sub>0
[PROOF STEP]
oops


[STATEMENT]
lemma "let n = s\<^sub>0 ''n'' 0 in n \<ge> 0
    \<Longrightarrow> wlp \<pi> exp_count_up1 (\<lambda>s. let a = s ''a'' 0; n\<^sub>0 = s\<^sub>0 ''n'' 0 in a = 2^nat (n\<^sub>0)) s\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Let (s\<^sub>0 ''n'' 0) ((\<le>) 0) \<Longrightarrow> wlp \<pi> exp_count_up1 (\<lambda>s. let a = s ''a'' 0; n\<^sub>0 = s\<^sub>0 ''n'' 0 in a = 2 ^ nat n\<^sub>0) s\<^sub>0
[PROOF STEP]
unfolding exp_count_up1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Let (s\<^sub>0 ''n'' 0) ((\<le>) 0) \<Longrightarrow> wlp \<pi> (''a'' ::= N 1;; ''c'' ::= N 0;; WHILE Cmpop (<) (V ''c'') (V ''n'') DO (''a'' ::= Binop (*) (N 2) (V ''a'');; ''c'' ::= Binop (+) (V ''c'') (N 1))) (\<lambda>s. let a = s ''a'' 0; n\<^sub>0 = s\<^sub>0 ''n'' 0 in a = 2 ^ nat n\<^sub>0) s\<^sub>0
[PROOF STEP]
apply (subst annotate_whileI[where
          I="\<lambda>s. s ''n'' 0 = s\<^sub>0 ''n'' 0 \<and>  s ''a'' 0 = 2 ^ nat (s ''c'' 0) \<and> 0 \<le> s ''c'' 0 \<and> s ''c'' 0 \<le> s\<^sub>0 ''n'' 0"
          (* Similar for invar! *)
        ])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Let (s\<^sub>0 ''n'' 0) ((\<le>) 0) \<Longrightarrow> wlp \<pi> (''a'' ::= N 1;; ''c'' ::= N 0;; WHILE {\<lambda>s. s ''n'' 0 = s\<^sub>0 ''n'' 0 \<and> s ''a'' 0 = 2 ^ nat (s ''c'' 0) \<and> 0 \<le> s ''c'' 0 \<and> s ''c'' 0 \<le> s\<^sub>0 ''n'' 0} Cmpop (<) (V ''c'') (V ''n'') DO (''a'' ::= Binop (*) (N 2) (V ''a'');; ''c'' ::= Binop (+) (V ''c'') (N 1))) (\<lambda>s. let a = s ''a'' 0; n\<^sub>0 = s\<^sub>0 ''n'' 0 in a = 2 ^ nat n\<^sub>0) s\<^sub>0
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n\<^sub>0. \<lbrakk>\<paragraph>''invar-initial''; Let n\<^sub>0 ((\<le>) 0)\<rbrakk> \<Longrightarrow> 1 = 2 ^ nat 0 \<and> 0 \<le> 0 \<and> 0 \<le> n\<^sub>0
 2. \<And>c a n\<^sub>0. \<lbrakk>\<paragraph>''invar-pres''; Let n\<^sub>0 ((\<le>) 0); n\<^sub>0 = n\<^sub>0 \<and> a = 2 ^ nat c \<and> 0 \<le> c \<and> c \<le> n\<^sub>0; c < n\<^sub>0\<rbrakk> \<Longrightarrow> 2 * 2 ^ nat c = 2 ^ nat (c + 1) \<and> 0 \<le> c + 1 \<and> c + 1 \<le> n\<^sub>0
 3. \<And>c a n\<^sub>0. \<lbrakk>\<paragraph>''invar-post''; Let n\<^sub>0 ((\<le>) 0); n\<^sub>0 = n\<^sub>0 \<and> a = 2 ^ nat c \<and> 0 \<le> c \<and> c \<le> n\<^sub>0; \<not> c < n\<^sub>0\<rbrakk> \<Longrightarrow> let a = 2 ^ nat c; n\<^sub>0 = n\<^sub>0 in a = 2 ^ nat n\<^sub>0
[PROOF STEP]
apply (auto simp: algebra_simps nat_distribs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "VAR (s x) P = (let v=s x in P v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VAR (s x) P = Let (s x) P
[PROOF STEP]
unfolding VAR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (s x) = Let (s x) P
[PROOF STEP]
by simp


[STATEMENT]
lemma I_in_S:
  assumes "pmf I s \<noteq> 0" shows "s \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
from \<open>pmf I s \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
pmf I s \<noteq> 0
[PROOF STEP]
have "0 \<noteq> \<P>(x in M. X 0 x = s)"
[PROOF STATE]
proof (prove)
using this:
pmf I s \<noteq> 0

goal (1 subgoal):
 1. 0 \<noteq> prob {x \<in> space M. X 0 x = s}
[PROOF STEP]
by transfer (auto simp: measure_distr vimage_def Int_def conj_commute)
[PROOF STATE]
proof (state)
this:
0 \<noteq> prob {x \<in> space M. X 0 x = s}

goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<noteq> prob {x \<in> space M. X 0 x = s}

goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
have "\<P>(x in M. X 0 x = s) = \<P>(x in M. X 0 x = s \<and> s \<in> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {x \<in> space M. X 0 x = s} = prob {x \<in> space M. X 0 x = s \<and> s \<in> S}
[PROOF STEP]
using S(2)[of 0]
[PROOF STATE]
proof (prove)
using this:
AE x in M. X 0 x \<in> S

goal (1 subgoal):
 1. prob {x \<in> space M. X 0 x = s} = prob {x \<in> space M. X 0 x = s \<and> s \<in> S}
[PROOF STEP]
by (intro M.finite_measure_eq_AE) auto
[PROOF STATE]
proof (state)
this:
prob {x \<in> space M. X 0 x = s} = prob {x \<in> space M. X 0 x = s \<and> s \<in> S}

goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<noteq> prob {x \<in> space M. X 0 x = s \<and> s \<in> S}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> prob {x \<in> space M. X 0 x = s \<and> s \<in> S}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmf_K:
  assumes n: "0 < \<P>(\<omega> in M. X n \<omega> = s)"
  shows "pmf (K s) t = \<P>(\<omega> in M. X (Suc n) \<omega> = t \<bar> X n \<omega> = s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (K s) t = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
proof (transfer fixing: n s t)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Sigma_Algebra.measure (with (\<lambda>n. prob {\<omega> \<in> space M. X n \<omega> = s} \<noteq> 0) (\<lambda>n. distr (uniform_measure M {\<omega> \<in> space M. X n \<omega> = s}) (count_space UNIV) (X (Suc n))) (uniform_measure (count_space UNIV) {s})) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
let ?P = "\<lambda>n. \<P>(\<omega> in M. X n \<omega> = s) \<noteq> 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Sigma_Algebra.measure (with (\<lambda>n. prob {\<omega> \<in> space M. X n \<omega> = s} \<noteq> 0) (\<lambda>n. distr (uniform_measure M {\<omega> \<in> space M. X n \<omega> = s}) (count_space UNIV) (X (Suc n))) (uniform_measure (count_space UNIV) {s})) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
let ?D = "\<lambda>n. distr (uniform_measure M {\<omega>\<in>space M. X n \<omega> = s}) (count_space UNIV) (X (Suc n))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Sigma_Algebra.measure (with (\<lambda>n. prob {\<omega> \<in> space M. X n \<omega> = s} \<noteq> 0) (\<lambda>n. distr (uniform_measure M {\<omega> \<in> space M. X n \<omega> = s}) (count_space UNIV) (X (Suc n))) (uniform_measure (count_space UNIV) {s})) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
let ?U = "uniform_measure (count_space UNIV) {s}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Sigma_Algebra.measure (with (\<lambda>n. prob {\<omega> \<in> space M. X n \<omega> = s} \<noteq> 0) (\<lambda>n. distr (uniform_measure M {\<omega> \<in> space M. X n \<omega> = s}) (count_space UNIV) (X (Suc n))) (uniform_measure (count_space UNIV) {s})) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
show "measure (with ?P ?D ?U) {t} = \<P>(\<omega> in M. X (Suc n) \<omega> = t \<bar> X n \<omega> = s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure (with (\<lambda>n. prob {\<omega> \<in> space M. X n \<omega> = s} \<noteq> 0) (\<lambda>n. distr (uniform_measure M {\<omega> \<in> space M. X n \<omega> = s}) (count_space UNIV) (X (Suc n))) (uniform_measure (count_space UNIV) {s})) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
proof (rule withI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>x. \<not> prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0) \<Longrightarrow> Sigma_Algebra.measure (uniform_measure (count_space UNIV) {s}) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
 2. \<And>x. prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0 \<Longrightarrow> Sigma_Algebra.measure (distr (uniform_measure M {\<omega> \<in> space M. X x \<omega> = s}) (count_space UNIV) (X (Suc x))) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
fix n'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>x. \<not> prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0) \<Longrightarrow> Sigma_Algebra.measure (uniform_measure (count_space UNIV) {s}) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
 2. \<And>x. prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0 \<Longrightarrow> Sigma_Algebra.measure (distr (uniform_measure M {\<omega> \<in> space M. X x \<omega> = s}) (count_space UNIV) (X (Suc x))) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
assume "?P n'"
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. X n' \<omega> = s} \<noteq> 0

goal (2 subgoals):
 1. (\<And>x. \<not> prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0) \<Longrightarrow> Sigma_Algebra.measure (uniform_measure (count_space UNIV) {s}) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
 2. \<And>x. prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0 \<Longrightarrow> Sigma_Algebra.measure (distr (uniform_measure M {\<omega> \<in> space M. X x \<omega> = s}) (count_space UNIV) (X (Suc x))) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. X n' \<omega> = s} \<noteq> 0

goal (2 subgoals):
 1. (\<And>x. \<not> prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0) \<Longrightarrow> Sigma_Algebra.measure (uniform_measure (count_space UNIV) {s}) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
 2. \<And>x. prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0 \<Longrightarrow> Sigma_Algebra.measure (distr (uniform_measure M {\<omega> \<in> space M. X x \<omega> = s}) (count_space UNIV) (X (Suc x))) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
have "X (Suc n') -` {t} \<inter> space M = {x\<in>space M. X (Suc n') x = t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X (Suc n') -` {t} \<inter> space M = {x \<in> space M. X (Suc n') x = t}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X (Suc n') -` {t} \<inter> space M = {x \<in> space M. X (Suc n') x = t}

goal (2 subgoals):
 1. (\<And>x. \<not> prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0) \<Longrightarrow> Sigma_Algebra.measure (uniform_measure (count_space UNIV) {s}) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
 2. \<And>x. prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0 \<Longrightarrow> Sigma_Algebra.measure (distr (uniform_measure M {\<omega> \<in> space M. X x \<omega> = s}) (count_space UNIV) (X (Suc x))) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prob {\<omega> \<in> space M. X n' \<omega> = s} \<noteq> 0
X (Suc n') -` {t} \<inter> space M = {x \<in> space M. X (Suc n') x = t}
[PROOF STEP]
show "measure (?D n') {t} = \<P>(\<omega> in M. X (Suc n) \<omega> = t \<bar> X n \<omega> = s)"
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space M. X n' \<omega> = s} \<noteq> 0
X (Suc n') -` {t} \<inter> space M = {x \<in> space M. X (Suc n') x = t}

goal (1 subgoal):
 1. Sigma_Algebra.measure (distr (uniform_measure M {\<omega> \<in> space M. X n' \<omega> = s}) (count_space UNIV) (X (Suc n'))) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
using n M.measure_uniform_measure_eq_cond_prob[of "\<lambda>x. X (Suc n') x = t" "\<lambda>x. X n' x = s"]
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space M. X n' \<omega> = s} \<noteq> 0
X (Suc n') -` {t} \<inter> space M = {x \<in> space M. X (Suc n') x = t}
0 < prob {\<omega> \<in> space M. X n \<omega> = s}
\<lbrakk>random_variable (count_space UNIV) (\<lambda>x. X (Suc n') x = t); random_variable (count_space UNIV) (\<lambda>x. X n' x = s)\<rbrakk> \<Longrightarrow> \<P>(x in uniform_measure M {x \<in> space M. X n' x = s}. X (Suc n') x = t) = cond_prob M (\<lambda>x. X (Suc n') x = t) (\<lambda>x. X n' x = s)

goal (1 subgoal):
 1. Sigma_Algebra.measure (distr (uniform_measure M {\<omega> \<in> space M. X n' \<omega> = s}) (count_space UNIV) (X (Suc n'))) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
by (auto simp: measure_distr M.emeasure_eq_measure simp del: measure_uniform_measure intro!: TH)
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (distr (uniform_measure M {\<omega> \<in> space M. X n' \<omega> = s}) (count_space UNIV) (X (Suc n'))) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)

goal (1 subgoal):
 1. (\<And>x. \<not> prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0) \<Longrightarrow> Sigma_Algebra.measure (uniform_measure (count_space UNIV) {s}) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)
[PROOF STEP]
qed (insert n, simp)
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (with (\<lambda>n. prob {\<omega> \<in> space M. X n \<omega> = s} \<noteq> 0) (\<lambda>n. distr (uniform_measure M {\<omega> \<in> space M. X n \<omega> = s}) (count_space UNIV) (X (Suc n))) (uniform_measure (count_space UNIV) {s})) {t} = cond_prob M (\<lambda>\<omega>. X (Suc n) \<omega> = t) (\<lambda>\<omega>. X n \<omega> = s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmf_K2:
  "(\<And>n. \<P>(\<omega> in M. X n \<omega> = s) = 0) \<Longrightarrow> pmf (K s) t = indicator {t} s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. prob {\<omega> \<in> space M. X n \<omega> = s} = 0) \<Longrightarrow> pmf (K s) t = indicat_real {t} s
[PROOF STEP]
apply (transfer fixing: s t)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. prob {\<omega> \<in> space M. X n \<omega> = s} = 0) \<Longrightarrow> Sigma_Algebra.measure (with (\<lambda>n. prob {\<omega> \<in> space M. X n \<omega> = s} \<noteq> 0) (\<lambda>n. distr (uniform_measure M {\<omega> \<in> space M. X n \<omega> = s}) (count_space UNIV) (X (Suc n))) (uniform_measure (count_space UNIV) {s})) {t} = indicat_real {t} s
[PROOF STEP]
apply (rule withI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>n. prob {\<omega> \<in> space M. X n \<omega> = s} = 0; \<And>x. \<not> prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0\<rbrakk> \<Longrightarrow> Sigma_Algebra.measure (uniform_measure (count_space UNIV) {s}) {t} = indicat_real {t} s
 2. \<And>x. \<lbrakk>\<And>n. prob {\<omega> \<in> space M. X n \<omega> = s} = 0; prob {\<omega> \<in> space M. X x \<omega> = s} \<noteq> 0\<rbrakk> \<Longrightarrow> Sigma_Algebra.measure (distr (uniform_measure M {\<omega> \<in> space M. X x \<omega> = s}) (count_space UNIV) (X (Suc x))) {t} = indicat_real {t} s
[PROOF STEP]
apply (auto split: split_indicator)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done