theory Oblivious

lemma oblivious_bind:
  "\<lbrakk> oblivious f m; \<And>rv. oblivious f (m' rv) \<rbrakk> \<Longrightarrow> oblivious f (m >>= m')" apply (simp add: oblivious_def) apply (rule allI) apply (erule allE) apply (intro conjI) apply (drule conjunct1) apply (clarsimp simp: in_monad) apply fastforce apply (drule conjunct2, drule conjunct1) apply (clarsimp simp: in_monad) apply fastforce apply (clarsimp simp: bind_def disj_commute) apply (rule disj_cong [OF refl]) apply (rule iffI) apply (clarsimp simp: split_def) apply fastforce apply clarsimp apply (drule(1) bspec) apply (clarsimp simp: split_def) apply (drule (1) bspec) apply (rule bexI [rotated], assumption) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oblivious f m; \<And>rv. oblivious f (m' rv)\<rbrakk> \<Longrightarrow> oblivious f (m >>= m') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); \<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s)\<rbrakk> \<Longrightarrow> \<forall>s. (\<forall>x\<in>fst ((m >>= m') s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst ((m >>= m') (f s))) \<and> (\<forall>x\<in>fst ((m >>= m') (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst ((m >>= m') s) \<and> s' = f s'') \<and> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s); \<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((m >>= m') s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst ((m >>= m') (f s))) \<and> (\<forall>x\<in>fst ((m >>= m') (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst ((m >>= m') s) \<and> s' = f s'') \<and> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s)))) \<and> (\<forall>x\<in>fst (m (f (?s6 s))). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m (?s6 s)) \<and> s' = f s'') \<and> snd (m (f (?s6 s))) = snd (m (?s6 s))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((m >>= m') s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst ((m >>= m') (f s))) \<and> (\<forall>x\<in>fst ((m >>= m') (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst ((m >>= m') s) \<and> s' = f s'') \<and> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s)))) \<and> (\<forall>x\<in>fst (m (f (?s6 s))). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m (?s6 s)) \<and> s' = f s'') \<and> snd (m (f (?s6 s))) = snd (m (?s6 s))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m >>= m') s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst ((m >>= m') (f s))
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s)))) \<and> (\<forall>x\<in>fst (m (f (?s6 s))). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m (?s6 s)) \<and> s' = f s'') \<and> snd (m (f (?s6 s))) = snd (m (?s6 s))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m >>= m') (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst ((m >>= m') s) \<and> s' = f s''
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s)))) \<and> (\<forall>x\<in>fst (m (f (?s6 s))). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m (?s6 s)) \<and> s' = f s'') \<and> snd (m (f (?s6 s))) = snd (m (?s6 s))\<rbrakk> \<Longrightarrow> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s)))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m >>= m') s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst ((m >>= m') (f s))
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s)))) \<and> (\<forall>x\<in>fst (m (f (?s6 s))). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m (?s6 s)) \<and> s' = f s'') \<and> snd (m (f (?s6 s))) = snd (m (?s6 s))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m >>= m') (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst ((m >>= m') s) \<and> s' = f s''
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s)))) \<and> (\<forall>x\<in>fst (m (f (?s6 s))). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m (?s6 s)) \<and> s' = f s'') \<and> snd (m (f (?s6 s))) = snd (m (?s6 s))\<rbrakk> \<Longrightarrow> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (3 subgoals):
 1. \<And>s a b s'' x. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s))); (x, s'') \<in> fst (m s); (a, b) \<in> fst (m' x s'')\<rbrakk> \<Longrightarrow> \<exists>s'' x. (x, s'') \<in> fst (m (f s)) \<and> (a, f b) \<in> fst (m' x s'')
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s)))) \<and> (\<forall>x\<in>fst (m (f (?s6 s))). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m (?s6 s)) \<and> s' = f s'') \<and> snd (m (f (?s6 s))) = snd (m (?s6 s))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m >>= m') (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst ((m >>= m') s) \<and> s' = f s''
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m (?s6 s)). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f (?s6 s)))) \<and> (\<forall>x\<in>fst (m (f (?s6 s))). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m (?s6 s)) \<and> s' = f s'') \<and> snd (m (f (?s6 s))) = snd (m (?s6 s))\<rbrakk> \<Longrightarrow> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m >>= m') (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst ((m >>= m') s) \<and> s' = f s''
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m >>= m') (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst ((m >>= m') s) \<and> s' = f s''
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b s'' x. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''; (x, s'') \<in> fst (m (f s)); (a, b) \<in> fst (m' x s'')\<rbrakk> \<Longrightarrow> \<exists>s''. (\<exists>s''a x. (x, s''a) \<in> fst (m s) \<and> (a, s'') \<in> fst (m' x s''a)) \<and> b = f s''
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); (\<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s))) \<and> (\<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s'') \<and> snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> snd ((m >>= m') (f s)) = snd ((m >>= m') s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s)); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''; snd (m (f s)) = snd (m s)\<rbrakk> \<Longrightarrow> (snd (m s) \<or> (\<exists>x\<in>fst (m (f s)). snd (case x of (x, xa) \<Rightarrow> m' x xa))) = (snd (m s) \<or> (\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> m' x xa))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s)); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''; snd (m (f s)) = snd (m s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (m (f s)). snd (case x of (x, xa) \<Rightarrow> m' x xa)) = (\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> m' x xa)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s)); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''; snd (m (f s)) = snd (m s); \<not> snd (m s); \<exists>x\<in>fst (m (f s)). snd (case x of (x, xa) \<Rightarrow> m' x xa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> m' x xa)
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s)); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''; snd (m (f s)) = snd (m s); \<not> snd (m s); \<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> m' x xa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m (f s)). snd (case x of (x, xa) \<Rightarrow> m' x xa) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). (fst x, f (snd x)) \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). \<exists>s''. (fst x, s'') \<in> fst (m' rv s) \<and> snd x = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m s). (fst x, f (snd x)) \<in> fst (m (f s)); \<forall>x\<in>fst (m (f s)). \<exists>s''. (fst x, s'') \<in> fst (m s) \<and> snd x = f s''; \<not> snd (m (f s)); \<not> snd (m s); (a, b) \<in> fst (m (f s)); snd (m' a b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m s). snd (m' (fst x) (snd x))
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s)); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''; snd (m (f s)) = snd (m s); \<not> snd (m s); \<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> m' x xa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m (f s)). snd (case x of (x, xa) \<Rightarrow> m' x xa) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s)); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''; snd (m (f s)) = snd (m s); \<not> snd (m s); \<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> m' x xa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m (f s)). snd (case x of (x, xa) \<Rightarrow> m' x xa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s)); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''; \<not> snd (m (f s)); \<not> snd (m s); (a, b) \<in> fst (m s); snd (m' a b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m (f s)). snd (case x of (x, xa) \<Rightarrow> m' x xa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). case x of (rva, s') \<Rightarrow> (rva, f s') \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). case x of (rva, s') \<Rightarrow> \<exists>s''. (rva, s'') \<in> fst (m' rv s) \<and> s' = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m (f s)). case x of (rv, s') \<Rightarrow> \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s''; \<not> snd (m (f s)); \<not> snd (m s); (a, b) \<in> fst (m s); snd (m' a b); case (a, b) of (rv, s') \<Rightarrow> (rv, f s') \<in> fst (m (f s))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m (f s)). snd (case x of (x, xa) \<Rightarrow> m' x xa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). (fst x, f (snd x)) \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). \<exists>s''. (fst x, s'') \<in> fst (m' rv s) \<and> snd x = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<forall>x\<in>fst (m (f s)). \<exists>s''. (fst x, s'') \<in> fst (m s) \<and> snd x = f s''; \<not> snd (m (f s)); \<not> snd (m s); (a, b) \<in> fst (m s); snd (m' a b); (a, f b) \<in> fst (m (f s))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m (f s)). snd (m' (fst x) (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). (fst x, f (snd x)) \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). \<exists>s''. (fst x, s'') \<in> fst (m' rv s) \<and> snd x = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<not> snd (m (f s)); \<not> snd (m s); (a, b) \<in> fst (m s); snd (m' a b); (a, f b) \<in> fst (m (f s)); \<exists>s''. (fst (a, f b), s'') \<in> fst (m s) \<and> snd (a, f b) = f s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m (f s)). snd (m' (fst x) (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. (\<forall>x\<in>fst (m' rv s). (fst x, f (snd x)) \<in> fst (m' rv (f s))) \<and> (\<forall>x\<in>fst (m' rv (f s)). \<exists>s''. (fst x, s'') \<in> fst (m' rv s) \<and> snd x = f s'') \<and> snd (m' rv (f s)) = snd (m' rv s); \<not> snd (m (f s)); \<not> snd (m s); (a, b) \<in> fst (m s); snd (m' a b); (a, f b) \<in> fst (m (f s)); \<exists>s''. (fst (a, f b), s'') \<in> fst (m s) \<and> snd (a, f b) = f s''\<rbrakk> \<Longrightarrow> snd (m' (fst (a, f b)) (snd (a, f b))) proof (prove)
goal:
No subgoals!