# Theory Separation_Logic_Imperative_HOL.Hoare_Triple

section ‹Hoare-Triples›
theory Hoare_Triple
imports Run Assertions
begin

text ‹In this theory, we define Hoare-Triples, which are our basic tool
for specifying properties of Imperative HOL programs.›

subsection ‹Definition›

text ‹Analyze the heap before and after executing a command, to add
"new_addrs h as h' = as  {a. lim h  a  a < lim h'}"

text ‹
Apart from correctness of the program wrt. the pre- and post condition,
a Hoare-triple also encodes some well-formedness conditions of the command:
The command must not change addresses outside the address range of the
precondition, and it must not decrease the heap limit.

Note that we do not require that the command only reads from heap locations
inside the precondition's address range, as this condition would be quite
complicated to express with the heap model of Imperative/HOL, and is not
necessary in our formalization of partial heaps, that always contain the
›
definition hoare_triple
:: "assn  'a Heap  ('a  assn)  bool" ("<_>/ _/ <_>")
where
"<P> c <Q>  h as σ r. (h,as)P  run c (Some h) σ r
(let h'=the_state σ; as'=new_addrs h as h' in
¬is_exn σ  (h',as')Q r  relH ({a . a<lim h  aas}) h h'
lim h  lim h')"

text ‹Sanity checking theorems for Hoare-Triples›
lemma
assumes "<P> c <Q>"
assumes "(h,as)P"
shows hoare_triple_success: "success c h"
and hoare_triple_effect: "h' r. effect c h h' r  (h',new_addrs h as h')Q r"
using assms
unfolding hoare_triple_def success_def effect_def
apply -
apply (auto simp: Let_def run.simps) apply fastforce
by (metis is_exn.simps(2) not_Some_eq2 the_state.simps)

lemma hoare_tripleD:
fixes h h' as as' σ r
assumes "<P> c <Q>"
assumes "(h,as)P"
assumes "run c (Some h) σ r"
defines "h'the_state σ" and "as'new_addrs h as h'"
shows "¬is_exn σ"
and "(h',as')Q r"
and "relH ({a . a<lim h  aas}) h h'"
and "lim h  lim h'"
using assms
unfolding hoare_triple_def h'_def as'_def
by (auto simp: Let_def)

text ‹For garbage-collected languages, specifications usually allow for some
arbitrary heap parts in the postcondition. The following abbreviation defines
a handy shortcut notation for such specifications.›
abbreviation hoare_triple'
:: "assn  'r Heap  ('r  assn)  bool" ("<_> _ <_>t")
where "<P> c <Q>t  <P> c <λr. Q r * true>"

subsection ‹Rules›
text ‹
In this section, we provide a set of rules to prove Hoare-Triples correct.
›
subsubsection ‹Basic Rules›

lemma hoare_triple_preI:
assumes "h. hP  <P> c <Q>"
shows "<P> c <Q>"
using assms
unfolding hoare_triple_def
by auto

lemma frame_rule:
assumes A: "<P> c <Q>"
shows "<P*R> c <λx. Q x * R>"
unfolding hoare_triple_def Let_def
apply (intro allI impI)
apply (elim conjE)
apply (intro conjI)
proof -
fix h as
assume "(h,as)  P * R"
then obtain as1 as2 where [simp]: "as=as1as2" and DJ: "as1as2={}"
and M1: "(h,as1)P" and M2: "(h,as2)R"
unfolding times_assn_def
by (auto simp: Abs_assn_inverse)

fix σ r
assume RUN: "run c (Some h) σ r"
from hoare_tripleD(1)[OF A M1 RUN] show "¬ is_exn σ" .
from hoare_tripleD(4)[OF A M1 RUN]
show "lim h  lim (the_state σ)" .

from hoare_tripleD(3)[OF A M1 RUN] have
RH1: "relH {a. a < lim h  a  as1} h (the_state σ)" .
moreover have "{a. a < lim h  a  as}  {a. a < lim h  a  as1}"
by auto
ultimately show "relH {a. a < lim h  a  as} h (the_state σ)"
by (blast intro: relH_subset)

from hoare_tripleD(2)[OF A M1 RUN] have
"(the_state σ, new_addrs h as1 (the_state σ))  Q r" .
moreover have DJN: "new_addrs h as1 (the_state σ)  as2 = {}"
using DJ models_in_range[OF M2]
moreover have "as2  {a. a < lim h  a  as1}"
using DJ models_in_range[OF M2]
by (auto simp: in_range.simps)
hence "relH as2 h (the_state σ)" using RH1
by (blast intro: relH_subset)
with M2 have "(the_state σ, as2)R"
by (metis mem_Collect_eq Rep_assn
proper_iff relH_in_rangeI(2))
moreover have "new_addrs h as (the_state σ)
= new_addrs h as1 (the_state σ)  as2"
ultimately show
"(the_state σ, new_addrs h as (the_state σ))  Q r * R"
unfolding times_assn_def
apply blast
done
qed

lemma false_rule[simp, intro!]: "<false> c <Q>"
unfolding hoare_triple_def by simp

lemma cons_rule:
assumes CPRE: "P A P'"
assumes CPOST: "x. Q x A Q' x"
assumes R: "<P'> c <Q>"
shows "<P> c <Q'>"
unfolding hoare_triple_def Let_def
using hoare_tripleD[OF R entailsD[OF CPRE]] entailsD[OF CPOST]
by blast

lemmas cons_pre_rule = cons_rule[OF _ ent_refl]
lemmas cons_post_rule = cons_rule[OF ent_refl, rotated]

lemma cons_rulet: "PtP'; x. Q x t Q' x; <P'> c <Q>t   <P> c <Q'>t"
unfolding entailst_def
apply (rule cons_pre_rule)
apply assumption
apply (rule cons_post_rule)
apply (erule frame_rule)

lemmas cons_pre_rulet = cons_rulet[OF _ entt_refl]
lemmas cons_post_rulet = cons_rulet[OF entt_refl, rotated]

lemma norm_pre_ex_rule:
assumes A: "x. <P x> f <Q>"
shows "<Ax. P x> f <Q>"
unfolding hoare_triple_def Let_def
apply (intro allI impI, elim conjE mod_exE)
using hoare_tripleD[OF A]
by blast

lemma norm_pre_pure_iff[simp]:
"<P*b> f <Q>  (b  <P> f <Q>)"
unfolding hoare_triple_def Let_def
by auto

lemma norm_pre_pure_iff_sng[simp]:
"<b> f <Q>  (b  <emp> f <Q>)"
using norm_pre_pure_iff[where P=emp]
by simp

lemma norm_pre_pure_rule1:
"b  <P> f <Q>  <P*b> f <Q>" by simp

lemma norm_pre_pure_rule2:
" b  <emp> f <Q>   <b> f <Q>" by simp

lemmas norm_pre_pure_rule = norm_pre_pure_rule1 norm_pre_pure_rule2

lemma post_exI_rule: "<P> c <λr. Q r x>  <P> c <λr. Ax. Q r x>"
by (blast intro: cons_post_rule ent_ex_postI ent_refl)

subsubsection ‹Rules for Atomic Commands›
lemma ref_rule:
"<emp> ref x <λr. r r x>"
unfolding one_assn_def sngr_assn_def hoare_triple_def
apply (intro allI impI)
apply (elim conjE run_elims)
apply simp
apply (auto
Ref.set_def Ref.get_def relH_def in_range.simps)
done

lemma lookup_rule:
"<p r x> !p <λr. p r x * (r = x)>"
unfolding hoare_triple_def sngr_assn_def
done

lemma update_rule:
"<p r y> p := x <λr. p r x>"
unfolding hoare_triple_def sngr_assn_def
apply (auto elim!: run_update
intro!: relH_set_ref)
done

lemma update_wp_rule:
"<r r y * ((r r x) -* (Q ()))> r := x <Q>"
apply (rule cons_post_rule)
apply (rule frame_rule[OF update_rule[where p=r and x=x],
where R="((r r x) -* (Q ()))"])
apply (rule ent_trans)
apply (rule ent_mp)
by simp

lemma new_rule:
"<emp> Array.new n x <λr. r a replicate n x>"
unfolding hoare_triple_def snga_assn_def one_assn_def
apply (auto
elim!: run_elims
simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
relH_def in_range.simps
)
done

lemma make_rule: "<emp> Array.make n f <λr. r a (map f [0 ..< n])>"
unfolding hoare_triple_def snga_assn_def one_assn_def
apply (auto
elim!: run_elims
simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
relH_def in_range.simps
)
done

lemma of_list_rule: "<emp> Array.of_list xs <λr. r a xs>"
unfolding hoare_triple_def snga_assn_def one_assn_def
apply (auto
elim!: run_elims
simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
relH_def in_range.simps
)
done

lemma length_rule:
"<a a xs> Array.len a <λr. a a xs * (r = length xs)>"
unfolding hoare_triple_def snga_assn_def
apply (auto
elim!: run_elims
simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
relH_def in_range.simps Array.length_def
)
done

text ‹Note that the Boolean expression is placed at meta level and not
inside the precondition. This makes frame inference simpler.›
lemma nth_rule:
"i < length xs  <a a xs> Array.nth a i <λr. a a xs * (r = xs ! i)>"
unfolding hoare_triple_def snga_assn_def
apply (auto
elim!: run_elims
simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
relH_def in_range.simps Array.length_def
)
done

lemma upd_rule:
"i < length xs
<a a xs>
Array.upd i x a
<λr. (a a (list_update xs i x)) * (r = a)>"
unfolding hoare_triple_def snga_assn_def
apply (auto
elim!: run_elims
simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
relH_def in_range.simps Array.length_def Array.update_def comp_def
)
done

lemma freeze_rule:
"<a a xs> Array.freeze a <λr. a a xs * (r = xs)>"
unfolding hoare_triple_def snga_assn_def
apply (auto
elim!: run_elims
simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
relH_def in_range.simps Array.length_def Array.update_def
)
done

lemma return_wp_rule:
"<Q x> return x <Q>"
unfolding hoare_triple_def Let_def
apply (auto elim!: run_elims)
apply (rule relH_refl)
done

lemma return_sp_rule:
"<P> return x <λr. P * (r = x)>"
unfolding hoare_triple_def Let_def
apply (auto elim!: run_elims intro!: relH_refl intro: models_in_range)
done

lemma raise_iff:
"<P> raise s <Q>  P = false"
unfolding hoare_triple_def Let_def
apply (rule iffI)
apply (unfold bot_assn_def) []
apply rule
apply (auto simp add: run_raise_iff) []

apply (auto simp add: run_raise_iff) []
done

lemma raise_rule: "<false> raise s <Q>"

subsubsection ‹Rules for Composed Commands›
lemma bind_rule:
assumes T1: "<P> f <R>"
assumes T2: "x. <R x> g x <Q>"
shows "<P> bind f g <Q>"
unfolding hoare_triple_def Let_def
apply (intro allI impI)
apply (elim conjE run_elims)
apply (intro conjI)
proof -
fix h as σ'' r'' σ' r'
assume M: "(h,as)  P"
and R1: "run f (Some h) σ' r'"
and R2: "run (g r') σ' σ'' r''"

from hoare_tripleD[OF T1 M R1] have NO_E: "¬ is_exn σ'"
and M': "(the_state σ', new_addrs h as (the_state σ'))  R r'"
and RH': "relH {a. a < lim h  a  as} h (the_state σ')"
and LIM: "lim h  lim (the_state σ')"
by auto

from NO_E have [simp]: "Some (the_state σ') = σ'" by (cases σ') auto

from hoare_tripleD[OF T2 M', simplified, OF R2] have
NO_E'': "¬ is_exn σ''"
and M'': "(the_state σ'',
(new_addrs h as (the_state σ')) (the_state σ''))
Q r''"
and RH'':
"relH
{a. a < lim (the_state σ')
a  new_addrs h as (the_state σ')
}
(the_state σ') (the_state σ'')"
and LIM': "lim (the_state σ')  lim (the_state σ'')" by auto

show "¬ is_exn σ''" by fact

have
(the_state σ')
(the_state σ'')
= new_addrs h as (the_state σ'')"
using LIM LIM'
with M'' show
"(the_state σ'', new_addrs h as (the_state σ''))  Q r''"
by simp

note RH'
also have "relH {a. a < lim h  a  as} (the_state σ') (the_state σ'')"
apply (rule relH_subset[OF RH''])
using LIM LIM'
finally show "relH {a. a < lim h  a  as} h (the_state σ'')" .

note LIM
also note LIM'
finally show "lim h  lim (the_state σ'')" .
qed

lemma if_rule:
assumes  "b  <P> f <Q>"
assumes  "¬b  <P> g <Q>"
shows "<P> if b then f else g <Q>"
using assms by auto

lemma if_rule_split:
assumes  B: "b  <P> f <Q1>"
assumes  NB: "¬b  <P> g <Q2>"
assumes M: "x. (Q1 x * b) A (Q2 x * (¬b)) A Q x"
shows "<P> if b then f else g <Q>"
apply (cases b)
apply simp_all
apply (rule cons_post_rule)
apply (erule B)
apply (rule ent_trans[OF _ ent_disjI1[OF M]])
apply simp

apply (rule cons_post_rule)
apply (erule NB)
apply (rule ent_trans[OF _ ent_disjI2[OF M]])
apply simp
done

lemma split_rule:
assumes P: "<P> c <R>"
assumes Q: "<Q> c <R>"
shows "<P A Q> c <R>"
unfolding hoare_triple_def
apply (intro allI impI)
apply (elim conjE)
apply simp
apply (erule disjE)
using hoare_tripleD[OF P] apply simp
using hoare_tripleD[OF Q] apply simp
done

lemmas decon_if_split = if_rule_split split_rule
― ‹Use with care: Complete splitting of if statements›

lemma case_prod_rule:
"(a b. x = (a, b)  <P> f a b <Q>)  <P> case x of (a, b)  f a b <Q>"
by (auto split: prod.split)

lemma case_list_rule:
" l=[]  <P> fn <Q>; x xs. l=x#xs  <P> fc x xs <Q>
<P> case_list fn fc l <Q>"
by (auto split: list.split)

lemma case_option_rule:
" v=None  <P> fn <Q>; x. v=Some x  <P> fs x <Q>
<P> case_option fn fs v <Q>"
by (auto split: option.split)

lemma case_sum_rule:
" x. v=Inl x  <P> fl x <Q>;
x. v=Inr x  <P> fr x <Q>
<P> case_sum fl fr v <Q>"
by (auto split: sum.split)

lemma let_rule: "(x. x = t  <P> f x <Q>)  <P> Let t f <Q>"
by (auto)

end