header {* +
−
  Generic Separation Logic+
−
*}+
−
+
−
theory Hoare_gen+
−
imports Main +
−
  "../progtut/Tactical" "../Separation_Algebra/Sep_Tactics"+
−
begin+
−
+
−
ML_file "../Separation_Algebra/sep_tactics.ML"+
−
+
−
definition pasrt :: "bool \<Rightarrow> (('a::sep_algebra) \<Rightarrow> bool)" ("<_>" [72] 71)+
−
where "pasrt b = (\<lambda> s . s = 0 \<and> b)"+
−
+
−
lemma sep_conj_cond1: "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"+
−
  by(simp add: sep_conj_ac)+
−
+
−
lemma sep_conj_cond2: "(p \<and>* <cond>) = (<cond> \<and>* p)"+
−
  by(simp add: sep_conj_ac)+
−
+
−
lemma sep_conj_cond3: "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)"+
−
  by (metis sep.mult_assoc)+
−
+
−
lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3+
−
+
−
lemma cond_true_eq[simp]: "<True> = \<box>"+
−
  by(unfold sep_empty_def pasrt_def, auto)+
−
+
−
lemma cond_true_eq1: "(<True> \<and>* p) = p"+
−
  by(simp)+
−
+
−
lemma false_simp [simp]: "<False> = sep_false" (* move *)+
−
  by (simp add:pasrt_def)+
−
+
−
lemma cond_true_eq2: "(p \<and>* <True>) = p"+
−
  by simp+
−
+
−
lemma condD: "(<b> ** r) s \<Longrightarrow> b \<and> r s" +
−
by (unfold sep_conj_def pasrt_def, auto)+
−
+
−
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)"+
−
  apply (unfold run_def)+
−
  by (metis funpow_add o_apply)+
−
+
−
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**c**r) (recse s) \<longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s)))))"+
−
+
−
lemma HoareI [case_names Pre]: +
−
  assumes h: "\<And> r s. (p**c**r) (recse s) \<Longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s))))"+
−
  shows "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"+
−
  using h+
−
  by (unfold Hoare_gen_def, auto)+
−
+
−
lemma frame_rule: +
−
  assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"+
−
  shows "\<lbrace> p ** r \<rbrace> c \<lbrace> q ** r \<rbrace>"+
−
proof(induct rule: HoareI)+
−
  case (Pre r' s')+
−
  hence "(p \<and>* c \<and>* r \<and>* r') (recse s')" by (auto simp:sep_conj_ac)+
−
  from h[unfolded Hoare_gen_def, rule_format, OF this]+
−
  show ?case+
−
    by (metis sep_conj_assoc sep_conj_left_commute)+
−
qed+
−
+
−
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')+
−
  from h1[unfolded Hoare_gen_def, rule_format, OF Pre]+
−
  obtain k1 where "(q \<and>* c \<and>* r') (recse (run (Suc k1) s'))" by auto+
−
  from h2[unfolded Hoare_gen_def, rule_format, OF this]+
−
  obtain k2 where "(r \<and>* c \<and>* r') (recse (run (Suc k2) (run (Suc k1) s')))" by auto+
−
  thus ?case+
−
    apply (rule_tac x = "Suc (k1 + k2)" in exI)+
−
    by (metis add_Suc_right nat_add_commute sep_exec.run_add)+
−
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>"+
−
proof(induct rule:HoareI)+
−
  case (Pre r' s')+
−
  with h2+
−
  have "(p \<and>* c \<and>* r') (recse s')"+
−
    by (metis sep_conj_impl1)+
−
  from h1[unfolded Hoare_gen_def, rule_format, OF this]+
−
  show ?case .+
−
qed+
−
+
−
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>"+
−
proof(induct rule:HoareI)+
−
  case (Pre r' s')+
−
  from h1[unfolded Hoare_gen_def, rule_format, OF this]+
−
  obtain k where "(q \<and>* c \<and>* r') (recse (run (Suc k) s'))" by blast+
−
  with h2+
−
  show ?case+
−
    by (metis sep_conj_impl1)+
−
qed+
−
+
−
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 (metis)+
−
+
−
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>"+
−
proof(unfold pred_ex_def, 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)+
−
  from h[unfolded Hoare_gen_def, rule_format, OF this]+
−
  show ?case+
−
   by (auto elim!:sep_conjE intro!:sep_conjI)+
−
qed+
−
+
−
lemma code_extension: +
−
  assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"+
−
  shows "\<lbrace> p \<rbrace> c ** e \<lbrace> q \<rbrace>"+
−
proof(induct rule:HoareI)+
−
  case (Pre r' s')+
−
  hence "(p \<and>* c \<and>* e \<and>* r') (recse s')" by (auto simp:sep_conj_ac)+
−
  from h[unfolded Hoare_gen_def, rule_format, OF this]+
−
  show ?case+
−
    by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)+
−
qed+
−
+
−
lemma code_extension1: +
−
  assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"+
−
  shows "\<lbrace> p \<rbrace> e ** c \<lbrace> q \<rbrace>"+
−
  by (metis code_extension h sep.mult_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 ** c2 \<lbrace>r\<rbrace>"+
−
proof(induct rule:HoareI)+
−
  case (Pre r' s')+
−
  hence "(p \<and>* c1 \<and>* c2 \<and>* r') (recse s')" by (auto simp:sep_conj_ac)+
−
  from h1[unfolded Hoare_gen_def, rule_format, OF this]+
−
  obtain k1 where "(q \<and>* c2 \<and>* c1 \<and>* r') (recse (run (Suc k1) s'))" +
−
    by (auto simp:sep_conj_ac)+
−
  from h2[unfolded Hoare_gen_def, rule_format, OF this, folded run_add]+
−
  show ?case+
−
    by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)+
