Theory SepAuto

(*
  File: SepAuto.thy
  Author: Bohua Zhan
*)

section ‹Separation logic›

theory SepAuto
  imports SepLogic_Base "HOL-Imperative_HOL.Imperative_HOL"
begin

text ‹
  Separation logic for Imperative\_HOL, and setup of auto2. The development of
  separation logic here follows \<^cite>‹"Separation_Logic_Imperative_HOL-AFP"› by Lammich and Meis.
›

subsection ‹Partial Heaps›

datatype pheap = pHeap (heapOf: heap) (addrOf: "addr set")
setup ‹add_simple_datatype "pheap"›

fun in_range :: "(heap × addr set) ⇒ bool" where
  "in_range (h,as) ⟷ (∀a∈as. a < lim h)"
setup ‹add_rewrite_rule @{thm in_range.simps}›

text ‹Two heaps agree on a set of addresses.›
definition relH :: "addr set ⇒ heap ⇒ heap ⇒ bool" where [rewrite]:
  "relH as h h' = (in_range (h, as) ∧ in_range (h', as) ∧
     (∀t. ∀a∈as. refs h t a = refs h' t a ∧ arrays h t a = arrays h' t a))"

lemma relH_D [forward]:
  "relH as h h' ⟹ in_range (h, as) ∧ in_range (h', as)" by auto2

lemma relH_D2 [rewrite]:
  "relH as h h' ⟹ a ∈ as ⟹ refs h t a = refs h' t a"
  "relH as h h' ⟹ a ∈ as ⟹ arrays h t a = arrays h' t a" by auto2+
setup ‹del_prfstep_thm_eqforward @{thm relH_def}›

lemma relH_dist_union [forward]:
  "relH (as ∪ as') h h' ⟹ relH as h h' ∧ relH as' h h'" by auto2

lemma relH_ref [rewrite]:
  "relH as h h' ⟹ addr_of_ref r ∈ as ⟹ Ref.get h r = Ref.get h' r"
  by (auto intro: relH_D2 arg_cong simp: Ref.get_def)

lemma relH_array [rewrite]:
  "relH as h h' ⟹ addr_of_array r ∈ as ⟹ Array.get h r = Array.get h' r"
  by (auto intro: relH_D2 arg_cong simp: Array.get_def)

lemma relH_set_ref [resolve]:
  "relH {a. a < lim h ∧ a ∉ {addr_of_ref r}} h (Ref.set r x h)"
  by (simp add: Ref.set_def relH_def)

lemma relH_set_array [resolve]:
  "relH {a. a < lim h ∧ a ∉ {addr_of_array r}} h (Array.set r x h)"
  by (simp add: Array.set_def relH_def)

subsection ‹Assertions›

datatype assn_raw = Assn (assn_fn: "pheap ⇒ bool")

fun aseval :: "assn_raw ⇒ pheap ⇒ bool" where
  "aseval (Assn f) h = f h"
setup ‹add_rewrite_rule @{thm aseval.simps}›

definition proper :: "assn_raw ⇒ bool" where [rewrite]:
  "proper P = (
    (∀h as. aseval P (pHeap h as) ⟶ in_range (h,as)) ∧
    (∀h h' as. aseval P (pHeap h as) ⟶ relH as h h' ⟶ in_range (h',as) ⟶ aseval P (pHeap h' as)))"

fun in_range_assn :: "pheap ⇒ bool" where
  "in_range_assn (pHeap h as) ⟷ (∀a∈as. a < lim h)"
setup ‹add_rewrite_rule @{thm in_range_assn.simps}›

typedef assn = "Collect proper"
@proof @have "Assn in_range_assn ∈ Collect proper" @qed

setup ‹add_rewrite_rule @{thm Rep_assn_inject}›
setup ‹register_wellform_data ("Abs_assn P", ["proper P"])›
setup ‹add_prfstep_check_req ("Abs_assn P", "proper P")›

