Theory Sep_Algebra_Add

section ‹Additions to Separation Algebra Library›
theory Sep_Algebra_Add
imports "Separation_Algebra.Sep_Tactics"
begin

no_notation pred_K ("⟨_⟩")
hide_const (open) Separation_Algebra.pure

subsection ‹Simp-Lemmas for Separation Algebra›

named_theorems sep_algebra_simps ‹Advanced simplification lemmas for separation algebra›

lemmas [sep_algebra_simps] = sep_conj_exists sep_add_ac
lemmas [simp] = sep_conj_assoc

lemmas sep_conj_c = sep_conj_commute sep_conj_left_commute

lemmas sep_conj_aci = sep_conj_ac sep_conj_empty sep_conj_empty'

subsection ‹Separation Algebra with a Unique Zero›

class unique_zero_sep_algebra = stronger_sep_algebra +
  assumes unique_zero: "x##x ⟹ x=0"
begin
  lemma unique_zero_simps[simp]: 
    "a##a ⟷ a=0"
    "a##b ⟹ a+b = a ⟷ b=0"
    "a##b ⟹ a+b = b ⟷ a=0"
    "a##b ⟹ a + b = 0 ⟷ a=0 ∧ b=0"
    apply -
    using local.sep_disj_zero local.unique_zero apply blast
    apply (metis local.sep_add_disjD local.sep_add_zero local.unique_zero)
    apply (metis local.sep_add_disjD local.sep_add_zero_sym local.sep_disj_commute local.unique_zero)
    by (metis local.sep_add_disjD local.sep_add_zero local.sep_disj_zero local.unique_zero)

end

subsection ‹Standard Instantiations›

instantiation "fun" :: (type,stronger_sep_algebra) stronger_sep_algebra
begin
  definition "f1 ## f2 ⟷ (∀x. f1 x ## f2 x)"
  definition [simp]: "(f1 + f2) x = (f1 x + f2 x)"
  definition [simp]: "0 x ≡ 0"

  instance
    apply standard
    unfolding sep_disj_fun_def plus_fun_def zero_fun_def
    apply (auto)
    subgoal
      by (simp add: sep_disj_commute)
    subgoal
      using sep_add_commute by auto
    subgoal 
      by (simp add: sep_add_assoc) 
    (*subgoal 
      using sep_disj_addD1 by blast 
    subgoal 
      by (simp add: sep_disj_addI1) 
    *)
    done  
  
end

instance "fun" :: (type,unique_zero_sep_algebra) unique_zero_sep_algebra
  apply standard
  unfolding sep_disj_fun_def plus_fun_def zero_fun_def
  by (metis unique_zero)
  
lemma disj_fun_upd_iff[simp]: 
  "⟦f a = 0; g a = 0⟧ ⟹ (f(a:=x) ## g(a:=y)) ⟷ (f ## g ∧ x ## y)"
  unfolding sep_disj_fun_def by force

lemma fun_upd_Z_Z[simp]: "fun_upd 0 i 0 = 0" by auto

lemma sep_disj_fun_updI[sep_algebra_simps, intro]: "⟦f##g; a##b⟧ ⟹ f(x:=a) ## g(x:=b)"
  by (simp add: sep_disj_fun_def)
    
lemma sep_disj_fun_Zupd_eq[sep_algebra_simps]: 
  "f##0(x:=y) ⟷ f x ## y" 
  "0(x:=y) ## f ⟷ y ## f x" 
  by (auto simp add: sep_disj_fun_def)
  
  
lemma sep_disj_funD: "f##g ⟹ f x ## g x" by (auto simp: sep_disj_fun_def) 

lemma merge_fun_singleton: "fun_upd 0 i a + fun_upd 0 i b = fun_upd 0 i (a+b)" by auto

lemma split_fun_upd_0: "fun_upd (a+b) i 0 = fun_upd a i 0 + fun_upd b i 0" by auto
  

