kings-crown/FVELER_Isabelle huggingface dataset:
theory Separation_Algebra

lemma intuitionistic_sep_impl_sep_true_simp:
  "intuitionistic P \<Longrightarrow> (sep_true \<longrightarrow>* P) = P" by (fast elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intuitionistic P \<Longrightarrow> ((\<lambda>s. True) \<longrightarrow>* P) = P
theory Separation_Algebra

lemma strictly_exactI:
  "(\<And>h h'. \<lbrakk> P h; P h' \<rbrakk> \<Longrightarrow> h = h') \<Longrightarrow> strictly_exact P" by (unfold strictly_exact_def, fast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>h h'. \<lbrakk>P h; P h'\<rbrakk> \<Longrightarrow> h = h') \<Longrightarrow> strictly_exact P
theory Separation_Algebra

lemma strictly_exact_sep_conj:
  "\<lbrakk> strictly_exact P; strictly_exact Q \<rbrakk> \<Longrightarrow> strictly_exact (P \<and>* Q)" apply (rule strictly_exactI) apply (erule sep_conjE)+ apply (drule_tac h="x" and h'="xa" in strictly_exactD, assumption+) apply (drule_tac h="y" and h'="ya" in strictly_exactD, assumption+) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strictly_exact P; strictly_exact Q\<rbrakk> \<Longrightarrow> strictly_exact (P \<and>* Q) proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>strictly_exact P; strictly_exact Q; (P \<and>* Q) h; (P \<and>* Q) h'\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h' x y xa ya. \<lbrakk>strictly_exact P; strictly_exact Q; P x; Q y; x ## y; h = x + y; P xa; Q ya; xa ## ya; h' = xa + ya\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h' x y xa ya. \<lbrakk>strictly_exact Q; P x; Q y; x ## y; h = x + y; P xa; Q ya; xa ## ya; h' = xa + ya; x = xa\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h' x y xa ya. \<lbrakk>P x; Q y; x ## y; h = x + y; P xa; Q ya; xa ## ya; h' = xa + ya; x = xa; y = ya\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma sep_disj_add_eq [simp]: "x ## y \<Longrightarrow> x + y ## z = (x ## z \<and> y ## z)" by (metis sep_add_disj_eq sep_disj_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x ## y \<Longrightarrow> x + y ## z = (x ## z \<and> y ## z)
theory Separation_Algebra

lemma "\<And>* [\<box>,P] = P" by (simp add: sep_list_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* [\<box>, P] = P
theory Separation_Algebra

lemma "\<And>* {\<box>} = \<box>" by (simp add: sep_set_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* {\<box>} = \<box>
theory Separation_Algebra

lemma "\<And>* {P,\<box>} = P" by (cases "P = \<box>", auto simp: sep_set_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* {P, \<box>} = P
theory Separation_Algebra

lemma "(\<And>* x\<in>{0,1::nat}. if x=0 then \<box> else P) = P" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (SETSEPCONJ x:{0, 1}. if x = 0 then \<box> else P) = P
theory Separation_Algebra

lemma map_sep_list_conj_cong:
  "(\<And>x. x \<in> set xs \<Longrightarrow> f x = g x) \<Longrightarrow> \<And>* map f xs = \<And>* map g xs" by (metis map_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x) \<Longrightarrow> \<And>* map f xs = \<And>* map g xs
theory Separation_Algebra

lemma sep_list_conj_Nil [simp]: "\<And>* [] = \<box>" by (simp add: sep_list_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* [] = \<box>
theory Separation_Algebra

lemma (in semigroup) foldl_assoc:
   "foldl f (f x y) zs = f x (foldl f y zs)" by (induct zs arbitrary: y) (simp_all add:assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<^bold>*) (x \<^bold>* y) zs = x \<^bold>* foldl (\<^bold>*) y zs
theory Separation_Algebra

lemma foldl_map_add:
  "foldl f z (map (\<lambda>x. f (P x) (Q x)) xs) = f (foldl f z (map P xs)) (foldl f z (map Q xs))" apply (induct xs) apply clarsimp apply simp by (metis (full_types) commute foldl_absorb1 foldl_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<^bold>*) \<^bold>1 (map (\<lambda>x. P x \<^bold>* Q x) xs) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map Q xs) proof (prove)
goal (2 subgoals):
 1. foldl (\<^bold>*) \<^bold>1 (map (\<lambda>x. P x \<^bold>* Q x) []) = foldl (\<^bold>*) \<^bold>1 (map P []) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map Q [])
 2. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map (\<lambda>x. P x \<^bold>* Q x) xs) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map Q xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map (\<lambda>x. P x \<^bold>* Q x) (a # xs)) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map Q (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map (\<lambda>x. P x \<^bold>* Q x) xs) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map Q xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map (\<lambda>x. P x \<^bold>* Q x) (a # xs)) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map Q (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map (\<lambda>x. P x \<^bold>* Q x) xs) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map Q xs) \<Longrightarrow> foldl (\<^bold>*) (P a \<^bold>* Q a) (map (\<lambda>x. P x \<^bold>* Q x) xs) = foldl (\<^bold>*) (P a) (map P xs) \<^bold>* foldl (\<^bold>*) (Q a) (map Q xs)
theory Separation_Algebra

lemma foldl_map_remove1:
  "x \<in> set xs \<Longrightarrow> foldl f z (map P xs) = f (P x) (foldl f z (map P (remove1 x xs)))" apply (induction xs, simp) apply clarsimp by (metis foldl_absorb1 left_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P xs) = P x \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (remove1 x xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>x \<in> set xs \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P xs) = P x \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (remove1 x xs)); x \<in> set (a # xs)\<rbrakk> \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) = P x \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (remove1 x (a # xs))) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>x \<in> set xs \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P xs) = P x \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (remove1 x xs)); x = a \<or> x \<in> set xs\<rbrakk> \<Longrightarrow> (x = a \<longrightarrow> foldl (\<^bold>*) (P a) (map P xs) = P a \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P xs)) \<and> (x \<noteq> a \<longrightarrow> foldl (\<^bold>*) (P a) (map P xs) = P x \<^bold>* foldl (\<^bold>*) (P a) (map P (remove1 x xs)))
theory Separation_Algebra

lemma sep_list_conj_Cons [simp]: "\<And>* (x#xs) = (x ** \<And>* xs)" by (simp add: sep_list_conj_def sep.foldl_absorb1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* x # xs = (x \<and>* \<And>* xs)
theory Separation_Algebra

lemma sep_list_conj_append [simp]: "\<And>* (xs @ ys) = (\<And>* xs ** \<And>* ys)" by (simp add: sep_list_conj_def sep.foldl_absorb1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* xs @ ys = (\<And>* xs \<and>* \<And>* ys)
theory Separation_Algebra

lemma sep_list_conj_map_append:
  "\<And>* map f (xs @ ys) = (\<And>* map f xs \<and>* \<And>* map f ys)" by (metis map_append sep_list_conj_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* map f (xs @ ys) = (\<And>* map f xs \<and>* \<And>* map f ys)
theory Separation_Algebra

lemma sep_list_con_map_filter:
  "(\<And>* map P (filter t xs) \<and>* \<And>* map P (filter (not t) xs))
   = \<And>* map P xs" apply (simp add: sep_list_conj_def) apply (rule sep.foldl_map_filter) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>* map P (filter t xs) \<and>* \<And>* map P (filter (\<lambda>s. \<not> t s) xs)) = \<And>* map P xs proof (prove)
goal (1 subgoal):
 1. (foldl (\<and>*) \<box> (map P (filter t xs)) \<and>* foldl (\<and>*) \<box> (map P (filter (\<lambda>s. \<not> t s) xs))) = foldl (\<and>*) \<box> (map P xs) proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma union_filter:
  "({x \<in> xs. P x} \<union> {x \<in> xs. \<not> P x}) = xs" by fast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x \<in> xs. P x} \<union> {x \<in> xs. \<not> P x} = xs
theory Separation_Algebra

lemma sep_map_set_conj_restrict:
  "finite xs \<Longrightarrow>
    sep_map_set_conj P xs =
   (sep_map_set_conj P {x \<in> xs. t x} \<and>*
    sep_map_set_conj P {x \<in> xs. \<not> t x})" by (subst sep.prod.union_disjoint [symmetric], (fastforce simp: union_filter)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite xs \<Longrightarrow> sep_map_set_conj P xs = (sep_map_set_conj P {x \<in> xs. t x} \<and>* sep_map_set_conj P {x \<in> xs. \<not> t x})
theory Separation_Algebra

lemma sep_list_conj_map_add:
  "\<And>* map (\<lambda>x. f x \<and>* g x) xs = (\<And>* map f xs \<and>* \<And>* map g xs)" apply (simp add: sep_list_conj_def) apply (rule sep.foldl_map_add) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* map (\<lambda>x. f x \<and>* g x) xs = (\<And>* map f xs \<and>* \<And>* map g xs) proof (prove)
goal (1 subgoal):
 1. foldl (\<and>*) \<box> (map (\<lambda>x. f x \<and>* g x) xs) = (foldl (\<and>*) \<box> (map f xs) \<and>* foldl (\<and>*) \<box> (map g xs)) proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma filter_empty:
  "x \<notin> set xs \<Longrightarrow> filter ((=) x) xs = []" by (induct xs, clarsimp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> filter ((=) x) xs = []
theory Separation_Algebra

lemma filter_singleton:
  "\<lbrakk>x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> [x'\<leftarrow>xs . x = x'] = [x]" by (induct xs, auto simp: filter_empty)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> filter ((=) x) xs = [x]
theory Separation_Algebra

lemma remove1_filter:
  "distinct xs \<Longrightarrow> remove1 x xs = filter (\<lambda>y. x \<noteq> y) xs" apply (induct xs) apply simp apply clarsimp apply (rule sym, rule filter_True) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> remove1 x xs = filter ((\<noteq>) x) xs proof (prove)
goal (2 subgoals):
 1. distinct [] \<Longrightarrow> remove1 x [] = filter ((\<noteq>) x) []
 2. \<And>a xs. \<lbrakk>distinct xs \<Longrightarrow> remove1 x xs = filter ((\<noteq>) x) xs; distinct (a # xs)\<rbrakk> \<Longrightarrow> remove1 x (a # xs) = filter ((\<noteq>) x) (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct xs \<Longrightarrow> remove1 x xs = filter ((\<noteq>) x) xs; distinct (a # xs)\<rbrakk> \<Longrightarrow> remove1 x (a # xs) = filter ((\<noteq>) x) (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>remove1 x xs = filter ((\<noteq>) x) xs; x \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> xs = filter ((\<noteq>) x) xs proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>remove1 x xs = filter ((\<noteq>) x) xs; x \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set xs. x \<noteq> xa proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma sep_list_conj_map_remove1:
  "x \<in> set xs \<Longrightarrow> \<And>* map P xs = (P x \<and>* \<And>* map P (remove1 x xs))" apply (simp add: sep_list_conj_def) apply (erule sep.foldl_map_remove1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> \<And>* map P xs = (P x \<and>* \<And>* map P (remove1 x xs)) proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> foldl (\<and>*) \<box> (map P xs) = (P x \<and>* foldl (\<and>*) \<box> (map P (remove1 x xs))) proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma sep_map_take_Suc:
  "i < length xs \<Longrightarrow>
  \<And>* map P (take (Suc i) xs) = (\<And>* map P (take i xs) \<and>* P (xs ! i))" by (subst take_Suc_conv_app_nth, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < length xs \<Longrightarrow> \<And>* map P (take (Suc i) xs) = (\<And>* map P (take i xs) \<and>* P (xs ! i))
theory Separation_Algebra

lemma sep_conj_map_split:
  "(\<And>* map f xs \<and>* f a \<and>* \<And>* map f ys)
  = (\<And>* map f (xs @ a # ys))" by (metis list.map(2) map_append sep_list_conj_Cons sep_list_conj_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>* map f xs \<and>* f a \<and>* \<And>* map f ys) = \<And>* map f (xs @ a # ys)
theory Separation_Algebra

lemma sep_map_set_conj_cong:
  "\<lbrakk>P = Q; xs = ys\<rbrakk> \<Longrightarrow> sep_map_set_conj P xs = sep_map_set_conj Q ys" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = Q; xs = ys\<rbrakk> \<Longrightarrow> sep_map_set_conj P xs = sep_map_set_conj Q ys
theory Separation_Algebra

lemma sep_set_conj_empty [simp]:
  "sep_set_conj {} = \<box>" by (simp add: sep_set_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* {} = \<box>
theory Separation_Algebra

lemma sep_map_set_conj_reindex_cong:
   "\<lbrakk>inj_on f A; B = f ` A; \<And>a. a \<in> A \<Longrightarrow> g a = h (f a)\<rbrakk>
    \<Longrightarrow> sep_map_set_conj h B = sep_map_set_conj g A" by (simp add: sep.prod.reindex)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f A; B = f ` A; \<And>a. a \<in> A \<Longrightarrow> g a = h (f a)\<rbrakk> \<Longrightarrow> sep_map_set_conj h B = sep_map_set_conj g A
theory Separation_Algebra

lemma sep_list_conj_sep_map_set_conj:
  "distinct xs
  \<Longrightarrow> \<And>* (map P xs) = (\<And>* x \<in> set xs. P x)" by (induct xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> \<And>* map P xs = sep_map_set_conj P (set xs)
theory Separation_Algebra

lemma sep_list_conj_sep_set_conj:
  "\<lbrakk>distinct xs; inj_on P (set xs)\<rbrakk>
  \<Longrightarrow> \<And>* (map P xs) = \<And>* (P ` set xs)" apply (subst sep_list_conj_sep_map_set_conj, assumption) apply (clarsimp simp: sep_set_conj_def sep.prod.reindex) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; inj_on P (set xs)\<rbrakk> \<Longrightarrow> \<And>* map P xs = \<And>* P ` set xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; inj_on P (set xs)\<rbrakk> \<Longrightarrow> sep_map_set_conj P (set xs) = \<And>* P ` set xs proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma sep_map_set_conj_sep_list_conj:
  "finite A \<Longrightarrow>
   \<exists>xs. set xs = A \<and> distinct xs \<and> sep_map_set_conj P A = \<And>* map P xs" apply (frule finite_distinct_list) apply (erule exE) apply (rule_tac x=xs in exI) apply clarsimp apply (erule sep_list_conj_sep_map_set_conj [symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> \<exists>xs. set xs = A \<and> distinct xs \<and> sep_map_set_conj P A = \<And>* map P xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; \<exists>xs. set xs = A \<and> distinct xs\<rbrakk> \<Longrightarrow> \<exists>xs. set xs = A \<and> distinct xs \<and> sep_map_set_conj P A = \<And>* map P xs proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>finite A; set xs = A \<and> distinct xs\<rbrakk> \<Longrightarrow> \<exists>xs. set xs = A \<and> distinct xs \<and> sep_map_set_conj P A = \<And>* map P xs proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>finite A; set xs = A \<and> distinct xs\<rbrakk> \<Longrightarrow> set xs = A \<and> distinct xs \<and> sep_map_set_conj P A = \<And>* map P xs proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>distinct xs; A = set xs\<rbrakk> \<Longrightarrow> sep_map_set_conj P (set xs) = \<And>* map P xs proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma sep_list_conj_impl:
  "\<lbrakk> list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) xs ys; (\<And>* xs) s \<rbrakk> \<Longrightarrow> (\<And>* ys) s" apply (induct arbitrary: s rule: list_all2_induct) apply simp apply simp apply (erule sep_conj_impl, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) xs ys; (\<And>* xs) s\<rbrakk> \<Longrightarrow> (\<And>* ys) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<And>* []) s \<Longrightarrow> (\<And>* []) s
 2. \<And>x xs y ys s. \<lbrakk>\<forall>s. x s \<longrightarrow> y s; list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) xs ys; \<And>s. (\<And>* xs) s \<Longrightarrow> (\<And>* ys) s; (\<And>* x # xs) s\<rbrakk> \<Longrightarrow> (\<And>* y # ys) s proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys s. \<lbrakk>\<forall>s. x s \<longrightarrow> y s; list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) xs ys; \<And>s. (\<And>* xs) s \<Longrightarrow> (\<And>* ys) s; (\<And>* x # xs) s\<rbrakk> \<Longrightarrow> (\<And>* y # ys) s proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys s. \<lbrakk>\<forall>s. x s \<longrightarrow> y s; list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) xs ys; \<And>s. (\<And>* xs) s \<Longrightarrow> (\<And>* ys) s; (x \<and>* \<And>* xs) s\<rbrakk> \<Longrightarrow> (y \<and>* \<And>* ys) s proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma sep_list_conj_exists:
  "(\<exists>x. (\<And>* map (\<lambda>y s. P x y s) ys) s) \<Longrightarrow> ((\<And>* map (\<lambda>y s. \<exists>x. P x y s) ys) s)" apply clarsimp apply (erule sep_list_conj_impl[rotated]) apply (rule list_all2I, simp_all) by (fastforce simp: in_set_zip)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. (\<And>* map (P x) ys) s \<Longrightarrow> (\<And>* map (\<lambda>y s. \<exists>x. P x y s) ys) s proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>* map (P x) ys) s \<Longrightarrow> (\<And>* map (\<lambda>y s. \<exists>x. P x y s) ys) s proof (prove)
goal (1 subgoal):
 1. \<And>x. list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) (map (P x) ys) (map (\<lambda>y s. \<exists>x. P x y s) ys) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x\<in>set (zip (map (P x) ys) (map (\<lambda>y s. \<exists>x. P x y s) ys)). case x of (x, y) \<Rightarrow> \<forall>s. x s \<longrightarrow> y s
theory Separation_Algebra

lemma sep_list_conj_map_impl:
  "\<lbrakk>\<And>s x. \<lbrakk>x \<in> set xs; P x s\<rbrakk> \<Longrightarrow> Q x s; (\<And>* map P xs) s\<rbrakk>
  \<Longrightarrow> (\<And>* map Q xs) s" apply (erule sep_list_conj_impl[rotated]) apply (rule list_all2I, simp_all) by (fastforce simp: in_set_zip)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s x. \<lbrakk>x \<in> set xs; P x s\<rbrakk> \<Longrightarrow> Q x s; (\<And>* map P xs) s\<rbrakk> \<Longrightarrow> (\<And>* map Q xs) s proof (prove)
goal (1 subgoal):
 1. (\<And>s x. \<lbrakk>x \<in> set xs; P x s\<rbrakk> \<Longrightarrow> Q x s) \<Longrightarrow> list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) (map P xs) (map Q xs) proof (prove)
goal (1 subgoal):
 1. (\<And>s x. \<lbrakk>x \<in> set xs; P x s\<rbrakk> \<Longrightarrow> Q x s) \<Longrightarrow> \<forall>x\<in>set (zip (map P xs) (map Q xs)). case x of (x, y) \<Rightarrow> \<forall>s. x s \<longrightarrow> y s
theory Separation_Algebra

lemma sep_map_set_conj_impl:
  "\<lbrakk>sep_map_set_conj P A s; \<And>s x. \<lbrakk>x \<in> A; P x s\<rbrakk> \<Longrightarrow> Q x s; finite A\<rbrakk>
  \<Longrightarrow> sep_map_set_conj Q A s" apply (frule sep_map_set_conj_sep_list_conj [where P=P]) apply (drule sep_map_set_conj_sep_list_conj [where P=Q]) by (metis sep_list_conj_map_impl sep_list_conj_sep_map_set_conj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_map_set_conj P A s; \<And>s x. \<lbrakk>x \<in> A; P x s\<rbrakk> \<Longrightarrow> Q x s; finite A\<rbrakk> \<Longrightarrow> sep_map_set_conj Q A s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_map_set_conj P A s; \<And>s x. \<lbrakk>x \<in> A; P x s\<rbrakk> \<Longrightarrow> Q x s; finite A; \<exists>xs. set xs = A \<and> distinct xs \<and> sep_map_set_conj P A = \<And>* map P xs\<rbrakk> \<Longrightarrow> sep_map_set_conj Q A s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_map_set_conj P A s; \<And>s x. \<lbrakk>x \<in> A; P x s\<rbrakk> \<Longrightarrow> Q x s; \<exists>xs. set xs = A \<and> distinct xs \<and> sep_map_set_conj P A = \<And>* map P xs; \<exists>xs. set xs = A \<and> distinct xs \<and> sep_map_set_conj Q A = \<And>* map Q xs\<rbrakk> \<Longrightarrow> sep_map_set_conj Q A s
theory Separation_Algebra

lemma set_sub_sub:
  "\<lbrakk>zs \<subseteq> ys\<rbrakk> \<Longrightarrow> (xs - zs) - (ys - zs) = (xs - ys)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zs \<subseteq> ys \<Longrightarrow> xs - zs - (ys - zs) = xs - ys
theory Separation_Algebra

lemma sep_map_set_conj_sub_sub_disjoint:
  "\<lbrakk>finite xs; zs \<subseteq> ys; ys \<subseteq> xs\<rbrakk>
  \<Longrightarrow> sep_map_set_conj P (xs - zs) = (sep_map_set_conj P (xs - ys) \<and>* sep_map_set_conj P (ys - zs))" apply (cut_tac sep.prod.subset_diff [where A="xs-zs" and B="ys-zs" and g=P]) apply (subst (asm) set_sub_sub, fast+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite xs; zs \<subseteq> ys; ys \<subseteq> xs\<rbrakk> \<Longrightarrow> sep_map_set_conj P (xs - zs) = (sep_map_set_conj P (xs - ys) \<and>* sep_map_set_conj P (ys - zs)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>finite xs; zs \<subseteq> ys; ys \<subseteq> xs; sep_map_set_conj P (xs - zs) = (sep_map_set_conj P (xs - zs - (ys - zs)) \<and>* sep_map_set_conj P (ys - zs))\<rbrakk> \<Longrightarrow> sep_map_set_conj P (xs - zs) = (sep_map_set_conj P (xs - ys) \<and>* sep_map_set_conj P (ys - zs))
 2. \<lbrakk>finite xs; zs \<subseteq> ys; ys \<subseteq> xs\<rbrakk> \<Longrightarrow> ys - zs \<subseteq> xs - zs
 3. \<lbrakk>finite xs; zs \<subseteq> ys; ys \<subseteq> xs\<rbrakk> \<Longrightarrow> finite (xs - zs) proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma foldl_use_filter_map:
  "foldl (\<and>*) Q (map (\<lambda>x. if T x then P x else \<box>) xs) =
   foldl (\<and>*) Q (map P (filter T xs))" by (induct xs arbitrary: Q, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<and>*) Q (map (\<lambda>x. if T x then P x else \<box>) xs) = foldl (\<and>*) Q (map P (filter T xs))
theory Separation_Algebra

lemma sep_list_conj_filter_map:
  "\<And>* (map (\<lambda>x. if T x then P x else \<box>) xs) =
   \<And>* (map P (filter T xs))" by (clarsimp simp: sep_list_conj_def foldl_use_filter_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>* map (\<lambda>x. if T x then P x else \<box>) xs = \<And>* map P (filter T xs)
theory Separation_Algebra

lemma sep_map_set_conj_restrict_predicate:
  "finite A \<Longrightarrow> (\<And>* x\<in>A. if T x then P x else \<box>) = (\<And>* x\<in>(Set.filter T A). P x)" by (simp add: Set.filter_def sep.prod.inter_filter)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> (SETSEPCONJ x:A. if T x then P x else \<box>) = sep_map_set_conj P (Set.filter T A)
theory Separation_Algebra

lemma distinct_filters:
  "\<lbrakk>distinct xs; \<And>x. (f x \<and> g x) = False\<rbrakk> \<Longrightarrow>
  set [x\<leftarrow>xs . f x \<or> g x] = set [x\<leftarrow>xs . f x] \<union> set [x\<leftarrow>xs . g x]" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<And>x. (f x \<and> g x) = False\<rbrakk> \<Longrightarrow> set (filter (\<lambda>x. f x \<or> g x) xs) = set (filter f xs) \<union> set (filter g xs)