lemma Abs_assn_inverse' [rewrite]: "proper y ⟹ Rep_assn (Abs_assn y) = y"
  by (simp add: Abs_assn_inverse)

lemma proper_Rep_assn [forward]: "proper (Rep_assn P)" using Rep_assn by auto

definition models :: "pheap ⇒ assn ⇒ bool" (infix "⊨" 50) where [rewrite_bidir]:
  "h ⊨ P ⟷ aseval (Rep_assn P) h"

lemma models_in_range [resolve]: "pHeap h as ⊨ P ⟹ in_range (h,as)" by auto2

lemma mod_relH [forward]: "relH as h h' ⟹ pHeap h as ⊨ P ⟹ pHeap h' as ⊨ P" by auto2

instantiation assn :: one begin
definition one_assn :: assn where [rewrite]:
  "1 ≡ Abs_assn (Assn (λh. addrOf h = {}))"
instance .. end

abbreviation one_assn :: assn ("emp") where "one_assn ≡ 1"

lemma one_assn_rule [rewrite]: "h ⊨ emp ⟷ addrOf h = {}" by auto2
setup ‹del_prfstep_thm @{thm one_assn_def}›

instantiation assn :: times begin
definition times_assn where [rewrite]:
  "P * Q = Abs_assn (Assn (
    λh. (∃as1 as2. addrOf h = as1 ∪ as2 ∧ as1 ∩ as2 = {} ∧
                   aseval (Rep_assn P) (pHeap (heapOf h) as1) ∧ aseval (Rep_assn Q) (pHeap (heapOf h) as2))))"
instance .. end

lemma mod_star_conv [rewrite]:
  "pHeap h as ⊨ A * B ⟷ (∃as1 as2. as = as1 ∪ as2 ∧ as1 ∩ as2 = {} ∧ pHeap h as1 ⊨ A ∧ pHeap h as2 ⊨ B)" by auto2
setup ‹del_prfstep_thm @{thm times_assn_def}›