instantiation option :: (stronger_sep_algebra) stronger_sep_algebra begin

  fun sep_disj_option :: "'a option ⇒ 'a option ⇒ bool" where
    "sep_disj None None ⟷ True"
  | "sep_disj None (Some _) ⟷ True"  
  | "sep_disj (Some _) None ⟷ True"
  | "sep_disj (Some x) (Some y) ⟷ x##y"

  lemma sep_disj_option_add_simps[simp]: 
    "sep_disj None x" 
    "sep_disj x None" 
    by (cases x; simp)+
        
  fun plus_option :: "'a option ⇒ 'a option ⇒ 'a option" where 
    "plus None None = None"
  | "plus None (Some x) = Some x"
  | "plus (Some x) None = Some x" 
  | "plus (Some x) (Some y) = Some (x+y)"

  lemma plus_option_add_simps[simp]: "plus None x = x" "plus x None = x"
    by (cases x; simp)+
  
  definition "0 = None"
    
  instance 
    apply standard
    apply (simp_all add: zero_option_def)
    apply (case_tac x; case_tac y; simp add: sep_disj_commute)
    apply (case_tac x; case_tac y; auto simp add: sep_disj_commute sep_add_commute)
    apply (case_tac x; case_tac y; case_tac z; simp add: sep_add_assoc)
    apply (case_tac x; case_tac y; case_tac z; auto dest: sep_disj_addD1)
    (*apply (case_tac x; case_tac y; case_tac z; auto dest: sep_disj_addI1)*)
    done    
  
end


instantiation prod :: (stronger_sep_algebra, stronger_sep_algebra) stronger_sep_algebra
begin
  definition "a##b ⟷ fst a ## fst b ∧ snd a ## snd b"
  definition "a+b = (fst a + fst b, snd a + snd b)"  
  definition "0 = (0,0)"
  
  instance
    apply standard
    unfolding sep_disj_prod_def plus_prod_def zero_prod_def
    by (auto 
      simp: sep_add_ac 
      intro: sep_disj_commuteI sep_disj_addD1 sep_disj_addI1)
end

lemma sep_disj_prod_lower[sep_algebra_simps]: "(a,b) ## (c,d) ⟷ a##c ∧ b##d"
  by (simp add: sep_disj_prod_def)
  
lemma plus_prod_lower[sep_algebra_simps]: "(a,b) + (c,d) = (a+c,b+d)"
  by (simp add: plus_prod_def)

instance prod :: (unique_zero_sep_algebra,unique_zero_sep_algebra) unique_zero_sep_algebra
  by standard (auto simp: zero_prod_def sep_algebra_simps)

lemma prod_Z_lower[sep_algebra_simps]: 
  "(a,b) = 0 ⟷ a=0 ∧ b=0"
  "0 = (a,b) ⟷ a=0 ∧ b=0"
  by (auto simp: zero_prod_def)

lemma plus_prod_eqI: "(a+b,c+d) = (a,c) + (b,d)" by (simp add: sep_algebra_simps)
      
lemma fst_Z[simp]: "fst 0 = 0" by (simp add: zero_prod_def)
lemma snd_Z[simp]: "snd 0 = 0" by (simp add: zero_prod_def)

lemma fst_plus[sep_algebra_simps]: "fst (a+b) = fst a + fst b" by (auto simp: plus_prod_def)
lemma snd_plus[sep_algebra_simps]: "snd (a+b) = snd a + snd b" by (auto simp: plus_prod_def)
lemma disj_fstI[sep_algebra_simps]: "a##b ⟹ fst a ## fst b" by (auto simp: sep_disj_prod_def)
lemma disj_sndI[sep_algebra_simps]: "a##b ⟹ snd a ## snd b" by (auto simp: sep_disj_prod_def)


datatype 'a tsa_opt = ZERO | TRIV (the_tsa: 'a)

instantiation tsa_opt :: (type) unique_zero_sep_algebra begin
  definition sep_disj_tsa_opt :: "'a tsa_opt ⇒ 'a tsa_opt ⇒ bool" 
    where "a##b ⟷ a=ZERO ∨ b=ZERO"

  definition "a+b ≡ (case (a,b) of (ZERO,x) ⇒ x | (x,ZERO) ⇒ x)"
  definition "0 = ZERO"

  instance
    apply standard
    by (auto simp: zero_tsa_opt_def sep_disj_tsa_opt_def plus_tsa_opt_def split: tsa_opt.splits)
  
end
  
instance tsa_opt :: (type) cancellative_sep_algebra
  apply standard
  by (auto simp: zero_tsa_opt_def sep_disj_tsa_opt_def plus_tsa_opt_def split: tsa_opt.splits)
  

(* Lowering lemmas. If one side of operation breaks abstraction level, 
  the other side is also lowered
*)  
lemma TRIV_not_zero[simp]: "TRIV x ≠ 0" "0≠TRIV x" by (auto simp: zero_tsa_opt_def)
lemma TRIV_Z_lower[intro!]: 
  "ZERO = 0" 
  "0 = ZERO" 
  by (auto simp: zero_tsa_opt_def)  
  
