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
  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')"

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 ∧ 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 cons_rulet: "⟦P⟹⇩tP'; ⋀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)
  by (simp add: enttD enttI)  

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 (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 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 (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