theory SubMonadLib

lemma is_stateAssert_gets:
  "\<lbrakk> \<forall>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; \<lbrace>\<top>\<rbrace> f \<lbrace>\<lambda>_. guard\<rbrace>;
     empty_fail f; no_fail guard f; \<lbrace>guard\<rbrace> f \<lbrace>\<lambda>rv s. fetch s = rv\<rbrace> \<rbrakk>
    \<Longrightarrow> f = do stateAssert guard []; gets fetch od" apply (rule ext) apply (clarsimp simp: bind_def empty_fail_def valid_def no_fail_def
                        stateAssert_def assert_def gets_def get_def
                        return_def fail_def image_def split_def) apply (case_tac "f x") apply (intro conjI impI) apply (drule_tac x=x in spec)+ apply (subgoal_tac "\<forall>xa\<in>fst (f x). fst xa = fetch x \<and> snd xa = x") apply fastforce apply clarsimp apply (drule_tac x=x in spec)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; \<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>\<lambda>_. guard\<rbrace>; empty_fail f; no_fail guard f; \<lbrace>guard\<rbrace> f \<lbrace>\<lambda>rv s. fetch s = rv\<rbrace>\<rbrakk> \<Longrightarrow> f = do stateAssert guard [];
gets fetch
od proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; \<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>\<lambda>_. guard\<rbrace>; empty_fail f; no_fail guard f; \<lbrace>guard\<rbrace> f \<lbrace>\<lambda>rv s. fetch s = rv\<rbrace>\<rbrakk> \<Longrightarrow> f x = (do stateAssert guard [];
gets fetch
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. \<forall>x\<in>fst (f s). s = snd x; \<forall>s. (\<exists>a b. (a, b) \<in> fst (f s)) \<longrightarrow> guard s; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); \<forall>s. guard s \<longrightarrow> (\<forall>x\<in>fst (f s). fetch s = fst x)\<rbrakk> \<Longrightarrow> (guard x \<longrightarrow> f x = ({(fetch x, x)}, False)) \<and> (\<not> guard x \<longrightarrow> f x = ({}, True)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>\<forall>s. \<forall>x\<in>fst (f s). s = snd x; \<forall>s. (\<exists>a b. (a, b) \<in> fst (f s)) \<longrightarrow> guard s; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); \<forall>s. guard s \<longrightarrow> (\<forall>x\<in>fst (f s). fetch s = fst x); f x = (a, b)\<rbrakk> \<Longrightarrow> (guard x \<longrightarrow> f x = ({(fetch x, x)}, False)) \<and> (\<not> guard x \<longrightarrow> f x = ({}, True)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>\<forall>s. \<forall>x\<in>fst (f s). s = snd x; \<forall>s. (\<exists>a b. (a, b) \<in> fst (f s)) \<longrightarrow> guard s; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); \<forall>s. guard s \<longrightarrow> (\<forall>x\<in>fst (f s). fetch s = fst x); f x = (a, b); guard x\<rbrakk> \<Longrightarrow> f x = ({(fetch x, x)}, False)
 2. \<And>x a b. \<lbrakk>\<forall>s. \<forall>x\<in>fst (f s). s = snd x; \<forall>s. (\<exists>a b. (a, b) \<in> fst (f s)) \<longrightarrow> guard s; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); \<forall>s. guard s \<longrightarrow> (\<forall>x\<in>fst (f s). fetch s = fst x); f x = (a, b); \<not> guard x\<rbrakk> \<Longrightarrow> f x = ({}, True) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>f x = (a, b); guard x; \<forall>xa\<in>fst (f x). x = snd xa; (\<exists>a b. (a, b) \<in> fst (f x)) \<longrightarrow> guard x; fst (f x) = {} \<longrightarrow> snd (f x); guard x \<longrightarrow> \<not> snd (f x); guard x \<longrightarrow> (\<forall>xa\<in>fst (f x). fetch x = fst xa)\<rbrakk> \<Longrightarrow> f x = ({(fetch x, x)}, False)
 2. \<And>x a b. \<lbrakk>\<forall>s. \<forall>x\<in>fst (f s). s = snd x; \<forall>s. (\<exists>a b. (a, b) \<in> fst (f s)) \<longrightarrow> guard s; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); \<forall>s. guard s \<longrightarrow> (\<forall>x\<in>fst (f s). fetch s = fst x); f x = (a, b); \<not> guard x\<rbrakk> \<Longrightarrow> f x = ({}, True) proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>f x = (a, b); guard x; \<forall>xa\<in>fst (f x). x = snd xa; (\<exists>a b. (a, b) \<in> fst (f x)) \<longrightarrow> guard x; fst (f x) = {} \<longrightarrow> snd (f x); guard x \<longrightarrow> \<not> snd (f x); guard x \<longrightarrow> (\<forall>xa\<in>fst (f x). fetch x = fst xa); \<forall>xa\<in>fst (f x). fst xa = fetch x \<and> snd xa = x\<rbrakk> \<Longrightarrow> f x = ({(fetch x, x)}, False)
 2. \<And>x a b. \<lbrakk>f x = (a, b); guard x; \<forall>xa\<in>fst (f x). x = snd xa; (\<exists>a b. (a, b) \<in> fst (f x)) \<longrightarrow> guard x; fst (f x) = {} \<longrightarrow> snd (f x); guard x \<longrightarrow> \<not> snd (f x); guard x \<longrightarrow> (\<forall>xa\<in>fst (f x). fetch x = fst xa)\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (f x). fst xa = fetch x \<and> snd xa = x
 3. \<And>x a b. \<lbrakk>\<forall>s. \<forall>x\<in>fst (f s). s = snd x; \<forall>s. (\<exists>a b. (a, b) \<in> fst (f s)) \<longrightarrow> guard s; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); \<forall>s. guard s \<longrightarrow> (\<forall>x\<in>fst (f s). fetch s = fst x); f x = (a, b); \<not> guard x\<rbrakk> \<Longrightarrow> f x = ({}, True) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>f x = (a, b); guard x; \<forall>xa\<in>fst (f x). x = snd xa; (\<exists>a b. (a, b) \<in> fst (f x)) \<longrightarrow> guard x; fst (f x) = {} \<longrightarrow> snd (f x); guard x \<longrightarrow> \<not> snd (f x); guard x \<longrightarrow> (\<forall>xa\<in>fst (f x). fetch x = fst xa)\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (f x). fst xa = fetch x \<and> snd xa = x
 2. \<And>x a b. \<lbrakk>\<forall>s. \<forall>x\<in>fst (f s). s = snd x; \<forall>s. (\<exists>a b. (a, b) \<in> fst (f s)) \<longrightarrow> guard s; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); \<forall>s. guard s \<longrightarrow> (\<forall>x\<in>fst (f s). fetch s = fst x); f x = (a, b); \<not> guard x\<rbrakk> \<Longrightarrow> f x = ({}, True) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>\<forall>s. \<forall>x\<in>fst (f s). s = snd x; \<forall>s. (\<exists>a b. (a, b) \<in> fst (f s)) \<longrightarrow> guard s; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); \<forall>s. guard s \<longrightarrow> (\<forall>x\<in>fst (f s). fetch s = fst x); f x = (a, b); \<not> guard x\<rbrakk> \<Longrightarrow> f x = ({}, True) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>f x = (a, b); \<not> guard x; \<forall>xa\<in>fst (f x). x = snd xa; (\<exists>a b. (a, b) \<in> fst (f x)) \<longrightarrow> guard x; fst (f x) = {} \<longrightarrow> snd (f x); guard x \<longrightarrow> \<not> snd (f x); guard x \<longrightarrow> (\<forall>xa\<in>fst (f x). fetch x = fst xa)\<rbrakk> \<Longrightarrow> f x = ({}, True) proof (prove)
goal:
No subgoals!