[STATEMENT]
lemma rreq_rrep_sn_simps [simp]:
  "\<And>hops rreqid dip dsn dsk oip osn sip.
           rreq_rrep_sn (Rreq hops rreqid dip dsn dsk oip osn sip) = (osn \<ge> 1)"
  "\<And>hops dip dsn oip sip. rreq_rrep_sn (Rrep hops dip dsn oip sip) = (dsn \<ge> 1)"
  "\<And>dests sip.            rreq_rrep_sn (Rerr dests sip) = True"
  "\<And>d dip.                rreq_rrep_sn (Newpkt d dip)   = True"
  "\<And>d dip sip.            rreq_rrep_sn (Pkt d dip sip)  = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. rreq_rrep_sn (Rreq hops rreqid dip dsn dsk oip osn sip) = (1 \<le> osn)) &&& (\<And>hops dip dsn oip sip. rreq_rrep_sn (Rrep hops dip dsn oip sip) = (1 \<le> dsn))) &&& (\<And>dests sip. rreq_rrep_sn (Rerr dests sip) = True) &&& (\<And>d dip. rreq_rrep_sn (Newpkt d dip) = True) &&& (\<And>d dip sip. rreq_rrep_sn (Pkt d dip sip) = True)
[PROOF STEP]
unfolding rreq_rrep_sn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. (case Rreq hops rreqid dip dsn dsk oip osn sip of Rreq x xa xb xc xd xe osnc xf \<Rightarrow> 1 \<le> osnc | Rrep x xa dsnc xb xc \<Rightarrow> 1 \<le> dsnc | _ \<Rightarrow> True) = (1 \<le> osn)) &&& (\<And>hops dip dsn oip sip. (case Rrep hops dip dsn oip sip of Rreq x xa xb xc xd xe osnc xf \<Rightarrow> 1 \<le> osnc | Rrep x xa dsnc xb xc \<Rightarrow> 1 \<le> dsnc | _ \<Rightarrow> True) = (1 \<le> dsn))) &&& (\<And>dests sip. (case Rerr dests sip of Rreq x xa xb xc xd xe osnc xf \<Rightarrow> 1 \<le> osnc | Rrep x xa dsnc xb xc \<Rightarrow> 1 \<le> dsnc | _ \<Rightarrow> True) = True) &&& (\<And>d dip. (case Newpkt d dip of Rreq x xa xb xc xd xe osnc xf \<Rightarrow> 1 \<le> osnc | Rrep x xa dsnc xb xc \<Rightarrow> 1 \<le> dsnc | _ \<Rightarrow> True) = True) &&& (\<And>d dip sip. (case Pkt d dip sip of Rreq x xa xb xc xd xe osnc xf \<Rightarrow> 1 \<le> osnc | Rrep x xa dsnc xb xc \<Rightarrow> 1 \<le> dsnc | _ \<Rightarrow> True) = True)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma rreq_rrep_fresh [simp]:
  "\<And>hops rreqid dip dsn dsk oip osn sip.
           rreq_rrep_fresh crt (Rreq hops rreqid dip dsn dsk oip osn sip) =
                               (sip \<noteq> oip \<longrightarrow> oip\<in>kD(crt)
                                            \<and> (sqn crt oip > osn
                                               \<or> (sqn crt oip = osn
                                                  \<and> the (dhops crt oip) \<le> hops
                                                  \<and> the (flag crt oip) = val)))"
  "\<And>hops dip dsn oip sip. rreq_rrep_fresh crt (Rrep hops dip dsn oip sip) =
                               (sip \<noteq> dip \<longrightarrow> dip\<in>kD(crt)
                                              \<and> sqn crt dip = dsn
                                              \<and> the (dhops crt dip) = hops
                                              \<and> the (flag crt dip) = val)"
  "\<And>dests sip.            rreq_rrep_fresh crt (Rerr dests sip) = True"
  "\<And>d dip.                rreq_rrep_fresh crt (Newpkt d dip)   = True"
  "\<And>d dip sip.            rreq_rrep_fresh crt (Pkt d dip sip)  = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. rreq_rrep_fresh crt (Rreq hops rreqid dip dsn dsk oip osn sip) = (sip \<noteq> oip \<longrightarrow> oip \<in> kD crt \<and> (osn < sqn crt oip \<or> sqn crt oip = osn \<and> the (dhops crt oip) \<le> hops \<and> the (flag crt oip) = val))) &&& (\<And>hops dip dsn oip sip. rreq_rrep_fresh crt (Rrep hops dip dsn oip sip) = (sip \<noteq> dip \<longrightarrow> dip \<in> kD crt \<and> sqn crt dip = dsn \<and> the (dhops crt dip) = hops \<and> the (flag crt dip) = val))) &&& (\<And>dests sip. rreq_rrep_fresh crt (Rerr dests sip) = True) &&& (\<And>d dip. rreq_rrep_fresh crt (Newpkt d dip) = True) &&& (\<And>d dip sip. rreq_rrep_fresh crt (Pkt d dip sip) = True)
[PROOF STEP]
unfolding rreq_rrep_fresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. (case Rreq hops rreqid dip dsn dsk oip osn sip of Rreq hopsc x xa xb xc oipc osnc ipcc \<Rightarrow> ipcc \<noteq> oipc \<longrightarrow> oipc \<in> kD crt \<and> (osnc < sqn crt oipc \<or> sqn crt oipc = osnc \<and> the (dhops crt oipc) \<le> hopsc \<and> the (flag crt oipc) = val) | Rrep hopsc dipc dsnc x ipcc \<Rightarrow> ipcc \<noteq> dipc \<longrightarrow> dipc \<in> kD crt \<and> sqn crt dipc = dsnc \<and> the (dhops crt dipc) = hopsc \<and> the (flag crt dipc) = val | _ \<Rightarrow> True) = (sip \<noteq> oip \<longrightarrow> oip \<in> kD crt \<and> (osn < sqn crt oip \<or> sqn crt oip = osn \<and> the (dhops crt oip) \<le> hops \<and> the (flag crt oip) = val))) &&& (\<And>hops dip dsn oip sip. (case Rrep hops dip dsn oip sip of Rreq hopsc x xa xb xc oipc osnc ipcc \<Rightarrow> ipcc \<noteq> oipc \<longrightarrow> oipc \<in> kD crt \<and> (osnc < sqn crt oipc \<or> sqn crt oipc = osnc \<and> the (dhops crt oipc) \<le> hopsc \<and> the (flag crt oipc) = val) | Rrep hopsc dipc dsnc x ipcc \<Rightarrow> ipcc \<noteq> dipc \<longrightarrow> dipc \<in> kD crt \<and> sqn crt dipc = dsnc \<and> the (dhops crt dipc) = hopsc \<and> the (flag crt dipc) = val | _ \<Rightarrow> True) = (sip \<noteq> dip \<longrightarrow> dip \<in> kD crt \<and> sqn crt dip = dsn \<and> the (dhops crt dip) = hops \<and> the (flag crt dip) = val))) &&& (\<And>dests sip. (case Rerr dests sip of Rreq hopsc x xa xb xc oipc osnc ipcc \<Rightarrow> ipcc \<noteq> oipc \<longrightarrow> oipc \<in> kD crt \<and> (osnc < sqn crt oipc \<or> sqn crt oipc = osnc \<and> the (dhops crt oipc) \<le> hopsc \<and> the (flag crt oipc) = val) | Rrep hopsc dipc dsnc x ipcc \<Rightarrow> ipcc \<noteq> dipc \<longrightarrow> dipc \<in> kD crt \<and> sqn crt dipc = dsnc \<and> the (dhops crt dipc) = hopsc \<and> the (flag crt dipc) = val | _ \<Rightarrow> True) = True) &&& (\<And>d dip. (case Newpkt d dip of Rreq hopsc x xa xb xc oipc osnc ipcc \<Rightarrow> ipcc \<noteq> oipc \<longrightarrow> oipc \<in> kD crt \<and> (osnc < sqn crt oipc \<or> sqn crt oipc = osnc \<and> the (dhops crt oipc) \<le> hopsc \<and> the (flag crt oipc) = val) | Rrep hopsc dipc dsnc x ipcc \<Rightarrow> ipcc \<noteq> dipc \<longrightarrow> dipc \<in> kD crt \<and> sqn crt dipc = dsnc \<and> the (dhops crt dipc) = hopsc \<and> the (flag crt dipc) = val | _ \<Rightarrow> True) = True) &&& (\<And>d dip sip. (case Pkt d dip sip of Rreq hopsc x xa xb xc oipc osnc ipcc \<Rightarrow> ipcc \<noteq> oipc \<longrightarrow> oipc \<in> kD crt \<and> (osnc < sqn crt oipc \<or> sqn crt oipc = osnc \<and> the (dhops crt oipc) \<le> hopsc \<and> the (flag crt oipc) = val) | Rrep hopsc dipc dsnc x ipcc \<Rightarrow> ipcc \<noteq> dipc \<longrightarrow> dipc \<in> kD crt \<and> sqn crt dipc = dsnc \<and> the (dhops crt dipc) = hopsc \<and> the (flag crt dipc) = val | _ \<Rightarrow> True) = True)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma rerr_invalid [simp]:
  "\<And>hops rreqid dip dsn dsk oip osn sip.
                           rerr_invalid crt (Rreq hops rreqid dip dsn dsk oip osn sip) = True"
  "\<And>hops dip dsn oip sip. rerr_invalid crt (Rrep hops dip dsn oip sip) = True"
  "\<And>dests sip.            rerr_invalid crt (Rerr dests sip) = (\<forall>rip\<in>dom(dests).
                                                 rip\<in>iD(crt) \<and> the (dests rip) = sqn crt rip)"
  "\<And>d dip.                rerr_invalid crt (Newpkt d dip)   = True"
  "\<And>d dip sip.            rerr_invalid crt (Pkt d dip sip)  = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. rerr_invalid crt (Rreq hops rreqid dip dsn dsk oip osn sip) = True) &&& (\<And>hops dip dsn oip sip. rerr_invalid crt (Rrep hops dip dsn oip sip) = True)) &&& (\<And>dests sip. rerr_invalid crt (Rerr dests sip) = (\<forall>rip\<in>dom dests. rip \<in> iD crt \<and> the (dests rip) = sqn crt rip)) &&& (\<And>d dip. rerr_invalid crt (Newpkt d dip) = True) &&& (\<And>d dip sip. rerr_invalid crt (Pkt d dip sip) = True)