−
qed+
−
+
−
+
−
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 ** 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 ** c2 \<lbrace>R\<rbrace>"+
−
  using h1 h2+
−
by (smt IHoare_def sep_exec.composition)+
−
+
−
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 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 code_condI: +
−
  assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"+
−
  shows "\<lbrace>p\<rbrace> <b>**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 I_code_condI: +
−
  assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"+
−
  shows "I.\<lbrace>P\<rbrace> <b>**c \<lbrace>Q\<rbrace>"+
−
  using h+
−
by (smt IHoareI condD cond_true_eq2 sep.mult_commute sep_conj_cond1)+
−
+
−
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 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 hoare_sep_false: +
−
     "\<lbrace>sep_false\<rbrace> c+
−
      \<lbrace>q\<rbrace>" +
−
  by(unfold Hoare_gen_def, clarify, simp)+
−
+
−
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(simp add:set_ins_def)+
−
  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)+
−
  apply (metis inf_commute)+
−
  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)+
−
  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)+
−
  apply (metis sup_commute)+
−
  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)+
−
  apply (metis (lifting) Un_assoc)+
−
  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)+
−
  apply (metis (lifting) Int_Un_distrib Un_empty inf_sup_distrib1 sup_eq_bot_iff)+
−
  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)+
−
  by (metis (lifting) Int_Un_distrib Int_Un_distrib2 sup_eq_bot_iff)+
−
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+
−
+
−
lemma fam_conj_elm_simp:+
−
  assumes h: "i \<in> I"+
−
  shows "fam_conj I cpt = (cpt(i) \<and>* fam_conj (I - {i}) cpt)"+
−
proof+
−
  fix s+
−
  show "fam_conj I cpt s = (cpt i \<and>* fam_conj (I - {i}) cpt) s"+
−
  proof+
−
    assume pre: "fam_conj I cpt s"+
−
    show "(cpt i \<and>* fam_conj (I - {i}) cpt) s"+
−
    proof -+
−
      from pre obtain p where pres:+
−
            "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+
−
      let ?s = "(\<Union>i\<in>(I - {i}). p i)"+
−
      from pres(3) h have disj: "(p i) ## ?s"+
−
        by (auto simp:set_ins_def)+
−
      moreover from pres(1) h have eq_s: "s = (p i) +  ?s"+
−
        by (auto simp:set_ins_def)+
−
      moreover from pres(2) h have "cpt i (p i)" by auto+
−
      moreover from pres have "(fam_conj (I - {i}) cpt) ?s"+
−
        by (unfold fam_conj_def, rule_tac x = p in exI, auto)+
−
      ultimately show ?thesis by (auto intro!:sep_conjI)+
−
    qed+
−
  next+
−
    let ?fam = "fam_conj (I - {i}) cpt"+
−
    assume "(cpt i \<and>* ?fam) s"+
−
    then obtain s1 s2 where pre:+
−
      "s = s1 + s2" "s1 ## s2" "cpt i s1" "?fam s2"+
−
      by (auto dest!:sep_conjD)+
−
    from pre(4) obtain p where pres:+
−
            "s2 = (\<Union> ia \<in> I - {i}. p(ia))"+
−
            "(\<forall> ia \<in> I - {i}. cpt ia (p ia))"+
−
            "(\<forall> ia \<in> I - {i}. \<forall> j \<in> I - {i}. ia \<noteq> j \<longrightarrow> p(ia) ## p(j))"+
−
      unfolding fam_conj_def by metis+
−
    let ?p = "p(i:=s1)"+
−
    from h pres(3) pre(2)[unfolded pres(1)] +
−
    have " \<forall>ia\<in>I. \<forall>j\<in>I. ia \<noteq> j \<longrightarrow> ?p ia ## ?p j" by  (auto simp:set_ins_def)+
−
    moreover from pres(1) pre(1) h pre(2)+
−
    have "(s = (\<Union> i \<in> I. ?p(i)))" by (auto simp:set_ins_def split:if_splits)+
−
    moreover from pre(3) pres(2) h+
−
    have "(\<forall> i \<in> I. cpt i (?p i))" by (auto simp:set_ins_def split:if_splits)+
−
    ultimately show "fam_conj I cpt s"+
−
      by (unfold fam_conj_def, auto)+
−
  qed+
−
qed+
−
+
−
lemma fam_conj_insert_simp:+
−
  assumes h:"i \<notin> I"+
−
  shows "fam_conj (insert i I) cpt = (cpt(i) \<and>* fam_conj I cpt)"+
−
proof -+
−
  have "i \<in> insert i I" by auto+
−
  from fam_conj_elm_simp[OF this] and h+
−
  show ?thesis by auto+
−
qed+
−
+
−
lemmas fam_conj_simps = fam_conj_insert_simp fam_conj_zero_simp+
−
+
−
lemma "fam_conj {0, 2, 3} cpt = (cpt 2 \<and>* cpt (0::int) \<and>* cpt 3)"+
−
  by (simp add:fam_conj_simps sep_conj_ac)+
−
+
−
lemma fam_conj_ext_eq:+
−
  assumes h: "\<And> i . i \<in> I \<Longrightarrow> f i = g i"+
−
  shows "fam_conj I f = fam_conj I g"+
−
proof+
−
  fix s+
−
  show "fam_conj I f s = fam_conj I g s"+
−
   by (unfold fam_conj_def, auto simp:h)+
−
qed+
−
+
−
end+
−
+
−