theory Decode_IF

lemma no_state_changes:
  "(\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> f = (do s \<leftarrow> get; (rv,s') \<leftarrow> select_f (f s); return rv od)" apply (simp add: get_def select_f_def return_def bind_def) apply (rule ext) apply (subgoal_tac "\<forall>r s'. (r,s') \<in> fst (f s) \<longrightarrow> s' = s") defer apply clarsimp apply (rule use_valid,assumption+) apply simp apply (case_tac "f s") apply clarsimp apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> f = do s <- get;
(rv, s') <- select_f (f s);
return rv
od proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> f = (\<lambda>s. (\<Union>a\<in>fst (f s) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) xa), (\<exists>x\<in>fst (f s). snd ((case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) s)) \<or> snd (f s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> f s = (\<Union>a\<in>fst (f s) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) xa), (\<exists>x\<in>fst (f s). snd ((case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) s)) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<forall>r s'. (r, s') \<in> fst (f s) \<longrightarrow> s' = s\<rbrakk> \<Longrightarrow> f s = (\<Union>a\<in>fst (f s) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) xa), (\<exists>x\<in>fst (f s). snd ((case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) s)) \<or> snd (f s))
 2. \<And>s. (\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> \<forall>r s'. (r, s') \<in> fst (f s) \<longrightarrow> s' = s proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> \<forall>r s'. (r, s') \<in> fst (f s) \<longrightarrow> s' = s
 2. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<forall>r s'. (r, s') \<in> fst (f s) \<longrightarrow> s' = s\<rbrakk> \<Longrightarrow> f s = (\<Union>a\<in>fst (f s) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) xa), (\<exists>x\<in>fst (f s). snd ((case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) s)) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s r s'. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; (r, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> s' = s
 2. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<forall>r s'. (r, s') \<in> fst (f s) \<longrightarrow> s' = s\<rbrakk> \<Longrightarrow> f s = (\<Union>a\<in>fst (f s) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) xa), (\<exists>x\<in>fst (f s). snd ((case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) s)) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s r s'. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; (r, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> s = s
 2. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<forall>r s'. (r, s') \<in> fst (f s) \<longrightarrow> s' = s\<rbrakk> \<Longrightarrow> f s = (\<Union>a\<in>fst (f s) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) xa), (\<exists>x\<in>fst (f s). snd ((case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) s)) \<or> snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<forall>r s'. (r, s') \<in> fst (f s) \<longrightarrow> s' = s\<rbrakk> \<Longrightarrow> f s = (\<Union>a\<in>fst (f s) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) xa), (\<exists>x\<in>fst (f s). snd ((case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) s)) \<or> snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<forall>r s'. (r, s') \<in> fst (f s) \<longrightarrow> s' = s; f s = (a, b)\<rbrakk> \<Longrightarrow> f s = (\<Union>a\<in>fst (f s) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) xa), (\<exists>x\<in>fst (f s). snd ((case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) s)) \<or> snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<forall>r s'. (r, s') \<in> a \<longrightarrow> s' = s; f s = (a, b)\<rbrakk> \<Longrightarrow> a = (\<Union>x\<in>a \<times> {s}. fst (case x of (x, xa) \<Rightarrow> (case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) xa)) \<and> b = ((\<exists>x\<in>a. snd ((case x of (rv, s') \<Rightarrow> \<lambda>s. ({(rv, s)}, False)) s)) \<or> b) proof (prove)
goal:
No subgoals!