[PROOF STEP]
unfolding rerr_invalid_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. (case Rreq hops rreqid dip dsn dsk oip osn sip of Rerr destsc x \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> iD crt \<and> the (destsc ripc) = sqn crt ripc | _ \<Rightarrow> True) = True) &&& (\<And>hops dip dsn oip sip. (case Rrep hops dip dsn oip sip of Rerr destsc x \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> iD crt \<and> the (destsc ripc) = sqn crt ripc | _ \<Rightarrow> True) = True)) &&& (\<And>dests sip. (case Rerr dests sip of Rerr destsc x \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> iD crt \<and> the (destsc ripc) = sqn crt ripc | _ \<Rightarrow> True) = (\<forall>rip\<in>dom dests. rip \<in> iD crt \<and> the (dests rip) = sqn crt rip)) &&& (\<And>d dip. (case Newpkt d dip of Rerr destsc x \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> iD crt \<and> the (destsc ripc) = sqn crt ripc | _ \<Rightarrow> True) = True) &&& (\<And>d dip sip. (case Pkt d dip sip of Rerr destsc x \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> iD crt \<and> the (destsc ripc) = sqn crt ripc | _ \<Rightarrow> True) = True)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma not_in_net_ips_fst_init_missing [simp]:
  assumes "i \<notin> net_ips \<sigma>"
    shows "fst (initmissing (netgmap fst \<sigma>)) i = aodv_init i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (initmissing (netgmap fst \<sigma>)) i = aodv_init i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<notin> net_ips \<sigma>

goal (1 subgoal):
 1. fst (initmissing (netgmap fst \<sigma>)) i = aodv_init i
[PROOF STEP]
unfolding initmissing_def
[PROOF STATE]
proof (prove)
using this:
i \<notin> net_ips \<sigma>

goal (1 subgoal):
 1. fst (\<lambda>i. case fst (netgmap fst \<sigma>) i of None \<Rightarrow> aodv_init i | Some s \<Rightarrow> s, snd (netgmap fst \<sigma>)) i = aodv_init i
[PROOF STEP]
by simp


