theory Oblivious

lemma oblivious_modify_swap:
  "oblivious f m \<Longrightarrow> (modify f >>= (\<lambda>rv. m)) = (m >>= (\<lambda>rv. modify f))" apply (clarsimp simp: bind_def simpler_modify_def) apply (rule ext)+ apply (case_tac "m (f s)", clarsimp) apply (simp add: oblivious_def) apply (drule_tac x=s in spec) apply (rule conjI) apply (rule set_eqI) apply (rule iffI) apply (drule conjunct2, drule conjunct1) apply (drule_tac x=x in bspec, simp) apply clarsimp apply (rule_tac x="((), s'')" in bexI) apply simp apply simp apply (drule conjunct1) apply fastforce apply (drule conjunct2)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f m \<Longrightarrow> do rv <- modify f;
m
od = do rv <- m;
modify f
od proof (prove)
goal (1 subgoal):
 1. oblivious f m \<Longrightarrow> (\<lambda>s. m (f s)) = (\<lambda>s. (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)), (\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. oblivious f m \<Longrightarrow> m (f s) = (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)), (\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>oblivious f m; m (f s) = (a, b)\<rbrakk> \<Longrightarrow> a = (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<and> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); m (f s) = (a, b)\<rbrakk> \<Longrightarrow> a = (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<and> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> a = (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<and> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> a = (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))
 2. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> (x \<in> a) = (x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False))))
 2. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b x. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); x \<in> a\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))
 2. \<And>s a b x. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))\<rbrakk> \<Longrightarrow> x \<in> a
 3. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b x. \<lbrakk>m (f s) = (a, b); x \<in> a; \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s''\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))
 2. \<And>s a b x. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))\<rbrakk> \<Longrightarrow> x \<in> a
 3. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b x. \<lbrakk>m (f s) = (a, b); x \<in> a; case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s''\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))
 2. \<And>s a b x. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))\<rbrakk> \<Longrightarrow> x \<in> a
 3. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b s''. \<lbrakk>m (f s) = (a, b); ((), f s'') \<in> a; ((), s'') \<in> fst (m s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m s). ((), f s'') \<in> fst (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))
 2. \<And>s a b x. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))\<rbrakk> \<Longrightarrow> x \<in> a
 3. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (4 subgoals):
 1. \<And>s a b s''. \<lbrakk>m (f s) = (a, b); ((), f s'') \<in> a; ((), s'') \<in> fst (m s)\<rbrakk> \<Longrightarrow> ((), f s'') \<in> fst (case ((), s'') of (rv, s) \<Rightarrow> ({((), f s)}, False))
 2. \<And>s a b s''. \<lbrakk>m (f s) = (a, b); ((), f s'') \<in> a; ((), s'') \<in> fst (m s)\<rbrakk> \<Longrightarrow> ((), s'') \<in> fst (m s)
 3. \<And>s a b x. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))\<rbrakk> \<Longrightarrow> x \<in> a
 4. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b s''. \<lbrakk>m (f s) = (a, b); ((), f s'') \<in> a; ((), s'') \<in> fst (m s)\<rbrakk> \<Longrightarrow> ((), s'') \<in> fst (m s)
 2. \<And>s a b x. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))\<rbrakk> \<Longrightarrow> x \<in> a
 3. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False)))\<rbrakk> \<Longrightarrow> x \<in> a
 2. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>m (f s) = (a, b); x \<in> (\<Union>a\<in>fst (m s). fst (case a of (rv, s) \<Rightarrow> ({((), f s)}, False))); \<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))\<rbrakk> \<Longrightarrow> x \<in> a
 2. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>m (f s) = (a, b); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> ((), f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. ((), s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>m (f s) = (a, b); snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> b = ((\<exists>x\<in>fst (m s). snd (case x of (rv, s) \<Rightarrow> ({((), f s)}, False))) \<or> snd (m s)) proof (prove)
goal:
No subgoals!