header {* 

  Generic Separation Logic

*}

theory Hoare_gen

imports Main  

  "../Separation_Algebra/Sep_Tactics"

begin

definition 

  pasrt :: "bool \<Rightarrow> 'a::sep_algebra \<Rightarrow> bool" ("<_>" [72] 71)

where "pasrt b = (\<lambda> s . s = 0 \<and> b)"

(* same as sep.mult.left_commute *)

lemma sep_conj_cond1: 

  "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"

  by (rule sep.mult.left_commute)

(* same as sep.mult.commute *)

lemma sep_conj_cond2: 

  "(p \<and>* <cond>) = (<cond> \<and>* p)"

  by(rule sep.mult.commute)

(* same as sep.mult_assoc *)

lemma sep_conj_cond3: 

  "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)"

  by (rule sep.mult_assoc)

lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3

  by(unfold sep_empty_def pasrt_def, auto)

  by (simp add:pasrt_def)

locale sep_exec = 

   fixes step :: "'conf \<Rightarrow> 'conf"

    and  recse:: "'conf \<Rightarrow> 'a::sep_algebra"

begin 

definition "run n = step ^^ n"

lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"

  unfolding run_def

  by (simp add: funpow_add)

(* separation Hoare tripple *)

definition

  Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"  ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)

where

  "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> \<equiv> 

      \<forall>s r. (p \<and>* c \<and>* r) (recse s) \<longrightarrow> (\<exists>k. (q \<and>* c \<and>* r) (recse (run (Suc k) s)))"

lemma HoareI [case_names Pre]: 

  assumes h: "\<And> r s. (p \<and>* c \<and>* r) (recse s) \<Longrightarrow> \<exists>k. (q \<and>* c \<and>* r) (recse (run (Suc k) s))"

  shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  using h

  unfolding Hoare_gen_def

  by simp

lemma frame_rule: 

  assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  shows "\<lbrace>p \<and>* r\<rbrace> c \<lbrace>q \<and>* r\<rbrace>"

using assms

unfolding Hoare_gen_def

by (metis sep_conj_assoc sep_conj_left_commute)

lemma sequencing: 

  assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  and h2: "\<lbrace>q\<rbrace> c \<lbrace>r\<rbrace>"

  shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"

proof(induct rule: HoareI)

  case (Pre r' s')

  have "(p \<and>* c \<and>* r') (recse s')" by fact

  with h1[unfolded Hoare_gen_def]

  obtain k1 where "(q \<and>* c \<and>* r') (recse (run (Suc k1) s'))" by auto

  with h2[unfolded Hoare_gen_def]

  obtain k2 where "(r \<and>* c \<and>* r') (recse (run (Suc k2) (run (Suc k1) s')))" by auto

  thus "\<exists>k. (r \<and>* c \<and>* r') (recse (run (Suc k) s'))"

    by (auto simp add: run_add[symmetric])

qed

lemma pre_stren: 

  assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  and h2: "\<And>s. r s \<Longrightarrow> p s"

  shows "\<lbrace>r\<rbrace> c \<lbrace>q\<rbrace>"

using assms

unfolding Hoare_gen_def

by (metis sep_globalise)

lemma post_weaken: 

  assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

    and h2: "\<And> s. q s \<Longrightarrow> r s"

  shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"

using assms

unfolding Hoare_gen_def

by (metis sep_globalise)

lemma hoare_adjust:

  assumes h1: "\<lbrace>p1\<rbrace> c \<lbrace>q1\<rbrace>"

  and h2: "\<And>s. p s \<Longrightarrow> p1 s"

  and h3: "\<And>s. q1 s \<Longrightarrow> q s"

  shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  using h1 h2 h3 post_weaken pre_stren

  by (blast)

lemma code_exI: 

  assumes h: "\<And> k. \<lbrace>p\<rbrace> c(k) \<lbrace>q\<rbrace>"

  shows "\<lbrace>p\<rbrace> EXS k. c(k) \<lbrace>q\<rbrace>"

unfolding pred_ex_def

proof(induct rule:HoareI)

  case (Pre r' s')

  then obtain k where "(p \<and>* (\<lambda> s. c k s) \<and>* r') (recse s')"

    by (auto elim!: sep_conjE intro!: sep_conjI)

  with h[unfolded Hoare_gen_def]

  show "\<exists>k. (q \<and>* (\<lambda>s. \<exists>x. c x s) \<and>* r') (recse (run (Suc k) s'))"

    by (blast elim!: sep_conjE intro!: sep_conjI)

qed

lemma code_extension: 

  assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  shows "\<lbrace>p\<rbrace> c \<and>* e \<lbrace>q\<rbrace>"

