[STATEMENT]
lemma rp_rf:
  assumes bound: "interaction_any_bounded_by \<A> q"
    and lossless: "lossless_gpv \<I> \<A>"
    and WT: "\<I> \<turnstile>g \<A> \<surd>"
  shows "advantage \<A> \<le> q * q / card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
including lifting_syntax
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
let ?run = "\<lambda>b. exec_gpv (if b then rp.random_permutation else rf.random_oracle) \<A> Map.empty"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
define rp_bad :: "bool \<times> ('a \<rightharpoonup> 'a) \<Rightarrow> 'a \<Rightarrow> ('a \<times> (bool \<times> ('a \<rightharpoonup> 'a))) spmf"
    where "rp_bad = (\<lambda>(bad, \<sigma>) x. case \<sigma> x of Some y \<Rightarrow> return_spmf (y, (bad, \<sigma>))
      | None \<Rightarrow> bind_spmf (spmf_of_set A) (\<lambda>y. if y \<in> ran \<sigma> then map_spmf (\<lambda>y'. (y', (True, \<sigma>(x \<mapsto> y')))) (spmf_of_set (A - ran \<sigma>)) else return_spmf (y, (bad, (\<sigma>(x \<mapsto> y))))))"
[PROOF STATE]
proof (state)
this:
rp_bad = (\<lambda>(bad, \<sigma>) x. case \<sigma> x of None \<Rightarrow> spmf_of_set A \<bind> (\<lambda>y. if y \<in> ran \<sigma> then map_spmf (\<lambda>y'. (y', True, \<sigma>(x \<mapsto> y'))) (spmf_of_set (A - ran \<sigma>)) else return_spmf (y, bad, \<sigma>(x \<mapsto> y))) | Some y \<Rightarrow> return_spmf (y, bad, \<sigma>))

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have rp_bad_simps: "rp_bad (bad, \<sigma>) x = (case \<sigma> x of Some y \<Rightarrow> return_spmf (y, (bad, \<sigma>))
      | None \<Rightarrow> bind_spmf (spmf_of_set A) (\<lambda>y. if y \<in> ran \<sigma> then map_spmf (\<lambda>y'. (y', (True, \<sigma>(x \<mapsto> y')))) (spmf_of_set (A - ran \<sigma>)) else return_spmf (y, (bad, (\<sigma>(x \<mapsto> y))))))"
    for bad \<sigma> x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rp_bad (bad, \<sigma>) x = (case \<sigma> x of None \<Rightarrow> spmf_of_set A \<bind> (\<lambda>y. if y \<in> ran \<sigma> then map_spmf (\<lambda>y'. (y', True, \<sigma>(x \<mapsto> y'))) (spmf_of_set (A - ran \<sigma>)) else return_spmf (y, bad, \<sigma>(x \<mapsto> y))) | Some y \<Rightarrow> return_spmf (y, bad, \<sigma>))
[PROOF STEP]
by(simp add: rp_bad_def)
[PROOF STATE]
proof (state)
this:
rp_bad (?bad2, ?\<sigma>2) ?x2 = (case ?\<sigma>2 ?x2 of None \<Rightarrow> spmf_of_set A \<bind> (\<lambda>y. if y \<in> ran ?\<sigma>2 then map_spmf (\<lambda>y'. (y', True, ?\<sigma>2(?x2 \<mapsto> y'))) (spmf_of_set (A - ran ?\<sigma>2)) else return_spmf (y, ?bad2, ?\<sigma>2(?x2 \<mapsto> y))) | Some y \<Rightarrow> return_spmf (y, ?bad2, ?\<sigma>2))

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
let ?S = "rel_prod2 (=)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
define init :: "bool \<times> ('a \<rightharpoonup> 'a)" where "init = (False, Map.empty)"
[PROOF STATE]
proof (state)
this:
init = (False, Map.empty)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have rp: "rp.random_permutation = (\<lambda>\<sigma> x. case \<sigma> x of Some y \<Rightarrow> return_spmf (y, \<sigma>)
    | None \<Rightarrow> bind_spmf (bind_spmf (spmf_of_set A) (\<lambda>y. if y \<in> ran \<sigma> then spmf_of_set (A - ran \<sigma>) else return_spmf y)) (\<lambda>y. return_spmf (y, \<sigma>(x \<mapsto> y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rp.random_permutation = (\<lambda>\<sigma> x. case \<sigma> x of None \<Rightarrow> spmf_of_set A \<bind> (\<lambda>y. if y \<in> ran \<sigma> then spmf_of_set (A - ran \<sigma>) else return_spmf y) \<bind> (\<lambda>y. return_spmf (y, \<sigma>(x \<mapsto> y))) | Some y \<Rightarrow> return_spmf (y, \<sigma>))
[PROOF STEP]
by(subst rp_resample)(auto simp add: finite_A rp.random_permutation_def[abs_def])
[PROOF STATE]
proof (state)
this:
rp.random_permutation = (\<lambda>\<sigma> x. case \<sigma> x of None \<Rightarrow> spmf_of_set A \<bind> (\<lambda>y. if y \<in> ran \<sigma> then spmf_of_set (A - ran \<sigma>) else return_spmf y) \<bind> (\<lambda>y. return_spmf (y, \<sigma>(x \<mapsto> y))) | Some y \<Rightarrow> return_spmf (y, \<sigma>))

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [transfer_rule]: "(?S ===> (=) ===> rel_spmf (rel_prod (=) ?S)) rp.random_permutation rp_bad"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_prod2 (=) ===> (=) ===> rel_spmf (rel_prod (=) (rel_prod2 (=)))) rp.random_permutation rp_bad
[PROOF STEP]
unfolding rp rp_bad_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_prod2 (=) ===> (=) ===> rel_spmf (rel_prod (=) (rel_prod2 (=)))) (\<lambda>\<sigma> x. case \<sigma> x of None \<Rightarrow> spmf_of_set A \<bind> (\<lambda>y. if y \<in> ran \<sigma> then spmf_of_set (A - ran \<sigma>) else return_spmf y) \<bind> (\<lambda>y. return_spmf (y, \<sigma>(x \<mapsto> y))) | Some y \<Rightarrow> return_spmf (y, \<sigma>)) (\<lambda>(bad, \<sigma>) x. case \<sigma> x of None \<Rightarrow> spmf_of_set A \<bind> (\<lambda>y. if y \<in> ran \<sigma> then map_spmf (\<lambda>y'. (y', True, \<sigma>(x \<mapsto> y'))) (spmf_of_set (A - ran \<sigma>)) else return_spmf (y, bad, \<sigma>(x \<mapsto> y))) | Some y \<Rightarrow> return_spmf (y, bad, \<sigma>))
[PROOF STEP]
by(auto simp add: rel_fun_def map_spmf_conv_bind_spmf split: option.split intro!: rel_spmf_bind_reflI)
[PROOF STATE]
proof (state)
this:
(rel_prod2 (=) ===> (=) ===> rel_spmf (rel_prod (=) (rel_prod2 (=)))) rp.random_permutation rp_bad

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [transfer_rule]: "?S Map.empty init"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_prod2 (=) Map.empty init
[PROOF STEP]
by(simp add: init_def)
[PROOF STATE]
proof (state)
this:
rel_prod2 (=) Map.empty init

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have "spmf (prp_game \<A>) True = spmf (run_gpv rp_bad \<A> init) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (prp_game \<A>) True = spmf (run_gpv rp_bad \<A> init) True
[PROOF STEP]
unfolding vimage_def game_def if_True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (run_gpv rp.random_permutation \<A> Map.empty) True = spmf (run_gpv rp_bad \<A> init) True
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
spmf (prp_game \<A>) True = spmf (run_gpv rp_bad \<A> init) True

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
spmf (prp_game \<A>) True = spmf (run_gpv rp_bad \<A> init) True

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
spmf (prp_game \<A>) True = spmf (run_gpv rp_bad \<A> init) True

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
define collision :: "('a \<rightharpoonup> 'a) \<Rightarrow> bool" where "collision m \<longleftrightarrow> \<not> inj_on m (dom m)" for m
[PROOF STATE]
proof (state)
this:
collision ?m = (\<not> inj_on ?m (dom ?m))

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "\<not> collision Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> collision Map.empty
[PROOF STEP]
by(simp add: collision_def)
[PROOF STATE]
proof (state)
this:
\<not> collision Map.empty

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "\<lbrakk> collision m; m x = None \<rbrakk> \<Longrightarrow> collision (m(x := y))" for m x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>collision m; m x = None\<rbrakk> \<Longrightarrow> collision (m(x := y))
[PROOF STEP]
by(auto simp add: collision_def fun_upd_idem dom_minus fun_upd_image dest: inj_on_fun_updD)
[PROOF STATE]
proof (state)
this:
\<lbrakk>collision ?m4; ?m4 ?x4 = None\<rbrakk> \<Longrightarrow> collision (?m4(?x4 := ?y4))

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have collision_map_updI: "\<lbrakk> m x = None; y \<in> ran m \<rbrakk> \<Longrightarrow> collision (m(x \<mapsto> y))" for m x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = None; y \<in> ran m\<rbrakk> \<Longrightarrow> collision (m(x \<mapsto> y))
[PROOF STEP]
by(auto simp add: collision_def ran_def intro: rev_image_eqI)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?m4 ?x4 = None; ?y4 \<in> ran ?m4\<rbrakk> \<Longrightarrow> collision (?m4(?x4 \<mapsto> ?y4))

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have collision_map_upd_iff: "\<not> collision m \<Longrightarrow> collision (m(x \<mapsto> y)) \<longleftrightarrow> y \<in> ran m \<and> m x \<noteq> Some y" for m x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> collision m \<Longrightarrow> collision (m(x \<mapsto> y)) = (y \<in> ran m \<and> m x \<noteq> Some y)
[PROOF STEP]
by(auto simp add: collision_def ran_def fun_upd_idem intro: inj_on_fun_updI rev_image_eqI dest: inj_on_eq_iff)
[PROOF STATE]
proof (state)
this:
\<not> collision ?m4 \<Longrightarrow> collision (?m4(?x4 \<mapsto> ?y4)) = (?y4 \<in> ran ?m4 \<and> ?m4 ?x4 \<noteq> Some ?y4)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
let ?bad1 = "collision" and ?bad2 = "fst"
      and ?X = "\<lambda>\<sigma>1 (bad, \<sigma>2). \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad"
      and ?I1 = "\<lambda>\<sigma>1. dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A"
      and ?I2 = "\<lambda>(bad, \<sigma>2). dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
let ?X_bad = "\<lambda>\<sigma>1 s2. ?I1 \<sigma>1 \<and> ?I2 s2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "\<I> \<turnstile>c rf.random_oracle s1 \<surd>" if "ran s1 \<subseteq> A" for s1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>c rf.random_oracle s1 \<surd>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
ran s1 \<subseteq> A

goal (1 subgoal):
 1. \<I> \<turnstile>c rf.random_oracle s1 \<surd>
[PROOF STEP]
by(intro WT_calleeI)(auto simp add: rf.random_oracle_def[abs_def] finite_A nonempty_A ran_def split: option.split_asm)
[PROOF STATE]
proof (state)
this:
ran ?s1.6 \<subseteq> A \<Longrightarrow> \<I> \<turnstile>c rf.random_oracle ?s1.6 \<surd>

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "callee_invariant_on rf.random_oracle ?I1 \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. callee_invariant_on rf.random_oracle (\<lambda>\<sigma>1. dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<I>
[PROOF STEP]
by(unfold_locales)(auto simp add: rf.random_oracle_def finite_A split: option.split_asm)
[PROOF STATE]
proof (state)
this:
callee_invariant_on rf.random_oracle (\<lambda>\<sigma>1. dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<I>

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
callee_invariant_on rf.random_oracle (\<lambda>\<sigma>1. dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<I>
[PROOF STEP]
interpret rf: callee_invariant_on rf.random_oracle ?I1 \<I>
[PROOF STATE]
proof (prove)
using this:
callee_invariant_on rf.random_oracle (\<lambda>\<sigma>1. dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<I>

goal (1 subgoal):
 1. callee_invariant_on rf.random_oracle (\<lambda>\<sigma>1. dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<I>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "\<I> \<turnstile>c rp_bad s2 \<surd> " if "ran (snd s2) \<subseteq> A" for s2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>c rp_bad s2 \<surd>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
ran (snd s2) \<subseteq> A

goal (1 subgoal):
 1. \<I> \<turnstile>c rp_bad s2 \<surd>
[PROOF STEP]
by(intro WT_calleeI)(auto simp add: rp_bad_def finite_A split: prod.split_asm option.split_asm if_split_asm intro: ranI)
[PROOF STATE]
proof (state)
this:
ran (snd ?s2.6) \<subseteq> A \<Longrightarrow> \<I> \<turnstile>c rp_bad ?s2.6 \<surd>

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "callee_invariant_on rf.random_oracle (\<lambda>\<sigma>1. ?bad1 \<sigma>1 \<and> ?I1 \<sigma>1) \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. callee_invariant_on rf.random_oracle (\<lambda>\<sigma>1. collision \<sigma>1 \<and> dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<I>
[PROOF STEP]
by(unfold_locales)(clarsimp simp add: rf.random_oracle_def finite_A  split: option.split_asm)+
[PROOF STATE]
proof (state)
this:
callee_invariant_on rf.random_oracle (\<lambda>\<sigma>1. collision \<sigma>1 \<and> dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<I>

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "callee_invariant_on rp_bad (\<lambda>s2. ?I2 s2) \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. callee_invariant_on rp_bad (\<lambda>s2. case s2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) \<I>
[PROOF STEP]
by(unfold_locales)(auto 4 3 simp add: rp_bad_simps finite_A split: option.splits if_split_asm iff del: domIff)
[PROOF STATE]
proof (state)
this:
callee_invariant_on rp_bad (\<lambda>s2. case s2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) \<I>

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "callee_invariant_on rp_bad (\<lambda>s2. ?bad2 s2 \<and> ?I2 s2) \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. callee_invariant_on rp_bad (\<lambda>s2. fst s2 \<and> (case s2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A)) \<I>
[PROOF STEP]
by(unfold_locales)(auto 4 3 simp add: rp_bad_simps finite_A split: option.splits if_split_asm iff del: domIff)
[PROOF STATE]
proof (state)
this:
callee_invariant_on rp_bad (\<lambda>s2. fst s2 \<and> (case s2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A)) \<I>

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "\<I> \<turnstile>c rp_bad (bad, \<sigma>2) \<surd>" if "ran \<sigma>2 \<subseteq> A" for bad \<sigma>2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>c rp_bad (bad, \<sigma>2) \<surd>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
ran \<sigma>2 \<subseteq> A

goal (1 subgoal):
 1. \<I> \<turnstile>c rp_bad (bad, \<sigma>2) \<surd>
[PROOF STEP]
by(intro WT_calleeI)(auto simp add: rp_bad_def finite_A nonempty_A ran_def split: option.split_asm if_split_asm)
[PROOF STATE]
proof (state)
this:
ran ?\<sigma>2.6 \<subseteq> A \<Longrightarrow> \<I> \<turnstile>c rp_bad (?bad6, ?\<sigma>2.6) \<surd>

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have [simp]: "lossless_spmf (rp_bad (b, \<sigma>2) x)" if "x \<in> A" "dom \<sigma>2 \<subseteq> A" "ran \<sigma>2 \<subseteq> A" for b \<sigma>2 x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (rp_bad (b, \<sigma>2) x)
[PROOF STEP]
using finite_A that
[PROOF STATE]
proof (prove)
using this:
finite A
x \<in> A
dom \<sigma>2 \<subseteq> A
ran \<sigma>2 \<subseteq> A

goal (1 subgoal):
 1. lossless_spmf (rp_bad (b, \<sigma>2) x)
[PROOF STEP]
unfolding rp_bad_def
[PROOF STATE]
proof (prove)
using this:
finite A
x \<in> A
dom \<sigma>2 \<subseteq> A
ran \<sigma>2 \<subseteq> A

goal (1 subgoal):
 1. lossless_spmf ((case (b, \<sigma>2) of (bad, \<sigma>) \<Rightarrow> \<lambda>x. case \<sigma> x of None \<Rightarrow> spmf_of_set A \<bind> (\<lambda>y. if y \<in> ran \<sigma> then map_spmf (\<lambda>y'. (y', True, \<sigma>(x \<mapsto> y'))) (spmf_of_set (A - ran \<sigma>)) else return_spmf (y, bad, \<sigma>(x \<mapsto> y))) | Some y \<Rightarrow> return_spmf (y, bad, \<sigma>)) x)
[PROOF STEP]
by(clarsimp simp add: nonempty_A dom_subset_ran_iff eq_None_iff_not_dom split: option.split)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x6 \<in> A; dom ?\<sigma>2.6 \<subseteq> A; ran ?\<sigma>2.6 \<subseteq> A\<rbrakk> \<Longrightarrow> lossless_spmf (rp_bad (?b6, ?\<sigma>2.6) ?x6)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have "rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). (?bad1 \<sigma>1 \<longleftrightarrow> ?bad2 state2) \<and> (if ?bad2 state2 then ?X_bad \<sigma>1 state2 else b1 = b2 \<and> ?X \<sigma>1 state2))
            ((if False then rp.random_permutation else rf.random_oracle) s1 x) (rp_bad s2 x)"
      if "?X s1 s2" "x \<in> outs_\<I> \<I>" "?I1 s1" "?I2 s2" for s1 s2 x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) ((if False then rp.random_permutation else rf.random_oracle) s1 x) (rp_bad s2 x)
[PROOF STEP]
using that finite_A
[PROOF STATE]
proof (prove)
using this:
case s2 of (bad, \<sigma>2) \<Rightarrow> s1 = \<sigma>2 \<and> \<not> collision s1 \<and> \<not> bad
x \<in> outs_\<I> \<I>
dom s1 \<subseteq> A \<and> ran s1 \<subseteq> A
case s2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A
finite A

goal (1 subgoal):
 1. rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) ((if False then rp.random_permutation else rf.random_oracle) s1 x) (rp_bad s2 x)
[PROOF STEP]
by(auto split!: option.split simp add: rf.random_oracle_def rp_bad_def rel_spmf_return_spmf1 collision_map_updI dom_subset_ran_iff eq_None_iff_not_dom collision_map_upd_iff intro!: rel_spmf_bind_reflI)
[PROOF STATE]
proof (state)
this:
\<lbrakk>case ?s2.6 of (bad, \<sigma>2) \<Rightarrow> ?s1.6 = \<sigma>2 \<and> \<not> collision ?s1.6 \<and> \<not> bad; ?x6 \<in> outs_\<I> \<I>; dom ?s1.6 \<subseteq> A \<and> ran ?s1.6 \<subseteq> A; case ?s2.6 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A\<rbrakk> \<Longrightarrow> rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) ((if False then rp.random_permutation else rf.random_oracle) ?s1.6 ?x6) (rp_bad ?s2.6 ?x6)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
with _ _
[PROOF STATE]
proof (chain)
picking this:
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
\<lbrakk>case ?s2.6 of (bad, \<sigma>2) \<Rightarrow> ?s1.6 = \<sigma>2 \<and> \<not> collision ?s1.6 \<and> \<not> bad; ?x6 \<in> outs_\<I> \<I>; dom ?s1.6 \<subseteq> A \<and> ran ?s1.6 \<subseteq> A; case ?s2.6 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A\<rbrakk> \<Longrightarrow> rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) ((if False then rp.random_permutation else rf.random_oracle) ?s1.6 ?x6) (rp_bad ?s2.6 ?x6)
[PROOF STEP]
have "rel_spmf
       (\<lambda>(b1, \<sigma>1) (b2, state2). (?bad1 \<sigma>1 \<longleftrightarrow> ?bad2 state2) \<and> (if ?bad2 state2 then ?X_bad \<sigma>1 state2 else b1 = b2 \<and> ?X \<sigma>1 state2))
       (?run False) (exec_gpv rp_bad \<A> init)"
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
\<lbrakk>case ?s2.6 of (bad, \<sigma>2) \<Rightarrow> ?s1.6 = \<sigma>2 \<and> \<not> collision ?s1.6 \<and> \<not> bad; ?x6 \<in> outs_\<I> \<I>; dom ?s1.6 \<subseteq> A \<and> ran ?s1.6 \<subseteq> A; case ?s2.6 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A\<rbrakk> \<Longrightarrow> rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) ((if False then rp.random_permutation else rf.random_oracle) ?s1.6 ?x6) (rp_bad ?s2.6 ?x6)

goal (1 subgoal):
 1. rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) (exec_gpv rp_bad \<A> init)
[PROOF STEP]
by(rule exec_gpv_oracle_bisim_bad_invariant[where \<I> = \<I> and ?I1.0 = "?I1" and ?I2.0="?I2"])(auto simp add: init_def WT lossless finite_A nonempty_A)
[PROOF STATE]
proof (state)
this:
rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) (exec_gpv rp_bad \<A> init)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) (exec_gpv rp_bad \<A> init)
[PROOF STEP]
have "\<bar>spmf (map_spmf fst (?run False)) True - spmf (run_gpv rp_bad \<A> init) True\<bar> \<le> spmf (map_spmf (?bad1 \<circ> snd) (?run False)) True"
[PROOF STATE]
proof (prove)
using this:
rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) (exec_gpv rp_bad \<A> init)

goal (1 subgoal):
 1. \<bar>spmf (run_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) True - spmf (run_gpv rp_bad \<A> init) True\<bar> \<le> spmf (map_spmf (collision \<circ> snd) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) True
[PROOF STEP]
unfolding spmf_conv_measure_spmf measure_map_spmf vimage_def
[PROOF STATE]
proof (prove)
using this:
rel_spmf (\<lambda>(b1, \<sigma>1) (b2, state2). collision \<sigma>1 = fst state2 \<and> (if fst state2 then (dom \<sigma>1 \<subseteq> A \<and> ran \<sigma>1 \<subseteq> A) \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> dom \<sigma>2 \<subseteq> A \<and> ran \<sigma>2 \<subseteq> A) else b1 = b2 \<and> (case state2 of (bad, \<sigma>2) \<Rightarrow> \<sigma>1 = \<sigma>2 \<and> \<not> collision \<sigma>1 \<and> \<not> bad))) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) (exec_gpv rp_bad \<A> init)

goal (1 subgoal):
 1. \<bar>Sigma_Algebra.measure (measure_spmf (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) {x. fst x \<in> {True}} - Sigma_Algebra.measure (measure_spmf (exec_gpv rp_bad \<A> init)) {x. fst x \<in> {True}}\<bar> \<le> Sigma_Algebra.measure (measure_spmf (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) {x. (collision \<circ> snd) x \<in> {True}}
[PROOF STEP]
by(intro fundamental_lemma[where ?bad2.0="\<lambda>(_, s2). ?bad2 s2"])(auto simp add: split_def elim: rel_spmf_mono)
[PROOF STATE]
proof (state)
this:
\<bar>spmf (run_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) True - spmf (run_gpv rp_bad \<A> init) True\<bar> \<le> spmf (map_spmf (collision \<circ> snd) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) True

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>spmf (run_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) True - spmf (run_gpv rp_bad \<A> init) True\<bar> \<le> spmf (map_spmf (collision \<circ> snd) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) True

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
have "ennreal \<dots> \<le> ennreal (q / card A) * (enat q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (spmf (map_spmf (collision \<circ> snd) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) True) \<le> ennreal (real q / real (card A)) * ennreal_of_enat (enat q)
[PROOF STEP]
unfolding if_False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (spmf (map_spmf (collision \<circ> snd) (exec_gpv rf.random_oracle \<A> Map.empty)) True) \<le> ennreal (real q / real (card A)) * ennreal_of_enat (enat q)
[PROOF STEP]
using bound _ _ _ _ _ _ _ WT
[PROOF STATE]
proof (prove)
using this:
interaction_bounded_by' (\<lambda>_. True) \<A> q
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
\<I> \<turnstile>g \<A> \<surd>

goal (1 subgoal):
 1. ennreal (spmf (map_spmf (collision \<circ> snd) (exec_gpv rf.random_oracle \<A> Map.empty)) True) \<le> ennreal (real q / real (card A)) * ennreal_of_enat (enat q)
[PROOF STEP]
by(rule rf.interaction_bounded_by_exec_gpv_bad_count[where count="\<lambda>s. card (dom s)"])
        (auto simp add: rf.random_oracle_def finite_A nonempty_A card_insert_if finite_subset[OF _ finite_A] map_spmf_conv_bind_spmf[symmetric] spmf.map_comp o_def collision_map_upd_iff map_mem_spmf_of_set card_gt_0_iff card_mono field_simps Int_absorb2 intro: card_ran_le_dom[OF finite_subset, OF _ finite_A, THEN order_trans] split: option.splits)
[PROOF STATE]
proof (state)
this:
ennreal (spmf (map_spmf (collision \<circ> snd) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) True) \<le> ennreal (real q / real (card A)) * ennreal_of_enat (enat q)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
hence "spmf (map_spmf (?bad1 \<circ> snd) (?run False)) True \<le> q * q / card A"
[PROOF STATE]
proof (prove)
using this:
ennreal (spmf (map_spmf (collision \<circ> snd) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) True) \<le> ennreal (real q / real (card A)) * ennreal_of_enat (enat q)

goal (1 subgoal):
 1. spmf (map_spmf (collision \<circ> snd) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) True \<le> real (q * q) / real (card A)
[PROOF STEP]
by(simp add: ennreal_of_nat_eq_real_of_nat ennreal_times_divide ennreal_mult''[symmetric])
[PROOF STATE]
proof (state)
this:
spmf (map_spmf (collision \<circ> snd) (exec_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty)) True \<le> real (q * q) / real (card A)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>spmf (run_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) True - spmf (run_gpv rp_bad \<A> init) True\<bar> \<le> real (q * q) / real (card A)
[PROOF STEP]
have "\<bar>spmf (run_gpv rp_bad \<A> init) True - spmf (run_gpv rf.random_oracle \<A> Map.empty) True\<bar> \<le> q * q / card A"
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (run_gpv (if False then rp.random_permutation else rf.random_oracle) \<A> Map.empty) True - spmf (run_gpv rp_bad \<A> init) True\<bar> \<le> real (q * q) / real (card A)

goal (1 subgoal):
 1. \<bar>spmf (run_gpv rp_bad \<A> init) True - spmf (run_gpv rf.random_oracle \<A> Map.empty) True\<bar> \<le> real (q * q) / real (card A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>spmf (run_gpv rp_bad \<A> init) True - spmf (run_gpv rf.random_oracle \<A> Map.empty) True\<bar> \<le> real (q * q) / real (card A)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<bar>spmf (run_gpv rp_bad \<A> init) True - spmf (run_gpv rf.random_oracle \<A> Map.empty) True\<bar> \<le> real (q * q) / real (card A)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
spmf (prp_game \<A>) True = spmf (run_gpv rp_bad \<A> init) True
\<bar>spmf (run_gpv rp_bad \<A> init) True - spmf (run_gpv rf.random_oracle \<A> Map.empty) True\<bar> \<le> real (q * q) / real (card A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
spmf (prp_game \<A>) True = spmf (run_gpv rp_bad \<A> init) True
\<bar>spmf (run_gpv rp_bad \<A> init) True - spmf (run_gpv rf.random_oracle \<A> Map.empty) True\<bar> \<le> real (q * q) / real (card A)

goal (1 subgoal):
 1. advantage \<A> \<le> real q * real q / real (card A)
[PROOF STEP]
by(simp add: advantage_def game_def)
[PROOF STATE]
proof (state)
this:
advantage \<A> \<le> real q * real q / real (card A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infty_assn_pure_conv: "infty_assn (pure A) = pure (\<langle>A\<rangle>infty_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infty_assn (pure A) = pure (\<langle>A\<rangle>infty_rel)
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. infty_assn (pure A) x xa = pure (\<langle>A\<rangle>infty_rel) x xa
[PROOF STEP]
subgoal for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infty_assn (pure A) x y = pure (\<langle>A\<rangle>infty_rel) x y
[PROOF STEP]
by (cases x; cases y; simp add: pure_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma infty_assn_pure[safe_constraint_rules]: "is_pure A \<Longrightarrow> is_pure (infty_assn A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure A \<Longrightarrow> is_pure (infty_assn A)
[PROOF STEP]
by (auto simp: is_pure_conv infty_assn_pure_conv)


[STATEMENT]
lemma infty_assn_id[simp]: "infty_assn id_assn = id_assn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infty_assn id_assn = id_assn
[PROOF STEP]
by (simp add: infty_assn_pure_conv)


[STATEMENT]
lemma [safe_constraint_rules]: "IS_BELOW_ID R \<Longrightarrow> IS_BELOW_ID (\<langle>R\<rangle>infty_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_BELOW_ID R \<Longrightarrow> IS_BELOW_ID (\<langle>R\<rangle>infty_rel)
[PROOF STEP]
by (auto simp: infty_rel_def IS_BELOW_ID_def)


[STATEMENT]
lemma Num_hnr[sepref_fr_rules]: "(return o Num,RETURN o Num)\<in>A\<^sup>d \<rightarrow>\<^sub>a infty_assn A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> Num, RETURN \<circ> Num) \<in> A\<^sup>d \<rightarrow>\<^sub>a infty_assn A
[PROOF STEP]
by sepref_to_hoare sep_auto


[STATEMENT]
lemma Infty_hnr[sepref_fr_rules]: "(uncurry0 (return Infty),uncurry0 (RETURN Infty))\<in>unit_assn\<^sup>k \<rightarrow>\<^sub>a infty_assn A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uncurry0 (return infty.Infty), uncurry0 (RETURN infty.Infty)) \<in> unit_assn\<^sup>k \<rightarrow>\<^sub>a infty_assn A
[PROOF STEP]
by sepref_to_hoare sep_auto


[STATEMENT]
lemma [sepref_monadify_arity]: "case_infty \<equiv> \<lambda>\<^sub>2f1 f2 x. SP case_infty$f1$(\<lambda>\<^sub>2x. f2$x)$x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case_infty \<equiv> \<lambda>x. (#\<lambda>xa. (#\<lambda>xb. (#SP case_infty $ x $ (\<lambda>x. (#xa $ x#)) $ xb#)#)#)
[PROOF STEP]
by simp


[STATEMENT]
lemma [sepref_monadify_comb]: "case_infty$f1$f2$x \<equiv> (\<bind>)$(EVAL$x)$(\<lambda>\<^sub>2x. SP case_infty$f1$f2$x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case_infty $ f1 $ f2 $ x \<equiv> (\<bind>) $ (EVAL $ x) $ (\<lambda>x. (#SP case_infty $ f1 $ f2 $ x#))
[PROOF STEP]
by simp


[STATEMENT]
lemma [sepref_monadify_comb]: "EVAL$(case_infty$f1$(\<lambda>\<^sub>2x. f2 x)$x)
  \<equiv> (\<bind>)$(EVAL$x)$(\<lambda>\<^sub>2x. SP case_infty$(EVAL $ f1)$(\<lambda>\<^sub>2x. EVAL $ f2 x)$x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EVAL $ (case_infty $ f1 $ (\<lambda>x. (#f2 x#)) $ x) \<equiv> (\<bind>) $ (EVAL $ x) $ (\<lambda>x. (#SP case_infty $ (EVAL $ f1) $ (\<lambda>x. (#EVAL $ f2 x#)) $ x#))
[PROOF STEP]
apply (rule eq_reflection)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EVAL $ (case_infty $ f1 $ (\<lambda>x. (#f2 x#)) $ x) = (\<bind>) $ (EVAL $ x) $ (\<lambda>x. (#SP case_infty $ (EVAL $ f1) $ (\<lambda>x. (#EVAL $ f2 x#)) $ x#))
[PROOF STEP]
by (simp split: infty.splits)


[STATEMENT]
lemma infty_assn_ctxt: "infty_assn A x y = z \<Longrightarrow> hn_ctxt (infty_assn A) x y = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infty_assn A x y = z \<Longrightarrow> hn_ctxt (infty_assn A) x y = z
[PROOF STEP]
by (simp add: hn_ctxt_def)


[STATEMENT]
lemma infty_cases_hnr[sepref_prep_comb_rule, sepref_comb_rules]:
  fixes A e e'
  defines [simp]: "INVe \<equiv> hn_invalid (infty_assn A) e e'"
  assumes FR: "\<Gamma> \<Longrightarrow>\<^sub>t hn_ctxt (infty_assn A) e e' * F"
  assumes Infty: "\<lbrakk>e = Infty; e' = Infty\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (infty_assn A) e e' * F) f1' (hn_ctxt XX1 e e' * \<Gamma>1') R f1"
  assumes Num: "\<And>x1 x1a. \<lbrakk>e = Num x1; e' = Num x1a\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt A x1 x1a * INVe * F) (f2' x1a) (hn_ctxt A' x1 x1a * hn_ctxt XX2 e e' * \<Gamma>2') R (f2 x1)"
  assumes MERGE2[unfolded hn_ctxt_def]: "\<Gamma>1' \<or>\<^sub>A \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'"
  shows "hn_refine \<Gamma> (case_infty f1' f2' e') (hn_ctxt (infty_assn A') e e' * \<Gamma>') R (case_infty$f1$(\<lambda>\<^sub>2x. f2 x)$e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine \<Gamma> (case e' of infty.Infty \<Rightarrow> f1' | Num x \<Rightarrow> f2' x) (hn_ctxt (infty_assn A') e e' * \<Gamma>') R (case_infty $ f1 $ (\<lambda>x. (#f2 x#)) $ e)
[PROOF STEP]
apply (rule hn_refine_cons_pre[OF FR])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (infty_assn A) e e' * F) (case e' of infty.Infty \<Rightarrow> f1' | Num x \<Rightarrow> f2' x) (hn_ctxt (infty_assn A') e e' * \<Gamma>') R (case_infty $ f1 $ (\<lambda>x. (#f2 x#)) $ e)
[PROOF STEP]
apply1 extract_hnr_invalids
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 h2. \<lbrakk>h2 \<Turnstile> F; hn_invalid (infty_assn A) e e' = true\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (infty_assn A) e e' * F) (case e' of infty.Infty \<Rightarrow> f1' | Num x \<Rightarrow> f2' x) (hn_ctxt (infty_assn A') e e' * \<Gamma>') R (case_infty $ f1 $ (\<lambda>x. (#f2 x#)) $ e)
[PROOF STEP]
apply (cases e; cases e'; simp add: infty_assn.simps[THEN infty_assn_ctxt])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h2. \<lbrakk>h2 \<Turnstile> F; hn_invalid (infty_assn A) infty.Infty infty.Infty = true; e = infty.Infty; e' = infty.Infty\<rbrakk> \<Longrightarrow> hn_refine F f1' \<Gamma>' R f1
 2. \<And>h2 x2 x2a. \<lbrakk>h2 \<Turnstile> F; hn_invalid (infty_assn A) (Num x2) (Num x2a) = true; e = Num x2; e' = Num x2a\<rbrakk> \<Longrightarrow> hn_refine (A x2 x2a * F) (f2' x2a) (A' x2 x2a * \<Gamma>') R (f2 x2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) infty.Infty infty.Infty = true; e = infty.Infty; e' = infty.Infty\<rbrakk> \<Longrightarrow> hn_refine F f1' \<Gamma>' R f1
[PROOF STEP]
apply (rule hn_refine_cons[OF _ Infty _ entt_refl]; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) infty.Infty infty.Infty = true; e = infty.Infty; e' = infty.Infty\<rbrakk> \<Longrightarrow> F \<Longrightarrow>\<^sub>t hn_ctxt (infty_assn A) e e' * F
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) infty.Infty infty.Infty = true; e = infty.Infty; e' = infty.Infty\<rbrakk> \<Longrightarrow> hn_ctxt XX1 e e' * \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) infty.Infty infty.Infty = true; e = infty.Infty; e' = infty.Infty\<rbrakk> \<Longrightarrow> hn_ctxt XX1 e e' * \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply (subst mult.commute, rule entt_fr_drop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) infty.Infty infty.Infty = true; e = infty.Infty; e' = infty.Infty\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply (rule entt_trans[OF _ MERGE2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) infty.Infty infty.Infty = true; e = infty.Infty; e' = infty.Infty\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>1' \<or>\<^sub>A \<Gamma>2'
[PROOF STEP]
apply (simp add:)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h2 x2 x2a. \<lbrakk>h2 \<Turnstile> F; hn_invalid (infty_assn A) (Num x2) (Num x2a) = true; e = Num x2; e' = Num x2a\<rbrakk> \<Longrightarrow> hn_refine (A x2 x2a * F) (f2' x2a) (A' x2 x2a * \<Gamma>') R (f2 x2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> hn_refine (A x2_ x2a_ * F) (f2' x2a_) (A' x2_ x2a_ * \<Gamma>') R (f2 x2_)
[PROOF STEP]
apply (rule hn_refine_cons[OF _ Num _ entt_refl]; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> A x2_ x2a_ * F \<Longrightarrow>\<^sub>t hn_ctxt A x2_ x2a_ * INVe * F
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> hn_ctxt A' x2_ x2a_ * hn_ctxt XX2 e e' * \<Gamma>2' \<Longrightarrow>\<^sub>t A' x2_ x2a_ * \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> hn_ctxt A' x2_ x2a_ * hn_ctxt XX2 e e' * \<Gamma>2' \<Longrightarrow>\<^sub>t A' x2_ x2a_ * \<Gamma>'
[PROOF STEP]
apply (rule entt_star_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> hn_ctxt A' x2_ x2a_ * hn_ctxt XX2 e e' \<Longrightarrow>\<^sub>t A' x2_ x2a_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_fr_drop)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> hn_ctxt A' x2_ x2a_ \<Longrightarrow>\<^sub>t A' x2_ x2a_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_trans[OF _ MERGE2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (infty_assn A) (Num x2_) (Num x2a_) = true; e = Num x2_; e' = Num x2a_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>1' \<or>\<^sub>A \<Gamma>2'
[PROOF STEP]
applyS (simp add:)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hnr_val[sepref_fr_rules]: "(return o Weight.val,RETURN o Weight.val) \<in> [\<lambda>x. x\<noteq>Infty]\<^sub>a (infty_assn A)\<^sup>d \<rightarrow> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> Weight.val, RETURN \<circ> Weight.val) \<in> [\<lambda>x. x \<noteq> infty.Infty]\<^sub>a (infty_assn A)\<^sup>d \<rightarrow> A
[PROOF STEP]
apply sepref_to_hoare
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xi. \<lbrakk>x \<noteq> infty.Infty; x ::\<^sub>i TYPE('b infty); nofail (RETURN (Weight.val x))\<rbrakk> \<Longrightarrow> <infty_assn A x xi> return (Weight.val xi) <\<lambda>r. true * (\<exists>\<^sub>Axa. A xa r * \<up> (RETURN xa \<le> RETURN (Weight.val x)))>\<^sub>t
[PROOF STEP]
subgoal for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> infty.Infty; x ::\<^sub>i TYPE('b infty); nofail (RETURN (Weight.val x))\<rbrakk> \<Longrightarrow> <infty_assn A x y> return (Weight.val y) <\<lambda>r. true * (\<exists>\<^sub>Axa. A xa r * \<up> (RETURN xa \<le> RETURN (Weight.val x)))>\<^sub>t
[PROOF STEP]
by (cases x; cases y; sep_auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma infty_less_param[param]:
  "(infty_less,infty_less) \<in> (R\<rightarrow>R\<rightarrow>bool_rel) \<rightarrow> \<langle>R\<rangle>infty_rel \<rightarrow> \<langle>R\<rangle>infty_rel \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (infty_less, infty_less) \<in> (R \<rightarrow> R \<rightarrow> bool_rel) \<rightarrow> \<langle>R\<rangle>infty_rel \<rightarrow> \<langle>R\<rangle>infty_rel \<rightarrow> bool_rel
[PROOF STEP]
unfolding infty_less_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>lt a b. case (a, b) of (infty.Infty, ba) \<Rightarrow> False | (Num a, infty.Infty) \<Rightarrow> True | (Num a, Num b) \<Rightarrow> lt a b, \<lambda>lt a b. case (a, b) of (infty.Infty, ba) \<Rightarrow> False | (Num a, infty.Infty) \<Rightarrow> True | (Num a, Num b) \<Rightarrow> lt a b) \<in> (R \<rightarrow> R \<rightarrow> bool_rel) \<rightarrow> \<langle>R\<rangle>infty_rel \<rightarrow> \<langle>R\<rangle>infty_rel \<rightarrow> bool_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma infty_less_eq_less: "infty_less (<) = (<)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infty_less (<) = (<)
[PROOF STEP]
unfolding infty_less_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b. case (a, b) of (infty.Infty, ba) \<Rightarrow> False | (Num a, infty.Infty) \<Rightarrow> True | (Num a, Num x) \<Rightarrow> a < x) = (<)
[PROOF STEP]
apply (clarsimp intro!: ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (case a of infty.Infty \<Rightarrow> False | Num a \<Rightarrow> case b of infty.Infty \<Rightarrow> True | Num x \<Rightarrow> a < x) = (a < b)
[PROOF STEP]
subgoal for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case a of infty.Infty \<Rightarrow> False | Num a \<Rightarrow> case b of infty.Infty \<Rightarrow> True | Num x \<Rightarrow> a < x) = (a < b)
[PROOF STEP]
by (cases a; cases b; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma param_mpath': "(mpath',mpath')
  \<in> \<langle>\<langle>A\<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel \<times>\<^sub>r B\<rangle>option_rel \<rightarrow> \<langle>\<langle>A\<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mpath', mpath') \<in> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel \<times>\<^sub>r B\<rangle>option_rel \<rightarrow> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel\<rangle>option_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (mpath', mpath') \<in> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel \<times>\<^sub>r B\<rangle>option_rel \<rightarrow> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel\<rangle>option_rel
[PROOF STEP]
have 1: "mpath' = map_option fst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpath' = map_option fst
[PROOF STEP]
apply (intro ext, rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. mpath' x = map_option fst x
[PROOF STEP]
apply (case_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x = None \<Longrightarrow> mpath' x = map_option fst x
 2. \<And>x a. x = Some a \<Longrightarrow> mpath' x = map_option fst x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a. x = Some a \<Longrightarrow> mpath' x = map_option fst x
[PROOF STEP]
apply (rename_tac a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a. x = Some a \<Longrightarrow> mpath' x = map_option fst x
[PROOF STEP]
apply (case_tac a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a aa b. \<lbrakk>x = Some a; a = (aa, b)\<rbrakk> \<Longrightarrow> mpath' x = map_option fst x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mpath' = map_option fst

goal (1 subgoal):
 1. (mpath', mpath') \<in> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel \<times>\<^sub>r B\<rangle>option_rel \<rightarrow> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel\<rangle>option_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mpath', mpath') \<in> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel \<times>\<^sub>r B\<rangle>option_rel \<rightarrow> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel\<rangle>option_rel
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_option fst, map_option fst) \<in> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel \<times>\<^sub>r B\<rangle>option_rel \<rightarrow> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel\<rangle>option_rel
[PROOF STEP]
by parametricity
[PROOF STATE]
proof (state)
this:
(mpath', mpath') \<in> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel \<times>\<^sub>r B\<rangle>option_rel \<rightarrow> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel\<rangle>option_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma param_mpath_weight':
  "(mpath_weight', mpath_weight') \<in> \<langle>\<langle>A\<times>\<^sub>rB\<times>\<^sub>rA\<rangle>list_rel \<times>\<^sub>r B\<rangle>option_rel \<rightarrow> \<langle>B\<rangle>infty_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mpath_weight', mpath_weight') \<in> \<langle>\<langle>A \<times>\<^sub>r B \<times>\<^sub>r A\<rangle>list_rel \<times>\<^sub>r B\<rangle>option_rel \<rightarrow> \<langle>B\<rangle>infty_rel
[PROOF STEP]
by (auto elim!: option_relE simp: infty_rel_def top_infty_def)


[STATEMENT]
lemma mdijkstra_correct:
    "(mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel
[PROOF STEP]
note mdijkstra_refines
[PROOF STATE]
proof (state)
this:
mdijkstra \<le> \<Down> (br \<alpha>r res_invarm) dijkstra'

goal (1 subgoal):
 1. (mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mdijkstra \<le> \<Down> (br \<alpha>r res_invarm) dijkstra'

goal (1 subgoal):
 1. (mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel
[PROOF STEP]
note dijkstra'_refines
[PROOF STATE]
proof (state)
this:
dijkstra' \<le> \<Down> Id dijkstra

goal (1 subgoal):
 1. (mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dijkstra' \<le> \<Down> Id dijkstra

goal (1 subgoal):
 1. (mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel
[PROOF STEP]
note dijkstra_correct
[PROOF STATE]
proof (state)
this:
dijkstra \<le> SPEC (is_shortest_path_map v0)

goal (1 subgoal):
 1. (mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mdijkstra \<le> \<Down> (br \<alpha>r res_invarm) (SPEC (is_shortest_path_map v0))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mdijkstra \<le> \<Down> (br \<alpha>r res_invarm) (SPEC (is_shortest_path_map v0))

goal (1 subgoal):
 1. (mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel
[PROOF STEP]
by (rule nres_relI)
[PROOF STATE]
proof (state)
this:
(mdijkstra, SPEC (is_shortest_path_map v0)) \<in> \<langle>br \<alpha>r res_invarm\<rangle>nres_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma w_plus_param: "((+), (+)::'W\<Rightarrow>_) \<in> Id \<rightarrow> Id \<rightarrow> Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((+), (+)) \<in> Id \<rightarrow> Id \<rightarrow> Id
[PROOF STEP]
by simp


[STATEMENT]
lemma w_less_param: "((<), (<)::'W\<Rightarrow>_) \<in> Id \<rightarrow> Id \<rightarrow> Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((<), (<)) \<in> Id \<rightarrow> Id \<rightarrow> bool_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma [sepref_gen_algo_rules]:
    "GEN_ALGO (return oo (+)) (\<lambda>f. (uncurry f, uncurry (RETURN \<circ>\<circ> (+))) \<in> id_assn\<^sup>k *\<^sub>a id_assn\<^sup>k \<rightarrow>\<^sub>a id_assn)"
    "GEN_ALGO (return oo (<)) (\<lambda>f. (uncurry f, uncurry (RETURN \<circ>\<circ> (<))) \<in> id_assn\<^sup>k *\<^sub>a id_assn\<^sup>k \<rightarrow>\<^sub>a id_assn)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GEN_ALGO (return \<circ>\<circ> (+)) (\<lambda>f. (uncurry f, uncurry (RETURN \<circ>\<circ> (+))) \<in> id_assn\<^sup>k *\<^sub>a id_assn\<^sup>k \<rightarrow>\<^sub>a id_assn) &&& GEN_ALGO (return \<circ>\<circ> (<)) (\<lambda>f. (uncurry f, uncurry (RETURN \<circ>\<circ> (<))) \<in> id_assn\<^sup>k *\<^sub>a id_assn\<^sup>k \<rightarrow>\<^sub>a bool_assn)
[PROOF STEP]
by (sep_auto simp: GEN_ALGO_def pure_def intro!: hfrefI hn_refineI)+


[STATEMENT]
lemma conv_prio_pop_min: "prio_pop_min m = do {
      ASSERT (dom m \<noteq> {});
      ((k,v),m) \<leftarrow> mop_pm_pop_min id m;
      RETURN (k,v,m)
    }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prio_pop_min m = ASSERT (dom m \<noteq> {}) \<bind> (\<lambda>_. mop_pm_pop_min id m \<bind> (\<lambda>((k, v), m). RETURN (k, v, m)))
[PROOF STEP]
unfolding prio_pop_min_def mop_pm_pop_min_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (dom m \<noteq> {}) \<bind> (\<lambda>_. SPEC (\<lambda>(e, w, q'). q' = m(e := None) \<and> m e = Some w \<and> (\<forall>e' w'. m e' = Some w' \<longrightarrow> w \<le> w'))) = ASSERT (dom m \<noteq> {}) \<bind> (\<lambda>_. mop pre_pm_pop_min (PR_CONST (op_pm_pop_min id)) m \<bind> (\<lambda>((k, v), m). RETURN (k, v, m)))
[PROOF STEP]
by (auto simp: pw_eq_iff refine_pw_simps ran_def)


[STATEMENT]
lemma mdijkstra'_aref: "(uncurry mdijkstra',uncurry (SPEC oo weighted_graph.is_shortest_path_map))
  \<in> [\<lambda>(G,v0). Dijkstra G v0]\<^sub>f Id\<times>\<^sub>rId \<rightarrow> \<langle>br Dijkstra.\<alpha>r Dijkstra.res_invarm\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uncurry mdijkstra', uncurry (SPEC \<circ>\<circ> weighted_graph.is_shortest_path_map)) \<in> [\<lambda>(G, v0). Dijkstra G v0]\<^sub>f Id \<times>\<^sub>r Id \<rightarrow> \<langle>br Dijkstra.\<alpha>r Dijkstra.res_invarm\<rangle>nres_rel
[PROOF STEP]
using Dijkstra.mdijkstra_correct
[PROOF STATE]
proof (prove)
using this:
Dijkstra ?G ?v0.0 \<Longrightarrow> (Dijkstra.mdijkstra ?G ?v0.0, SPEC (weighted_graph.is_shortest_path_map ?G ?v0.0)) \<in> \<langle>br Dijkstra.\<alpha>r Dijkstra.res_invarm\<rangle>nres_rel

goal (1 subgoal):
 1. (uncurry mdijkstra', uncurry (SPEC \<circ>\<circ> weighted_graph.is_shortest_path_map)) \<in> [\<lambda>(G, v0). Dijkstra G v0]\<^sub>f Id \<times>\<^sub>r Id \<rightarrow> \<langle>br Dijkstra.\<alpha>r Dijkstra.res_invarm\<rangle>nres_rel
[PROOF STEP]
by (fastforce intro!: frefI simp: mdijkstra'.refine[symmetric])


[STATEMENT]
theorem dijkstra_imp_correct: "(uncurry (dijkstra_imp N), uncurry (SPEC \<circ>\<circ> weighted_graph.is_shortest_path_map))
  \<in> [\<lambda>(G, v0). v0 \<in> nodes G \<and> (\<forall>(v, w, v') \<in> edges G. 0 \<le> w)]\<^sub>a (is_graph N Id)\<^sup>k *\<^sub>a (node_assn N)\<^sup>k \<rightarrow> drmap_assn N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uncurry (dijkstra_imp N), uncurry (SPEC \<circ>\<circ> weighted_graph.is_shortest_path_map)) \<in> [\<lambda>(G, v0). v0 \<in> nodes G \<and> (\<forall>(v, w, v')\<in>edges G. (0::'a) \<le> w)]\<^sub>a (is_graph N Id)\<^sup>k *\<^sub>a (nbn_assn N)\<^sup>k \<rightarrow> drmap_assn N
[PROOF STEP]
apply (rule hfref_weaken_pre'[OF _ dijkstra_imp.refine[FCOMP mdijkstra'_aref]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>case x of (G, v0) \<Rightarrow> v0 \<in> nodes G \<and> (\<forall>(v, w, v')\<in>edges G. (0::'a) \<le> w); rdomp (fst ((is_graph N Id)\<^sup>k *\<^sub>a (nbn_assn N)\<^sup>k)) x\<rbrakk> \<Longrightarrow> case x of (x, xa) \<Rightarrow> Dijkstra x xa
[PROOF STEP]
proof clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
fix G :: "(nat,'w::{weight,heap}) graph" and v0
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
assume v0_is_node: "v0 \<in> nodes G"
    and nonneg_weights: "\<forall>(v, w, v') \<in> edges G. 0 \<le> w"
    and "v0<N"
    and RDOM: "rdomp (is_graph N Id) G"
[PROOF STATE]
proof (state)
this:
v0 \<in> nodes G
\<forall>(v, w, v')\<in>edges G. (0::'w) \<le> w
v0 < N
rdomp (is_graph N Id) G

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
from RDOM
[PROOF STATE]
proof (chain)
picking this:
rdomp (is_graph N Id) G
[PROOF STEP]
interpret valid_graph G
[PROOF STATE]
proof (prove)
using this:
rdomp (is_graph N Id) G

goal (1 subgoal):
 1. valid_graph G
[PROOF STEP]
unfolding is_graph_def rdomp_def
[PROOF STATE]
proof (prove)
using this:
\<exists>h c. h \<Turnstile> (\<exists>\<^sub>Al. c \<mapsto>\<^sub>a l * \<up> (valid_graph G \<and> N = length l \<and> nodes G = {0..<length l} \<and> (\<forall>v\<in>nodes G. (l ! v, succ G v) \<in> \<langle>Id \<times>\<^sub>r nbn_rel (length l)\<rangle>list_set_rel)))

goal (1 subgoal):
 1. valid_graph G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
from RDOM
[PROOF STATE]
proof (chain)
picking this:
rdomp (is_graph N Id) G
[PROOF STEP]
have [simp]: "finite V"
[PROOF STATE]
proof (prove)
using this:
rdomp (is_graph N Id) G

goal (1 subgoal):
 1. finite V
[PROOF STEP]
unfolding is_graph_def rdomp_def
[PROOF STATE]
proof (prove)
using this:
\<exists>h c. h \<Turnstile> (\<exists>\<^sub>Al. c \<mapsto>\<^sub>a l * \<up> (valid_graph G \<and> N = length l \<and> V = {0..<length l} \<and> (\<forall>v\<in>V. (l ! v, succ G v) \<in> \<langle>Id \<times>\<^sub>r nbn_rel (length l)\<rangle>list_set_rel)))

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

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
from RDOM
[PROOF STATE]
proof (chain)
picking this:
rdomp (is_graph N Id) G
[PROOF STEP]
have "\<forall>v\<in>V. {(w, v'). (v, w, v') \<in> E} \<in>
    Range (\<langle>Id \<times>\<^sub>r node_rel N\<rangle>list_set_rel)"
[PROOF STATE]
proof (prove)
using this:
rdomp (is_graph N Id) G

goal (1 subgoal):
 1. \<forall>v\<in>V. {(w, v'). (v, w, v') \<in> E} \<in> Range (\<langle>Id \<times>\<^sub>r nbn_rel N\<rangle>list_set_rel)
[PROOF STEP]
by (auto simp: succ_def is_graph_def rdomp_def)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>V. {(w, v'). (v, w, v') \<in> E} \<in> Range (\<langle>Id \<times>\<^sub>r nbn_rel N\<rangle>list_set_rel)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
hence "\<forall>v\<in>V. finite {(w, v'). (v, w, v') \<in> E}"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V. {(w, v'). (v, w, v') \<in> E} \<in> Range (\<langle>Id \<times>\<^sub>r nbn_rel N\<rangle>list_set_rel)

goal (1 subgoal):
 1. \<forall>v\<in>V. finite {(w, v'). (v, w, v') \<in> E}
[PROOF STEP]
unfolding list_set_rel_range
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V. {(w, v'). (v, w, v') \<in> E} \<in> {S. finite S \<and> S \<subseteq> Range (Id \<times>\<^sub>r nbn_rel N)}

goal (1 subgoal):
 1. \<forall>v\<in>V. finite {(w, v'). (v, w, v') \<in> E}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>V. finite {(w, v'). (v, w, v') \<in> E}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
hence "finite (Sigma V (\<lambda>v. {(w, v'). (v, w, v') \<in> E}))"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V. finite {(w, v'). (v, w, v') \<in> E}

goal (1 subgoal):
 1. finite (SIGMA v:V. {(w, v'). (v, w, v') \<in> E})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (SIGMA v:V. {(w, v'). (v, w, v') \<in> E})

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
finite (SIGMA v:V. {(w, v'). (v, w, v') \<in> E})

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
have "E \<subseteq> (Sigma V (\<lambda>v. {(w, v'). (v, w, v') \<in> E}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<subseteq> (SIGMA v:V. {(w, v'). (v, w, v') \<in> E})
[PROOF STEP]
using E_valid
[PROOF STATE]
proof (prove)
using this:
fst ` E \<subseteq> V
snd ` snd ` E \<subseteq> V

goal (1 subgoal):
 1. E \<subseteq> (SIGMA v:V. {(w, v'). (v, w, v') \<in> E})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E \<subseteq> (SIGMA v:V. {(w, v'). (v, w, v') \<in> E})

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
finally (finite_subset[rotated])
[PROOF STATE]
proof (chain)
picking this:
finite E
[PROOF STEP]
have [simp]: "finite E"
[PROOF STATE]
proof (prove)
using this:
finite E

goal (1 subgoal):
 1. finite E
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite E

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<in> nodes a; \<forall>x\<in>edges a. case x of (v, w, v') \<Rightarrow> (0::'a) \<le> w; rdomp (is_graph N Id) a; b < N\<rbrakk> \<Longrightarrow> Dijkstra a b
[PROOF STEP]
show "Dijkstra G v0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dijkstra G v0
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. finite V
 2. finite E
 3. v0 \<in> V
 4. \<And>v w v'. (v, w, v') \<in> E \<Longrightarrow> (0::'w) \<le> w
[PROOF STEP]
unfolding is_graph_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. finite V
 2. finite E
 3. v0 \<in> V
 4. \<And>v w v'. (v, w, v') \<in> E \<Longrightarrow> (0::'w) \<le> w
[PROOF STEP]
using v0_is_node nonneg_weights
[PROOF STATE]
proof (prove)
using this:
v0 \<in> V
\<forall>(v, w, v')\<in>E. (0::'w) \<le> w

goal (4 subgoals):
 1. finite V
 2. finite E
 3. v0 \<in> V
 4. \<And>v w v'. (v, w, v') \<in> E \<Longrightarrow> (0::'w) \<le> w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Dijkstra G v0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (ccTransform a e) \<subseteq> supp e
[PROOF STEP]
by (induction rule: transform.induct)
       (auto simp add: exp_assn.supp Let_supp dest!: subsetD[OF supp_map_transform] subsetD[OF supp_map_transform_step] )


[STATEMENT]
lemma transform_alts_Nil[simp]: "transform_alts [] S = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transform_alts [] S = S
[PROOF STEP]
by (induction  S) auto


[STATEMENT]
lemma Astack_transform_alts[simp]:
    "Astack (transform_alts as S) = Astack S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Astack (transform_alts as S) = Astack S
[PROOF STEP]
by (induction rule: transform_alts.induct) auto


[STATEMENT]
lemma fresh_star_transform_alts[intro]: "a \<sharp>* S \<Longrightarrow> a \<sharp>* transform_alts as S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp>* S \<Longrightarrow> a \<sharp>* transform_alts as S
[PROOF STEP]
by (induction as S  rule: transform_alts.induct) (auto simp add: fresh_star_Cons)


[STATEMENT]
lemma closed_consistent:
    assumes "fv e = ({}::var set)"
    shows "consistent (\<bottom>, \<bottom>, 0, [], []) ([], e, [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent (\<bottom>, \<bottom>, 0, [], []) ([], e, [])
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. consistent (\<bottom>, \<bottom>, 0, [], []) ([], e, [])
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
fv e = {}
[PROOF STEP]
have "edom (prognosis \<bottom> [] 0 ([], e, [])) = {}"
[PROOF STATE]
proof (prove)
using this:
fv e = {}

goal (1 subgoal):
 1. edom (prognosis \<bottom> [] 0 ([], e, [])) = {}
[PROOF STEP]
by (auto dest!: subsetD[OF edom_prognosis])
[PROOF STATE]
proof (state)
this:
edom (prognosis \<bottom> [] 0 ([], e, [])) = {}

goal (1 subgoal):
 1. consistent (\<bottom>, \<bottom>, 0, [], []) ([], e, [])
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
edom (prognosis \<bottom> [] 0 ([], e, [])) = {}

goal (1 subgoal):
 1. consistent (\<bottom>, \<bottom>, 0, [], []) ([], e, [])
[PROOF STEP]
by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])
[PROOF STATE]
proof (state)
this:
consistent (\<bottom>, \<bottom>, 0, [], []) ([], e, [])

goal:
No subgoals!
[PROOF STEP]
qed