theory StateTranslation_D

lemma evalMonad_bind:
  assumes f: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  assumes det: "det_or_fail f"
  shows "evalMonad (f >>= g) s = (if evalMonad f s = None then None else evalMonad (g (the (evalMonad f s))) s)" apply (case_tac "evalMonad f s") apply (simp add: evalMonad_def split: if_split_asm) apply (simp add: bind_def) apply simp apply (simp add: evalMonad_def) apply (clarsimp simp: bind_def) apply (insert det) apply (clarsimp simp: det_or_fail_def split: if_split_asm) apply (erule_tac x=s in allE) apply clarsimp apply (subgoal_tac "b = s") apply simp apply (subgoal_tac "(a,b) \<in> fst (f s)") apply (drule use_valid, rule f [where P="(=) s"]) apply (rule refl) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (f >>= g) s = (if evalMonad f s = None then None else evalMonad (g (the (evalMonad f s))) s) proof (prove)
goal (2 subgoals):
 1. evalMonad f s = None \<Longrightarrow> evalMonad (f >>= g) s = (if evalMonad f s = None then None else evalMonad (g (the (evalMonad f s))) s)
 2. \<And>a. evalMonad f s = Some a \<Longrightarrow> evalMonad (f >>= g) s = (if evalMonad f s = None then None else evalMonad (g (the (evalMonad f s))) s) proof (prove)
goal (2 subgoals):
 1. fst (f s) = {} \<Longrightarrow> fst ((f >>= g) s) = {}
 2. \<And>a. evalMonad f s = Some a \<Longrightarrow> evalMonad (f >>= g) s = (if evalMonad f s = None then None else evalMonad (g (the (evalMonad f s))) s) proof (prove)
goal (1 subgoal):
 1. \<And>a. evalMonad f s = Some a \<Longrightarrow> evalMonad (f >>= g) s = (if evalMonad f s = None then None else evalMonad (g (the (evalMonad f s))) s) proof (prove)
goal (1 subgoal):
 1. \<And>a. evalMonad f s = Some a \<Longrightarrow> evalMonad (f >>= g) s = evalMonad (g a) s proof (prove)
goal (1 subgoal):
 1. \<And>a. (if fst (f s) = {} then None else Some (pick (fst ` fst (f s)))) = Some a \<Longrightarrow> (fst ((f >>= g) s) = {} \<longrightarrow> fst (g a s) = {}) \<and> (fst ((f >>= g) s) \<noteq> {} \<longrightarrow> fst (g a s) \<noteq> {} \<and> (fst (g a s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((f >>= g) s)) = pick (fst ` fst (g a s)))) proof (prove)
goal (1 subgoal):
 1. \<And>a. (if fst (f s) = {} then None else Some (pick (fst ` fst (f s)))) = Some a \<Longrightarrow> ((\<forall>x\<in>fst (f s). fst (case x of (x, xa) \<Rightarrow> g x xa) = {}) \<longrightarrow> fst (g a s) = {}) \<and> ((\<exists>x\<in>fst (f s). fst (case x of (x, xa) \<Rightarrow> g x xa) \<noteq> {}) \<longrightarrow> fst (g a s) \<noteq> {} \<and> (fst (g a s) \<noteq> {} \<longrightarrow> pick (fst ` (\<Union>a\<in>fst (f s). fst (case a of (x, xa) \<Rightarrow> g x xa))) = pick (fst ` fst (g a s)))) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(if fst (f s) = {} then None else Some (pick (fst ` fst (f s)))) = Some a; det_or_fail f\<rbrakk> \<Longrightarrow> ((\<forall>x\<in>fst (f s). fst (case x of (x, xa) \<Rightarrow> g x xa) = {}) \<longrightarrow> fst (g a s) = {}) \<and> ((\<exists>x\<in>fst (f s). fst (case x of (x, xa) \<Rightarrow> g x xa) \<noteq> {}) \<longrightarrow> fst (g a s) \<noteq> {} \<and> (fst (g a s) \<noteq> {} \<longrightarrow> pick (fst ` (\<Union>a\<in>fst (f s). fst (case a of (x, xa) \<Rightarrow> g x xa))) = pick (fst ` fst (g a s)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. fst (f s) = {} \<or> (\<exists>a b. fst (f s) = {(a, b)}); fst (f s) \<noteq> {}\<rbrakk> \<Longrightarrow> ((\<forall>x\<in>fst (f s). fst (case x of (x, xa) \<Rightarrow> g x xa) = {}) \<longrightarrow> fst (g (pick (fst ` fst (f s))) s) = {}) \<and> ((\<exists>x\<in>fst (f s). fst (case x of (x, xa) \<Rightarrow> g x xa) \<noteq> {}) \<longrightarrow> fst (g (pick (fst ` fst (f s))) s) \<noteq> {} \<and> (fst (g (pick (fst ` fst (f s))) s) \<noteq> {} \<longrightarrow> pick (fst ` (\<Union>a\<in>fst (f s). fst (case a of (x, xa) \<Rightarrow> g x xa))) = pick (fst ` fst (g (pick (fst ` fst (f s))) s)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (f s) \<noteq> {}; fst (f s) = {} \<or> (\<exists>a b. fst (f s) = {(a, b)})\<rbrakk> \<Longrightarrow> ((\<forall>x\<in>fst (f s). fst (case x of (x, xa) \<Rightarrow> g x xa) = {}) \<longrightarrow> fst (g (pick (fst ` fst (f s))) s) = {}) \<and> ((\<exists>x\<in>fst (f s). fst (case x of (x, xa) \<Rightarrow> g x xa) \<noteq> {}) \<longrightarrow> fst (g (pick (fst ` fst (f s))) s) \<noteq> {} \<and> (fst (g (pick (fst ` fst (f s))) s) \<noteq> {} \<longrightarrow> pick (fst ` (\<Union>a\<in>fst (f s). fst (case a of (x, xa) \<Rightarrow> g x xa))) = pick (fst ` fst (g (pick (fst ` fst (f s))) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> (fst (g a b) = {} \<longrightarrow> fst (g a s) = {}) \<and> (fst (g a b) \<noteq> {} \<longrightarrow> fst (g a s) \<noteq> {} \<and> (fst (g a s) \<noteq> {} \<longrightarrow> pick (fst ` fst (g a b)) = pick (fst ` fst (g a s)))) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>fst (f s) = {(a, b)}; b = s\<rbrakk> \<Longrightarrow> (fst (g a b) = {} \<longrightarrow> fst (g a s) = {}) \<and> (fst (g a b) \<noteq> {} \<longrightarrow> fst (g a s) \<noteq> {} \<and> (fst (g a s) \<noteq> {} \<longrightarrow> pick (fst ` fst (g a b)) = pick (fst ` fst (g a s))))
 2. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> b = s proof (prove)
goal (1 subgoal):
 1. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> b = s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>fst (f s) = {(a, b)}; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> b = s
 2. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> (a, b) \<in> fst (f s) proof (prove)
goal (3 subgoals):
 1. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> s = s
 2. \<And>a b. \<lbrakk>fst (f s) = {(a, b)}; s = b\<rbrakk> \<Longrightarrow> b = s
 3. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> (a, b) \<in> fst (f s) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>fst (f s) = {(a, b)}; s = b\<rbrakk> \<Longrightarrow> b = s
 2. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> (a, b) \<in> fst (f s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> (a, b) \<in> fst (f s) proof (prove)
goal:
No subgoals!