thys/Hoare_gen.thy
changeset 0 1378b654acde
child 2 995eb45bbadc
equal deleted inserted replaced
-1:000000000000 0:1378b654acde
       
     1 header {* 
       
     2   Generic Separation Logic
       
     3 *}
       
     4 
       
     5 theory Hoare_gen
       
     6 imports Main  
       
     7   (*"../progtut/Tactical" *)
       
     8   "../Separation_Algebra/Sep_Tactics"
       
     9 begin
       
    10 
       
    11 ML_file "../Separation_Algebra/sep_tactics.ML"
       
    12 
       
    13 definition pasrt :: "bool \<Rightarrow> (('a::sep_algebra) \<Rightarrow> bool)" ("<_>" [72] 71)
       
    14 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"
       
    15 
       
    16 lemma sep_conj_cond1: "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"
       
    17   by(simp add: sep_conj_ac)
       
    18 
       
    19 lemma sep_conj_cond2: "(p \<and>* <cond>) = (<cond> \<and>* p)"
       
    20   by(simp add: sep_conj_ac)
       
    21 
       
    22 lemma sep_conj_cond3: "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)"
       
    23   by (metis sep.mult_assoc)
       
    24 
       
    25 lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3
       
    26 
       
    27 lemma cond_true_eq[simp]: "<True> = \<box>"
       
    28   by(unfold sep_empty_def pasrt_def, auto)
       
    29 
       
    30 lemma cond_true_eq1: "(<True> \<and>* p) = p"
       
    31   by(simp)
       
    32 
       
    33 lemma false_simp [simp]: "<False> = sep_false" (* move *)
       
    34   by (simp add:pasrt_def)
       
    35 
       
    36 lemma cond_true_eq2: "(p \<and>* <True>) = p"
       
    37   by simp
       
    38 
       
    39 lemma condD: "(<b> ** r) s \<Longrightarrow> b \<and> r s" 
       
    40 by (unfold sep_conj_def pasrt_def, auto)
       
    41 
       
    42 locale sep_exec = 
       
    43    fixes step :: "'conf \<Rightarrow> 'conf"
       
    44     and  recse:: "'conf \<Rightarrow> 'a::sep_algebra"
       
    45 begin 
       
    46 
       
    47 definition "run n = step ^^ n"
       
    48 
       
    49 lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"
       
    50   apply (unfold run_def)
       
    51   by (metis funpow_add o_apply)
       
    52 
       
    53 definition
       
    54   Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
       
    55                   ("(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
       
    56 where
       
    57   "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace> \<equiv> 
       
    58       (\<forall> s r. (p**c**r) (recse s) \<longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s)))))"
       
    59 
       
    60 lemma HoareI [case_names Pre]: 
       
    61   assumes h: "\<And> r s. (p**c**r) (recse s) \<Longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s))))"
       
    62   shows "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
       
    63   using h
       
    64   by (unfold Hoare_gen_def, auto)
       
    65 
       
    66 lemma frame_rule: 
       
    67   assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
       
    68   shows "\<lbrace> p ** r \<rbrace> c \<lbrace> q ** r \<rbrace>"
       
    69 proof(induct rule: HoareI)
       
    70   case (Pre r' s')
       
    71   hence "(p \<and>* c \<and>* r \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
       
    72   from h[unfolded Hoare_gen_def, rule_format, OF this]
       
    73   show ?case
       
    74     by (metis sep_conj_assoc sep_conj_left_commute)
       
    75 qed
       
    76 
       
    77 lemma sequencing: 
       
    78   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
       
    79   and h2: "\<lbrace>q\<rbrace> c \<lbrace>r\<rbrace>"
       
    80   shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
       
    81 proof(induct rule:HoareI)
       
    82   case (Pre r' s')
       
    83   from h1[unfolded Hoare_gen_def, rule_format, OF Pre]
       
    84   obtain k1 where "(q \<and>* c \<and>* r') (recse (run (Suc k1) s'))" by auto
       
    85   from h2[unfolded Hoare_gen_def, rule_format, OF this]
       
    86   obtain k2 where "(r \<and>* c \<and>* r') (recse (run (Suc k2) (run (Suc k1) s')))" by auto
       
    87   thus ?case
       
    88     apply (rule_tac x = "Suc (k1 + k2)" in exI)
       
    89     by (metis add_Suc_right nat_add_commute sep_exec.run_add)
       
    90 qed
       
    91 
       
    92 lemma pre_stren: 
       
    93   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
       
    94   and h2:  "\<And>s. r s \<Longrightarrow> p s"
       
    95   shows "\<lbrace>r\<rbrace> c \<lbrace>q\<rbrace>"
       
    96 proof(induct rule:HoareI)
       
    97   case (Pre r' s')
       
    98   with h2
       
    99   have "(p \<and>* c \<and>* r') (recse s')"
       
   100     by (metis sep_conj_impl1)
       
   101   from h1[unfolded Hoare_gen_def, rule_format, OF this]
       
   102   show ?case .
       
   103 qed
       
   104 
       
   105 lemma post_weaken: 
       
   106   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
       
   107     and h2: "\<And> s. q s \<Longrightarrow> r s"
       
   108   shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
       
   109 proof(induct rule:HoareI)
       
   110   case (Pre r' s')
       
   111   from h1[unfolded Hoare_gen_def, rule_format, OF this]
       
   112   obtain k where "(q \<and>* c \<and>* r') (recse (run (Suc k) s'))" by blast
       
   113   with h2
       
   114   show ?case
       
   115     by (metis sep_conj_impl1)
       
   116 qed
       
   117 
       
   118 lemma hoare_adjust:
       
   119   assumes h1: "\<lbrace>p1\<rbrace> c \<lbrace>q1\<rbrace>"
       
   120   and h2: "\<And>s. p s \<Longrightarrow> p1 s"
       
   121   and h3: "\<And>s. q1 s \<Longrightarrow> q s"
       
   122   shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
       
   123   using h1 h2 h3 post_weaken pre_stren
       
   124   by (metis)
       
   125 
       
   126 lemma code_exI: 
       
   127   assumes h: "\<And> k. \<lbrace>p\<rbrace> c(k) \<lbrace>q\<rbrace>"
       
   128   shows "\<lbrace>p\<rbrace> EXS k. c(k) \<lbrace>q\<rbrace>"
       
   129 proof(unfold pred_ex_def, induct rule:HoareI)
       
   130   case (Pre r' s')
       
   131   then obtain k where "(p \<and>* (\<lambda> s. c k s) \<and>* r') (recse s')"
       
   132     by (auto elim!:sep_conjE intro!:sep_conjI)
       
   133   from h[unfolded Hoare_gen_def, rule_format, OF this]
       
   134   show ?case
       
   135    by (auto elim!:sep_conjE intro!:sep_conjI)
       
   136 qed
       
   137 
       
   138 lemma code_extension: 
       
   139   assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
       
   140   shows "\<lbrace> p \<rbrace> c ** e \<lbrace> q \<rbrace>"
       
   141 proof(induct rule:HoareI)
       
   142   case (Pre r' s')
       
   143   hence "(p \<and>* c \<and>* e \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
       
   144   from h[unfolded Hoare_gen_def, rule_format, OF this]
       
   145   show ?case
       
   146     by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
       
   147 qed
       
   148 
       
   149 lemma code_extension1: 
       
   150   assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
       
   151   shows "\<lbrace> p \<rbrace> e ** c \<lbrace> q \<rbrace>"
       
   152   by (metis code_extension h sep.mult_commute)
       
   153 
       
   154 lemma composition: 
       
   155   assumes h1: "\<lbrace>p\<rbrace> c1 \<lbrace>q\<rbrace>"
       
   156     and h2: "\<lbrace>q\<rbrace> c2 \<lbrace>r\<rbrace>"
       
   157   shows "\<lbrace>p\<rbrace> c1 ** c2 \<lbrace>r\<rbrace>"
       
   158 proof(induct rule:HoareI)
       
   159   case (Pre r' s')
       
   160   hence "(p \<and>* c1 \<and>* c2 \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
       
   161   from h1[unfolded Hoare_gen_def, rule_format, OF this]
       
   162   obtain k1 where "(q \<and>* c2 \<and>* c1 \<and>* r') (recse (run (Suc k1) s'))" 
       
   163     by (auto simp:sep_conj_ac)
       
   164   from h2[unfolded Hoare_gen_def, rule_format, OF this, folded run_add]
       
   165   show ?case
       
   166     by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
       
   167 qed
       
   168 
       
   169 
       
   170 definition
       
   171   IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 
       
   172                 ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
       
   173                   ("(1_).(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
       
   174 where
       
   175   "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace> EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c 
       
   176                          \<lbrace> EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)"
       
   177 
       
   178 lemma IHoareI [case_names IPre]: 
       
   179   assumes h: "\<And>s' s r cnf .  (<P s> \<and>* <(s ## s')> \<and>* I(s + s') \<and>* c \<and>* r) (recse cnf) \<Longrightarrow> 
       
   180                    (\<exists>k t. (<Q t> \<and>* <(t ## s')>  \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) cnf)))"
       
   181   shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
       
   182   unfolding IHoare_def
       
   183 proof
       
   184   fix s'
       
   185   show " \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c
       
   186          \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"
       
   187   proof(unfold pred_ex_def, induct rule:HoareI)
       
   188     case (Pre r s)
       
   189     then obtain sa where "(<P sa> \<and>* <(sa ## s')> \<and>* I (sa + s') \<and>* c \<and>* r) (recse s)"
       
   190       by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
       
   191     hence " (\<exists>k t. (<Q t> \<and>* <(t##s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) s)))" 
       
   192       by (rule h)
       
   193     then obtain k t where h2: "(<Q t> \<and>* <(t ## s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) s))"
       
   194       by auto
       
   195     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))"
       
   196       apply (rule_tac x = k in exI)
       
   197       by (auto intro!:sep_conjI elim!:sep_conjE simp:sep_conj_ac)
       
   198     qed
       
   199   qed
       
   200 
       
   201 lemma I_frame_rule: 
       
   202   assumes h: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
       
   203   shows "I. \<lbrace>P \<and>* R\<rbrace> c \<lbrace>Q \<and>* R\<rbrace>"
       
   204 proof(induct rule:IHoareI)
       
   205   case (IPre s' s r cnf)
       
   206   hence "((<(P \<and>* R) s> \<and>* <(s##s')> \<and>* I (s + s')) \<and>* c \<and>* r) (recse cnf)"
       
   207     by (auto simp:sep_conj_ac)
       
   208   then obtain s1 s2 
       
   209   where h1: "((<P s1> \<and>* <((s1 + s2) ## s')> \<and>*I (s1 + s2 + s')) \<and>* c \<and>* r) (recse cnf)" 
       
   210               "s1 ## s2" "s1 + s2 ## s'" "P s1" "R s2"
       
   211     by (unfold pasrt_def, auto elim!:sep_conjE intro!:sep_conjI)
       
   212   hence "((EXS s. <P s> \<and>* <(s ## s2 +s')> \<and>*I (s + (s2 + s'))) \<and>* c \<and>* r) (recse cnf)"
       
   213     apply (sep_cancel, unfold pred_ex_def, auto intro!:sep_conjI sep_disj_addI3 elim!:sep_conjE)
       
   214     apply (rule_tac x = s1 in exI, unfold pasrt_def,
       
   215        auto intro!:sep_conjI sep_disj_addI3 elim!:sep_conjE simp:sep_conj_ac)
       
   216     by (metis sep_add_assoc sep_add_disjD)
       
   217   from h[unfolded IHoare_def Hoare_gen_def, rule_format, OF this]
       
   218   obtain k s where
       
   219      "((<Q s> \<and>* <(s ## s2 + s')> \<and>* I (s + (s2 + s'))) \<and>* c \<and>* r) (recse (run (Suc k) cnf))"
       
   220     by (unfold pasrt_def pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI)
       
   221   thus ?case
       
   222   proof(rule_tac x = k in exI, rule_tac x = "s + s2" in exI, sep_cancel+)
       
   223     fix  h ha
       
   224     assume hh: "(<Q s> \<and>* <(s ## s2 + s')> \<and>* I (s + (s2 + s'))) ha"
       
   225     show " (<(Q \<and>* R) (s + s2)> \<and>* <(s + s2 ## s')> \<and>* I (s + s2 + s')) ha"
       
   226     proof -
       
   227       from hh have h0: "s ## s2 + s'"
       
   228         by (metis pasrt_def sep_conjD)
       
   229       with h1(2, 3)
       
   230       have h2: "s + s2 ## s'" 
       
   231         by (metis sep_add_disjD sep_disj_addI1)
       
   232       moreover from h1(2, 3) h2 have h3: "(s + (s2 + s')) = (s + s2 + s')"
       
   233         by (metis `s ## s2 + s'` sep_add_assoc sep_add_disjD sep_disj_addD1)
       
   234       moreover from hh have "Q s" by (metis pasrt_def sep_conjD)
       
   235       moreover from h0 h1(2) h1(3) have "s ## s2"
       
   236         by (metis sep_add_disjD sep_disj_addD)
       
   237       moreover note h1(5)
       
   238       ultimately show ?thesis
       
   239         by (smt h0 hh sep_conjI)
       
   240     qed
       
   241   qed
       
   242 qed
       
   243 
       
   244 lemma I_sequencing: 
       
   245   assumes h1: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
       
   246   and h2: "I. \<lbrace>Q\<rbrace> c \<lbrace>R\<rbrace>"
       
   247   shows "I. \<lbrace>P\<rbrace> c \<lbrace>R\<rbrace>"
       
   248   using h1 h2 sequencing
       
   249   by (smt IHoare_def)
       
   250 
       
   251 lemma I_pre_stren: 
       
   252   assumes h1: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
       
   253   and h2:  "\<And>s. R s \<Longrightarrow> P s"
       
   254   shows "I. \<lbrace>R\<rbrace> c \<lbrace>Q\<rbrace>"
       
   255 proof(unfold IHoare_def, default)
       
   256   fix s'
       
   257   show "\<lbrace>EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c 
       
   258        \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"
       
   259   proof(rule pre_stren)
       
   260     from h1[unfolded IHoare_def, rule_format, of s']
       
   261     show "\<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c 
       
   262           \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" .
       
   263   next
       
   264     fix s
       
   265     show "(EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')) s \<Longrightarrow> 
       
   266             (EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')) s"
       
   267       apply (unfold pred_ex_def, clarify)
       
   268       apply (rule_tac x = sa in exI, sep_cancel+)
       
   269       by (insert h2, auto simp:pasrt_def)
       
   270   qed
       
   271 qed
       
   272 
       
   273 lemma I_post_weaken: 
       
   274   assumes h1: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
       
   275     and h2: "\<And> s. Q s \<Longrightarrow> R s"
       
   276   shows "I. \<lbrace>P\<rbrace> c \<lbrace>R\<rbrace>"
       
   277 proof(unfold IHoare_def, default)
       
   278   fix s'
       
   279   show "\<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c 
       
   280         \<lbrace>EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"
       
   281   proof(rule post_weaken)
       
   282     from h1[unfolded IHoare_def, rule_format, of s']
       
   283     show "\<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c 
       
   284           \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" .
       
   285   next
       
   286     fix s
       
   287     show "(EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')) s \<Longrightarrow> 
       
   288           (EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')) s"
       
   289       apply (unfold pred_ex_def, clarify)
       
   290       apply (rule_tac x = sa in exI, sep_cancel+)
       
   291       by (insert h2, auto simp:pasrt_def)
       
   292   qed
       
   293 qed
       
   294 
       
   295 lemma I_hoare_adjust:
       
   296   assumes h1: "I. \<lbrace>P1\<rbrace> c \<lbrace>Q1\<rbrace>"
       
   297   and h2: "\<And>s. P s \<Longrightarrow> P1 s"
       
   298   and h3: "\<And>s. Q1 s \<Longrightarrow> Q s"
       
   299   shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
       
   300   using h1 h2 h3 I_post_weaken I_pre_stren
       
   301   by (metis)
       
   302 
       
   303 lemma I_code_exI: 
       
   304   assumes h: "\<And> k. I. \<lbrace>P\<rbrace> c(k) \<lbrace>Q\<rbrace>"
       
   305   shows "I. \<lbrace>P\<rbrace> EXS k. c(k) \<lbrace>Q\<rbrace>"
       
   306 using h
       
   307 by (smt IHoare_def code_exI)
       
   308 
       
   309 lemma I_code_extension: 
       
   310   assumes h: "I. \<lbrace> P \<rbrace> c \<lbrace> Q \<rbrace>"
       
   311   shows "I. \<lbrace> P \<rbrace> c ** e \<lbrace> Q \<rbrace>"
       
   312   using h
       
   313   by (smt IHoare_def sep_exec.code_extension)
       
   314 
       
   315 lemma I_composition: 
       
   316   assumes h1: "I. \<lbrace>P\<rbrace> c1 \<lbrace>Q\<rbrace>"
       
   317     and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>"
       
   318   shows "I. \<lbrace>P\<rbrace> c1 ** c2 \<lbrace>R\<rbrace>"
       
   319   using h1 h2
       
   320 by (smt IHoare_def sep_exec.composition)
       
   321 
       
   322 lemma pre_condI: 
       
   323   assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" 
       
   324   shows "\<lbrace><cond> \<and>* p\<rbrace> c \<lbrace>q\<rbrace>"
       
   325 proof(induct rule:HoareI)
       
   326   case (Pre r s)
       
   327   hence "cond" "(p \<and>* c \<and>* r) (recse s)"
       
   328     apply (metis pasrt_def sep_conjD)
       
   329     by (smt Pre.hyps pasrt_def sep_add_zero sep_conj_commute sep_conj_def)
       
   330   from h[OF this(1), unfolded Hoare_gen_def, rule_format, OF this(2)]
       
   331   show ?case .
       
   332 qed
       
   333 
       
   334 lemma I_pre_condI: 
       
   335   assumes h: "cond \<Longrightarrow> I.\<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" 
       
   336   shows "I.\<lbrace><cond> \<and>* P\<rbrace> c \<lbrace>Q\<rbrace>"
       
   337   using h
       
   338 by (smt IHoareI condD cond_true_eq2 sep.mult_commute)
       
   339 
       
   340 lemma code_condI: 
       
   341   assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
       
   342   shows "\<lbrace>p\<rbrace> <b>**c \<lbrace>q\<rbrace>"
       
   343 proof(induct rule: HoareI)
       
   344   case (Pre r s)
       
   345   hence h1: "b" "(p \<and>* c \<and>* r) (recse s)"
       
   346     apply (metis condD sep_conjD sep_conj_assoc)
       
   347     by (smt Pre.hyps condD sep_conj_impl)
       
   348   from h[OF h1(1), unfolded Hoare_gen_def, rule_format, OF h1(2)]
       
   349   and h1(1)
       
   350   show ?case
       
   351     by (metis (full_types) cond_true_eq1)
       
   352 qed
       
   353 
       
   354 lemma I_code_condI: 
       
   355   assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
       
   356   shows "I.\<lbrace>P\<rbrace> <b>**c \<lbrace>Q\<rbrace>"
       
   357   using h
       
   358 by (smt IHoareI condD cond_true_eq2 sep.mult_commute sep_conj_cond1)
       
   359 
       
   360 lemma precond_exI: 
       
   361   assumes h:"\<And>x. \<lbrace>p x\<rbrace> c \<lbrace>q\<rbrace>"
       
   362   shows "\<lbrace>EXS x. p x\<rbrace> c \<lbrace>q\<rbrace>"
       
   363 proof(induct rule:HoareI)
       
   364   case (Pre r s)
       
   365   then obtain x where "(p x \<and>* c \<and>* r) (recse s)"
       
   366     by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI)
       
   367   from h[of x, unfolded Hoare_gen_def, rule_format, OF this]  
       
   368   show ?case .
       
   369 qed
       
   370 
       
   371 lemma I_precond_exI: 
       
   372   assumes h:"\<And>x. I. \<lbrace>P x\<rbrace> c \<lbrace>Q\<rbrace>"
       
   373   shows "I.\<lbrace>EXS x. P x\<rbrace> c \<lbrace>Q\<rbrace>"
       
   374 proof(induct rule:IHoareI)
       
   375   case (IPre s' s r cnf)
       
   376   then obtain x
       
   377     where "((EXS s. <P x s> \<and>* <(s ## s')> \<and>* I (s + s')) \<and>* c \<and>* r) (recse cnf)"
       
   378     by ( auto elim!:sep_conjE intro!:sep_conjI simp:pred_ex_def pasrt_def sep_conj_ac)
       
   379   from h[unfolded IHoare_def Hoare_gen_def, rule_format, OF this]
       
   380   obtain k t 
       
   381     where "((<Q t> \<and>* <(t ## s')> \<and>* I (t + s')) \<and>* c \<and>* r) (recse (run (Suc k) cnf))"
       
   382     by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI)
       
   383   thus ?case 
       
   384     by (auto simp:sep_conj_ac)
       
   385 qed
       
   386 
       
   387 lemma hoare_sep_false: 
       
   388      "\<lbrace>sep_false\<rbrace> c
       
   389       \<lbrace>q\<rbrace>" 
       
   390   by(unfold Hoare_gen_def, clarify, simp)
       
   391 
       
   392 lemma I_hoare_sep_false:
       
   393   "I. \<lbrace>sep_false\<rbrace> c
       
   394       \<lbrace>Q\<rbrace>"
       
   395 by (smt IHoareI condD)
       
   396 
       
   397 end
       
   398 
       
   399 instantiation set :: (type)sep_algebra
       
   400 begin
       
   401 
       
   402 definition set_zero_def: "0 = {}"
       
   403 
       
   404 definition plus_set_def: "s1 + s2 = s1 \<union> s2"
       
   405 
       
   406 definition sep_disj_set_def: "sep_disj s1 s2 = (s1 \<inter> s2 = {})"
       
   407 
       
   408 lemmas set_ins_def = sep_disj_set_def plus_set_def set_zero_def
       
   409 
       
   410 instance
       
   411   apply(default)
       
   412   apply(simp add:set_ins_def)
       
   413   apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
       
   414   apply (metis inf_commute)
       
   415   apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
       
   416   apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
       
   417   apply (metis sup_commute)
       
   418   apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
       
   419   apply (metis (lifting) Un_assoc)
       
   420   apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
       
   421   apply (metis (lifting) Int_Un_distrib Un_empty inf_sup_distrib1 sup_eq_bot_iff)
       
   422   apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
       
   423   by (metis (lifting) Int_Un_distrib Int_Un_distrib2 sup_eq_bot_iff)
       
   424 end
       
   425 
       
   426 section {* A big operator of infinite separation conjunction *}
       
   427 
       
   428 definition "fam_conj I cpt s = (\<exists> p. (s = (\<Union> i \<in> I. p(i))) \<and>
       
   429                                      (\<forall> i \<in> I. cpt i (p i)) \<and>
       
   430                                      (\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> p(i) ## p(j)))"
       
   431 
       
   432 lemma fam_conj_zero_simp: "fam_conj {} cpt = <True>"
       
   433 proof
       
   434   fix s
       
   435   show "fam_conj {} cpt s = (<True>) s"
       
   436   proof
       
   437     assume "fam_conj {} cpt s"
       
   438     then obtain p where "s = (\<Union> i \<in> {}. p(i))"
       
   439       by (unfold fam_conj_def, auto)
       
   440     hence "s = {}" by auto
       
   441     thus "(<True>) s" by (metis pasrt_def set_zero_def) 
       
   442   next
       
   443     assume "(<True>) s"
       
   444     hence eq_s: "s = {}" by (metis pasrt_def set_zero_def)
       
   445     let ?p = "\<lambda> i. {}"
       
   446     have "(s = (\<Union> i \<in> {}. ?p(i)))" by (unfold eq_s, auto)
       
   447     moreover have "(\<forall> i \<in> {}. cpt i (?p i))" by auto
       
   448     moreover have "(\<forall> i \<in> {}. \<forall> j \<in> {}. i \<noteq> j \<longrightarrow> ?p(i) ## ?p(j))" by auto
       
   449     ultimately show "fam_conj {} cpt s"
       
   450       by (unfold eq_s fam_conj_def, auto)
       
   451   qed
       
   452 qed
       
   453 
       
   454 lemma fam_conj_disj_simp_pre:
       
   455   assumes h1: "I = I1 + I2"
       
   456   and h2: "I1 ## I2"
       
   457   shows "fam_conj I cpt = (fam_conj I1 cpt \<and>* fam_conj I2 cpt)"
       
   458 proof
       
   459   fix s
       
   460   let ?fm = "fam_conj I cpt" and ?fm1 = "fam_conj I1 cpt" and ?fm2 = "fam_conj I2 cpt"
       
   461   show "?fm s = (?fm1 \<and>* ?fm2) s"
       
   462   proof
       
   463     assume "?fm s"
       
   464     then obtain p where pre:
       
   465             "s = (\<Union> i \<in> I. p(i))"
       
   466             "(\<forall> i \<in> I. cpt i (p i))"
       
   467             "(\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> p(i) ## p(j))"
       
   468       unfolding fam_conj_def by metis
       
   469     from pre(1) h1 h2 have "s = (\<Union> i \<in> I1. p(i)) + (\<Union> i \<in> I2. p(i))"
       
   470       by (auto simp:set_ins_def)
       
   471     moreover from pre h1 have "?fm1 (\<Union> i \<in> I1. p(i))"
       
   472       by (unfold fam_conj_def, rule_tac x = p in exI, auto simp:set_ins_def)
       
   473     moreover from pre h1 have "?fm2 (\<Union> i \<in> I2. p(i))"
       
   474       by (unfold fam_conj_def, rule_tac x = p in exI, auto simp:set_ins_def)
       
   475     moreover have "(\<Union> i \<in> I1. p(i)) ## (\<Union> i \<in> I2. p(i))"
       
   476     proof -
       
   477       { fix x xa xb
       
   478         assume h: "I1 \<inter> I2 = {}"
       
   479                   "\<forall>i\<in>I1 \<union> I2. \<forall>j\<in>I1 \<union> I2. i \<noteq> j \<longrightarrow> p i \<inter> p j = {}"
       
   480                   "xa \<in> I1" "x \<in> p xa" "xb \<in> I2" "x \<in> p xb"
       
   481         have "p xa \<inter> p xb = {}"
       
   482         proof(rule h(2)[rule_format])
       
   483           from h(1, 3, 5) show "xa \<in> I1 \<union> I2" by auto
       
   484         next
       
   485           from h(1, 3, 5) show "xb \<in> I1 \<union> I2" by auto
       
   486         next
       
   487           from h(1, 3, 5) show "xa \<noteq> xb" by auto
       
   488         qed with h(4, 6) have False by auto
       
   489       } with h1 h2 pre(3) show ?thesis by (auto simp:set_ins_def) 
       
   490     qed
       
   491     ultimately show "(?fm1 \<and>* ?fm2) s" by (auto intro!:sep_conjI)
       
   492   next
       
   493     assume "(?fm1 \<and>* ?fm2) s"
       
   494     then obtain s1 s2 where pre:
       
   495       "s = s1 + s2" "s1 ## s2" "?fm1 s1" "?fm2 s2"
       
   496       by (auto dest!:sep_conjD)
       
   497     from pre(3) obtain p1 where pre1:
       
   498             "s1 = (\<Union> i \<in> I1. p1(i))"
       
   499             "(\<forall> i \<in> I1. cpt i (p1 i))"
       
   500             "(\<forall> i \<in> I1. \<forall> j \<in> I1. i \<noteq> j \<longrightarrow> p1(i) ## p1(j))"
       
   501        unfolding fam_conj_def by metis
       
   502     from pre(4) obtain p2 where pre2:
       
   503             "s2 = (\<Union> i \<in> I2. p2(i))"
       
   504             "(\<forall> i \<in> I2. cpt i (p2 i))"
       
   505             "(\<forall> i \<in> I2. \<forall> j \<in> I2. i \<noteq> j \<longrightarrow> p2(i) ## p2(j))"
       
   506        unfolding fam_conj_def by metis
       
   507      let ?p = "\<lambda> i. if i \<in> I1 then p1 i else p2 i"
       
   508      from h2 pre(2)
       
   509      have "s = (\<Union> i \<in> I. ?p(i))" 
       
   510        apply (unfold h1 pre(1) pre1(1) pre2(1) set_ins_def, auto split:if_splits)
       
   511        by (metis disjoint_iff_not_equal)
       
   512      moreover from h2 pre1(2) pre2(2) have "(\<forall> i \<in> I. cpt i (?p i))" 
       
   513        by (unfold h1 set_ins_def, auto split:if_splits)
       
   514      moreover from pre1(1, 3) pre2(1, 3) pre(2) h2
       
   515      have "(\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> ?p(i) ## ?p(j))" 
       
   516        apply (unfold h1 set_ins_def, auto split:if_splits)
       
   517        by (metis IntI empty_iff)
       
   518      ultimately show "?fm s" by (unfold fam_conj_def, auto)
       
   519   qed
       
   520 qed
       
   521 
       
   522 lemma fam_conj_disj_simp:
       
   523   assumes h: "I1 ## I2"
       
   524   shows "fam_conj (I1 + I2) cpt = (fam_conj I1 cpt \<and>* fam_conj I2 cpt)"
       
   525 proof -
       
   526   from fam_conj_disj_simp_pre[OF _ h, of "I1 + I2"]
       
   527   show ?thesis by simp
       
   528 qed
       
   529 
       
   530 lemma fam_conj_elm_simp:
       
   531   assumes h: "i \<in> I"
       
   532   shows "fam_conj I cpt = (cpt(i) \<and>* fam_conj (I - {i}) cpt)"
       
   533 proof
       
   534   fix s
       
   535   show "fam_conj I cpt s = (cpt i \<and>* fam_conj (I - {i}) cpt) s"
       
   536   proof
       
   537     assume pre: "fam_conj I cpt s"
       
   538     show "(cpt i \<and>* fam_conj (I - {i}) cpt) s"
       
   539     proof -
       
   540       from pre obtain p where pres:
       
   541             "s = (\<Union> i \<in> I. p(i))"
       
   542             "(\<forall> i \<in> I. cpt i (p i))"
       
   543             "(\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> p(i) ## p(j))"
       
   544         unfolding fam_conj_def by metis
       
   545       let ?s = "(\<Union>i\<in>(I - {i}). p i)"
       
   546       from pres(3) h have disj: "(p i) ## ?s"
       
   547         by (auto simp:set_ins_def)
       
   548       moreover from pres(1) h have eq_s: "s = (p i) +  ?s"
       
   549         by (auto simp:set_ins_def)
       
   550       moreover from pres(2) h have "cpt i (p i)" by auto
       
   551       moreover from pres have "(fam_conj (I - {i}) cpt) ?s"
       
   552         by (unfold fam_conj_def, rule_tac x = p in exI, auto)
       
   553       ultimately show ?thesis by (auto intro!:sep_conjI)
       
   554     qed
       
   555   next
       
   556     let ?fam = "fam_conj (I - {i}) cpt"
       
   557     assume "(cpt i \<and>* ?fam) s"
       
   558     then obtain s1 s2 where pre:
       
   559       "s = s1 + s2" "s1 ## s2" "cpt i s1" "?fam s2"
       
   560       by (auto dest!:sep_conjD)
       
   561     from pre(4) obtain p where pres:
       
   562             "s2 = (\<Union> ia \<in> I - {i}. p(ia))"
       
   563             "(\<forall> ia \<in> I - {i}. cpt ia (p ia))"
       
   564             "(\<forall> ia \<in> I - {i}. \<forall> j \<in> I - {i}. ia \<noteq> j \<longrightarrow> p(ia) ## p(j))"
       
   565       unfolding fam_conj_def by metis
       
   566     let ?p = "p(i:=s1)"
       
   567     from h pres(3) pre(2)[unfolded pres(1)] 
       
   568     have " \<forall>ia\<in>I. \<forall>j\<in>I. ia \<noteq> j \<longrightarrow> ?p ia ## ?p j" by  (auto simp:set_ins_def)
       
   569     moreover from pres(1) pre(1) h pre(2)
       
   570     have "(s = (\<Union> i \<in> I. ?p(i)))" by (auto simp:set_ins_def split:if_splits)
       
   571     moreover from pre(3) pres(2) h
       
   572     have "(\<forall> i \<in> I. cpt i (?p i))" by (auto simp:set_ins_def split:if_splits)
       
   573     ultimately show "fam_conj I cpt s"
       
   574       by (unfold fam_conj_def, auto)
       
   575   qed
       
   576 qed
       
   577 
       
   578 lemma fam_conj_insert_simp:
       
   579   assumes h:"i \<notin> I"
       
   580   shows "fam_conj (insert i I) cpt = (cpt(i) \<and>* fam_conj I cpt)"
       
   581 proof -
       
   582   have "i \<in> insert i I" by auto
       
   583   from fam_conj_elm_simp[OF this] and h
       
   584   show ?thesis by auto
       
   585 qed
       
   586 
       
   587 lemmas fam_conj_simps = fam_conj_insert_simp fam_conj_zero_simp
       
   588 
       
   589 lemma "fam_conj {0, 2, 3} cpt = (cpt 2 \<and>* cpt (0::int) \<and>* cpt 3)"
       
   590   by (simp add:fam_conj_simps sep_conj_ac)
       
   591 
       
   592 lemma fam_conj_ext_eq:
       
   593   assumes h: "\<And> i . i \<in> I \<Longrightarrow> f i = g i"
       
   594   shows "fam_conj I f = fam_conj I g"
       
   595 proof
       
   596   fix s
       
   597   show "fam_conj I f s = fam_conj I g s"
       
   598    by (unfold fam_conj_def, auto simp:h)
       
   599 qed
       
   600 
       
   601 end
       
   602