kings-crown/FVELER_Isabelle huggingface dataset:
theory Sep_Fold_Cancel

lemma sep_factor_foldI_:
  "(\<And>* map (\<lambda>_. I) xs \<and>* sep_fold P Q R xs) s \<Longrightarrow> sep_fold (\<lambda>x. I \<and>* P x) Q R xs s" apply (induct xs arbitrary: s) apply (clarsimp simp: sep_fold_def) apply (clarsimp simp: sep_fold_def) apply (sep_cancel+, clarsimp, sep_mp) apply (clarsimp simp: sep_conj_ac) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>* map (\<lambda>_. I) xs \<and>* \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs) s \<Longrightarrow> \<lparr>{\<lambda>x. I \<and>* P x} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<And>* map (\<lambda>_. I) [] \<and>* \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> []) s \<Longrightarrow> \<lparr>{\<lambda>x. I \<and>* P x} \<and>* {Q} \<longrightarrow>* {R}\<rparr> [] s
 2. \<And>a xs s. \<lbrakk>\<And>s. (\<And>* map (\<lambda>_. I) xs \<and>* \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs) s \<Longrightarrow> \<lparr>{\<lambda>x. I \<and>* P x} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s; (\<And>* map (\<lambda>_. I) (a # xs) \<and>* \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> a # xs) s\<rbrakk> \<Longrightarrow> \<lparr>{\<lambda>x. I \<and>* P x} \<and>* {Q} \<longrightarrow>* {R}\<rparr> a # xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. (\<And>* map (\<lambda>_. I) xs \<and>* \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs) s \<Longrightarrow> \<lparr>{\<lambda>x. I \<and>* P x} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s; (\<And>* map (\<lambda>_. I) (a # xs) \<and>* \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> a # xs) s\<rbrakk> \<Longrightarrow> \<lparr>{\<lambda>x. I \<and>* P x} \<and>* {Q} \<longrightarrow>* {R}\<rparr> a # xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. (\<And>* map (\<lambda>_. I) xs \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. (I \<and>* P x) \<and>* (Q x \<longrightarrow>* R)) xs R s; ((I \<and>* \<And>* map (\<lambda>_. I) xs) \<and>* P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) s\<rbrakk> \<Longrightarrow> ((I \<and>* P a) \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. (I \<and>* P x) \<and>* (Q x \<longrightarrow>* R)) xs R)) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs sc. \<lbrakk>\<And>s. (\<And>* map (\<lambda>_. I) xs \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. I \<and>* P x \<and>* (Q x \<longrightarrow>* R)) xs R s; (foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R \<and>* \<And>* map (\<lambda>_. I) xs) sc\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. I \<and>* P x \<and>* (Q x \<longrightarrow>* R)) xs R sc proof (prove)
goal:
No subgoals!
theory Sep_Fold_Cancel

lemma sep_factor_foldI':
  "(I \<and>* (sep_fold P Q (I \<longrightarrow>* R) xs)) s \<Longrightarrow> sep_fold (\<lambda>x. I \<and>* P x) (\<lambda>x. I \<and>* Q x) R xs s" apply (induct xs arbitrary:s; clarsimp simp: sep_fold_def) apply (sep_solve) apply (sep_cancel)+ apply (sep_mp) apply (clarsimp simp: sep_conj_ac) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (I \<and>* \<lparr>{P} \<and>* {Q} \<longrightarrow>* {I \<longrightarrow>* R}\<rparr> xs) s \<Longrightarrow> \<lparr>{\<lambda>x. I \<and>* P x} \<and>* {\<lambda>x. I \<and>* Q x} \<longrightarrow>* {R}\<rparr> xs s proof (prove)
goal (2 subgoals):
 1. \<And>s. (I \<and>* (I \<longrightarrow>* R)) s \<Longrightarrow> R s
 2. \<And>a xs s. \<lbrakk>\<And>s. (I \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (I \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. (I \<and>* P x) \<and>* (I \<and>* Q x \<longrightarrow>* R)) xs R s; (I \<and>* P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (I \<longrightarrow>* R))) s\<rbrakk> \<Longrightarrow> ((I \<and>* P a) \<and>* (I \<and>* Q a \<longrightarrow>* foldr (\<lambda>x R. (I \<and>* P x) \<and>* (I \<and>* Q x \<longrightarrow>* R)) xs R)) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. (I \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (I \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. (I \<and>* P x) \<and>* (I \<and>* Q x \<longrightarrow>* R)) xs R s; (I \<and>* P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (I \<longrightarrow>* R))) s\<rbrakk> \<Longrightarrow> ((I \<and>* P a) \<and>* (I \<and>* Q a \<longrightarrow>* foldr (\<lambda>x R. (I \<and>* P x) \<and>* (I \<and>* Q x \<longrightarrow>* R)) xs R)) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb sc. \<lbrakk>\<And>s. (I \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (I \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. I \<and>* P x \<and>* (I \<and>* Q x \<longrightarrow>* R)) xs R s; ((Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (I \<longrightarrow>* R)) \<and>* I \<and>* Q a) sc\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. I \<and>* P x \<and>* (I \<and>* Q x \<longrightarrow>* R)) xs R sc proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb sc. \<lbrakk>\<And>s. (I \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (I \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. I \<and>* P x \<and>* (I \<and>* Q x \<longrightarrow>* R)) xs R s; (foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (I \<longrightarrow>* R) \<and>* I) sc\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. I \<and>* P x \<and>* (I \<and>* Q x \<longrightarrow>* R)) xs R sc proof (prove)
goal:
No subgoals!
theory Sep_Fold_Cancel

lemma sep_map_set_sep_foldI:
  "distinct xs \<Longrightarrow>
   (sep_map_set_conj P (set xs) \<and>* (sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s \<Longrightarrow>
   \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s" apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) apply (sep_solve) apply (sep_cancel)+ apply (sep_mp) apply (clarsimp simp: sep_conj_ac) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; (sep_map_set_conj P (set xs) \<and>* (sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s\<rbrakk> \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<box> \<longrightarrow>* R) s \<Longrightarrow> R s
 2. \<And>a xs s. \<lbrakk>\<And>s. (sep_map_set_conj P (set xs) \<and>* (sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; ((P a \<and>* sep_map_set_conj P (set xs)) \<and>* (Q a \<and>* sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s; a \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. (sep_map_set_conj P (set xs) \<and>* (sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; ((P a \<and>* sep_map_set_conj P (set xs)) \<and>* (Q a \<and>* sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s; a \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb. \<lbrakk>\<And>s. (sep_map_set_conj P (set xs) \<and>* (sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; a \<notin> set xs; distinct xs; (Q a \<and>* sep_map_set_conj P (set xs) \<and>* (Q a \<and>* sep_map_set_conj Q (set xs) \<longrightarrow>* R)) sb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R sb proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb. \<lbrakk>\<And>s. (sep_map_set_conj P (set xs) \<and>* (sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; a \<notin> set xs; distinct xs; ((sep_map_set_conj Q (set xs) \<longrightarrow>* R) \<and>* sep_map_set_conj P (set xs)) sb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R sb proof (prove)
goal:
No subgoals!
theory Sep_Fold_Cancel

lemma sep_fold_pure':
  "sep_fold P' Q R xs s \<Longrightarrow>
   (\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow>
   sep_fold (\<lambda>x s. P x \<and> P' x s) Q R xs s " apply (clarsimp simp: sep_fold_def) apply (induct xs arbitrary: s; clarsimp) apply (sep_cancel)+ apply (sep_mp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lparr>{P'} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s; \<And>x. x \<in> set xs \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<lparr>{\<lambda>x s. P x \<and> P' x s} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R s; \<And>x. x \<in> set xs \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R s \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R s; (P' a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R)) s; \<And>x. x = a \<or> x \<in> set xs \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> (P' a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R)) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb. \<lbrakk>\<And>s. foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R s \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R s; \<And>x. x = a \<or> x \<in> set xs \<Longrightarrow> P x; ((Q a \<longrightarrow>* foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R) \<and>* Q a) sb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R sb proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb. \<lbrakk>\<And>s. foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R s \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R s; \<And>x. x = a \<or> x \<in> set xs \<Longrightarrow> P x; foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R sb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R sb proof (prove)
goal:
No subgoals!
theory Sep_Fold_Cancel

lemma sep_fold_pure'':
  "sep_fold P' Q R xs s \<Longrightarrow>
   (\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow>
   sep_fold (\<lambda>x s. P' x s \<and> P x ) Q R xs s " apply (clarsimp simp: sep_fold_def) apply (induct xs arbitrary: s; clarsimp) apply (sep_cancel)+ apply (sep_mp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lparr>{P'} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s; \<And>x. x \<in> set xs \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<lparr>{\<lambda>x s. P' x s \<and> P x} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R s; \<And>x. x \<in> set xs \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R s \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R s; (P' a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R)) s; \<And>x. x = a \<or> x \<in> set xs \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> (P' a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R)) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb. \<lbrakk>\<And>s. foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R s \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R s; \<And>x. x = a \<or> x \<in> set xs \<Longrightarrow> P x; ((Q a \<longrightarrow>* foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R) \<and>* Q a) sb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R sb proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb. \<lbrakk>\<And>s. foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R s \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R s; \<And>x. x = a \<or> x \<in> set xs \<Longrightarrow> P x; foldr (\<lambda>x R. P' x \<and>* (Q x \<longrightarrow>* R)) xs R sb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R s. P x \<and> (P' x \<and>* (Q x \<longrightarrow>* R)) s) xs R sb proof (prove)
goal:
No subgoals!
theory Guess_ExI

lemma "P x \<Longrightarrow> \<exists>x. P x" by guess_exI

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P x \<Longrightarrow> \<exists>x. P x
theory Corres_Adjust_Preconds

lemma consume_preconds:
  "preconds A True True True \<Longrightarrow> A"
  "preconds True B True True \<Longrightarrow> B"
  "preconds True True C True \<Longrightarrow> C"
  "preconds True True True D \<Longrightarrow> D" by (simp_all add: preconds_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((preconds A True True True \<Longrightarrow> A) &&& (preconds True B True True \<Longrightarrow> B)) &&& (preconds True True C True \<Longrightarrow> C) &&& (preconds True True True D \<Longrightarrow> D)
theory Corres_Adjust_Preconds

lemma split_preconds_left:
  "preconds (A \<and> A') (B \<and> B') (C \<and> C') (D \<and> D') \<Longrightarrow> preconds A B C D"
  "preconds (A \<and> A') (B \<and> B') (C \<and> C') True \<Longrightarrow> preconds A B C True"
  "preconds (A \<and> A') (B \<and> B') True True \<Longrightarrow> preconds A B True True"
  "preconds (A \<and> A') True True True \<Longrightarrow> preconds A True True True" by (simp_all add: preconds_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((preconds (A \<and> A') (B \<and> B') (C \<and> C') (D \<and> D') \<Longrightarrow> preconds A B C D) &&& (preconds (A \<and> A') (B \<and> B') (C \<and> C') True \<Longrightarrow> preconds A B C True)) &&& (preconds (A \<and> A') (B \<and> B') True True \<Longrightarrow> preconds A B True True) &&& (preconds (A \<and> A') True True True \<Longrightarrow> preconds A True True True)
theory Corres_Adjust_Preconds

lemma split_preconds_right:
  "preconds (A \<and> A') (B \<and> B') (C \<and> C') (D \<and> D') \<Longrightarrow> preconds A' B' C' D'"
  "preconds (A \<and> A') (B \<and> B') (C \<and> C') True \<Longrightarrow> preconds A' B' C' True"
  "preconds (A \<and> A') (B \<and> B') True True \<Longrightarrow> preconds A' B' True True"
  "preconds (A \<and> A') True True True \<Longrightarrow> preconds A' True True True" by (simp_all add: preconds_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((preconds (A \<and> A') (B \<and> B') (C \<and> C') (D \<and> D') \<Longrightarrow> preconds A' B' C' D') &&& (preconds (A \<and> A') (B \<and> B') (C \<and> C') True \<Longrightarrow> preconds A' B' C' True)) &&& (preconds (A \<and> A') (B \<and> B') True True \<Longrightarrow> preconds A' B' True True) &&& (preconds (A \<and> A') True True True \<Longrightarrow> preconds A' True True True)
theory Corres_Adjust_Preconds

lemma preconds_goal_initiate:
  "preconds A B C D \<Longrightarrow> (preconds A B C D \<Longrightarrow> Q)
    \<Longrightarrow> finalise_preconds (A \<and> B \<and> C \<and> D) \<Longrightarrow> Q" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preconds A B C D; preconds A B C D \<Longrightarrow> Q; finalise_preconds (A \<and> B \<and> C \<and> D)\<rbrakk> \<Longrightarrow> Q
theory Corres_Adjust_Preconds

lemma finalise_preconds:
  "finalise_preconds True"
  "finalise_preconds A \<Longrightarrow> finalise_preconds B \<Longrightarrow> finalise_preconds (A \<and> B)"
  "finalise_preconds X" by (simp_all add: finalise_preconds_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finalise_preconds True &&& (\<lbrakk>finalise_preconds A; finalise_preconds B\<rbrakk> \<Longrightarrow> finalise_preconds (A \<and> B)) &&& finalise_preconds X
theory Corres_Adjust_Preconds

lemma corres_adjust_pre:
  "corres_underlying R nf nf' rs P Q  f f'
    \<Longrightarrow> (\<And>s s'. (s, s') \<in> R \<Longrightarrow> preconds (P1 s) (Q1 s') True True \<Longrightarrow> P s)
    \<Longrightarrow> (\<And>s s'. (s, s') \<in> R \<Longrightarrow> preconds (Q2 s') (P2 s) True True \<Longrightarrow> Q s')
    \<Longrightarrow> corres_underlying R nf nf' rs (\<lambda>s. P1 s \<and> P2 s) (\<lambda>s'. Q1 s' \<and> Q2 s') f f'" apply (erule stronger_corres_guard_imp) apply (simp add: preconds_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying R nf nf' rs P Q f f'; \<And>s s'. \<lbrakk>(s, s') \<in> R; preconds (P1 s) (Q1 s') True True\<rbrakk> \<Longrightarrow> P s; \<And>s s'. \<lbrakk>(s, s') \<in> R; preconds (Q2 s') (P2 s) True True\<rbrakk> \<Longrightarrow> Q s'\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' rs (\<lambda>s. P1 s \<and> P2 s) (\<lambda>s'. Q1 s' \<and> Q2 s') f f' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> R; preconds (P1 s) (Q1 s') True True\<rbrakk> \<Longrightarrow> P s; \<And>s s'. \<lbrakk>(s, s') \<in> R; preconds (Q2 s') (P2 s) True True\<rbrakk> \<Longrightarrow> Q s'; P1 s \<and> P2 s; Q1 s' \<and> Q2 s'; (s, s') \<in> R\<rbrakk> \<Longrightarrow> P s
 2. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> R; preconds (P1 s) (Q1 s') True True\<rbrakk> \<Longrightarrow> P s; \<And>s s'. \<lbrakk>(s, s') \<in> R; preconds (Q2 s') (P2 s) True True\<rbrakk> \<Longrightarrow> Q s'; P1 s \<and> P2 s; Q1 s' \<and> Q2 s'; (s, s') \<in> R\<rbrakk> \<Longrightarrow> Q s' proof (prove)
goal:
No subgoals!
theory Corres_Adjust_Preconds

lemma test_corres:
  "corres_underlying test_sr nf nf' dc (\<lambda>x. x < 40) (\<lambda>y. y < 30 \<and> y = 6)
    (modify (\<lambda>x. x + 2)) (modify (\<lambda>y. 10))" by (simp add: corres_underlying_def simpler_modify_def test_sr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying test_sr nf nf' dc (\<lambda>x. x < 40) (\<lambda>y. y < 30 \<and> y = 6) (modify (\<lambda>x. x + 2)) (modify (\<lambda>y. 10))
theory Corres_Adjust_Preconds

lemma test_adj_precond:
  "(x, y) \<in> test_sr \<Longrightarrow> x = 3 \<Longrightarrow> y = 6" by (simp add: test_sr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> test_sr; x = 3\<rbrakk> \<Longrightarrow> y = 6
theory Corres_Adjust_Preconds

lemma foo_adj_corres:
  "corres_underlying test_sr nf nf' dc (\<lambda>s. s < 40 \<and> s = 3) (\<lambda>s'. s' < 30) (modify (\<lambda>x. x + 2))
       (modify (\<lambda>y. 10))" by (rule test_corres[adj_corres test_adj_precond])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying test_sr nf nf' dc (\<lambda>s. s < 40 \<and> s = 3) (\<lambda>s'. s' < 30) (modify (\<lambda>x. x + 2)) (modify (\<lambda>y. 10))
theory Solves_Tac

lemma "(A = B) = (B = A)" apply solves oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A = B) = (B = A) proof (prove)
goal:
No subgoals!
theory Solves_Tac

lemma "\<lbrakk> A \<Longrightarrow> B ; B \<Longrightarrow> A \<rbrakk> \<Longrightarrow> A = B" apply solves oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow> B; B \<Longrightarrow> A\<rbrakk> \<Longrightarrow> A = B proof (prove)
goal:
No subgoals!
theory Trace_Monad

lemma failed_simps[simp]:
  "failed {(x, y)} = (y = Failed)"
  "failed (r \<union> r') = (failed r \<or> failed r')"
  "\<not> failed {}" by (auto simp: failed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. failed {(x, y)} = (y = Failed) &&& failed (r \<union> r') = (failed r \<or> failed r') &&& \<not> failed {}
theory Trace_Monad

lemma simpler_gets_def:
  "gets f = (\<lambda>s. {([], Result ((f s), s))})" by (simp add: gets_def return_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets f = (\<lambda>s. {([], Result (f s, s))})
theory Trace_Monad

lemma simpler_modify_def:
  "modify f = (\<lambda>s. {([], Result ((),(f s)))})" by (simp add: modify_def bind_def get_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify f = (\<lambda>s. {([], Result ((), f s))})
theory Trace_Monad

lemma bind_def':
  "bind f g \<equiv>
     \<lambda>s. ((\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> f s})
         \<union> ((\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> f s})
         \<union> (\<Union>(xs, rv, s) \<in> {(xs, rv, s'). (xs, Result (rv, s')) \<in> f s}. fst_upd (\<lambda>ys. ys @ xs) ` g rv s)" apply (clarsimp simp add: bind_def fun_eq_iff
                            Un_Union_image split_def
                    intro!: eq_reflection) apply (fastforce split: tmres.splits elim!: rev_bexI[where A="f x" for x]
                   intro: image_eqI[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f >>= g \<equiv> \<lambda>s. (\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> f s} \<union> (\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> f s} \<union> (\<Union>(xs, rv, s)\<in>{(xs, rv, s'). (xs, Result (rv, s')) \<in> f s}. (\<lambda>(a, b). (a @ xs, b)) ` g rv s) proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<Union>x\<in>f x. case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> (\<lambda>xa. (fst xa @ fst x, snd xa)) ` g (fst p) (snd p)) = (\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> f x} \<union> (\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> f x} \<union> (\<Union>x\<in>{p. (fst p, Result (snd p)) \<in> f x}. (\<lambda>xa. (fst xa @ fst x, snd xa)) ` g (fst (snd x)) (snd (snd x))) proof (prove)
goal:
No subgoals!
theory Trace_Monad

lemma elem_bindE:
  "\<lbrakk>(tr, res) \<in> bind f g s;
    \<lbrakk>res = Incomplete \<or> res = Failed; (tr, map_tmres undefined undefined res) \<in> f s\<rbrakk> \<Longrightarrow> P;
    \<And>tr' tr'' x s'. \<lbrakk>(tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> P\<rbrakk>
   \<Longrightarrow> P" by (auto simp: bind_def')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, res) \<in> (f >>= g) s; \<lbrakk>res = Incomplete \<or> res = Failed; (tr, map_tmres undefined undefined res) \<in> f s\<rbrakk> \<Longrightarrow> P; \<And>tr' tr'' x s'. \<lbrakk>(tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Trace_Monad

lemma return_bind[simp]:
  "(return x >>= f) = f x" by (simp add: return_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. return x >>= f = f x
theory Trace_Monad

lemma bind_return[simp]:
  "(m >>= return) = m" by (auto simp: fun_eq_iff bind_def return_def
           split: tmres.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>= return = m