lemma triv_Z_lower2[sep_algebra_simps]:  
  "x + ZERO = x"
  "ZERO + x = x"
  by (auto simp: zero_tsa_opt_def plus_tsa_opt_def split: tsa_opt.splits)  
  
lemma TRIV_disj_simps[sep_algebra_simps]:
  "TRIV a ## b ⟷ b=ZERO"
  "b ## TRIV a ⟷ b=ZERO"
  by (auto simp: sep_disj_tsa_opt_def)
  
subsection ‹Additional Simplifier Setup›

(* 
  This may cause trouble on non-eta-normalized terms.
    (λs. □ s) → λs. s=0
  The next lemma hopefully fixes that.
*)    

lemma sep_empty_app[sep_algebra_simps]: "□ h ⟷ h=0"
  by (simp add: sep_empty_def)

lemma sep_empty_I[sep_algebra_simps]: "(λh. h=0) = □"
  by (simp add: sep_empty_def)
  
lemma sep_triv_ineqs[simp]: 
  "□ ≠ sep_false"  
  "sep_true ≠ sep_false"  
  "sep_false ≠ □"  
  "sep_false ≠ sep_true"  
  by (auto dest: fun_cong)
  
lemma sep_true_not_empty:
  assumes "(a::'a::sep_algebra) ≠ (b::'a)"  
  shows "(□::'a⇒bool) ≠ sep_true"  
  by (metis (mono_tags, lifting) assms sep_empty_I)
  
  
subsection ‹Pure Assertions›

text ‹The Separation Algebra entry only defines @{term "pred_K Φ"}, which
  makes no constraint on the heap. We define ‹↑Φ›, which requires an empty heap, 
  and is more natural when using separation logic with deallocation.
›      

definition pred_lift :: "bool ⇒ 'a::sep_algebra ⇒ bool" ("↑_" [100] 100)
  where "(↑Φ) s ≡ Φ ∧ □ s"

text ‹Relation between ‹pred_lift› and ‹pred_K›. Warning, do not use 
  as simp-lemma, as ‹sep_true› is an abbreviation for ‹⟨True⟩››  
lemma "pred_K Φ = (↑Φ ** sep_true)" by (auto simp: pred_lift_def sep_conj_def sep_algebra_simps) 
  
lemma pred_lift_merge_simps[sep_algebra_simps]:
  "(↑Φ ** ↑Ψ) = (↑(Φ∧Ψ))"
  "(↑Φ ** ↑Ψ ** B) = (↑(Φ∧Ψ) ** B)"
  by (auto simp: pred_lift_def sep_conj_def sep_algebra_simps)

lemma pred_lift_move_front_simps[sep_algebra_simps]:
  "NO_MATCH (↑X) A ⟹ (A ** ↑Φ ** B) = (↑Φ ** A ** B)"
  "NO_MATCH (↑X) A ⟹ (A ** ↑Φ) = (↑Φ ** A)"
  by (auto simp: pred_lift_def sep_conj_def sep_algebra_simps)
  
  
lemmas pred_lift_move_merge_simps = pred_lift_merge_simps pred_lift_move_front_simps

  
lemma pred_lift_extract_simps[sep_algebra_simps]:
  "(↑Φ) h ⟷ Φ ∧ h=0"
  "(↑Φ ** A) h ⟷ Φ ∧ A h"
  by (auto simp: pred_lift_def sep_conj_def sep_algebra_simps)
  
lemma pure_true_conv[sep_algebra_simps]: "↑True = □" by (auto simp: sep_algebra_simps)

lemma pred_lift_false_conv[simp]: "↑False = sep_false" by (auto simp: sep_algebra_simps)

lemma pure_assn_eq_conv[simp]: "(↑Φ) = (↑Ψ) ⟷ Φ=Ψ"
  by (smt pred_lift_extract_simps(1))

lemmas sep_conj_false_simps =
  pred_lift_false_conv
  sep_conj_false_left sep_conj_false_right

definition sep_is_pure_assn :: "('a::sep_algebra ⇒ bool) ⇒ bool" where
  "sep_is_pure_assn A ≡ ∀s. A s ⟶ s=0"

definition pure_part :: "('a::sep_algebra ⇒ bool) ⇒ bool" where
  "pure_part A ≡ Ex A"