lemma aseval_ext [backward]: "∀h. aseval P h = aseval P' h ⟹ P = P'"
  apply (cases P) apply (cases P') by auto

lemma assn_ext: "∀h as. pHeap h as ⊨ P ⟷ pHeap h as ⊨ Q ⟹ P = Q"
@proof @have "Rep_assn P = Rep_assn Q" @qed
setup ‹add_backward_prfstep_cond @{thm assn_ext} [with_filt (order_filter "P" "Q")]›

setup ‹del_prfstep_thm @{thm aseval_ext}›

lemma assn_one_left: "1 * P = (P::assn)"
@proof
  @have "∀h as. pHeap h as ⊨ P ⟷ pHeap h as ⊨ 1 * P" @with
    @have "as = {} ∪ as"
  @end
@qed

lemma assn_times_comm: "P * Q = Q * (P::assn)"
@proof
  @have "∀h as. pHeap h as ⊨ P * Q ⟷ pHeap h as ⊨ Q * P" @with
    @case "pHeap h as ⊨ P * Q" @with
      @obtain as1 as2 where "as = as1 ∪ as2" "as1 ∩ as2 = {}" "pHeap h as1 ⊨ P" "pHeap h as2 ⊨ Q"
      @have "as = as2 ∪ as1"
    @end
    @case "pHeap h as ⊨ Q * P" @with
      @obtain as1 as2 where "as = as1 ∪ as2" "as1 ∩ as2 = {}" "pHeap h as1 ⊨ Q" "pHeap h as2 ⊨ P"
      @have "as = as2 ∪ as1"
    @end
  @end
@qed

lemma assn_times_assoc: "(P * Q) * R = P * (Q * (R::assn))"
@proof
  @have "∀h as. pHeap h as ⊨ (P * Q) * R ⟷ pHeap h as ⊨ P * (Q * R)" @with
    @case "pHeap h as ⊨ (P * Q) * R" @with
      @obtain as1 as2 where "as = as1 ∪ as2" "as1 ∩ as2 = {}" "pHeap h as1 ⊨ P * Q" "pHeap h as2 ⊨ R"
      @obtain as11 as12 where "as1 = as11 ∪ as12" "as11 ∩ as12 = {}" "pHeap h as11 ⊨ P" "pHeap h as12 ⊨ Q"
      @have "as = as11 ∪ (as12 ∪ as2)"
    @end
    @case "pHeap h as ⊨ P * (Q * R)" @with
      @obtain as1 as2 where "as = as1 ∪ as2" "as1 ∩ as2 = {}" "pHeap h as1 ⊨ P" "pHeap h as2 ⊨ Q * R"
      @obtain as21 as22 where "as2 = as21 ∪ as22" "as21 ∩ as22 = {}" "pHeap h as21 ⊨ Q" "pHeap h as22 ⊨ R"
      @have "as = (as1 ∪ as21) ∪ as22"
    @end
  @end
@qed

instantiation assn :: comm_monoid_mult begin
  instance apply standard
  apply (rule assn_times_assoc) apply (rule assn_times_comm) by (rule assn_one_left)
end

subsubsection ‹Existential Quantification›

definition ex_assn :: "('a ⇒ assn) ⇒ assn" (binder "∃⇩A" 11) where [rewrite]:
  "(∃⇩Ax. P x) = Abs_assn (Assn (λh. ∃x. h ⊨ P x))"

lemma mod_ex_dist [rewrite]: "(h ⊨ (∃⇩Ax. P x)) ⟷ (∃x. h ⊨ P x)" by auto2
setup ‹del_prfstep_thm @{thm ex_assn_def}›

lemma ex_distrib_star: "(∃⇩Ax. P x * Q) = (∃⇩Ax. P x) * Q"
@proof
  @have "∀h as. pHeap h as ⊨ (∃⇩Ax. P x) * Q ⟷ pHeap h as ⊨ (∃⇩Ax. P x * Q)" @with
    @case "pHeap h as ⊨ (∃⇩Ax. P x) * Q" @with
      @obtain as1 as2 where "as = as1 ∪ as2" "as1 ∩ as2 = {}" "pHeap h as1 ⊨ (∃⇩Ax. P x)" "pHeap h as2 ⊨ Q"
      @obtain x where "pHeap h as1 ⊨ P x"
      @have "pHeap h as ⊨ P x * Q"
    @end
  @end
@qed

subsubsection ‹Pointers›

definition sngr_assn :: "'a::heap ref ⇒ 'a ⇒ assn" (infix "↦⇩r" 82) where [rewrite]:
  "r ↦⇩r x = Abs_assn (Assn (
    λh. Ref.get (heapOf h) r = x ∧ addrOf h = {addr_of_ref r} ∧ addr_of_ref r < lim (heapOf h)))"

lemma sngr_assn_rule [rewrite]:
  "pHeap h as ⊨ r ↦⇩r x ⟷ (Ref.get h r = x ∧ as = {addr_of_ref r} ∧ addr_of_ref r < lim h)" by auto2
setup ‹del_prfstep_thm @{thm sngr_assn_def}›

definition snga_assn :: "'a::heap array ⇒ 'a list ⇒ assn" (infix "↦⇩a" 82) where [rewrite]:
  "r ↦⇩a x = Abs_assn (Assn (
    λh. Array.get (heapOf h) r = x ∧ addrOf h = {addr_of_array r} ∧ addr_of_array r < lim (heapOf h)))"

lemma snga_assn_rule [rewrite]:
  "pHeap h as ⊨ r ↦⇩a x ⟷ (Array.get h r = x ∧ as = {addr_of_array r} ∧ addr_of_array r < lim h)" by auto2
setup ‹del_prfstep_thm @{thm snga_assn_def}›

