kings-crown/FVELER_Isabelle huggingface dataset:
theory Hoare_Sep_Tactics

lemma extract_exists: "((\<lambda>s. \<exists>x. (P x) s) \<and>* R) s \<Longrightarrow> \<exists>x. (P x \<and>*  R) s" apply (clarsimp simp: sep_conj_def, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. \<exists>x. P x s) \<and>* R) s \<Longrightarrow> \<exists>x. (P x \<and>* R) s proof (prove)
goal:
No subgoals!
theory Hoare_Sep_Tactics

lemma extract_all: "((\<lambda>s. \<forall>x. (P x) s) \<and>* R) s \<Longrightarrow> \<forall>x. (P x \<and>*  R) s" apply (clarsimp simp: sep_conj_def, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. \<forall>x. P x s) \<and>* R) s \<Longrightarrow> \<forall>x. (P x \<and>* R) s proof (prove)
goal:
No subgoals!
theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wp'':
    "\<And>sep_lift.
     (\<And>R. \<lbrace>(\<lambda>s. (P \<and>* R x) (sep_lift s) )\<rbrace> f \<lbrace>\<lambda>rv. (\<lambda>s. (Q rv \<and>* R rv) (sep_lift s))\<rbrace>) \<Longrightarrow>
     \<lbrace>(\<lambda>s. ( P \<and>* (Q x \<longrightarrow>* R x)) (sep_lift s))\<rbrace> f \<lbrace>\<lambda>rv s . R rv (sep_lift s)\<rbrace>" apply (atomize) apply (erule_tac x="(\<lambda>x. (Q x \<longrightarrow>* R x))" in allE) apply (rule hoare_strengthen_post) apply (assumption) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. (\<And>R. \<lbrace>\<lambda>s. (P \<and>* R x) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv \<and>* R rv) (sep_lift s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q x \<longrightarrow>* R x)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. R rv (sep_lift s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. \<forall>R. \<lbrace>\<lambda>s. (P \<and>* R x) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv \<and>* R rv) (sep_lift s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q x \<longrightarrow>* R x)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. R rv (sep_lift s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. \<lbrace>\<lambda>s. (P \<and>* (Q x \<longrightarrow>* R x)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv \<and>* (Q rv \<longrightarrow>* R rv)) (sep_lift s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q x \<longrightarrow>* R x)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. R rv (sep_lift s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift. \<lbrace>\<lambda>s. (P \<and>* (Q x \<longrightarrow>* R x)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv \<and>* (Q rv \<longrightarrow>* R rv)) (sep_lift s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q x \<longrightarrow>* R x)) (sep_lift s)\<rbrace> f \<lbrace>?Q1 sep_lift\<rbrace>
 2. \<And>sep_lift rv s. \<lbrakk>\<lbrace>\<lambda>s. (P \<and>* (Q x \<longrightarrow>* R x)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv \<and>* (Q rv \<longrightarrow>* R rv)) (sep_lift s)\<rbrace>; ?Q1 sep_lift rv s\<rbrakk> \<Longrightarrow> R rv (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s. \<lbrakk>\<lbrace>\<lambda>s. (P \<and>* (Q x \<longrightarrow>* R x)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv \<and>* (Q rv \<longrightarrow>* R rv)) (sep_lift s)\<rbrace>; (Q rv \<and>* (Q rv \<longrightarrow>* R rv)) (sep_lift s)\<rbrakk> \<Longrightarrow> R rv (sep_lift s) proof (prove)
goal:
No subgoals!
theory Hoare_Sep_Tactics

lemma auto_wp:"\<lbrace>P \<rbrace> f \<lbrace>Q \<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s.  P s \<and> (\<forall>s x. Q x s \<longrightarrow> R x s)\<rbrace> f \<lbrace>R\<rbrace>" by (clarsimp simp: valid_def split:prod.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> (\<forall>s x. Q x s \<longrightarrow> R x s)\<rbrace> f \<lbrace>R\<rbrace>
theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wp_rv':
    "\<And>sep_lift.
     (\<And>R. \<lbrace>(\<lambda>s. ((P \<and>* R) and K(p')) (sep_lift s) )\<rbrace> f \<lbrace>\<lambda>x. (\<lambda>s. (Q x \<and>* R) (sep_lift s))\<rbrace>) \<Longrightarrow>
     \<lbrace>(\<lambda>s. (( P \<and>* (\<lambda>s. \<forall>x. (Q x  \<longrightarrow>* R x) s )) and K(p') )(sep_lift s))\<rbrace> f \<lbrace>\<lambda>rv s . (R rv) (sep_lift s)\<rbrace>" apply (rule hoare_chain, assumption) apply (sep_solve) apply (sep_select_asm 2, erule sep_conj_sep_impl2) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. (\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R) (sep_lift s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (\<lambda>s. \<forall>x. (Q x \<longrightarrow>* R x) s) and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. R rv (sep_lift s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P \<and>* (\<lambda>s. \<forall>x. (Q x \<longrightarrow>* R x) s) and K p') (sep_lift s)\<rbrakk> \<Longrightarrow> (P \<and>* ?R13 sep_lift and K p') (sep_lift s)
 2. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (Q rv \<and>* ?R13 sep_lift) (sep_lift s)\<rbrakk> \<Longrightarrow> R rv (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (Q rv \<and>* (\<lambda>s. \<forall>x. (Q x \<longrightarrow>* R x) s)) (sep_lift s)\<rbrakk> \<Longrightarrow> R rv (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s h. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R) (sep_lift s)\<rbrace>; \<forall>x. (Q x \<longrightarrow>* R x) h\<rbrakk> \<Longrightarrow> (Q rv \<longrightarrow>* R rv) h proof (prove)
goal:
No subgoals!
theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wp_rv'':
    "\<And>sep_lift.
     (\<And>R. \<lbrace>(\<lambda>s. ((P \<and>* R)) (sep_lift s) )\<rbrace> f \<lbrace>\<lambda>x. (\<lambda>s. ((Q x \<and>* R) and K (p'' x)) (sep_lift s))\<rbrace>) \<Longrightarrow>
     \<lbrace>(\<lambda>s. (( P \<and>* (\<lambda>s. \<forall>x. p'' x \<longrightarrow> (Q x  \<longrightarrow>* R x) s )))(sep_lift s))\<rbrace> f \<lbrace>\<lambda>rv s . (R rv) (sep_lift s)\<rbrace>" apply (rule hoare_chain, assumption) apply (sep_solve) apply (clarsimp) apply (sep_select_asm 2, erule sep_conj_sep_impl2) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. (\<And>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R and K (p'' x)) (sep_lift s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (\<lambda>s. \<forall>x. p'' x \<longrightarrow> (Q x \<longrightarrow>* R x) s)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. R rv (sep_lift s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R and K (p'' x)) (sep_lift s)\<rbrace>; (P \<and>* (\<lambda>s. \<forall>x. p'' x \<longrightarrow> (Q x \<longrightarrow>* R x) s)) (sep_lift s)\<rbrakk> \<Longrightarrow> (P \<and>* ?R13 sep_lift) (sep_lift s)
 2. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R and K (p'' x)) (sep_lift s)\<rbrace>; (Q rv \<and>* ?R13 sep_lift and K (p'' rv)) (sep_lift s)\<rbrakk> \<Longrightarrow> R rv (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R and K (p'' x)) (sep_lift s)\<rbrace>; (Q rv \<and>* (\<lambda>s. \<forall>x. p'' x \<longrightarrow> (Q x \<longrightarrow>* R x) s) and K (p'' rv)) (sep_lift s)\<rbrakk> \<Longrightarrow> R rv (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R) (sep_lift s) \<and> p'' x\<rbrace>; (Q rv \<and>* (\<lambda>s. \<forall>x. p'' x \<longrightarrow> (Q x \<longrightarrow>* R x) s)) (sep_lift s); p'' rv\<rbrakk> \<Longrightarrow> R rv (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s h. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. (Q x \<and>* R) (sep_lift s) \<and> p'' x\<rbrace>; p'' rv; \<forall>x. p'' x \<longrightarrow> (Q x \<longrightarrow>* R x) h\<rbrakk> \<Longrightarrow> (Q rv \<longrightarrow>* R rv) h proof (prove)
goal:
No subgoals!
theory Hoare_Sep_Tactics

lemma boxsolve: "P s \<Longrightarrow> (\<box> \<and>* (\<box> \<longrightarrow>* P)) s" apply (clarsimp) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> (\<box> \<and>* (\<box> \<longrightarrow>* P)) s proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> (\<box> \<longrightarrow>* P) s proof (prove)
goal:
No subgoals!
theory Hoare_Sep_Tactics

lemma shift_inside_left:
  "\<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s) \<and> A\<rbrace> f \<lbrace>R'\<rbrace> \<longleftrightarrow> \<lbrace>\<lambda>s. ((P and K A) \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>R'\<rbrace>" apply (clarsimp simp: pred_conj_def conj_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s) \<and> A\<rbrace> f \<lbrace>R'\<rbrace> = \<lbrace>\<lambda>s. ((P and K A) \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>R'\<rbrace> proof (prove)
goal:
No subgoals!
theory Hoare_Sep_Tactics

lemma shift_inside_right:
  "\<lbrace>\<lambda>s. A \<and> (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>R'\<rbrace> \<longleftrightarrow> \<lbrace>\<lambda>s. ((P and K A) \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>R'\<rbrace>" apply (clarsimp simp: pred_conj_def conj_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. A \<and> (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>R'\<rbrace> = \<lbrace>\<lambda>s. ((P and K A) \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>R'\<rbrace> proof (prove)
goal:
No subgoals!
theory MonadSep

lemma hoare_gen_lifted_asm:
  "(P \<Longrightarrow> \<lbrace>\<lambda>s. P' (lft s)\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. (P' and K P) (lft s)\<rbrace> f \<lbrace>Q\<rbrace>" by (auto intro: hoare_assume_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace><P'>\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace><P' and K P>\<rbrace> f \<lbrace>Q\<rbrace>
theory MonadSep

lemma mapM_x_set_sep_inv:
  "\<lbrakk>distinct xs; set xs = X; (\<And>R x. x \<in> X \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R> and I'\<rbrace> f x \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R> and I'\<rbrace>)\<rbrakk> \<Longrightarrow>
  \<lbrace><(\<And>* x \<in> X. P x) \<and>* I \<and>* R> and I'\<rbrace> mapM_x f xs \<lbrace>\<lambda>_. <(\<And>* x \<in> X. Q x) \<and>* I \<and>* R> and I'\<rbrace>" apply (clarsimp simp: pred_conj_def) apply (drule mapM_x_sep_inv [where R=R]) apply (subst (asm) sep_list_conj_sep_map_set_conj, assumption)+ apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; set xs = X; \<And>R x. x \<in> X \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R> and I'\<rbrace> f x \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R> and I'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><sep_map_set_conj P X \<and>* I \<and>* R> and I'\<rbrace> mapM_x f xs \<lbrace>\<lambda>_. <sep_map_set_conj Q X \<and>* I \<and>* R> and I'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<And>R x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>xa. <P x \<and>* I \<and>* R> xa \<and> I' xa\<rbrace> f x \<lbrace>\<lambda>_ xa. <Q x \<and>* I \<and>* R> xa \<and> I' xa\<rbrace>; X = set xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. <sep_map_set_conj P (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ x. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; X = set xs; \<lbrace>\<lambda>x. <\<And>* map P xs \<and>* I \<and>* R> x \<and> I' x\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ x. <\<And>* map Q xs \<and>* I \<and>* R> x \<and> I' x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. <sep_map_set_conj P (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ x. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; X = set xs; \<lbrace>\<lambda>x. <sep_map_set_conj P (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ x. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. <sep_map_set_conj P (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ x. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> proof (prove)
goal:
No subgoals!
theory MonadSep

lemma mapM_x_set_sep:
  "\<lbrakk>distinct xs; \<And>R x. x \<in> set xs \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R>\<rbrace> f x \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R>\<rbrace>\<rbrakk>
 \<Longrightarrow> \<lbrace><(\<And>* x \<in> set xs. P x) \<and>* I \<and>* R>\<rbrace> mapM_x f xs \<lbrace>\<lambda>_. <(\<And>* x \<in> set xs. Q x) \<and>* I \<and>* R>\<rbrace>" by (erule mapM_x_set_sep', simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<And>R x. x \<in> set xs \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R>\<rbrace> f x \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><sep_map_set_conj P (set xs) \<and>* I \<and>* R>\<rbrace> mapM_x f xs \<lbrace>\<lambda>_. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R>\<rbrace>
theory MonadSep

lemma foldM_Cons:
  "foldM f (x # xs) acc =
    do acc' \<leftarrow> foldM f xs acc;
       f x acc'
    od" by (clarsimp simp: foldM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldM f (x # xs) acc = foldM f xs acc >>= f x
theory MonadSep

lemma foldM_set_sep_inv:
  "\<lbrakk>distinct xs;
    set xs = X;
    \<And>R x acc. x \<in> X \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R> and I'\<rbrace> f x acc \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R> and I'\<rbrace>\<rbrakk> \<Longrightarrow>
  \<lbrace><(\<And>* x \<in> X. P x) \<and>* I \<and>* R> and I'\<rbrace>
   foldM f xs acc
  \<lbrace>\<lambda>_. <(\<And>* x \<in> X. Q x) \<and>* I \<and>* R> and I'\<rbrace>" apply (clarsimp simp: pred_conj_def) apply (drule foldM_sep_inv [where R=R]) apply (subst (asm) sep_list_conj_sep_map_set_conj, assumption)+ apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; set xs = X; \<And>R x acc. x \<in> X \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R> and I'\<rbrace> f x acc \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R> and I'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><sep_map_set_conj P X \<and>* I \<and>* R> and I'\<rbrace> foldM f xs acc \<lbrace>\<lambda>_. <sep_map_set_conj Q X \<and>* I \<and>* R> and I'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<And>R x acc. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>xa. <P x \<and>* I \<and>* R> xa \<and> I' xa\<rbrace> f x acc \<lbrace>\<lambda>_ xa. <Q x \<and>* I \<and>* R> xa \<and> I' xa\<rbrace>; X = set xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. <sep_map_set_conj P (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> foldM f xs acc \<lbrace>\<lambda>_ x. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; X = set xs; \<lbrace>\<lambda>x. <\<And>* map P xs \<and>* I \<and>* R> x \<and> I' x\<rbrace> foldM f xs ?acc7 \<lbrace>\<lambda>_ x. <\<And>* map Q xs \<and>* I \<and>* R> x \<and> I' x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. <sep_map_set_conj P (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> foldM f xs acc \<lbrace>\<lambda>_ x. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; X = set xs; \<lbrace>\<lambda>x. <sep_map_set_conj P (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> foldM f xs ?acc7 \<lbrace>\<lambda>_ x. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. <sep_map_set_conj P (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> foldM f xs acc \<lbrace>\<lambda>_ x. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R> x \<and> I' x\<rbrace> proof (prove)
goal:
No subgoals!
theory MonadSep

lemma foldM_set_sep:
  "\<lbrakk>distinct xs;
    \<And>R x acc. x \<in> set xs \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R>\<rbrace> f x acc \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R>\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace><(\<And>* x \<in> set xs. P x) \<and>* I \<and>* R>\<rbrace> foldM f xs acc \<lbrace>\<lambda>_. <(\<And>* x \<in> set xs. Q x) \<and>* I \<and>* R>\<rbrace>" by (erule foldM_set_sep', simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<And>R x acc. x \<in> set xs \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R>\<rbrace> f x acc \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><sep_map_set_conj P (set xs) \<and>* I \<and>* R>\<rbrace> foldM f xs acc \<lbrace>\<lambda>_. <sep_map_set_conj Q (set xs) \<and>* I \<and>* R>\<rbrace>
theory MonadSep

lemma sep_set_conj_map_singleton_wp:
  "\<lbrakk>finite xs; x \<in> xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>\<rbrakk>
  \<Longrightarrow> \<lbrace><P \<and>* (\<And>* x\<in>xs. I x) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x\<in>xs. I x) \<and>* R>\<rbrace>" apply (rule hoare_chain [where P="<P \<and>* I x \<and>* (\<And>* x\<in>xs - {x}. I x) \<and>* R>" and
                                 Q="\<lambda>_. <Q \<and>* I x \<and>* (\<And>* x\<in>xs - {x}. I x) \<and>* R>"], assumption) apply (subst (asm) sep.prod.remove, assumption+) apply sep_solve apply (subst sep.prod.remove, assumption+) apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite xs; x \<in> xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* sep_map_set_conj I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* sep_map_set_conj I xs \<and>* R>\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>finite xs; x \<in> xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <P \<and>* sep_map_set_conj I xs \<and>* R> s\<rbrakk> \<Longrightarrow> <P \<and>* I x \<and>* sep_map_set_conj I (xs - {x}) \<and>* R> s
 2. \<And>rv s. \<lbrakk>finite xs; x \<in> xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <Q \<and>* I x \<and>* sep_map_set_conj I (xs - {x}) \<and>* R> s\<rbrakk> \<Longrightarrow> <Q \<and>* sep_map_set_conj I xs \<and>* R> s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>finite xs; x \<in> xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <P \<and>* (I x \<and>* sep_map_set_conj I (xs - {x})) \<and>* R> s\<rbrakk> \<Longrightarrow> <P \<and>* I x \<and>* sep_map_set_conj I (xs - {x}) \<and>* R> s
 2. \<And>rv s. \<lbrakk>finite xs; x \<in> xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <Q \<and>* I x \<and>* sep_map_set_conj I (xs - {x}) \<and>* R> s\<rbrakk> \<Longrightarrow> <Q \<and>* sep_map_set_conj I xs \<and>* R> s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>finite xs; x \<in> xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <Q \<and>* I x \<and>* sep_map_set_conj I (xs - {x}) \<and>* R> s\<rbrakk> \<Longrightarrow> <Q \<and>* sep_map_set_conj I xs \<and>* R> s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>finite xs; x \<in> xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <Q \<and>* I x \<and>* sep_map_set_conj I (xs - {x}) \<and>* R> s\<rbrakk> \<Longrightarrow> <Q \<and>* (I x \<and>* sep_map_set_conj I (xs - {x})) \<and>* R> s proof (prove)
goal:
No subgoals!
theory MonadSep

lemma sep_list_conj_submap_wp':
  "\<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys;
   \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk>
  \<Longrightarrow> \<lbrace><P \<and>* \<And>* map I ys \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I ys \<and>* S \<and>* R>\<rbrace>" apply (cut_tac sep_list_conj_submap_wp [where P="P \<and>* S" and Q="Q \<and>* S" and
       I=I and R=R and ys=ys and xs=xs and f=f]) apply (fastforce simp: sep_conj_ac)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* \<And>* map I ys \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I ys \<and>* S \<and>* R>\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace>; \<lbrace><(P \<and>* S) \<and>* \<And>* map I ys \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <(Q \<and>* S) \<and>* \<And>* map I ys \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* \<And>* map I ys \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I ys \<and>* S \<and>* R>\<rbrace>
 2. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> set xs \<subseteq> set ys
 3. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> distinct xs
 4. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> distinct ys
 5. \<And>R. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><(P \<and>* S) \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <(Q \<and>* S) \<and>* \<And>* map I xs \<and>* R>\<rbrace> proof (prove)
goal:
No subgoals!