lemma pure_partI: "A s ⟹ pure_part A" by (auto simp: pure_part_def)
  
lemma pure_part_pure_eq[simp]: "sep_is_pure_assn A ⟹ ↑pure_part A = A"
  apply (rule ext)
  by (auto simp: sep_is_pure_assn_def pure_part_def pred_lift_def sep_algebra_simps)

  
lemma pure_part_triv_simps[simp]: 
  "¬pure_part sep_false"
  "pure_part □"
  by (auto simp: pure_part_def)

    
lemma pure_part_pure[simp]: "pure_part (↑Φ) = Φ"  
  by (auto simp: pure_part_def sep_algebra_simps pred_lift_def)
  
lemma pure_part_split_conj: "pure_part (A**B) ⟹ pure_part A ∧ pure_part B"  
  by (auto simp: pure_part_def sep_conj_def)
  
lemma sep_is_pure_lift_pred[simp]: "sep_is_pure_assn (↑Φ)"  
  by (auto simp: sep_is_pure_assn_def pred_lift_def sep_algebra_simps)
  
lemma sep_is_pure_assn_false[simp]: "sep_is_pure_assn sep_false" by (auto simp: sep_is_pure_assn_def)
lemma sep_is_pure_assn_empty[simp]: "sep_is_pure_assn □" by (auto simp: sep_is_pure_assn_def sep_algebra_simps)

lemma sep_is_pure_assn_conjI: "sep_is_pure_assn A ⟹ sep_is_pure_assn B ⟹ sep_is_pure_assn (A**B)"
  by (auto simp: sep_is_pure_assn_def sep_conj_def)

lemma pure_part_pure_conj_eq: "pure_part (↑P ** Q) ⟷ P ∧ pure_part Q"    
  unfolding pure_part_def by (auto simp: sep_algebra_simps)

lemma and_pure_true: "((A ** F) and ((↑Φ ** sep_true) ** F)) s ⟶ ((↑Φ ** A) ** F) s"  
  unfolding sep_conj_def pred_lift_def
  by (auto simp: sep_algebra_simps)
  
subsection ‹Exact Assertion›
  
definition EXACT :: "'a::sep_algebra ⇒ 'a ⇒ bool" where [sep_algebra_simps]: "EXACT h h' ≡ h'=h"
lemma strictly_exact_EXACT[simp]: "strictly_exact (EXACT h)"
  unfolding EXACT_def by (auto intro: strictly_exactI)

lemma EXACT_split: "a##b ⟹ EXACT (a+b) = (EXACT a ** EXACT b)"
  unfolding EXACT_def sep_conj_def by auto

lemma EXACT_zero[simp]: "EXACT 0 = □" by (auto simp: sep_algebra_simps)

lemma EXACT_eq_iff[simp]: "EXACT a = EXACT b ⟷ a=b"
  unfolding EXACT_def by metis
  
subsection ‹List-Sum over Separation Algebra›  
  
(* TODO: Move. Clean up *)

definition "sepsum_list l ≡ foldr (+) l (0::_::stronger_sep_algebra)"

lemma sepsum_list_simps[simp]:
  "sepsum_list [] = 0"
  "sepsum_list (x#xs) = x + sepsum_list xs"
  by (auto simp: sepsum_list_def)

context begin
  
private named_theorems ss

private definition "sep_ldisj1 x ys ≡ ∀y∈List.set ys. x##y"

private lemma sep_ldisj1_simps[ss]:
  "sep_ldisj1 x []"
  "sep_ldisj1 x (y#ys) ⟷ x##y ∧ sep_ldisj1 x ys"
  by (auto simp: sep_ldisj1_def)

private lemma sep_ldisj1_append[ss]: "sep_ldisj1 x (ys⇩1@ys⇩2) ⟷ sep_ldisj1 x ys⇩1 ∧ sep_ldisj1 x ys⇩2"
  by (induction ys⇩1) (auto simp: ss)
    
private definition "sep_ldisj xs ys ≡ ∀x∈List.set xs. sep_ldisj1 x ys"

private lemma sep_ldisj_simps[ss]:
  "sep_ldisj [] ys"
  "sep_ldisj xs []"
  "sep_ldisj (x#xs) ys ⟷ sep_ldisj1 x ys ∧ sep_ldisj xs ys"
  "sep_ldisj xs (y#ys) ⟷ sep_ldisj1 y xs ∧ sep_ldisj xs ys"
  by (auto simp: sep_ldisj_def sep_ldisj1_def sep_algebra_simps)