subsubsection ‹Pure Assertions›

definition pure_assn :: "bool ⇒ assn" ("↑") where [rewrite]:
  "↑b = Abs_assn (Assn (λh. addrOf h = {} ∧ b))"

lemma pure_assn_rule [rewrite]: "h ⊨ ↑b ⟷ (addrOf h = {} ∧ b)" by auto2
setup ‹del_prfstep_thm @{thm pure_assn_def}›

definition top_assn :: assn ("true") where [rewrite]:
  "top_assn = Abs_assn (Assn in_range_assn)"

lemma top_assn_rule [rewrite]: "pHeap h as ⊨ true ⟷ in_range (h, as)" by auto2
setup ‹del_prfstep_thm @{thm top_assn_def}›

setup ‹del_prfstep_thm @{thm models_def}›

subsubsection ‹Properties of assertions›

abbreviation bot_assn :: assn ("false") where "bot_assn ≡ ↑False"

lemma top_assn_reduce: "true * true = true"
@proof
  @have "∀h. h ⊨ true ⟷ h ⊨ true * true" @with
    @have "addrOf h = addrOf h ∪ {}"
  @end
@qed

lemma mod_pure_star_dist [rewrite]:
  "h ⊨ P * ↑b ⟷ (h ⊨ P ∧ b)"
@proof
  @case "h ⊨ P ∧ b" @with
    @have "addrOf h = addrOf h ∪ {}"
  @end
@qed

lemma pure_conj: "↑(P ∧ Q) = ↑P * ↑Q" by auto2

subsubsection ‹Entailment and its properties›

definition entails :: "assn ⇒ assn ⇒ bool" (infix "⟹⇩A" 10) where [rewrite]:
  "(P ⟹⇩A Q) ⟷ (∀h. h ⊨ P ⟶ h ⊨ Q)"

lemma entails_triv: "A ⟹⇩A A" by auto2
lemma entails_true: "A ⟹⇩A true" by auto2
lemma entails_frame [backward]: "P ⟹⇩A Q ⟹ P * R ⟹⇩A Q * R" by auto2
lemma entails_frame': "¬ (A * F ⟹⇩A Q) ⟹ A ⟹⇩A B ⟹ ¬ (B * F ⟹⇩A Q)" by auto2
lemma entails_frame'': "¬ (P ⟹⇩A B * F) ⟹ A ⟹⇩A B ⟹ ¬ (P ⟹⇩A A * F)" by auto2
lemma entails_equiv_forward: "P = Q ⟹ P ⟹⇩A Q" by auto2
lemma entails_equiv_backward: "P = Q ⟹ Q ⟹⇩A P" by auto2
lemma entailsD [forward]: "P ⟹⇩A Q ⟹ h ⊨ P ⟹ h ⊨ Q" by auto2
lemma entails_trans2: "A ⟹⇩A D * B ⟹ B ⟹⇩A C ⟹ A ⟹⇩A D * C" by auto2

lemma entails_pure': "¬(↑b ⟹⇩A Q) ⟷ (¬(emp ⟹⇩A Q) ∧ b)" by auto2
lemma entails_pure: "¬(P * ↑b ⟹⇩A Q) ⟷ (¬(P ⟹⇩A Q) ∧ b)" by auto2
lemma entails_ex: "¬((∃⇩Ax. P x) ⟹⇩A Q) ⟷ (∃x. ¬(P x ⟹⇩A Q))" by auto2
lemma entails_ex_post: "¬(P ⟹⇩A (∃⇩Ax. Q x)) ⟹ ∀x. ¬(P ⟹⇩A Q x)" by auto2
lemma entails_pure_post: "¬(P ⟹⇩A Q * ↑b) ⟹ P ⟹⇩A Q ⟹ ¬b" by auto2

setup ‹del_prfstep_thm @{thm entails_def}›

subsection ‹Definition of the run predicate›

