theory Detype_R

lemma curDomain_commute:
  assumes cur:"\<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>r s. P (ksCurDomain s)\<rbrace>"
  shows "monad_commute \<top> f curDomain" apply (clarsimp simp add:monad_commute_def curDomain_def get_def return_def
    gets_def bind_def) apply (rule conjI) apply (rule set_eqI) apply (rule iffI) apply clarsimp apply (rule bexI[rotated], assumption) apply clarsimp apply (frule_tac P1 = "\<lambda>x. x = ksCurDomain s" in use_valid[OF _ cur]) apply simp+ apply clarsimp apply (rule bexI[rotated], assumption) apply clarsimp apply (frule_tac P1 = "\<lambda>x. x = ksCurDomain s" in use_valid[OF _ cur]) apply simp+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) f curDomain proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) = (\<Union>a\<in>fst (f s). fst (case a of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<and> ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) = (\<Union>a\<in>fst (f s). fst (case a of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False)))
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x. (x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False)))) = (x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))))
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s x. x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False)))
 2. \<And>s x. x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False)))
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba. (a, ba) \<in> fst (f s) \<Longrightarrow> \<exists>x\<in>fst (f s). ((a, ksCurDomain ba), ba) \<in> fst (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))
 2. \<And>s x. x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False)))
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba. (a, ba) \<in> fst (f s) \<Longrightarrow> ((a, ksCurDomain ba), ba) \<in> fst (case (a, ba) of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))
 2. \<And>s x. x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False)))
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba. (a, ba) \<in> fst (f s) \<Longrightarrow> ksCurDomain ba = ksCurDomain s
 2. \<And>s x. x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False)))
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (4 subgoals):
 1. \<And>s a ba. (a, ba) \<in> fst (f s) \<Longrightarrow> ksCurDomain s = ksCurDomain s
 2. \<And>s a ba. \<lbrakk>(a, ba) \<in> fst (f s); ksCurDomain ba = ksCurDomain s\<rbrakk> \<Longrightarrow> ksCurDomain ba = ksCurDomain s
 3. \<And>s x. x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False)))
 4. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<exists>xa\<in>fst (f s). x \<in> fst (case xa of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False)) \<Longrightarrow> \<exists>xa\<in>fst (f s). x \<in> fst (case xa of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba. (a, ba) \<in> fst (f s) \<Longrightarrow> \<exists>x\<in>fst (f s). ((a, ksCurDomain s), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba. (a, ba) \<in> fst (f s) \<Longrightarrow> ((a, ksCurDomain s), ba) \<in> fst (case (a, ba) of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba. (a, ba) \<in> fst (f s) \<Longrightarrow> ksCurDomain s = ksCurDomain ba
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba. (a, ba) \<in> fst (f s) \<Longrightarrow> ksCurDomain s = ksCurDomain s
 2. \<And>s a ba. \<lbrakk>(a, ba) \<in> fst (f s); ksCurDomain ba = ksCurDomain s\<rbrakk> \<Longrightarrow> ksCurDomain s = ksCurDomain ba
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> ({((x, ksCurDomain s), s)}, False))) \<or> snd (f s)) = ((\<exists>x\<in>fst (f s). snd (case x of (x, sa) \<Rightarrow> ({((x, ksCurDomain s), sa)}, False))) \<or> snd (f s)) proof (prove)
goal:
No subgoals!