private lemma sep_ldisj_append1[ss]: "sep_ldisj (xs⇩1@xs⇩2) ys ⟷ sep_ldisj xs⇩1 ys ∧ sep_ldisj xs⇩2 ys"
  by (induction xs⇩1) (auto simp: ss)
  
private lemma sep_ldisj_append2[ss]: "sep_ldisj xs (ys⇩1@ys⇩2) ⟷ sep_ldisj xs ys⇩1 ∧ sep_ldisj xs ys⇩2"
  by (induction ys⇩1) (auto simp: ss)

private lemma sep_ldisj_commute[sep_algebra_simps]: "sep_ldisj xs ys ⟷ sep_ldisj ys xs"
  by (force simp: sep_ldisj_def sep_ldisj1_def sep_algebra_simps)
    
fun sep_distinct :: "_::stronger_sep_algebra list ⇒ bool" where
  "sep_distinct [] ⟷ True"  
| "sep_distinct (x#xs) ⟷ sep_ldisj1 x xs ∧ sep_distinct xs"  

declare sep_distinct.simps[simp del, ss add]

private lemma sep_distinct_append_aux[ss]: 
  "sep_distinct (xs@ys) ⟷ sep_distinct xs ∧ sep_distinct ys ∧ sep_ldisj xs ys"
  by (induction xs) (auto simp: ss)

private lemma norm_ldisj1[ss]: "sep_distinct ys ⟹ sep_ldisj1 x ys ⟷ x ## sepsum_list ys"  
  by (induction ys arbitrary: x) (auto simp: ss)
  
private lemma norm_ldisj[ss]: "sep_distinct xs ⟹ sep_distinct ys ⟹ sep_ldisj xs ys ⟷ sepsum_list xs ## sepsum_list ys"  
  by (induction xs) (auto simp: ss)
  
lemma sep_distinct_append[simp]: 
  "sep_distinct (xs@ys) ⟷ sep_distinct xs ∧ sep_distinct ys ∧ sepsum_list xs ## sepsum_list ys"  
  by (auto simp: ss)
  
lemma sepsum_append[simp]: "sep_distinct (xs@ys) ⟹ sepsum_list (xs@ys) = sepsum_list xs + sepsum_list ys"
  by (induction xs) (auto simp: sep_algebra_simps ss)

lemma sep_distinct_simps[simp]:  
  "sep_distinct []"
  "sep_distinct (x#xs) ⟷ x ## sepsum_list xs ∧ sep_distinct xs"
  by (auto simp: ss)
  
lemma disj_sepsum_list1[sep_algebra_simps]: 
  "sep_distinct bs ⟹ a ## sepsum_list bs ⟷ (∀b∈set bs. a ## b)"
  apply (induction bs)
  apply auto
  done

lemma disj_sepsum_list2[sep_algebra_simps]: 
  "sep_distinct bs ⟹ sepsum_list bs ## a ⟷ (∀b∈set bs. b ## a)"
  by (simp add: disj_sepsum_list1 sep_disj_commute)
  
  
  
end  
  
subsection ‹Finite Assertion Families›
interpretation sep_folding: folding "λi Q. P i ** Q" □ for P
  apply unfold_locales
  apply (intro ext) 
  apply (simp add: sep.add_ac)
  done
  
definition "sep_set_img S P ≡ ↑(finite S) ** sep_folding.F P S"
  
syntax
  "_SEP_SET_IMG"      :: "pttrn => 'a set => ('b ⇒ bool) => ('b ⇒ bool)"  ("(3⋃*_∈_./ _)" [0, 0, 10] 10)

translations 
  "⋃*x∈A. B"   ⇌ "CONST sep_set_img A (λx. B)"
  
print_translation ‹
  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax sep_set_img} @{syntax_const "_SEP_SET_IMG"}]
› ― ‹to avoid eta-contraction of body›
  
lemma sep_set_img_infinite[simp]: "infinite I ⟹ sep_set_img I P = sep_false"
  unfolding sep_set_img_def by auto