inductive run :: "'a Heap ⇒ heap option ⇒ heap option ⇒ 'a ⇒ bool" where
  "run c None None r"
| "execute c h = None ⟹ run c (Some h) None r"
| "execute c h = Some (r, h') ⟹ run c (Some h) (Some h') r"
setup ‹add_case_induct_rule @{thm run.cases}›
setup ‹fold add_resolve_prfstep @{thms run.intros(1,2)}›
setup ‹add_forward_prfstep @{thm run.intros(3)}›

lemma run_complete [resolve]:
  "∃σ' r. run c σ σ' (r::'a)"
@proof
  @obtain "r::'a" where "r = r"
  @case "σ = None" @with @have "run c None None r" @end
  @case "execute c (the σ) = None" @with @have "run c σ None r" @end
@qed

lemma run_to_execute [forward]:
  "run c (Some h) σ' r ⟹ if σ' = None then execute c h = None else execute c h = Some (r, the σ')"
@proof @case_induct "run c (Some h) σ' r" @qed

setup ‹add_rewrite_rule @{thm execute_bind(1)}›
lemma runE [forward]:
  "run f (Some h) (Some h') r' ⟹ run (f ⤜ g) (Some h) σ r ⟹ run (g r') (Some h') σ r" by auto2

setup ‹add_rewrite_rule @{thm Array.get_alloc}›
setup ‹add_rewrite_rule @{thm Ref.get_alloc}›
setup ‹add_rewrite_rule_bidir @{thm Array.length_def}›

subsection ‹Definition of hoare triple, and the frame rule.›

definition new_addrs :: "heap ⇒ addr set ⇒ heap ⇒ addr set" where [rewrite]:
  "new_addrs h as h' = as ∪ {a. lim h ≤ a ∧ a < lim h'}"

definition hoare_triple :: "assn ⇒ 'a Heap ⇒ ('a ⇒ assn) ⇒ bool" ("<_>/ _/ <_>") where [rewrite]:
  "<P> c <Q> ⟷ (∀h as σ r. pHeap h as ⊨ P ⟶ run c (Some h) σ r ⟶
    (σ ≠ None ∧ pHeap (the σ) (new_addrs h as (the σ)) ⊨ Q r ∧ relH {a . a < lim h ∧ a ∉ as} h (the σ) ∧
     lim h ≤ lim (the σ)))"

lemma hoare_tripleD [forward]:
  "<P> c <Q> ⟹ run c (Some h) σ r ⟹ ∀as. pHeap h as ⊨ P ⟶
     (σ ≠ None ∧ pHeap (the σ) (new_addrs h as (the σ)) ⊨ Q r ∧ relH {a . a < lim h ∧ a ∉ as} h (the σ) ∧
     lim h ≤ lim (the σ))"
  by auto2
setup ‹del_prfstep_thm_eqforward @{thm hoare_triple_def}›