using assms

unfolding Hoare_gen_def

by (metis sep_conj_assoc)

lemma code_extension1: 

  assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  shows "\<lbrace>p\<rbrace> e \<and>* c \<lbrace>q\<rbrace>"

using assms

unfolding Hoare_gen_def

by (metis sep_conj_commute sep_conj_left_commute)

lemma composition: 

  assumes h1: "\<lbrace>p\<rbrace> c1 \<lbrace>q\<rbrace>"

    and h2: "\<lbrace>q\<rbrace> c2 \<lbrace>r\<rbrace>"

  shows "\<lbrace>p\<rbrace> c1 \<and>* c2 \<lbrace>r\<rbrace>"

using assms

by (auto intro: sequencing code_extension code_extension1)

lemma pre_condI: 

  assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" 

  shows "\<lbrace><cond> \<and>* p\<rbrace> c \<lbrace>q\<rbrace>"

proof(induct rule:HoareI)

  case (Pre r s)

  hence "cond" "(p \<and>* c \<and>* r) (recse s)"

    apply (metis pasrt_def sep_conjD)

    by (smt Pre.hyps pasrt_def sep_add_zero sep_conj_commute sep_conj_def)

  from h[OF this(1), unfolded Hoare_gen_def, rule_format, OF this(2)]

  show ?case .

qed

lemma code_condI: 

  assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  shows "\<lbrace>p\<rbrace> <b> \<and>* c \<lbrace>q\<rbrace>"

proof(induct rule: HoareI)

  case (Pre r s)

  hence h1: "b" "(p \<and>* c \<and>* r) (recse s)"

    apply (metis condD sep_conjD sep_conj_assoc)

    by (smt Pre.hyps condD sep_conj_impl)

  from h[OF h1(1), unfolded Hoare_gen_def, rule_format, OF h1(2)]

  and h1(1)

  show ?case

    by (metis (full_types) cond_true_eq1)

qed

lemma precond_exI: 

  assumes h:"\<And>x. \<lbrace>p x\<rbrace> c \<lbrace>q\<rbrace>"

  shows "\<lbrace>EXS x. p x\<rbrace> c \<lbrace>q\<rbrace>"

proof(induct rule: HoareI)

  case (Pre r s)

  then obtain x where "(p x \<and>* c \<and>* r) (recse s)"

    by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI)

  from h[of x, unfolded Hoare_gen_def, rule_format, OF this]  

  show ?case .

qed

lemma hoare_sep_false: 

  "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" 

lemma pred_exI: 

  assumes "(P(x) \<and>* r) s"

  shows "((EXS x. P(x)) \<and>* r) s"

  by (metis assms pred_ex_def sep_globalise)

definition

  IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 

             ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)

where

  "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c 

                        \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)"