lemma sep_set_img_empty[simp]: "sep_set_img {} P = □"
  and sep_set_img_insert_remove: "sep_set_img (insert x S) P = (P x ** sep_set_img (S-{x}) P)"
  and sep_set_img_insert[simp]: "x∉S ⟹ sep_set_img (insert x S) P = (P x ** sep_set_img S P)"
  and sep_set_img_remove: "x∈S ⟹ sep_set_img S P = (P x ** sep_set_img (S-{x}) P)"
  by (auto 
    simp: sep_set_img_def sep_algebra_simps sep_folding.insert_remove sep_folding.remove 
    del: ext intro!: ext)
    
lemma sep_set_img_cong:
  assumes [simp]: "I=I'"
  assumes P: "⋀x. finite I' ⟹ x∈I' ⟹ P x = P' x"
  shows "sep_set_img I P = sep_set_img I' P'"
proof -
  {
    assume "finite I'"
    then have "sep_set_img I' P = sep_set_img I' P'" using P
      by induction auto
  }
  then show ?thesis by (cases "finite I'") auto
qed  
    
lemma sep_set_img_cong_strong[cong]:
  assumes [simp]: "I=I'"
  assumes P: "⋀x. finite I' =simp=> x∈I' =simp=> P x = P' x"
  shows "sep_set_img I P = sep_set_img I' P'"
  using assms
  unfolding simp_implies_def
  by (rule sep_set_img_cong)
    
lemma sep_set_img_union[simp]:
  assumes "S⇩1∩S⇩2={}"
  shows "sep_set_img (S⇩1∪S⇩2) P = (sep_set_img S⇩1 P ** sep_set_img S⇩2 P)"
proof -
  {
    assume "finite S⇩1" 
    then have ?thesis using assms
      by (induction S⇩1) auto
  }
  then show ?thesis by (cases "finite S⇩1") auto
    
qed  

lemmas sep_set_img_ins[simp] = sep_set_img_union[where S⇩1="{i}", simplified] for i

lemma sep_set_img_map:
  assumes "inj_on f I" 
  shows "(⋃*i∈f`I. A i) = (⋃*i∈I. A (f i))"
proof (cases "finite I")  
  case True
  thus ?thesis using assms apply (induction I)
    by (auto simp: sep_algebra_simps)
next
  case False thus ?thesis
    using assms
    apply simp
    using finite_image_iff sep_set_img_infinite by blast
qed    

lemma sep_set_img_unionI':
  assumes NDUP: "⋀x. ⟦x∈S⇩2 ⟧ ⟹ (P x ** P x) = sep_false"
  assumes P: "(sep_set_img S⇩1 P ** sep_set_img S⇩2 P) s"
  shows "sep_set_img (S⇩1∪S⇩2) P s"
proof -

  have A: "(P x ** P x ** F) = sep_false" if "x∈S⇩2" for x F
    using assms
    by (simp add: sep.mult_commute sep_conj_left_commute that)

  {
    assume "finite S⇩1" 
    then have "?thesis" using P
    proof (induction S⇩1 arbitrary: s)
      case empty
      then show ?case by simp
    next
      case (insert x S⇩1)
      then show ?case 
        apply (cases "x∉S⇩2")
        apply (auto simp: sep_set_img_remove sep_set_img_insert_remove sep_algebra_simps sep_conj_impl)
        by (simp add: A sep_conj_left_commute) 
    qed
  }
  then show ?thesis using P by (cases "finite S⇩1") auto
qed

lemma sep_set_img_pull_EXS: "(⋃*x∈I. EXS y. f x y) = (EXS Y. ⋃*x∈I. f x (Y x))"
proof -
  {
    assume "finite I"
    then have ?thesis
      apply (induction I)
      apply simp
      apply (rule ext)
      apply (clarsimp simp: sep_algebra_simps; safe)
      subgoal for x F s xa xb
        apply (rule exI[where x="xb(x:=xa)"])
        apply auto
        by (smt sep_set_img_cong)
      subgoal by auto  
      done
  }
  then show ?thesis by (cases "finite I") auto
qed  

lemma list_conj_eq_sep_set_img: "distinct xs ⟹ (⋀*map P xs) = sep_set_img (List.set xs) P"  
  by (induction xs) auto


lemma sep_is_pure_assn_imgI:
  assumes "⋀i. i∈I ⟹ sep_is_pure_assn (f i)" 
  shows "sep_is_pure_assn (⋃*i∈I. f i)"
proof (cases "finite I")
  assume "finite I"
  then show ?thesis using assms
    by (induction I) (auto simp: sep_is_pure_assn_conjI)
qed simp
  

  
end