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 the allocated addresses to the covered address range. *} definition new_addrs :: "heap ⇒ addr set ⇒ heap ⇒ addr set" where "new_addrs h as h' = as ∪ {a. lim h ≤ a ∧ a < lim h'}" lemma new_addr_refl[simp]: "new_addrs h as h = as" unfolding new_addrs_def by auto 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 information for all addresses. *} 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 ∧ a∉as}) h h' ∧ lim h ≤ lim h')" 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 ∧ a∉as}) 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. h⊨P ⟹ <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=as1∪as2" and DJ: "as1∩as2={}" 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] by (auto simp: in_range.simps new_addrs_def) 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" by (auto simp: new_addrs_def) ultimately show "(the_state σ, new_addrs h as (the_state σ)) ⊨ Q r * R" unfolding times_assn_def apply (simp add: Abs_assn_inverse) 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 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 (simp add: Let_def Abs_assn_inverse) apply (intro allI impI) apply (elim conjE run_elims) apply simp apply (auto simp: new_addrs_def Ref.alloc_def Let_def 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 apply (simp add: Let_def Abs_assn_inverse) apply (auto elim: run_elims simp add: relH_refl in_range.simps new_addrs_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 simp: Let_def Abs_assn_inverse new_addrs_def in_range.simps 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 (simp add: Let_def Abs_assn_inverse) 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 (simp add: Let_def Abs_assn_inverse) 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 (simp add: Let_def Abs_assn_inverse) 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 (simp add: Let_def Abs_assn_inverse) 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 (simp add: Let_def Abs_assn_inverse) 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 (simp add: Let_def Abs_assn_inverse) 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) apply (simp add: in_range.simps) done lemma return_sp_rule: "<P> return x <λr. P * ↑(r = x)>" unfolding hoare_triple_def Let_def apply (simp add: Abs_assn_inverse) apply (auto elim!: run_elims intro!: relH_refl intro: models_in_range) apply (simp add: in_range.simps) 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>" by (simp add: raise_iff) 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 (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 "new_addrs (the_state σ') (new_addrs h as (the_state σ')) (the_state σ'') = new_addrs h as (the_state σ'')" using LIM LIM' by (auto simp add: new_addrs_def) 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' by (auto simp: new_addrs_def) 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