[STATEMENT]
lemma fst_initmissing_netgmap_pair_fst [simp]:
  "fst (initmissing (netgmap (\<lambda>(p, q). (fst (id p), snd (id p), q)) s))
                                               = fst (initmissing (netgmap fst s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (initmissing (netgmap (\<lambda>(p, q). (fst (id p), snd (id p), q)) s)) = fst (initmissing (netgmap fst s))
[PROOF STEP]
unfolding initmissing_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (\<lambda>i. case fst (netgmap (\<lambda>(p, q). (fst (id p), snd (id p), q)) s) i of None \<Rightarrow> aodv_init i | Some s \<Rightarrow> s, snd (netgmap (\<lambda>(p, q). (fst (id p), snd (id p), q)) s)) = fst (\<lambda>i. case fst (netgmap fst s) i of None \<Rightarrow> aodv_init i | Some s \<Rightarrow> s, snd (netgmap fst s))
[PROOF STEP]
by auto


[STATEMENT]
lemma fst_initmissing_netgmap_default_aodv_init_netlift:
  "fst (initmissing (netgmap fst s)) = default aodv_init (netlift fst s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (initmissing (netgmap fst s)) = Lib.default aodv_init (netlift fst s)
[PROOF STEP]
unfolding initmissing_def default_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (\<lambda>i. case fst (netgmap fst s) i of None \<Rightarrow> aodv_init i | Some s \<Rightarrow> s, snd (netgmap fst s)) = (\<lambda>i. case netlift fst s i of None \<Rightarrow> aodv_init i | Some s \<Rightarrow> s)
[PROOF STEP]
by (simp add: fst_netgmap_netlift del: One_nat_def)


[STATEMENT]
lemma \<epsilon>_uh_nonneg : "\<epsilon>_uh \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<epsilon>_uh
[PROOF STEP]
by(auto 4 3 intro!: cSUP_upper2 bdd_aboveI2[where M=1] cSUP_least pmf_le_1 pmf_nonneg simp add: \<epsilon>_uh_def)


[STATEMENT]
lemma hash_ineq_card:
  assumes "finite W"
  shows "spmf (game_hash_set W) True \<le> \<epsilon>_uh * card W * card W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
let ?M = "measure (measure_spmf seed_gen)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
have bound: "?M {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh" for w w'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh
[PROOF STEP]
have "?M {x. hash x w = hash x w' \<and> w \<noteq> w'} = spmf (game_hash w w') True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} = spmf (game_hash w w') True
[PROOF STEP]
by(simp add: game_hash_def spmf_conv_measure_spmf map_spmf_conv_bind_spmf[symmetric] measure_map_spmf vimage_def)
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} = spmf (game_hash w w') True

goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} = spmf (game_hash w w') True

goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh
[PROOF STEP]
have "\<dots> \<le> \<epsilon>_uh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (game_hash w w') True \<le> \<epsilon>_uh
[PROOF STEP]
unfolding \<epsilon>_uh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (game_hash w w') True \<le> (\<Squnion>w w'. spmf (game_hash w w') True)
[PROOF STEP]
by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] cSUP_least simp add: pmf_le_1)
[PROOF STATE]
proof (state)
this:
spmf (game_hash w w') True \<le> \<epsilon>_uh

goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh

goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'} \<le> \<epsilon>_uh

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x ?w = hash x ?w' \<and> ?w \<noteq> ?w'} \<le> \<epsilon>_uh

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
have "spmf (game_hash_set W) True = ?M {x. \<exists>xa\<in>W. \<exists>y\<in>W. hash x xa = hash x y \<and> xa \<noteq> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (game_hash_set W) True = Sigma_Algebra.measure (measure_spmf seed_gen) {x. \<exists>xa\<in>W. \<exists>y\<in>W. hash x xa = hash x y \<and> xa \<noteq> y}
[PROOF STEP]
by(auto simp add: game_hash_set_def inj_on_def map_spmf_conv_bind_spmf[symmetric] spmf_conv_measure_spmf measure_map_spmf vimage_def)
[PROOF STATE]
proof (state)
this:
spmf (game_hash_set W) True = Sigma_Algebra.measure (measure_spmf seed_gen) {x. \<exists>xa\<in>W. \<exists>y\<in>W. hash x xa = hash x y \<and> xa \<noteq> y}

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
spmf (game_hash_set W) True = Sigma_Algebra.measure (measure_spmf seed_gen) {x. \<exists>xa\<in>W. \<exists>y\<in>W. hash x xa = hash x y \<and> xa \<noteq> y}

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
have "{x. \<exists>xa\<in>W. \<exists>y\<in>W. hash x xa = hash x y \<and> xa \<noteq> y} = (\<Union>(w, w') \<in> W\<times> W. {x. hash x w = hash x w' \<and> w \<noteq> w'})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<exists>xa\<in>W. \<exists>y\<in>W. hash x xa = hash x y \<and> xa \<noteq> y} = (\<Union>(w, w')\<in>W \<times> W. {x. hash x w = hash x w' \<and> w \<noteq> w'})
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
{x. \<exists>xa\<in>W. \<exists>y\<in>W. hash x xa = hash x y \<and> xa \<noteq> y} = (\<Union>(w, w')\<in>W \<times> W. {x. hash x w = hash x w' \<and> w \<noteq> w'})

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x. \<exists>xa\<in>W. \<exists>y\<in>W. hash x xa = hash x y \<and> xa \<noteq> y} = (\<Union>(w, w')\<in>W \<times> W. {x. hash x w = hash x w' \<and> w \<noteq> w'})

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
have "?M \<dots> \<le> (\<Sum>(w, w')\<in>W \<times> W. ?M {x. hash x w = hash x w' \<and> w \<noteq> w'})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_spmf seed_gen) (\<Union>(w, w')\<in>W \<times> W. {x. hash x w = hash x w' \<and> w \<noteq> w'}) \<le> (\<Sum>(w, w')\<in>W \<times> W. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'})
[PROOF STEP]
by(auto intro!: measure_spmf.finite_measure_subadditive_finite simp add: split_def assms)
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (measure_spmf seed_gen) (\<Union>(w, w')\<in>W \<times> W. {x. hash x w = hash x w' \<and> w \<noteq> w'}) \<le> (\<Sum>(w, w')\<in>W \<times> W. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'})

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (measure_spmf seed_gen) (\<Union>(w, w')\<in>W \<times> W. {x. hash x w = hash x w' \<and> w \<noteq> w'}) \<le> (\<Sum>(w, w')\<in>W \<times> W. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'})

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
have "\<dots> \<le> (\<Sum>(w, w')\<in>W \<times> W. \<epsilon>_uh)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(w, w')\<in>W \<times> W. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'}) \<le> (\<Sum>(w, w')\<in>W \<times> W. \<epsilon>_uh)
[PROOF STEP]
by(rule sum_mono)(clarsimp simp add: bound)
[PROOF STATE]
proof (state)
this:
(\<Sum>(w, w')\<in>W \<times> W. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'}) \<le> (\<Sum>(w, w')\<in>W \<times> W. \<epsilon>_uh)

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(w, w')\<in>W \<times> W. Sigma_Algebra.measure (measure_spmf seed_gen) {x. hash x w = hash x w' \<and> w \<noteq> w'}) \<le> (\<Sum>(w, w')\<in>W \<times> W. \<epsilon>_uh)

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
have "\<dots> =  \<epsilon>_uh * card(W) * card(W)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(w, w')\<in>W \<times> W. \<epsilon>_uh) = \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
by(simp add: card_cartesian_product)
[PROOF STATE]
proof (state)
this:
(\<Sum>(w, w')\<in>W \<times> W. \<epsilon>_uh) = \<epsilon>_uh * real (card W) * real (card W)

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)

goal (1 subgoal):
 1. spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
spmf (game_hash_set W) True \<le> \<epsilon>_uh * real (card W) * real (card W)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lossless_rand [simp]: "lossless_spmf rand"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf rand
[PROOF STEP]
by(simp add: rand_def range_f_finite range_f_nonempty)


[STATEMENT]
theorem prf_prf'_advantage:
  assumes "prf'.lossless \"
  and bounded: "prf'.ibounded_by \ q"
  shows "prf'.advantage \  \<le> prf.advantage (prf'_reduction \) + hash.\<epsilon>_uh * q * q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
including lifting_syntax
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
let ?\ = "prf'_reduction \"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
define cr where "cr = (\<lambda>_ :: unit \<times> unit. \<lambda>_ :: unit. True)"
[PROOF STATE]
proof (state)
this:
cr = (\<lambda>_ _. True)

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have [transfer_rule]: "cr ((), ()) ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr ((), ()) ()
[PROOF STEP]
by(simp add: cr_def)
[PROOF STATE]
proof (state)
this:
cr ((), ()) ()

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have "prf.game_0 ?\ = prf'.game_0 \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.prf.game_0 (prf'_reduction \) = prf'.game_0 \
[PROOF STEP]
unfolding prf'.game_0_def prf.game_0_def prf'_reduction_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. key_gen \<bind> (\<lambda>key. exec_gpv (local.prf.prf_oracle key) (lift_spmf seed_gen \<bind> (\<lambda>seed. inline (reduction_oracle seed) \ () \<bind> (\<lambda>(b, \<sigma>). Generative_Probabilistic_Value.Done b))) () \<bind> (\<lambda>(b, uu_). return_spmf b)) = key_seed_gen \<bind> (\<lambda>key. exec_gpv (prf'.prf_oracle key) \ () \<bind> (\<lambda>(b, uu_). return_spmf b))
[PROOF STEP]
unfolding key_seed_gen_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. key_gen \<bind> (\<lambda>key. exec_gpv (local.prf.prf_oracle key) (lift_spmf seed_gen \<bind> (\<lambda>seed. inline (reduction_oracle seed) \ () \<bind> (\<lambda>(b, \<sigma>). Generative_Probabilistic_Value.Done b))) () \<bind> (\<lambda>(b, uu_). return_spmf b)) = key_gen \<bind> (\<lambda>k. seed_gen \<bind> (\<lambda>s. return_spmf (k, s))) \<bind> (\<lambda>key. exec_gpv (prf'.prf_oracle key) \ () \<bind> (\<lambda>(b, uu_). return_spmf b))
[PROOF STEP]
by(simp add: exec_gpv_bind split_def exec_gpv_inline reduction_oracle_def bind_map_spmf prf.prf_oracle_def prf'.prf_oracle_def[abs_def])
        (transfer_prover)
[PROOF STATE]
proof (state)
this:
local.prf.game_0 (prf'_reduction \) = prf'.game_0 \

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
local.prf.game_0 (prf'_reduction \) = prf'.game_0 \

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
note hop1 = this[symmetric]
[PROOF STATE]
proof (state)
this:
prf'.game_0 \ = local.prf.game_0 (prf'_reduction \)

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
define semi_forgetful_RO where "semi_forgetful_RO = (\<lambda>seed :: 'seed. \<lambda>(\<sigma> :: '\<alpha> \<rightharpoonup> '\<beta> \<times> '\<gamma>, b :: bool). \<lambda>x.
    case \<sigma> (h seed x) of Some (a, y) \<Rightarrow> return_spmf (y, (\<sigma>, a \<noteq> x \<or> b))
     | None \<Rightarrow> bind_spmf rand (\<lambda>y. return_spmf (y, (\<sigma>(h seed x \<mapsto> (x, y)), b))))"
[PROOF STATE]
proof (state)
this:
semi_forgetful_RO = (\<lambda>seed (\<sigma>, b) x. case \<sigma> (h seed x) of None \<Rightarrow> rand \<bind> (\<lambda>y. return_spmf (y, \<sigma>(h seed x \<mapsto> (x, y)), b)) | Some (a, y) \<Rightarrow> return_spmf (y, \<sigma>, a \<noteq> x \<or> b))

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
define game_semi_forgetful where "game_semi_forgetful = do {
     seed :: 'seed \<leftarrow> seed_gen;
     (b, rep) \<leftarrow> exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False);
     return_spmf (b, rep)
   }"
[PROOF STATE]
proof (state)
this:
game_semi_forgetful = seed_gen \<bind> (\<lambda>seed. exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False) \<bind> (\<lambda>(b, rep). return_spmf (b, rep)))

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have bad_semi_forgetful [simp]: "callee_invariant (semi_forgetful_RO seed) snd" for seed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. callee_invariant (semi_forgetful_RO seed) snd
[PROOF STEP]
by(unfold_locales)(auto simp add: semi_forgetful_RO_def split: option.split_asm)
[PROOF STATE]
proof (state)
this:
callee_invariant (semi_forgetful_RO ?seed1) snd

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have lossless_semi_forgetful [simp]: "lossless_spmf (semi_forgetful_RO seed s1 x)" for seed s1 x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (semi_forgetful_RO seed s1 x)
[PROOF STEP]
by(simp add: semi_forgetful_RO_def split_def split: option.split)
[PROOF STATE]
proof (state)
this:
lossless_spmf (semi_forgetful_RO ?seed1 ?s1.1 ?x1)

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
lossless_spmf (semi_forgetful_RO ?seed1 ?s1.1 ?x1)

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
define cr
      where "cr = (\<lambda>(_ :: unit, \<sigma>) (\<sigma>' :: '\<alpha> \<Rightarrow> ('\<beta> \<times> '\<gamma>) option, _ :: bool). \<sigma> = map_option snd \<circ> \<sigma>')"
[PROOF STATE]
proof (state)
this:
cr = (\<lambda>(uu_, \<sigma>) (\<sigma>', uu_). \<sigma> = map_option snd \<circ> \<sigma>')

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
define initial where "initial = (Map.empty :: '\<alpha> \<Rightarrow> ('\<beta> \<times> '\<gamma>) option, False)"
[PROOF STATE]
proof (state)
this:
initial = (Map.empty, False)

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have [transfer_rule]: "cr ((), Map.empty) initial"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr ((), Map.empty) initial
[PROOF STEP]
by(simp add: cr_def initial_def fun_eq_iff)
[PROOF STATE]
proof (state)
this:
cr ((), Map.empty) initial

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have [transfer_rule]:  "((=) ===> cr ===> (=) ===> rel_spmf (rel_prod (=) cr))
        (\<lambda>y p ya. do {y \<leftarrow> prf.random_oracle (snd p) (h y ya); return_spmf (fst y, (), snd y) })
        semi_forgetful_RO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> cr ===> (=) ===> rel_spmf (rel_prod (=) cr)) (\<lambda>y p ya. prf.random_oracle (snd p) (h y ya) \<bind> (\<lambda>y. return_spmf (fst y, (), snd y))) semi_forgetful_RO
[PROOF STEP]
by(auto simp add: semi_forgetful_RO_def cr_def prf.random_oracle_def rel_fun_def fun_eq_iff split: option.split intro!: rel_spmf_bind_reflI)
[PROOF STATE]
proof (state)
this:
((=) ===> cr ===> (=) ===> rel_spmf (rel_prod (=) cr)) (\<lambda>y p ya. prf.random_oracle (snd p) (h y ya) \<bind> (\<lambda>y. return_spmf (fst y, (), snd y))) semi_forgetful_RO

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have "prf.game_1 ?\ = map_spmf fst game_semi_forgetful"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.prf.game_1 (prf'_reduction \) = map_spmf fst game_semi_forgetful
[PROOF STEP]
unfolding prf.game_1_def prf'_reduction_def game_semi_forgetful_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_gpv prf.random_oracle (lift_spmf seed_gen \<bind> (\<lambda>seed. inline (reduction_oracle seed) \ () \<bind> (\<lambda>(b, \<sigma>). Generative_Probabilistic_Value.Done b))) Map.empty \<bind> (\<lambda>(b, uu_). return_spmf b) = map_spmf fst (seed_gen \<bind> (\<lambda>seed. exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False) \<bind> (\<lambda>(b, rep). return_spmf (b, rep))))
[PROOF STEP]
by(simp add: exec_gpv_bind exec_gpv_inline split_def bind_map_spmf map_spmf_bind_spmf o_def map_spmf_conv_bind_spmf reduction_oracle_def initial_def[symmetric])
        (transfer_prover)
[PROOF STATE]
proof (state)
this:
local.prf.game_1 (prf'_reduction \) = map_spmf fst game_semi_forgetful

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
local.prf.game_1 (prf'_reduction \) = map_spmf fst game_semi_forgetful

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
note hop2 = this
[PROOF STATE]
proof (state)
this:
local.prf.game_1 (prf'_reduction \) = map_spmf fst game_semi_forgetful

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
define game_semi_forgetful_bad where "game_semi_forgetful_bad = do {
       seed :: 'seed \<leftarrow> seed_gen;
       x \<leftarrow> exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False);
       return_spmf (snd x)
       }"
[PROOF STATE]
proof (state)
this:
game_semi_forgetful_bad = seed_gen \<bind> (\<lambda>seed. exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False) \<bind> (\<lambda>x. return_spmf (snd x)))

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have game_semi_forgetful_bad : "map_spmf snd game_semi_forgetful = game_semi_forgetful_bad"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf snd game_semi_forgetful = game_semi_forgetful_bad
[PROOF STEP]
unfolding game_semi_forgetful_bad_def game_semi_forgetful_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf snd (seed_gen \<bind> (\<lambda>seed. exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False) \<bind> (\<lambda>(b, rep). return_spmf (b, rep)))) = seed_gen \<bind> (\<lambda>seed. exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False) \<bind> (\<lambda>x. return_spmf (snd x)))
[PROOF STEP]
by(simp add: map_spmf_bind_spmf o_def)
[PROOF STATE]
proof (state)
this:
map_spmf snd game_semi_forgetful = game_semi_forgetful_bad

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have bad_random_oracle_A [simp]: "callee_invariant prf.random_oracle (\<lambda>\<sigma>. \<not> inj_on (h seed) (dom \<sigma>))" for seed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. callee_invariant prf.random_oracle (\<lambda>\<sigma>. \<not> inj_on (h seed) (dom \<sigma>))
[PROOF STEP]
by unfold_locales(auto simp add: prf.random_oracle_def split: option.split_asm)
[PROOF STATE]
proof (state)
this:
callee_invariant prf.random_oracle (\<lambda>\<sigma>. \<not> inj_on (h ?seed1) (dom \<sigma>))

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
define invar
    where "invar = (\<lambda>seed (\<sigma>1, b) (\<sigma>2 :: '\<beta> \<Rightarrow> '\<gamma> option). \<not> b \<and> dom \<sigma>1 = h seed ` dom \<sigma>2 \<and>
      (\<forall>x \<in> dom \<sigma>2. \<sigma>1 (h seed x) = map_option (Pair x) (\<sigma>2 x)))"
[PROOF STATE]
proof (state)
this:
invar = (\<lambda>seed (\<sigma>1, b) \<sigma>2. \<not> b \<and> dom \<sigma>1 = h seed ` dom \<sigma>2 \<and> (\<forall>x\<in>dom \<sigma>2. \<sigma>1 (h seed x) = map_option (Pair x) (\<sigma>2 x)))

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have rel_spmf_oracle_adv:
    "rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h seed) (dom s2) \<and> (inj_on (h seed) (dom s2) \<longrightarrow> x = y \<and> invar seed s1 s2))
      (exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False))
      (exec_gpv prf.random_oracle \ Map.empty)"
    if seed: "seed \<in> set_spmf seed_gen" for seed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h seed) (dom s2) \<and> (inj_on (h seed) (dom s2) \<longrightarrow> x = y \<and> invar seed s1 s2)) (exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False)) (exec_gpv prf.random_oracle \ Map.empty)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h seed) (dom s2) \<and> (inj_on (h seed) (dom s2) \<longrightarrow> x = y \<and> invar seed s1 s2)) (exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False)) (exec_gpv prf.random_oracle \ Map.empty)
[PROOF STEP]
have invar_initial [simp]: "invar seed (Map.empty, False) Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar seed (Map.empty, False) Map.empty
[PROOF STEP]
by(simp add: invar_def)
[PROOF STATE]
proof (state)
this:
invar seed (Map.empty, False) Map.empty

goal (1 subgoal):
 1. rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h seed) (dom s2) \<and> (inj_on (h seed) (dom s2) \<longrightarrow> x = y \<and> invar seed s1 s2)) (exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False)) (exec_gpv prf.random_oracle \ Map.empty)
[PROOF STEP]
have invarD_inj: "inj_on (h seed) (dom s2)" if "invar seed bs1 s2" for bs1 s2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (h seed) (dom s2)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
invar seed bs1 s2

goal (1 subgoal):
 1. inj_on (h seed) (dom s2)
[PROOF STEP]
by(auto intro!: inj_onI simp add: invar_def)(metis domI domIff option.map_sel prod.inject)
[PROOF STATE]
proof (state)
this:
invar seed ?bs1.1 ?s2.1 \<Longrightarrow> inj_on (h seed) (dom ?s2.1)

goal (1 subgoal):
 1. rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h seed) (dom s2) \<and> (inj_on (h seed) (dom s2) \<longrightarrow> x = y \<and> invar seed s1 s2)) (exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False)) (exec_gpv prf.random_oracle \ Map.empty)
[PROOF STEP]
let ?R = "\<lambda>(a, s1) (b, s2 :: '\<beta> \<Rightarrow> '\<gamma> option).
        snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and>
        (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h seed) (dom s2) \<and> (inj_on (h seed) (dom s2) \<longrightarrow> x = y \<and> invar seed s1 s2)) (exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False)) (exec_gpv prf.random_oracle \ Map.empty)
[PROOF STEP]
have step: "rel_spmf ?R (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)"
      if X: "invar seed \<sigma>1b s2" for s2 \<sigma>1b x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
obtain \<sigma>1 b where [simp]: "\<sigma>1b = (\<sigma>1, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<sigma>1 b. \<sigma>1b = (\<sigma>1, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases \<sigma>1b)
[PROOF STATE]
proof (state)
this:
\<sigma>1b = (\<sigma>1, b)

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
invar seed \<sigma>1b s2
[PROOF STEP]
have not_b: "\<not> b"
        and dom: "dom \<sigma>1 = h seed ` dom s2"
        and eq: "\<forall>x\<in>dom s2. \<sigma>1 (h seed x) = map_option (Pair x) (s2 x)"
[PROOF STATE]
proof (prove)
using this:
invar seed \<sigma>1b s2

goal (1 subgoal):
 1. \<not> b &&& dom \<sigma>1 = h seed ` dom s2 &&& \<forall>x\<in>dom s2. \<sigma>1 (h seed x) = map_option (Pair x) (s2 x)
[PROOF STEP]
by(simp_all add: invar_def)
[PROOF STATE]
proof (state)
this:
\<not> b
dom \<sigma>1 = h seed ` dom s2
\<forall>x\<in>dom s2. \<sigma>1 (h seed x) = map_option (Pair x) (s2 x)

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
invar seed \<sigma>1b s2
[PROOF STEP]
have inj: "inj_on (h seed) (dom s2)"
[PROOF STATE]
proof (prove)
using this:
invar seed \<sigma>1b s2

goal (1 subgoal):
 1. inj_on (h seed) (dom s2)
[PROOF STEP]
by(rule invarD_inj)
[PROOF STATE]
proof (state)
this:
inj_on (h seed) (dom s2)

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
have not_in_image: "h seed x \<notin> h seed ` (dom s2 - {x})" if "\<sigma>1 (h seed x) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h seed x \<notin> h seed ` (dom s2 - {x})
[PROOF STEP]
proof (rule notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h seed x \<in> h seed ` (dom s2 - {x}) \<Longrightarrow> False
[PROOF STEP]
assume "h seed x \<in> h seed ` (dom s2 - {x})"
[PROOF STATE]
proof (state)
this:
h seed x \<in> h seed ` (dom s2 - {x})

goal (1 subgoal):
 1. h seed x \<in> h seed ` (dom s2 - {x}) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h seed x \<in> h seed ` (dom s2 - {x})
[PROOF STEP]
obtain y where "y \<in> dom s2" and hx_hy: "h seed x = h seed y"
[PROOF STATE]
proof (prove)
using this:
h seed x \<in> h seed ` (dom s2 - {x})

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> dom s2; h seed x = h seed y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
y \<in> dom s2
h seed x = h seed y

goal (1 subgoal):
 1. h seed x \<in> h seed ` (dom s2 - {x}) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> dom s2
h seed x = h seed y
[PROOF STEP]
have "\<sigma>1 (h seed y) = None"
[PROOF STATE]
proof (prove)
using this:
y \<in> dom s2
h seed x = h seed y

goal (1 subgoal):
 1. \<sigma>1 (h seed y) = None
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
y \<in> dom s2
h seed x = h seed y
\<sigma>1 (h seed x) = None

goal (1 subgoal):
 1. \<sigma>1 (h seed y) = None
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
\<sigma>1 (h seed y) = None

goal (1 subgoal):
 1. h seed x \<in> h seed ` (dom s2 - {x}) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<sigma>1 (h seed y) = None
[PROOF STEP]
have "h seed y \<notin> h seed ` dom s2"
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 (h seed y) = None

goal (1 subgoal):
 1. h seed y \<notin> h seed ` dom s2
[PROOF STEP]
using dom
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 (h seed y) = None
dom \<sigma>1 = h seed ` dom s2

goal (1 subgoal):
 1. h seed y \<notin> h seed ` dom s2
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
h seed y \<notin> h seed ` dom s2

goal (1 subgoal):
 1. h seed x \<in> h seed ` (dom s2 - {x}) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h seed y \<notin> h seed ` dom s2
[PROOF STEP]
have "y \<notin> dom s2"
[PROOF STATE]
proof (prove)
using this:
h seed y \<notin> h seed ` dom s2

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

goal (1 subgoal):
 1. h seed x \<in> h seed ` (dom s2 - {x}) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<notin> dom s2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y \<notin> dom s2

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>y \<in> dom s2\<close>
[PROOF STATE]
proof (prove)
using this:
y \<notin> dom s2
y \<in> dom s2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma>1 (h seed x) = None \<Longrightarrow> h seed x \<notin> h seed ` (dom s2 - {x})

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
proof(cases "\<sigma>1 (h seed x)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<sigma>1 (h seed x) = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
 2. \<And>a. \<sigma>1 (h seed x) = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
case \<sigma>1: None
[PROOF STATE]
proof (state)
this:
\<sigma>1 (h seed x) = None

goal (2 subgoals):
 1. \<sigma>1 (h seed x) = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
 2. \<And>a. \<sigma>1 (h seed x) = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
hence s2: "s2 x = None"
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 (h seed x) = None

goal (1 subgoal):
 1. s2 x = None
[PROOF STEP]
using dom
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 (h seed x) = None
dom \<sigma>1 = h seed ` dom s2

goal (1 subgoal):
 1. s2 x = None
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
s2 x = None

goal (2 subgoals):
 1. \<sigma>1 (h seed x) = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
 2. \<And>a. \<sigma>1 (h seed x) = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
have "insert (h seed x) (dom \<sigma>1) = insert (h seed x) (h seed ` dom s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (h seed x) (dom \<sigma>1) = insert (h seed x) (h seed ` dom s2)
[PROOF STEP]
by(simp add: dom)
[PROOF STATE]
proof (state)
this:
insert (h seed x) (dom \<sigma>1) = insert (h seed x) (h seed ` dom s2)

goal (2 subgoals):
 1. \<sigma>1 (h seed x) = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
 2. \<And>a. \<sigma>1 (h seed x) = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert (h seed x) (dom \<sigma>1) = insert (h seed x) (h seed ` dom s2)
[PROOF STEP]
have invar_update: "invar seed (\<sigma>1(h seed x \<mapsto> (x, bs)), False) (s2(x \<mapsto> bs))" for bs
[PROOF STATE]
proof (prove)
using this:
insert (h seed x) (dom \<sigma>1) = insert (h seed x) (h seed ` dom s2)

goal (1 subgoal):
 1. invar seed (\<sigma>1(h seed x \<mapsto> (x, bs)), False) (s2(x \<mapsto> bs))
[PROOF STEP]
using inj not_b not_in_image \<sigma>1 dom
[PROOF STATE]
proof (prove)
using this:
insert (h seed x) (dom \<sigma>1) = insert (h seed x) (h seed ` dom s2)
inj_on (h seed) (dom s2)
\<not> b
\<sigma>1 (h seed x) = None \<Longrightarrow> h seed x \<notin> h seed ` (dom s2 - {x})
\<sigma>1 (h seed x) = None
dom \<sigma>1 = h seed ` dom s2

goal (1 subgoal):
 1. invar seed (\<sigma>1(h seed x \<mapsto> (x, bs)), False) (s2(x \<mapsto> bs))
[PROOF STEP]
by(auto simp add: invar_def domIff eq) (metis domI domIff imageI)
[PROOF STATE]
proof (state)
this:
invar seed (\<sigma>1(h seed x \<mapsto> (x, ?bs2)), False) (s2(x \<mapsto> ?bs2))

goal (2 subgoals):
 1. \<sigma>1 (h seed x) = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
 2. \<And>a. \<sigma>1 (h seed x) = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
with \<sigma>1 s2
[PROOF STATE]
proof (chain)
picking this:
\<sigma>1 (h seed x) = None
s2 x = None
invar seed (\<sigma>1(h seed x \<mapsto> (x, ?bs2)), False) (s2(x \<mapsto> ?bs2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 (h seed x) = None
s2 x = None
invar seed (\<sigma>1(h seed x \<mapsto> (x, ?bs2)), False) (s2(x \<mapsto> ?bs2))

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
using inj not_b not_in_image
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 (h seed x) = None
s2 x = None
invar seed (\<sigma>1(h seed x \<mapsto> (x, ?bs2)), False) (s2(x \<mapsto> ?bs2))
inj_on (h seed) (dom s2)
\<not> b
\<sigma>1 (h seed x) = None \<Longrightarrow> h seed x \<notin> h seed ` (dom s2 - {x})

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
by(auto simp add: semi_forgetful_RO_def prf.random_oracle_def intro: rel_spmf_bind_reflI)
[PROOF STATE]
proof (state)
this:
rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)

goal (1 subgoal):
 1. \<And>a. \<sigma>1 (h seed x) = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<sigma>1 (h seed x) = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
case \<sigma>1: (Some "by")
[PROOF STATE]
proof (state)
this:
\<sigma>1 (h seed x) = Some by

goal (1 subgoal):
 1. \<And>a. \<sigma>1 (h seed x) = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
proof(cases "s2 x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
 2. \<And>a. s2 x = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
case s2: (Some z)
[PROOF STATE]
proof (state)
this:
s2 x = Some z

goal (2 subgoals):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
 2. \<And>a. s2 x = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
with eq \<sigma>1
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>dom s2. \<sigma>1 (h seed x) = map_option (Pair x) (s2 x)
\<sigma>1 (h seed x) = Some by
s2 x = Some z
[PROOF STEP]
have "by = (x, z)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>dom s2. \<sigma>1 (h seed x) = map_option (Pair x) (s2 x)
\<sigma>1 (h seed x) = Some by
s2 x = Some z

goal (1 subgoal):
 1. by = (x, z)
[PROOF STEP]
by(auto simp add: domIff)
[PROOF STATE]
proof (state)
this:
by = (x, z)

goal (2 subgoals):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
 2. \<And>a. s2 x = Some a \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
by = (x, z)

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
using \<sigma>1 inj not_b s2 X
[PROOF STATE]
proof (prove)
using this:
by = (x, z)
\<sigma>1 (h seed x) = Some by
inj_on (h seed) (dom s2)
\<not> b
s2 x = Some z
invar seed \<sigma>1b s2

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
by(simp add: semi_forgetful_RO_def prf.random_oracle_def split_beta)
[PROOF STATE]
proof (state)
this:
rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)

goal (1 subgoal):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
case s2: None
[PROOF STATE]
proof (state)
this:
s2 x = None

goal (1 subgoal):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
from \<sigma>1 dom
[PROOF STATE]
proof (chain)
picking this:
\<sigma>1 (h seed x) = Some by
dom \<sigma>1 = h seed ` dom s2
[PROOF STEP]
obtain y where y: "y \<in> dom s2" and *: "h seed x = h seed y"
[PROOF STATE]
proof (prove)
using this:
\<sigma>1 (h seed x) = Some by
dom \<sigma>1 = h seed ` dom s2

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> dom s2; h seed x = h seed y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(metis domIff imageE option.distinct(1))
[PROOF STATE]
proof (state)
this:
y \<in> dom s2
h seed x = h seed y

goal (1 subgoal):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y \<in> dom s2
[PROOF STEP]
obtain z where z: "s2 y = Some z"
[PROOF STATE]
proof (prove)
using this:
y \<in> dom s2

goal (1 subgoal):
 1. (\<And>z. s2 y = Some z \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s2 y = Some z

goal (1 subgoal):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
from eq z \<sigma>1
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>dom s2. \<sigma>1 (h seed x) = map_option (Pair x) (s2 x)
s2 y = Some z
\<sigma>1 (h seed x) = Some by
[PROOF STEP]
have "by": "by = (y, z)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>dom s2. \<sigma>1 (h seed x) = map_option (Pair x) (s2 x)
s2 y = Some z
\<sigma>1 (h seed x) = Some by

goal (1 subgoal):
 1. by = (y, z)
[PROOF STEP]
by(auto simp add: * domIff)
[PROOF STATE]
proof (state)
this:
by = (y, z)

goal (1 subgoal):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
from y s2
[PROOF STATE]
proof (chain)
picking this:
y \<in> dom s2
s2 x = None
[PROOF STEP]
have xny: "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
y \<in> dom s2
s2 x = None

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

goal (1 subgoal):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
with y *
[PROOF STATE]
proof (chain)
picking this:
y \<in> dom s2
h seed x = h seed y
x \<noteq> y
[PROOF STEP]
have "h seed x \<in> h seed ` (dom s2 - {x})"
[PROOF STATE]
proof (prove)
using this:
y \<in> dom s2
h seed x = h seed y
x \<noteq> y

goal (1 subgoal):
 1. h seed x \<in> h seed ` (dom s2 - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h seed x \<in> h seed ` (dom s2 - {x})

goal (1 subgoal):
 1. s2 x = None \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h seed x \<in> h seed ` (dom s2 - {x})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h seed x \<in> h seed ` (dom s2 - {x})

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
using \<sigma>1 s2 not_b "by" xny inj
[PROOF STATE]
proof (prove)
using this:
h seed x \<in> h seed ` (dom s2 - {x})
\<sigma>1 (h seed x) = Some by
s2 x = None
\<not> b
by = (y, z)
x \<noteq> y
inj_on (h seed) (dom s2)

goal (1 subgoal):
 1. rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)
[PROOF STEP]
by(simp add: semi_forgetful_RO_def prf.random_oracle_def split_beta)(rule rel_spmf_bindI2; simp)
[PROOF STATE]
proof (state)
this:
rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed \<sigma>1b x) (prf.random_oracle s2 x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar seed ?\<sigma>1b2 ?s2.2 \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed ?\<sigma>1b2 ?x2) (prf.random_oracle ?s2.2 ?x2)

goal (1 subgoal):
 1. rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h seed) (dom s2) \<and> (inj_on (h seed) (dom s2) \<longrightarrow> x = y \<and> invar seed s1 s2)) (exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False)) (exec_gpv prf.random_oracle \ Map.empty)
[PROOF STEP]
from invar_initial _ step
[PROOF STATE]
proof (chain)
picking this:
invar seed (Map.empty, False) Map.empty
PROP ?psi \<Longrightarrow> PROP ?psi
invar seed ?\<sigma>1b2 ?s2.2 \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed ?\<sigma>1b2 ?x2) (prf.random_oracle ?s2.2 ?x2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar seed (Map.empty, False) Map.empty
PROP ?psi \<Longrightarrow> PROP ?psi
invar seed ?\<sigma>1b2 ?s2.2 \<Longrightarrow> rel_spmf (\<lambda>(a, s1) (b, s2). snd s1 = (\<not> inj_on (h seed) (dom s2)) \<and> (\<not> \<not> inj_on (h seed) (dom s2) \<longrightarrow> a = b \<and> invar seed s1 s2)) (semi_forgetful_RO seed ?\<sigma>1b2 ?x2) (prf.random_oracle ?s2.2 ?x2)

goal (1 subgoal):
 1. rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h seed) (dom s2) \<and> (inj_on (h seed) (dom s2) \<longrightarrow> x = y \<and> invar seed s1 s2)) (exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False)) (exec_gpv prf.random_oracle \ Map.empty)
[PROOF STEP]
by(rule exec_gpv_oracle_bisim_bad_full[where ?bad1.0 = "snd" and ?bad2.0 = "\<lambda>\<sigma>. \<not> inj_on (h seed) (dom \<sigma>)"])
        (simp_all add: assms)
[PROOF STATE]
proof (state)
this:
rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h seed) (dom s2) \<and> (inj_on (h seed) (dom s2) \<longrightarrow> x = y \<and> invar seed s1 s2)) (exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False)) (exec_gpv prf.random_oracle \ Map.empty)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?seed1 \<in> set_spmf seed_gen \<Longrightarrow> rel_spmf (\<lambda>(x, s1) (y, s2). snd s1 \<noteq> inj_on (h ?seed1) (dom s2) \<and> (inj_on (h ?seed1) (dom s2) \<longrightarrow> x = y \<and> invar ?seed1 s1 s2)) (exec_gpv (semi_forgetful_RO ?seed1) \ (Map.empty, False)) (exec_gpv prf.random_oracle \ Map.empty)

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
define game_A where "game_A = do {
      seed :: 'seed \<leftarrow> seed_gen;
      (b, \<sigma>) \<leftarrow> exec_gpv prf.random_oracle \ Map.empty;
      return_spmf (b, \<not> inj_on (h seed) (dom \<sigma>))
    }"
[PROOF STATE]
proof (state)
this:
game_A = seed_gen \<bind> (\<lambda>seed. exec_gpv prf.random_oracle \ Map.empty \<bind> (\<lambda>(b, \<sigma>). return_spmf (b, \<not> inj_on (h seed) (dom \<sigma>))))

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
let ?bad1 = "\<lambda>x. snd (snd x)" and ?bad2 = "snd"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have hop3: "rel_spmf (\<lambda>x xa. (?bad1 x \<longleftrightarrow> ?bad2 xa) \<and> (\<not> ?bad2 xa \<longrightarrow> fst x \<longleftrightarrow> fst xa)) game_semi_forgetful game_A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_spmf (\<lambda>x xa. snd (snd x) = snd xa \<and> (\<not> snd xa \<longrightarrow> fst x = fst xa)) game_semi_forgetful game_A
[PROOF STEP]
unfolding game_semi_forgetful_def game_A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_spmf (\<lambda>x xa. snd (snd x) = snd xa \<and> (\<not> snd xa \<longrightarrow> fst x = fst xa)) (seed_gen \<bind> (\<lambda>seed. exec_gpv (semi_forgetful_RO seed) \ (Map.empty, False) \<bind> (\<lambda>(b, rep). return_spmf (b, rep)))) (seed_gen \<bind> (\<lambda>seed. exec_gpv prf.random_oracle \ Map.empty \<bind> (\<lambda>(b, \<sigma>). return_spmf (b, \<not> inj_on (h seed) (dom \<sigma>)))))
[PROOF STEP]
by(clarsimp simp add: restrict_bind_spmf split_def map_spmf_bind_spmf restrict_return_spmf o_def intro!: rel_spmf_bind_reflI simp del: bind_return_spmf)
      (rule rel_spmf_bindI[OF rel_spmf_oracle_adv]; auto)
[PROOF STATE]
proof (state)
this:
rel_spmf (\<lambda>x xa. snd (snd x) = snd xa \<and> (\<not> snd xa \<longrightarrow> fst x = fst xa)) game_semi_forgetful game_A

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have bad1_bad2: "spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True = spmf (map_spmf snd game_A) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True = spmf (map_spmf snd game_A) True
[PROOF STEP]
using fundamental_lemma_bad[OF hop3]
[PROOF STATE]
proof (prove)
using this:
Sigma_Algebra.measure (measure_spmf game_semi_forgetful) {x. snd (snd x)} = Sigma_Algebra.measure (measure_spmf game_A) {y. snd y}

goal (1 subgoal):
 1. spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True = spmf (map_spmf snd game_A) True
[PROOF STEP]
by(simp add: measure_map_spmf spmf_conv_measure_spmf vimage_def)
[PROOF STATE]
proof (state)
this:
spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True = spmf (map_spmf snd game_A) True

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have bound_bad1_event: "\<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True
[PROOF STEP]
using fundamental_lemma[OF hop3]
[PROOF STATE]
proof (prove)
using this:
\<bar>Sigma_Algebra.measure (measure_spmf game_semi_forgetful) {x. fst x} - Sigma_Algebra.measure (measure_spmf game_A) {y. fst y}\<bar> \<le> Sigma_Algebra.measure (measure_spmf game_semi_forgetful) {x. snd (snd x)}

goal (1 subgoal):
 1. \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True
[PROOF STEP]
by(simp add: measure_map_spmf spmf_conv_measure_spmf vimage_def)
[PROOF STATE]
proof (state)
this:
\<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True
[PROOF STEP]
have bound_bad2_event : "\<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf snd game_A) True"
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True

goal (1 subgoal):
 1. \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf snd game_A) True
[PROOF STEP]
using bad1_bad2
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True
spmf (map_spmf (snd \<circ> snd) game_semi_forgetful) True = spmf (map_spmf snd game_A) True

goal (1 subgoal):
 1. \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf snd game_A) True
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
\<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf snd game_A) True

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
define game_B where "game_B = do {
      (b, \<sigma>) \<leftarrow> exec_gpv prf.random_oracle \ Map.empty;
      hash.game_hash_set (dom \<sigma>)
    }"
[PROOF STATE]
proof (state)
this:
game_B = exec_gpv prf.random_oracle \ Map.empty \<bind> (\<lambda>(b, \<sigma>). local.hash.game_hash_set (dom \<sigma>))

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have game_A_game_B: "map_spmf snd game_A = game_B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf snd game_A = game_B
[PROOF STEP]
unfolding game_B_def game_A_def hash.game_hash_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf snd (seed_gen \<bind> (\<lambda>seed. exec_gpv prf.random_oracle \ Map.empty \<bind> (\<lambda>(b, \<sigma>). return_spmf (b, \<not> inj_on (h seed) (dom \<sigma>))))) = exec_gpv prf.random_oracle \ Map.empty \<bind> (\<lambda>(b, \<sigma>). seed_gen \<bind> (\<lambda>seed. return_spmf (\<not> inj_on (h seed) (dom \<sigma>))))
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf snd (seed_gen \<bind> (\<lambda>seed. exec_gpv prf.random_oracle \ Map.empty \<bind> (\<lambda>(b, \<sigma>). return_spmf (b, \<not> inj_on (h seed) (dom \<sigma>))))) = exec_gpv prf.random_oracle \ Map.empty \<bind> (\<lambda>(b, \<sigma>). seed_gen \<bind> (\<lambda>seed. return_spmf (\<not> inj_on (h seed) (dom \<sigma>))))
[PROOF STEP]
by(simp add: map_spmf_bind_spmf o_def split_def)
[PROOF STATE]
proof (state)
this:
map_spmf snd game_A = game_B

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have game_B_bound : "spmf game_B True \<le> hash.\<epsilon>_uh * q * q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf game_B True \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
unfolding game_B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (exec_gpv prf.random_oracle \ Map.empty \<bind> (\<lambda>(b, \<sigma>). local.hash.game_hash_set (dom \<sigma>))) True \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
proof(rule spmf_bind_leI, clarify)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty) \<Longrightarrow> spmf (local.hash.game_hash_set (dom b)) True \<le> local.hash.\<epsilon>_uh * real q * real q
 2. 0 \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
fix b \<sigma>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty) \<Longrightarrow> spmf (local.hash.game_hash_set (dom b)) True \<le> local.hash.\<epsilon>_uh * real q * real q
 2. 0 \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
assume *: "(b, \<sigma>) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty)"
[PROOF STATE]
proof (state)
this:
(b, \<sigma>) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty)

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty) \<Longrightarrow> spmf (local.hash.game_hash_set (dom b)) True \<le> local.hash.\<epsilon>_uh * real q * real q
 2. 0 \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have "finite (dom \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom \<sigma>)
[PROOF STEP]
by(rule prf.finite.exec_gpv_invariant[OF *]) simp_all
[PROOF STATE]
proof (state)
this:
finite (dom \<sigma>)

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty) \<Longrightarrow> spmf (local.hash.game_hash_set (dom b)) True \<le> local.hash.\<epsilon>_uh * real q * real q
 2. 0 \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (dom \<sigma>)
[PROOF STEP]
have "spmf (hash.game_hash_set (dom \<sigma>)) True \<le> hash.\<epsilon>_uh * (card (dom \<sigma>) * card (dom \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
finite (dom \<sigma>)

goal (1 subgoal):
 1. spmf (local.hash.game_hash_set (dom \<sigma>)) True \<le> local.hash.\<epsilon>_uh * real (card (dom \<sigma>) * card (dom \<sigma>))
[PROOF STEP]
using hash.hash_ineq_card[of "dom \<sigma>"]
[PROOF STATE]
proof (prove)
using this:
finite (dom \<sigma>)
finite (dom \<sigma>) \<Longrightarrow> spmf (local.hash.game_hash_set (dom \<sigma>)) True \<le> local.hash.\<epsilon>_uh * real (card (dom \<sigma>)) * real (card (dom \<sigma>))

goal (1 subgoal):
 1. spmf (local.hash.game_hash_set (dom \<sigma>)) True \<le> local.hash.\<epsilon>_uh * real (card (dom \<sigma>) * card (dom \<sigma>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spmf (local.hash.game_hash_set (dom \<sigma>)) True \<le> local.hash.\<epsilon>_uh * real (card (dom \<sigma>) * card (dom \<sigma>))

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty) \<Longrightarrow> spmf (local.hash.game_hash_set (dom b)) True \<le> local.hash.\<epsilon>_uh * real q * real q
 2. 0 \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
spmf (local.hash.game_hash_set (dom \<sigma>)) True \<le> local.hash.\<epsilon>_uh * real (card (dom \<sigma>) * card (dom \<sigma>))

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty) \<Longrightarrow> spmf (local.hash.game_hash_set (dom b)) True \<le> local.hash.\<epsilon>_uh * real q * real q
 2. 0 \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have p1: "card (dom \<sigma>) \<le> q + card (dom (Map.empty :: '\<beta> \<Rightarrow> '\<gamma> option))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (dom \<sigma>) \<le> q + card (dom Map.empty)
[PROOF STEP]
by(rule prf.card_dom_random_oracle[OF bounded *]) simp
[PROOF STATE]
proof (state)
this:
card (dom \<sigma>) \<le> q + card (dom Map.empty)

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty) \<Longrightarrow> spmf (local.hash.game_hash_set (dom b)) True \<le> local.hash.\<epsilon>_uh * real q * real q
 2. 0 \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (dom \<sigma>) \<le> q + card (dom Map.empty)
[PROOF STEP]
have "card (dom \<sigma>) * card (dom \<sigma>) \<le> q * q"
[PROOF STATE]
proof (prove)
using this:
card (dom \<sigma>) \<le> q + card (dom Map.empty)

goal (1 subgoal):
 1. card (dom \<sigma>) * card (dom \<sigma>) \<le> q * q
[PROOF STEP]
using mult_le_mono
[PROOF STATE]
proof (prove)
using this:
card (dom \<sigma>) \<le> q + card (dom Map.empty)
\<lbrakk>?i \<le> ?j; ?k \<le> ?l\<rbrakk> \<Longrightarrow> ?i * ?k \<le> ?j * ?l

goal (1 subgoal):
 1. card (dom \<sigma>) * card (dom \<sigma>) \<le> q * q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (dom \<sigma>) * card (dom \<sigma>) \<le> q * q

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set_spmf (exec_gpv prf.random_oracle \ Map.empty) \<Longrightarrow> spmf (local.hash.game_hash_set (dom b)) True \<le> local.hash.\<epsilon>_uh * real q * real q
 2. 0 \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> local.hash.\<epsilon>_uh * real x \<le> local.hash.\<epsilon>_uh * real y) \<Longrightarrow> spmf (local.hash.game_hash_set (dom \<sigma>)) True \<le> local.hash.\<epsilon>_uh * real (q * q)
[PROOF STEP]
show "spmf (hash.game_hash_set (dom \<sigma>)) True \<le> hash.\<epsilon>_uh * q * q"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> local.hash.\<epsilon>_uh * real x \<le> local.hash.\<epsilon>_uh * real y) \<Longrightarrow> spmf (local.hash.game_hash_set (dom \<sigma>)) True \<le> local.hash.\<epsilon>_uh * real (q * q)

goal (1 subgoal):
 1. spmf (local.hash.game_hash_set (dom \<sigma>)) True \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
by(simp add: hash.\<epsilon>_uh_nonneg mult_left_mono)
[PROOF STATE]
proof (state)
this:
spmf (local.hash.game_hash_set (dom \<sigma>)) True \<le> local.hash.\<epsilon>_uh * real q * real q

goal (1 subgoal):
 1. 0 \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
qed(simp add: hash.\<epsilon>_uh_nonneg)
[PROOF STATE]
proof (state)
this:
spmf game_B True \<le> local.hash.\<epsilon>_uh * real q * real q

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have hop4: "prf'.game_1 \ = map_spmf fst game_A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prf'.game_1 \ = map_spmf fst game_A
[PROOF STEP]
by(simp add: game_A_def prf'.game_1_def map_spmf_bind_spmf o_def split_def bind_spmf_const lossless_seed_gen lossless_weight_spmfD)
[PROOF STATE]
proof (state)
this:
prf'.game_1 \ = map_spmf fst game_A

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have "prf'.advantage \ \<le> \<bar>spmf (prf.game_0 ?\) True - spmf (prf'.game_1 \) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prf'.advantage \ \<le> \<bar>spmf (local.prf.game_0 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar>
[PROOF STEP]
using hop1
[PROOF STATE]
proof (prove)
using this:
prf'.game_0 \ = local.prf.game_0 (prf'_reduction \)

goal (1 subgoal):
 1. prf'.advantage \ \<le> \<bar>spmf (local.prf.game_0 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar>
[PROOF STEP]
by(simp add: prf'.advantage_def)
[PROOF STATE]
proof (state)
this:
prf'.advantage \ \<le> \<bar>spmf (local.prf.game_0 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar>

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prf'.advantage \ \<le> \<bar>spmf (local.prf.game_0 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar>

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have "\<dots> \<le> prf.advantage ?\ + \<bar>spmf (prf.game_1 ?\) True - spmf (prf'.game_1 \) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (local.prf.game_0 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar> \<le> local.prf.advantage (prf'_reduction \) + \<bar>spmf (local.prf.game_1 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar>
[PROOF STEP]
by(simp add: prf.advantage_def)
[PROOF STATE]
proof (state)
this:
\<bar>spmf (local.prf.game_0 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar> \<le> local.prf.advantage (prf'_reduction \) + \<bar>spmf (local.prf.game_1 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar>

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>spmf (local.prf.game_0 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar> \<le> local.prf.advantage (prf'_reduction \) + \<bar>spmf (local.prf.game_1 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar>

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have "\<bar>spmf (prf.game_1 ?\) True - spmf (prf'.game_1 \) True\<bar> \<le>
    \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 \) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (local.prf.game_1 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar> \<le> \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 \) True\<bar>
[PROOF STEP]
using hop2
[PROOF STATE]
proof (prove)
using this:
local.prf.game_1 (prf'_reduction \) = map_spmf fst game_semi_forgetful

goal (1 subgoal):
 1. \<bar>spmf (local.prf.game_1 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar> \<le> \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 \) True\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>spmf (local.prf.game_1 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar> \<le> \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 \) True\<bar>

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>spmf (local.prf.game_1 (prf'_reduction \)) True - spmf (prf'.game_1 \) True\<bar> \<le> \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 \) True\<bar>

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
have "\<dots> \<le> hash.\<epsilon>_uh * q * q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 \) True\<bar> \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
using game_A_game_B game_B_bound bound_bad2_event hop4
[PROOF STATE]
proof (prove)
using this:
map_spmf snd game_A = game_B
spmf game_B True \<le> local.hash.\<epsilon>_uh * real q * real q
\<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True\<bar> \<le> spmf (map_spmf snd game_A) True
prf'.game_1 \ = map_spmf fst game_A

goal (1 subgoal):
 1. \<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 \) True\<bar> \<le> local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<bar>spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 \) True\<bar> \<le> local.hash.\<epsilon>_uh * real q * real q

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> local.prf.advantage (prf'_reduction \) + x \<le> local.prf.advantage (prf'_reduction \) + y; \<And>x y. x \<le> y \<Longrightarrow> local.prf.advantage (prf'_reduction \) + x \<le> local.prf.advantage (prf'_reduction \) + y\<rbrakk> \<Longrightarrow> prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> local.prf.advantage (prf'_reduction \) + x \<le> local.prf.advantage (prf'_reduction \) + y; \<And>x y. x \<le> y \<Longrightarrow> local.prf.advantage (prf'_reduction \) + x \<le> local.prf.advantage (prf'_reduction \) + y\<rbrakk> \<Longrightarrow> prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q

goal (1 subgoal):
 1. prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q
[PROOF STEP]
by(simp add: add_left_mono)
[PROOF STATE]
proof (state)
this:
prf'.advantage \ \<le> local.prf.advantage (prf'_reduction \) + local.hash.\<epsilon>_uh * real q * real q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cap_object_simps:
  "cap_object (TcbCap x) = x"
  "cap_object (CNodeCap x) = x"
  "cap_object (EndpointCap x j) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cap_object (TcbCap x) = x &&& cap_object (CNodeCap x) = x &&& cap_object (EndpointCap x j) = x
[PROOF STEP]
by (simp_all add:cap_object_def cap_objects_def cap_has_object_def)


[STATEMENT]
lemma less_llength_ltake: "i < llength (ltake k Xs) \<longleftrightarrow> i < k \<and> i < llength Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < llength (ltake k Xs)) = (i < k \<and> i < llength Xs)
[PROOF STEP]
by simp


[STATEMENT]
lemma lnth_subset_Sup_llist: "enat i < llength Xs \<Longrightarrow> lnth Xs i \<subseteq> Sup_llist Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat i < llength Xs \<Longrightarrow> lnth Xs i \<subseteq> Sup_llist Xs
[PROOF STEP]
unfolding Sup_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat i < llength Xs \<Longrightarrow> lnth Xs i \<subseteq> \<Union> (lnth Xs ` {i. enat i < llength Xs})
[PROOF STEP]
by auto


[STATEMENT]
lemma Sup_llist_imp_exists_index: "x \<in> Sup_llist Xs \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Sup_llist Xs \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i
[PROOF STEP]
unfolding Sup_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<Union> (lnth Xs ` {i. enat i < llength Xs}) \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i
[PROOF STEP]
by auto


[STATEMENT]
lemma exists_index_imp_Sup_llist: "enat i < llength Xs \<Longrightarrow> x \<in> lnth Xs i \<Longrightarrow> x \<in> Sup_llist Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enat i < llength Xs; x \<in> lnth Xs i\<rbrakk> \<Longrightarrow> x \<in> Sup_llist Xs
[PROOF STEP]
unfolding Sup_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enat i < llength Xs; x \<in> lnth Xs i\<rbrakk> \<Longrightarrow> x \<in> \<Union> (lnth Xs ` {i. enat i < llength Xs})
[PROOF STEP]
by auto


[STATEMENT]
lemma Sup_llist_LNil[simp]: "Sup_llist LNil = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_llist LNil = {}
[PROOF STEP]
unfolding Sup_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (lnth LNil ` {i. enat i < llength LNil}) = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma Sup_llist_LCons[simp]: "Sup_llist (LCons X Xs) = X \<union> Sup_llist Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_llist (LCons X Xs) = X \<union> Sup_llist Xs
[PROOF STEP]
unfolding Sup_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)}) = X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs})
[PROOF STEP]
proof (intro subset_antisym subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)}) \<Longrightarrow> x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs})
 2. \<And>x. x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs}) \<Longrightarrow> x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)}) \<Longrightarrow> x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs})
 2. \<And>x. x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs}) \<Longrightarrow> x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})
[PROOF STEP]
assume "x \<in> (\<Union>i \<in> {i. enat i < llength (LCons X Xs)}. lnth (LCons X Xs) i)"
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})

goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)}) \<Longrightarrow> x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs})
 2. \<And>x. x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs}) \<Longrightarrow> x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})
[PROOF STEP]
obtain i where len: "enat i < llength (LCons X Xs)" and nth: "x \<in> lnth (LCons X Xs) i"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>enat i < llength (LCons X Xs); x \<in> lnth (LCons X Xs) i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
enat i < llength (LCons X Xs)
x \<in> lnth (LCons X Xs) i

goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)}) \<Longrightarrow> x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs})
 2. \<And>x. x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs}) \<Longrightarrow> x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})
[PROOF STEP]
from nth
[PROOF STATE]
proof (chain)
picking this:
x \<in> lnth (LCons X Xs) i
[PROOF STEP]
have "x \<in> X \<or> i > 0 \<and> x \<in> lnth Xs (i - 1)"
[PROOF STATE]
proof (prove)
using this:
x \<in> lnth (LCons X Xs) i

goal (1 subgoal):
 1. x \<in> X \<or> 0 < i \<and> x \<in> lnth Xs (i - 1)
[PROOF STEP]
by (metis lnth_LCons' neq0_conv)
[PROOF STATE]
proof (state)
this:
x \<in> X \<or> 0 < i \<and> x \<in> lnth Xs (i - 1)

goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)}) \<Longrightarrow> x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs})
 2. \<And>x. x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs}) \<Longrightarrow> x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X \<or> 0 < i \<and> x \<in> lnth Xs (i - 1)
[PROOF STEP]
have "x \<in> X \<or> (\<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i)"
[PROOF STATE]
proof (prove)
using this:
x \<in> X \<or> 0 < i \<and> x \<in> lnth Xs (i - 1)

goal (1 subgoal):
 1. x \<in> X \<or> (\<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i)
[PROOF STEP]
by (metis len Suc_pred' eSuc_enat iless_Suc_eq less_irrefl llength_LCons not_less order_trans)
[PROOF STATE]
proof (state)
this:
x \<in> X \<or> (\<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i)

goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)}) \<Longrightarrow> x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs})
 2. \<And>x. x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs}) \<Longrightarrow> x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X \<or> (\<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i)
[PROOF STEP]
show "x \<in> X \<union> (\<Union>i \<in> {i. enat i < llength Xs}. lnth Xs i)"
[PROOF STATE]
proof (prove)
using this:
x \<in> X \<or> (\<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i)

goal (1 subgoal):
 1. x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs})

goal (1 subgoal):
 1. \<And>x. x \<in> X \<union> \<Union> (lnth Xs ` {i. enat i < llength Xs}) \<Longrightarrow> x \<in> \<Union> (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})
[PROOF STEP]
qed ((auto)[], metis i0_lb lnth_0 zero_enat_def, metis Suc_ile_eq lnth_Suc_LCons)


[STATEMENT]
lemma lhd_subset_Sup_llist: "\<not> lnull Xs \<Longrightarrow> lhd Xs \<subseteq> Sup_llist Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> lhd Xs \<subseteq> Sup_llist Xs
[PROOF STEP]
by (cases Xs) simp_all


[STATEMENT]
lemma Sup_upto_llist_eq_Sup_llist_ltake: "Sup_upto_llist Xs j = Sup_llist (ltake (eSuc j) Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_upto_llist Xs j = Sup_llist (ltake (eSuc j) Xs)
[PROOF STEP]
unfolding Sup_upto_llist_def Sup_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (lnth Xs ` {i. enat i < llength Xs \<and> enat i \<le> j}) = \<Union> (lnth (ltake (eSuc j) Xs) ` {i. enat i < llength (ltake (eSuc j) Xs)})
[PROOF STEP]
by (smt Collect_cong Sup.SUP_cong iless_Suc_eq lnth_ltake less_llength_ltake mem_Collect_eq)


[STATEMENT]
lemma Sup_upto_llist_enat_0[simp]:
  "Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
proof (cases "lnull Xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lnull Xs \<Longrightarrow> Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
 2. \<not> lnull Xs \<Longrightarrow> Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
lnull Xs

goal (2 subgoals):
 1. lnull Xs \<Longrightarrow> Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
 2. \<not> lnull Xs \<Longrightarrow> Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lnull Xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lnull Xs

goal (1 subgoal):
 1. Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
unfolding Sup_upto_llist_def
[PROOF STATE]
proof (prove)
using this:
lnull Xs

goal (1 subgoal):
 1. \<Union> (lnth Xs ` {i. enat i < llength Xs \<and> enat i \<le> enat 0}) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)

goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> lnull Xs

goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
unfolding Sup_upto_llist_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {y. \<exists>x\<in>{i. enat i < llength Xs \<and> enat i \<le> enat 0}. y = lnth Xs x} = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
by (simp add: lhd_conv_lnth enat_0 enat_0_iff)
[PROOF STATE]
proof (state)
this:
Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Sup_upto_llist_Suc[simp]:
  "Sup_upto_llist Xs (enat (Suc j)) =
   Sup_upto_llist Xs (enat j) \<union> (if enat (Suc j) < llength Xs then lnth Xs (Suc j) else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_upto_llist Xs (enat (Suc j)) = Sup_upto_llist Xs (enat j) \<union> (if enat (Suc j) < llength Xs then lnth Xs (Suc j) else {})
[PROOF STEP]
unfolding Sup_upto_llist_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {y. \<exists>x\<in>{i. enat i < llength Xs \<and> enat i \<le> enat (Suc j)}. y = lnth Xs x} = \<Union> {y. \<exists>x\<in>{i. enat i < llength Xs \<and> enat i \<le> enat j}. y = lnth Xs x} \<union> (if enat (Suc j) < llength Xs then lnth Xs (Suc j) else {})
[PROOF STEP]
by (auto intro: le_SucI elim: le_SucE)


[STATEMENT]
lemma Sup_upto_llist_infinity[simp]: "Sup_upto_llist Xs \<infinity> = Sup_llist Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_upto_llist Xs \<infinity> = Sup_llist Xs
[PROOF STEP]
unfolding Sup_upto_llist_def Sup_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (lnth Xs ` {i. enat i < llength Xs \<and> enat i \<le> \<infinity>}) = \<Union> (lnth Xs ` {i. enat i < llength Xs})
[PROOF STEP]
by simp


[STATEMENT]
lemma Sup_upto_llist_0[simp]: "Sup_upto_llist Xs 0 = (if lnull Xs then {} else lhd Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_upto_llist Xs 0 = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
unfolding zero_enat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
by (rule Sup_upto_llist_enat_0)


[STATEMENT]
lemma Sup_upto_llist_eSuc[simp]:
  "Sup_upto_llist Xs (eSuc j) =
   (case j of
      enat k \<Rightarrow> Sup_upto_llist Xs (enat (Suc k))
    | \<infinity> \<Rightarrow> Sup_llist Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_upto_llist Xs (eSuc j) = (case j of enat k \<Rightarrow> Sup_upto_llist Xs (enat (Suc k)) | \<infinity> \<Rightarrow> Sup_llist Xs)
[PROOF STEP]
by (auto simp: eSuc_enat split: enat.split)


[STATEMENT]
lemma Sup_upto_llist_mono[simp]: "j \<le> k \<Longrightarrow> Sup_upto_llist Xs j \<subseteq> Sup_upto_llist Xs k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> k \<Longrightarrow> Sup_upto_llist Xs j \<subseteq> Sup_upto_llist Xs k
[PROOF STEP]
unfolding Sup_upto_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> k \<Longrightarrow> \<Union> (lnth Xs ` {i. enat i < llength Xs \<and> enat i \<le> j}) \<subseteq> \<Union> (lnth Xs ` {i. enat i < llength Xs \<and> enat i \<le> k})
[PROOF STEP]
by auto