theory CNode_AC

lemma modify_get_commute:
  "(\<And>s0. \<lbrace>(=) s0\<rbrace> g \<lbrace>\<lambda>r t. s0 = t\<rbrace>)
   \<Longrightarrow> monad_commute (\<lambda>s. fst ` fst (g (f s)) = fst ` fst (g s) \<and>
                          snd (g (f s)) = snd (g s)) (modify f) g" 
  (* FIXME: proof cleanup *)
   apply (monad_eq simp: monad_commute_def valid_def
                        set_eq_iff_imp[where A="fst ` fst _"] image_iff) apply atomize apply (intro conjI; clarsimp) apply (rename_tac s0 r t) apply (clarsimp split: prod.splits) apply (rule_tac x=s0 in exI) apply (rule conjI) apply (drule_tac x=s0 in spec) apply fastforce apply fastforce apply (rename_tac s0 r t) apply (clarsimp split: prod.splits) apply (subgoal_tac "t = s0") apply (drule_tac x="f t" in spec) apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s0. \<lbrace>(=) s0\<rbrace> g \<lbrace>\<lambda>r. (=) s0\<rbrace>) \<Longrightarrow> monad_commute (\<lambda>s. fst ` fst (g (f s)) = fst ` fst (g s) \<and> snd (g (f s)) = snd (g s)) (modify f) g proof (prove)
goal (1 subgoal):
 1. (\<And>s0. \<lbrace>(=) s0\<rbrace> g \<lbrace>\<lambda>r. (=) s0\<rbrace>) \<Longrightarrow> monad_commute (\<lambda>s. fst ` fst (g (f s)) = fst ` fst (g s) \<and> snd (g (f s)) = snd (g s)) (modify f) g proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s)\<rbrakk> \<Longrightarrow> (\<forall>b t. (b, t) \<in> fst (g (f s)) \<longrightarrow> (\<exists>ba. (b, ba) \<in> fst (g s) \<and> t = f ba)) \<and> (\<forall>b t. (\<exists>ba. (b, ba) \<in> fst (g s) \<and> t = f ba) \<longrightarrow> (b, t) \<in> fst (g (f s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s0. \<forall>(r, y)\<in>fst (g s0). s0 = y; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s)\<rbrakk> \<Longrightarrow> (\<forall>b t. (b, t) \<in> fst (g (f s)) \<longrightarrow> (\<exists>ba. (b, ba) \<in> fst (g s) \<and> t = f ba)) \<and> (\<forall>b t. (\<exists>ba. (b, ba) \<in> fst (g s) \<and> t = f ba) \<longrightarrow> (b, t) \<in> fst (g (f s))) proof (prove)
goal (2 subgoals):
 1. \<And>s b t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s); (b, t) \<in> fst (g (f s))\<rbrakk> \<Longrightarrow> \<exists>ba. (b, ba) \<in> fst (g s) \<and> t = f ba
 2. \<And>s b ba. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s); (b, ba) \<in> fst (g s)\<rbrakk> \<Longrightarrow> (b, f ba) \<in> fst (g (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g (f s0))\<rbrakk> \<Longrightarrow> \<exists>b. (r, b) \<in> fst (g s0) \<and> t = f b
 2. \<And>s b ba. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s); (b, ba) \<in> fst (g s)\<rbrakk> \<Longrightarrow> (b, f ba) \<in> fst (g (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g (f s0))\<rbrakk> \<Longrightarrow> \<exists>b. (r, b) \<in> fst (g s0) \<and> t = f b
 2. \<And>s b ba. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s); (b, ba) \<in> fst (g s)\<rbrakk> \<Longrightarrow> (b, f ba) \<in> fst (g (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g (f s0))\<rbrakk> \<Longrightarrow> (r, s0) \<in> fst (g s0) \<and> t = f s0
 2. \<And>s b ba. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s); (b, ba) \<in> fst (g s)\<rbrakk> \<Longrightarrow> (b, f ba) \<in> fst (g (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g (f s0))\<rbrakk> \<Longrightarrow> (r, s0) \<in> fst (g s0)
 2. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g (f s0))\<rbrakk> \<Longrightarrow> t = f s0
 3. \<And>s b ba. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s); (b, ba) \<in> fst (g s)\<rbrakk> \<Longrightarrow> (b, f ba) \<in> fst (g (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s0 r t. \<lbrakk>\<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g (f s0)); \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2\<rbrakk> \<Longrightarrow> (r, s0) \<in> fst (g s0)
 2. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g (f s0))\<rbrakk> \<Longrightarrow> t = f s0
 3. \<And>s b ba. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s); (b, ba) \<in> fst (g s)\<rbrakk> \<Longrightarrow> (b, f ba) \<in> fst (g (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g (f s0))\<rbrakk> \<Longrightarrow> t = f s0
 2. \<And>s b ba. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s); (b, ba) \<in> fst (g s)\<rbrakk> \<Longrightarrow> (b, f ba) \<in> fst (g (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s b ba. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s)). x = fst xa); snd (g (f s)) = snd (g s); (b, ba) \<in> fst (g s)\<rbrakk> \<Longrightarrow> (b, f ba) \<in> fst (g (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). case x of (r, x) \<Rightarrow> s0 = x; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g s0)\<rbrakk> \<Longrightarrow> (r, f t) \<in> fst (g (f s0)) proof (prove)
goal (1 subgoal):
 1. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g s0)\<rbrakk> \<Longrightarrow> (r, f t) \<in> fst (g (f s0)) proof (prove)
goal (2 subgoals):
 1. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g s0); t = s0\<rbrakk> \<Longrightarrow> (r, f t) \<in> fst (g (f s0))
 2. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g s0)\<rbrakk> \<Longrightarrow> t = s0 proof (prove)
goal (2 subgoals):
 1. \<And>s0 r t. \<lbrakk>\<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g s0); t = s0; \<forall>x\<in>fst (g (f t)). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> f t = x2\<rbrakk> \<Longrightarrow> (r, f t) \<in> fst (g (f s0))
 2. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g s0)\<rbrakk> \<Longrightarrow> t = s0 proof (prove)
goal (1 subgoal):
 1. \<And>s0 r t. \<lbrakk>\<forall>s0. \<forall>x\<in>fst (g s0). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> s0 = x2; \<forall>x. (\<exists>xa\<in>fst (g (f s0)). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g s0). x = fst xa); \<forall>x. (\<exists>xa\<in>fst (g s0). x = fst xa) \<longrightarrow> (\<exists>xa\<in>fst (g (f s0)). x = fst xa); snd (g (f s0)) = snd (g s0); (r, t) \<in> fst (g s0)\<rbrakk> \<Longrightarrow> t = s0 proof (prove)
goal:
No subgoals!