abbreviation hoare_triple' :: "assn ⇒ 'r Heap ⇒ ('r ⇒ assn) ⇒ bool" ("<_> _ <_>⇩t") where
  "<P> c <Q>⇩t ≡ <P> c <λr. Q r * true>"

theorem frame_rule [backward]:
  "<P> c <Q> ⟹ <P * R> c <λx. Q x * R>"
@proof
  @have "∀h as σ r. pHeap h as ⊨ P * R ⟶ run c (Some h) σ r ⟶
                    (σ ≠ None ∧ pHeap (the σ) (new_addrs h as (the σ)) ⊨ Q r * R ∧
                     relH {a . a < lim h ∧ a ∉ as} h (the σ) ∧ lim h ≤ lim (the σ))" @with
    @obtain as1 as2 where "as = as1 ∪ as2" "as1 ∩ as2 = {}" "pHeap h as1 ⊨ P ∧ pHeap h as2 ⊨ R"
    @have "relH as2 h (the σ)"
    @have "new_addrs h as (the σ) = new_addrs h as1 (the σ) ∪ as2"
  @end
@qed

text ‹This is the last use of the definition of separating conjunction.›
setup ‹del_prfstep_thm @{thm mod_star_conv}›

theorem bind_rule:
  "<P> f <Q> ⟹ ∀x. <Q x> g x <R> ⟹ <P> f ⤜ g <R>"
@proof
  @have "∀h as σ r. pHeap h as ⊨ P ⟶ run (f ⤜ g) (Some h) σ r ⟶
                    (σ ≠ None ∧ pHeap (the σ) (new_addrs h as (the σ)) ⊨ R r ∧
                     relH {a . a < lim h ∧ a ∉ as} h (the σ) ∧ lim h ≤ lim (the σ))" @with
    ― ‹First step from h to h'›
    @obtain σ' r' where "run f (Some h) σ' r'"
    @obtain h' where "σ' = Some h'"
    @let "as' = new_addrs h as h'"
    @have "pHeap h' as' ⊨ Q r'"

    ― ‹Second step from h' to h''›
    @have "run (g r') (Some h') σ r"
    @obtain h'' where "σ = Some h''"
    @let "as'' = new_addrs h' as' h''"
    @have "pHeap h'' as'' ⊨ R r"
    @have "as'' = new_addrs h as h''"
  @end
@qed

text ‹Actual statement used:›
lemma bind_rule':
  "<P> f <Q> ⟹ ¬ <P> f ⤜ g <R> ⟹ ∃x. ¬ <Q x> g x <R>" using bind_rule by blast

lemma pre_rule':
  "¬ <P * R> f <Q> ⟹ P ⟹⇩A P' ⟹ ¬ <P' * R> f <Q>"
@proof @have "P * R ⟹⇩A P' * R" @qed

lemma pre_rule'':
  "<P> f <Q> ⟹ P' ⟹⇩A P * R ⟹ <P'> f <λx. Q x * R>"
@proof @have "<P * R> f <λx. Q x * R>" @qed

lemma pre_ex_rule:
  "¬ <∃⇩Ax. P x> f <Q> ⟷ (∃x. ¬ <P x> f <Q>)" by auto2

lemma pre_pure_rule:
  "¬ <P * ↑b> f <Q> ⟷ ¬ <P> f <Q> ∧ b" by auto2

lemma pre_pure_rule':
  "¬ <↑b> f <Q> ⟷ ¬ <emp> f <Q> ∧ b" by auto2

lemma post_rule:
  "<P> f <Q> ⟹ ∀x. Q x ⟹⇩A R x ⟹ <P> f <R>" by auto2

setup ‹fold del_prfstep_thm [@{thm entailsD}, @{thm entails_frame}, @{thm frame_rule}]›

text ‹Actual statement used:›
lemma post_rule':
  "<P> f <Q> ⟹ ¬ <P> f <R> ⟹ ∃x. ¬ (Q x ⟹⇩A R x)" using post_rule by blast

lemma norm_pre_pure_iff: "<P * ↑b> c <Q> ⟷ (b ⟶ <P> c <Q>)" by auto2
lemma norm_pre_pure_iff2: "<↑b> c <Q> ⟷ (b ⟶ <emp> c <Q>)" by auto2

subsection ‹Hoare triples for atomic commands›

text ‹First, those that do not modify the heap.›
setup ‹add_rewrite_rule @{thm execute_assert(1)}›
lemma assert_rule:
  "<↑(R x)> assert R x <λr. ↑(r = x)>" by auto2

lemma execute_return' [rewrite]: "execute (return x) h = Some (x, h)" by (metis comp_eq_dest_lhs execute_return)
lemma return_rule:
  "<emp> return x <λr. ↑(r = x)>" by auto2

setup ‹add_rewrite_rule @{thm execute_nth(1)}›
lemma nth_rule:
  "<a ↦⇩a xs * ↑(i < length xs)> Array.nth a i <λr. a ↦⇩a xs * ↑(r = xs ! i)>" by auto2

setup ‹add_rewrite_rule @{thm execute_len}›
lemma length_rule:
  "<a ↦⇩a xs> Array.len a <λr. a ↦⇩a xs * ↑(r = length xs)>" by auto2

setup ‹add_rewrite_rule @{thm execute_lookup}›
lemma lookup_rule:
  "<p ↦⇩r x> !p <λr. p ↦⇩r x * ↑(r = x)>" by auto2

setup ‹add_rewrite_rule @{thm execute_freeze}›
lemma freeze_rule:
  "<a ↦⇩a xs> Array.freeze a <λr. a ↦⇩a xs * ↑(r = xs)>" by auto2

text ‹Next, the update rules.›
setup ‹add_rewrite_rule @{thm Ref.lim_set}›
lemma Array_lim_set [rewrite]: "lim (Array.set p xs h) = lim h" by (simp add: Array.set_def)

setup ‹fold add_rewrite_rule [@{thm Ref.get_set_eq}, @{thm Array.get_set_eq}]›
setup ‹add_rewrite_rule @{thm Array.update_def}›

setup ‹add_rewrite_rule @{thm execute_upd(1)}›
lemma upd_rule:
  "<a ↦⇩a xs * ↑(i < length xs)> Array.upd i x a <λr. a ↦⇩a list_update xs i x * ↑(r = a)>" by auto2

setup ‹add_rewrite_rule @{thm execute_update}›
lemma update_rule:
  "<p ↦⇩r y> p := x <λr. p ↦⇩r x>" by auto2

text ‹Finally, the allocation rules.›
lemma lim_set_gen [rewrite]: "lim (h⦇lim := l⦈) = l" by simp

lemma Array_alloc_def' [rewrite]:
  "Array.alloc xs h = (let l = lim h; r = Array l in (r, (Array.set r xs (h⦇lim := l + 1⦈))))"
  by (simp add: Array.alloc_def)

setup ‹fold add_rewrite_rule [
  @{thm addr_of_array.simps}, @{thm addr_of_ref.simps}, @{thm Ref.alloc_def}]›

lemma refs_on_Array_set [rewrite]: "refs (Array.set p xs h) t i = refs h t i"
  by (simp add: Array.set_def)

lemma arrays_on_Ref_set [rewrite]: "arrays (Ref.set p x h) t i = arrays h t i"
  by (simp add: Ref.set_def)

lemma refs_on_Array_alloc [rewrite]: "refs (snd (Array.alloc xs h)) t i = refs h t i"
  by (metis (no_types, lifting) Array.alloc_def refs_on_Array_set select_convs(2) snd_conv surjective update_convs(3))

lemma arrays_on_Ref_alloc [rewrite]: "arrays (snd (Ref.alloc x h)) t i = arrays h t i"
  by (metis (no_types, lifting) Ref.alloc_def arrays_on_Ref_set select_convs(1) sndI surjective update_convs(3))

lemma arrays_on_Array_alloc [rewrite]: "i < lim h ⟹ arrays (snd (Array.alloc xs h)) t i = arrays h t i"
  by (smt Array.alloc_def Array.set_def addr_of_array.simps fun_upd_apply less_or_eq_imp_le
          linorder_not_less simps(1) snd_conv surjective update_convs(1) update_convs(3))

lemma refs_on_Ref_alloc [rewrite]: "i < lim h ⟹ refs (snd (Ref.alloc x h)) t i = refs h t i"
  by (smt Ref.alloc_def Ref.set_def addr_of_ref.simps fun_upd_apply less_or_eq_imp_le
          linorder_not_less select_convs(2) simps(6) snd_conv surjective update_convs(3))

setup ‹add_rewrite_rule @{thm execute_new}›
lemma new_rule:
  "<emp> Array.new n x <λr. r ↦⇩a replicate n x>" by auto2

setup ‹add_rewrite_rule @{thm execute_of_list}›
lemma of_list_rule:
  "<emp> Array.of_list xs <λr. r ↦⇩a xs>" by auto2

setup ‹add_rewrite_rule @{thm execute_ref}›
lemma ref_rule:
  "<emp> ref x <λr. r ↦⇩r x>" by auto2

setup ‹fold del_prfstep_thm [
  @{thm sngr_assn_rule}, @{thm snga_assn_rule}, @{thm pure_assn_rule}, @{thm top_assn_rule},
  @{thm mod_pure_star_dist}, @{thm one_assn_rule}, @{thm hoare_triple_def}, @{thm mod_ex_dist}]›
setup ‹del_simple_datatype "pheap"›

subsection ‹Definition of procedures›

text ‹ASCII abbreviations for ML files.›
abbreviation (input) ex_assn_ascii :: "('a ⇒ assn) ⇒ assn" (binder "EXA" 11)
  where "ex_assn_ascii ≡ ex_assn"

abbreviation (input) models_ascii :: "pheap ⇒ assn ⇒ bool" (infix "|=" 50)
  where "h |= P ≡ h ⊨ P"

ML_file "sep_util.ML"

ML ‹
structure AssnMatcher = AssnMatcher(SepUtil)
structure SepLogic = SepLogic(SepUtil)
val add_assn_matcher = AssnMatcher.add_assn_matcher
val add_entail_matcher = AssnMatcher.add_entail_matcher
val add_forward_ent_prfstep = SepLogic.add_forward_ent_prfstep
val add_rewrite_ent_rule = SepLogic.add_rewrite_ent_rule
val add_hoare_triple_prfstep = SepLogic.add_hoare_triple_prfstep
›
setup ‹AssnMatcher.add_assn_matcher_proofsteps›
setup ‹SepLogic.add_sep_logic_proofsteps›

ML_file "sep_steps_test.ML"

attribute_setup forward_ent = ‹setup_attrib add_forward_ent_prfstep›
attribute_setup rewrite_ent = ‹setup_attrib add_rewrite_ent_rule›
attribute_setup hoare_triple = ‹setup_attrib add_hoare_triple_prfstep›

setup ‹fold add_hoare_triple_prfstep [
  @{thm assert_rule}, @{thm update_rule}, @{thm nth_rule}, @{thm upd_rule},
  @{thm return_rule}, @{thm ref_rule}, @{thm lookup_rule}, @{thm new_rule},
  @{thm of_list_rule}, @{thm length_rule}, @{thm freeze_rule}]›

text ‹Some simple tests›

theorem "<emp> ref x <λr. r ↦⇩r x>" by auto2
theorem "<a ↦⇩r x> ref x <λr. a ↦⇩r x * r ↦⇩r x>" by auto2
theorem "<a ↦⇩r x> (!a) <λr. a ↦⇩r x * ↑(r = x)>" by auto2
theorem "<a ↦⇩r x * b ↦⇩r y> (!a) <λr. a ↦⇩r x * b ↦⇩r y * ↑(r = x)>" by auto2
theorem "<a ↦⇩r x * b ↦⇩r y> (!b) <λr. a ↦⇩r x * b ↦⇩r y * ↑(r = y)>" by auto2
theorem "<a ↦⇩r x> do { a := y; !a } <λr. a ↦⇩r y * ↑(r = y)>" by auto2
theorem "<a ↦⇩r x> do { a := y; a := z; !a } <λr. a ↦⇩r z * ↑(r = z)>" by auto2
theorem "<a ↦⇩r x> do { y ← !a; ref y} <λr. a ↦⇩r x * r ↦⇩r x>" by auto2
theorem "<emp> return x <λr. ↑(r = x)>" by auto2

end