theory Sep_Fold

lemma sep_map_sep_foldI: "(\<And>* map P xs \<and>* ((\<And>* map Q xs) \<longrightarrow>* R)) s \<Longrightarrow> sep_fold P Q R xs s" apply (clarsimp simp: sep_fold_def) apply (induct xs arbitrary: s; clarsimp) apply (metis sep_add_zero sep_disj_zero sep_empty_zero sep_impl_def) apply (clarsimp simp: sep_conj_ac) apply (erule (1) sep_conj_impl) apply (erule sep_conj_sep_impl) apply (clarsimp simp: sep_conj_ac) apply (drule meta_spec) apply (erule meta_mp) apply (subst (asm) sep_conj_assoc[symmetric]) apply (erule sep_conj_sep_impl2) apply (erule sep_conj_sep_impl2) apply (rule sep_wand_collapse) apply (rule sep_wand_match, assumption) apply (erule sep_curry[rotated]) apply (metis (no_types) sep_conj_sep_impl2 sep_conj_commute sep_wand_collapse) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) s \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s proof (prove)
goal (1 subgoal):
 1. (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<box> \<longrightarrow>* R) s \<Longrightarrow> R s
 2. \<And>a xs s. \<lbrakk>\<And>s. (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; ((P a \<and>* \<And>* map P xs) \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) s\<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. (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; ((P a \<and>* \<And>* map P xs) \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) s\<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. (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; (P a \<and>* \<And>* map P xs \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) s\<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 h. \<lbrakk>\<And>s. (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; (\<And>* map P xs \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) h\<rbrakk> \<Longrightarrow> (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) h proof (prove)
goal (1 subgoal):
 1. \<And>a xs s h ha. \<lbrakk>\<And>s. (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; ((\<And>* map P xs \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) \<and>* Q a) ha\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R ha proof (prove)
goal (1 subgoal):
 1. \<And>a xs ha. \<lbrakk>\<And>s. (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s; (Q a \<and>* \<And>* map P xs \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) ha\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R ha proof (prove)
goal (1 subgoal):
 1. \<And>a xs ha. \<lbrakk>(Q a \<and>* \<And>* map P xs \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) ha; (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) (?s15 a xs ha) \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (?s15 a xs ha)\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R ha proof (prove)
goal (1 subgoal):
 1. \<And>a xs ha. (Q a \<and>* \<And>* map P xs \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) ha \<Longrightarrow> (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) ha proof (prove)
goal (1 subgoal):
 1. \<And>a xs ha. ((Q a \<and>* \<And>* map P xs) \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) ha \<Longrightarrow> (\<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) ha proof (prove)
goal (1 subgoal):
 1. \<And>a xs ha h. (Q a \<and>* \<And>* map P xs) h \<Longrightarrow> ((Q a \<and>* \<And>* map Q xs \<longrightarrow>* R) \<longrightarrow>* \<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) h proof (prove)
goal (1 subgoal):
 1. \<And>a xs ha h hb. Q a hb \<Longrightarrow> (\<And>* map P xs \<longrightarrow>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R) \<longrightarrow>* \<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) hb proof (prove)
goal (1 subgoal):
 1. \<And>a xs ha h hb. Q a hb \<Longrightarrow> (\<And>* map P xs \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R) \<longrightarrow>* \<And>* map P xs \<and>* (\<And>* map Q xs \<longrightarrow>* R)) hb proof (prove)
goal (1 subgoal):
 1. \<And>a xs ha h hb. Q a hb \<Longrightarrow> ((Q a \<and>* \<And>* map Q xs \<longrightarrow>* R) \<longrightarrow>* \<And>* map Q xs \<longrightarrow>* R) hb proof (prove)
goal (1 subgoal):
 1. \<And>a xs ha h hb hc. (Q a \<and>* (Q a \<and>* \<And>* map Q xs \<longrightarrow>* R)) hc \<Longrightarrow> (\<And>* map Q xs \<longrightarrow>* R) hc proof (prove)
goal:
No subgoals!