lemma IHoareI [case_names IPre]: 

  assumes h: "\<And>s' s r cnf .  (<P s> \<and>* <(s ## s')> \<and>* I(s + s') \<and>* c \<and>* r) (recse cnf) \<Longrightarrow> 

                   \<exists>k t. (<Q t> \<and>* <(t ## s')>  \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) cnf))"

  shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"

unfolding IHoare_def

proof

  fix s'

  show " \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c

         \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"

  proof(unfold pred_ex_def, induct rule:HoareI)

    case (Pre r s)

    then obtain sa where "(<P sa> \<and>* <(sa ## s')> \<and>* I (sa + s') \<and>* c \<and>* r) (recse s)"

      by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)

    hence " (\<exists>k t. (<Q t> \<and>* <(t##s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) s)))" 

      by (rule h)

    then obtain k t where h2: "(<Q t> \<and>* <(t ## s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) s))"

      by auto

    thus "\<exists>k. ((\<lambda>s. \<exists>sa. (<Q sa> \<and>* <(sa ## s')> \<and>* I (sa + s')) s) \<and>* c \<and>* r) (recse (run (Suc k) s))"

      apply (rule_tac x = k in exI)

      by (auto intro!:sep_conjI elim!:sep_conjE simp:sep_conj_ac)

    qed

  qed

lemma I_frame_rule: 

  assumes h: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"

  shows "I. \<lbrace>P \<and>* R\<rbrace> c \<lbrace>Q \<and>* R\<rbrace>"

proof(induct rule:IHoareI)

  case (IPre s' s r cnf)

  hence "((<(P \<and>* R) s> \<and>* <(s##s')> \<and>* I (s + s')) \<and>* c \<and>* r) (recse cnf)"

    by (auto simp:sep_conj_ac)

  then obtain s1 s2 

  where h1: "((<P s1> \<and>* <((s1 + s2) ## s')> \<and>*I (s1 + s2 + s')) \<and>* c \<and>* r) (recse cnf)" 

              "s1 ## s2" "s1 + s2 ## s'" "P s1" "R s2"

    by (unfold pasrt_def, auto elim!:sep_conjE intro!:sep_conjI)

  hence "((EXS s. <P s> \<and>* <(s ## s2 +s')> \<and>*I (s + (s2 + s'))) \<and>* c \<and>* r) (recse cnf)"

    apply (sep_cancel, unfold pred_ex_def, auto intro!:sep_conjI sep_disj_addI3 elim!:sep_conjE)

    apply (rule_tac x = s1 in exI, unfold pasrt_def,

       auto intro!:sep_conjI sep_disj_addI3 elim!:sep_conjE simp:sep_conj_ac)

    by (metis sep_add_assoc sep_add_disjD)

  from h[unfolded IHoare_def Hoare_gen_def, rule_format, OF this]

  obtain k s where

     "((<Q s> \<and>* <(s ## s2 + s')> \<and>* I (s + (s2 + s'))) \<and>* c \<and>* r) (recse (run (Suc k) cnf))"

    by (unfold pasrt_def pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI)

  thus ?case

  proof(rule_tac x = k in exI, rule_tac x = "s + s2" in exI, sep_cancel+)

    fix  h ha

    assume hh: "(<Q s> \<and>* <(s ## s2 + s')> \<and>* I (s + (s2 + s'))) ha"

    show " (<(Q \<and>* R) (s + s2)> \<and>* <(s + s2 ## s')> \<and>* I (s + s2 + s')) ha"

    proof -

      from hh have h0: "s ## s2 + s'"

        by (metis pasrt_def sep_conjD)

      with h1(2, 3)

      have h2: "s + s2 ## s'" 

        by (metis sep_add_disjD sep_disj_addI1)

      moreover from h1(2, 3) h2 have h3: "(s + (s2 + s')) = (s + s2 + s')"

        by (metis `s ## s2 + s'` sep_add_assoc sep_add_disjD sep_disj_addD1)

      moreover from hh have "Q s" by (metis pasrt_def sep_conjD)

      moreover from h0 h1(2) h1(3) have "s ## s2"

        by (metis sep_add_disjD sep_disj_addD)

      moreover note h1(5)

      ultimately show ?thesis

        by (smt h0 hh sep_conjI)

    qed

  qed

qed

lemma I_sequencing: 

  assumes h1: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"

  and h2: "I. \<lbrace>Q\<rbrace> c \<lbrace>R\<rbrace>"

  shows "I. \<lbrace>P\<rbrace> c \<lbrace>R\<rbrace>"

  using h1 h2 sequencing

  by (smt IHoare_def)

lemma I_pre_stren: 

  assumes h1: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"

  and h2:  "\<And>s. R s \<Longrightarrow> P s"

  shows "I. \<lbrace>R\<rbrace> c \<lbrace>Q\<rbrace>"

proof(unfold IHoare_def, default)

  fix s'

  show "\<lbrace>EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c 

       \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"

  proof(rule pre_stren)

    from h1[unfolded IHoare_def, rule_format, of s']

    show "\<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c 

          \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" .

  next

    fix s

    show "(EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')) s \<Longrightarrow> 

            (EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')) s"

      apply (unfold pred_ex_def, clarify)

      apply (rule_tac x = sa in exI, sep_cancel+)

      by (insert h2, auto simp:pasrt_def)

  qed

qed

lemma I_post_weaken: 

  assumes h1: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"

    and h2: "\<And> s. Q s \<Longrightarrow> R s"

  shows "I. \<lbrace>P\<rbrace> c \<lbrace>R\<rbrace>"

proof(unfold IHoare_def, default)

  fix s'

  show "\<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c 

        \<lbrace>EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"

  proof(rule post_weaken)

    from h1[unfolded IHoare_def, rule_format, of s']

    show "\<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c 

          \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" .

  next

    fix s

    show "(EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')) s \<Longrightarrow> 

          (EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')) s"

      apply (unfold pred_ex_def, clarify)

      apply (rule_tac x = sa in exI, sep_cancel+)

      by (insert h2, auto simp:pasrt_def)

  qed

qed

lemma I_hoare_adjust:

  assumes h1: "I. \<lbrace>P1\<rbrace> c \<lbrace>Q1\<rbrace>"

  and h2: "\<And>s. P s \<Longrightarrow> P1 s"

  and h3: "\<And>s. Q1 s \<Longrightarrow> Q s"

  shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"

  using h1 h2 h3 I_post_weaken I_pre_stren

  by (metis)

lemma I_code_exI: 

  assumes h: "\<And> k. I. \<lbrace>P\<rbrace> c(k) \<lbrace>Q\<rbrace>"

  shows "I. \<lbrace>P\<rbrace> EXS k. c(k) \<lbrace>Q\<rbrace>"

using h

by (smt IHoare_def code_exI)

lemma I_code_extension: 

  assumes h: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"

  shows "I. \<lbrace>P\<rbrace> c \<and>* e \<lbrace>Q\<rbrace>"

  using h

  by (smt IHoare_def sep_exec.code_extension)

lemma I_composition: 

  assumes h1: "I. \<lbrace>P\<rbrace> c1 \<lbrace>Q\<rbrace>"

    and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>"

  shows "I. \<lbrace>P\<rbrace> c1 \<and>* c2 \<lbrace>R\<rbrace>"

  using h1 h2

by (smt IHoare_def sep_exec.composition)

lemma I_pre_condI: 

  assumes h: "cond \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" 

  shows "I. \<lbrace><cond> \<and>* P\<rbrace> c \<lbrace>Q\<rbrace>"

  using h

by (smt IHoareI condD cond_true_eq2 sep.mult_commute)

lemma I_code_condI: 

  assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"

  shows "I. \<lbrace>P\<rbrace> <b> \<and>* c \<lbrace>Q\<rbrace>"

  using h

by (smt IHoareI condD cond_true_eq2 sep.mult_commute sep_conj_cond1)

lemma I_precond_exI: 

  assumes h:"\<And>x. I. \<lbrace>P x\<rbrace> c \<lbrace>Q\<rbrace>"

  shows "I. \<lbrace>EXS x. P x\<rbrace> c \<lbrace>Q\<rbrace>"

proof(induct rule:IHoareI)

  case (IPre s' s r cnf)

  then obtain x

    where "((EXS s. <P x s> \<and>* <(s ## s')> \<and>* I (s + s')) \<and>* c \<and>* r) (recse cnf)"

    by ( auto elim!:sep_conjE intro!:sep_conjI simp:pred_ex_def pasrt_def sep_conj_ac)

  from h[unfolded IHoare_def Hoare_gen_def, rule_format, OF this]

  obtain k t 

    where "((<Q t> \<and>* <(t ## s')> \<and>* I (t + s')) \<and>* c \<and>* r) (recse (run (Suc k) cnf))"

    by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI)

  thus ?case 

    by (auto simp:sep_conj_ac)

qed

lemma I_hoare_sep_false:

  "I. \<lbrace>sep_false\<rbrace> c \<lbrace>Q\<rbrace>"

by (smt IHoareI condD)

end

instantiation set :: (type)sep_algebra

begin

definition set_zero_def: "0 = {}"

definition plus_set_def: "s1 + s2 = s1 \<union> s2"

definition sep_disj_set_def: "sep_disj s1 s2 = (s1 \<inter> s2 = {})"

lemmas set_ins_def = sep_disj_set_def plus_set_def set_zero_def

instance

  apply(default)

  apply(auto simp: set_ins_def)

done

end

section {* A big operator of infinite separation conjunction *}

definition "fam_conj I cpt s = (\<exists> p. (s = (\<Union> i \<in> I. p(i))) \<and>

                                     (\<forall> i \<in> I. cpt i (p i)) \<and>

                                     (\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> p(i) ## p(j)))"

lemma fam_conj_zero_simp: "fam_conj {} cpt = <True>"

proof

  fix s

  show "fam_conj {} cpt s = (<True>) s"

  proof

    assume "fam_conj {} cpt s"

    then obtain p where "s = (\<Union> i \<in> {}. p(i))"

      by (unfold fam_conj_def, auto)

    hence "s = {}" by auto

    thus "(<True>) s" by (metis pasrt_def set_zero_def) 

  next

    assume "(<True>) s"

    hence eq_s: "s = {}" by (metis pasrt_def set_zero_def)

    let ?p = "\<lambda> i. {}"

    have "(s = (\<Union> i \<in> {}. ?p(i)))" by (unfold eq_s, auto)

    moreover have "(\<forall> i \<in> {}. cpt i (?p i))" by auto

    moreover have "(\<forall> i \<in> {}. \<forall> j \<in> {}. i \<noteq> j \<longrightarrow> ?p(i) ## ?p(j))" by auto

    ultimately show "fam_conj {} cpt s"

      by (unfold eq_s fam_conj_def, auto)

  qed

qed

lemma fam_conj_disj_simp_pre:

  assumes h1: "I = I1 + I2"

  and h2: "I1 ## I2"

  shows "fam_conj I cpt = (fam_conj I1 cpt \<and>* fam_conj I2 cpt)"

proof

  fix s

  let ?fm = "fam_conj I cpt" and ?fm1 = "fam_conj I1 cpt" and ?fm2 = "fam_conj I2 cpt"

  show "?fm s = (?fm1 \<and>* ?fm2) s"

  proof

    assume "?fm s"

    then obtain p where pre:

            "s = (\<Union> i \<in> I. p(i))"

            "(\<forall> i \<in> I. cpt i (p i))"

            "(\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> p(i) ## p(j))"

      unfolding fam_conj_def by metis

    from pre(1) h1 h2 have "s = (\<Union> i \<in> I1. p(i)) + (\<Union> i \<in> I2. p(i))"

      by (auto simp:set_ins_def)

    moreover from pre h1 have "?fm1 (\<Union> i \<in> I1. p(i))"

      by (unfold fam_conj_def, rule_tac x = p in exI, auto simp:set_ins_def)

    moreover from pre h1 have "?fm2 (\<Union> i \<in> I2. p(i))"

      by (unfold fam_conj_def, rule_tac x = p in exI, auto simp:set_ins_def)

    moreover have "(\<Union> i \<in> I1. p(i)) ## (\<Union> i \<in> I2. p(i))"

    proof -

      { fix x xa xb

        assume h: "I1 \<inter> I2 = {}"

                  "\<forall>i\<in>I1 \<union> I2. \<forall>j\<in>I1 \<union> I2. i \<noteq> j \<longrightarrow> p i \<inter> p j = {}"

                  "xa \<in> I1" "x \<in> p xa" "xb \<in> I2" "x \<in> p xb"

        have "p xa \<inter> p xb = {}"

        proof(rule h(2)[rule_format])

          from h(1, 3, 5) show "xa \<in> I1 \<union> I2" by auto

        next

          from h(1, 3, 5) show "xb \<in> I1 \<union> I2" by auto

        next

          from h(1, 3, 5) show "xa \<noteq> xb" by auto

        qed with h(4, 6) have False by auto

      } with h1 h2 pre(3) show ?thesis by (auto simp:set_ins_def) 

    qed

    ultimately show "(?fm1 \<and>* ?fm2) s" by (auto intro!:sep_conjI)

  next

    assume "(?fm1 \<and>* ?fm2) s"

    then obtain s1 s2 where pre:

      "s = s1 + s2" "s1 ## s2" "?fm1 s1" "?fm2 s2"

      by (auto dest!:sep_conjD)

    from pre(3) obtain p1 where pre1:

            "s1 = (\<Union> i \<in> I1. p1(i))"

            "(\<forall> i \<in> I1. cpt i (p1 i))"

            "(\<forall> i \<in> I1. \<forall> j \<in> I1. i \<noteq> j \<longrightarrow> p1(i) ## p1(j))"

       unfolding fam_conj_def by metis

    from pre(4) obtain p2 where pre2:

            "s2 = (\<Union> i \<in> I2. p2(i))"

            "(\<forall> i \<in> I2. cpt i (p2 i))"

            "(\<forall> i \<in> I2. \<forall> j \<in> I2. i \<noteq> j \<longrightarrow> p2(i) ## p2(j))"

       unfolding fam_conj_def by metis

     let ?p = "\<lambda> i. if i \<in> I1 then p1 i else p2 i"

     from h2 pre(2)

     have "s = (\<Union> i \<in> I. ?p(i))" 

       apply (unfold h1 pre(1) pre1(1) pre2(1) set_ins_def, auto split:if_splits)

       by (metis disjoint_iff_not_equal)

     moreover from h2 pre1(2) pre2(2) have "(\<forall> i \<in> I. cpt i (?p i))" 

       by (unfold h1 set_ins_def, auto split:if_splits)

     moreover from pre1(1, 3) pre2(1, 3) pre(2) h2

     have "(\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> ?p(i) ## ?p(j))" 

       apply (unfold h1 set_ins_def, auto split:if_splits)

       by (metis IntI empty_iff)

     ultimately show "?fm s" by (unfold fam_conj_def, auto)

  qed

qed

lemma fam_conj_disj_simp:

  assumes h: "I1 ## I2"

  shows "fam_conj (I1 + I2) cpt = (fam_conj I1 cpt \<and>* fam_conj I2 cpt)"

proof -

  from fam_conj_disj_simp_pre[OF _ h, of "I1 + I2"]

  show ?thesis by simp

qed