# Session Separation_Logic_Imperative_HOL

section ‹Additions to Imperative/HOL›
imports "HOL-Imperative_HOL.Imperative_HOL"
begin

text ‹This theory loads the Imperative HOL framework and provides
some additional lemmas needed for the separation logic framework.›

text ‹A stronger elimination rule for ‹ref››

lemma effect_ref[effect_elims]:
assumes "effect (ref (x::('a::heap))) h h' r"
obtains "r = fst (Ref.alloc x h)" and "h' = snd (Ref.alloc x h)"
proof -
from assms have "execute (ref x) h = Some (r, h')" by (unfold effect_def)
then have "r = fst (Ref.alloc x h)" "h' = snd (Ref.alloc x h)"
then show thesis ..
qed

text ‹Some lemmas about the evaluation of the limit for modifications on
a heap›

lemma lim_Ref_alloc[simp]: "lim (snd (Ref.alloc x h)) = Suc (lim h)"
unfolding Ref.alloc_def

lemma lim_Array_alloc[simp]: "lim (snd (Array.alloc x h)) = Suc (lim h)"
unfolding Array.alloc_def Array.set_def

lemma lim_Array_set[simp]: "lim (Array.set a xs h) = lim h"
unfolding Array.set_def

thm Array.update_def
lemma lim_Array_update[simp]: "lim (Array.update a i x h) = lim h"
unfolding Array.update_def

text ‹Simplification rules for the addresses of new allocated arrays and
references›

"addr_of_ref (fst (Ref.alloc x h)) = lim h"
unfolding Ref.alloc_def

"addr_of_array (fst (Array.alloc x h)) = lim h"
unfolding Array.alloc_def

end


# Theory Syntax_Match

section ‹Syntactic Matching in the Simplifier›
theory Syntax_Match
imports Main
begin

subsection ‹Non-Matching›

text ‹
We define the predicates ‹syntax_nomatch›
and ‹syntax_fo_nomatch›. The expression
‹syntax_nomatch pattern object› is simplified to true only if
the term ‹pattern› syntactically matches the term ‹object›.
Note that, semantically, ‹syntax_nomatch pattern object› is always
true. While ‹syntax_nomatch› does higher-order matching,
‹syntax_fo_nomatch› does first-order matching.

The intended application of these predicates are as guards for simplification
rules, enforcing additional syntactic restrictions on the applicability of
the simplification rule.
›
definition syntax_nomatch :: "'a ⇒ 'b ⇒ bool"
where syntax_nomatch_def: "syntax_nomatch pat obj ≡ True"
definition syntax_fo_nomatch :: "'a ⇒ 'b ⇒ bool"
where syntax_fo_nomatch_def: "syntax_fo_nomatch pat obj ≡ True"

(* Prevent simplifier to simplify inside syntax_xx predicates *)
lemma [cong]: "syntax_fo_nomatch x y = syntax_fo_nomatch x y" by simp
lemma [cong]: "syntax_nomatch x y = syntax_nomatch x y" by simp

ML ‹
structure Syntax_Match = struct
val nomatch_thm = @{thm syntax_nomatch_def};
val fo_nomatch_thm = @{thm syntax_fo_nomatch_def};

fun fo_nomatch_simproc ctxt credex = let
(*val ctxt = Simplifier.the_context ss;*)
val thy = Proof_Context.theory_of ctxt;

val redex = Thm.term_of credex;
val (_,[pat,obj]) = strip_comb redex;

fun fo_matches po = (Pattern.first_order_match
thy po (Vartab.empty, Vartab.empty); true) handle Pattern.MATCH => false;
in
if fo_matches (pat,obj) then NONE else SOME fo_nomatch_thm
end

fun nomatch_simproc ctxt credex = let
(*val ctxt = Simplifier.the_context ss;*)
val thy = Proof_Context.theory_of ctxt;

val redex = Thm.term_of credex;
val (_,[pat,obj]) = strip_comb redex;
in
if Pattern.matches thy (pat,obj) then NONE else SOME nomatch_thm
end
end
›
simproc_setup nomatch ("syntax_nomatch pat obj")
= ‹K Syntax_Match.nomatch_simproc›
simproc_setup fo_nomatch ("syntax_fo_nomatch pat obj")
= ‹K Syntax_Match.fo_nomatch_simproc›

subsection ‹Examples›
subsubsection ‹Ordering AC-structures›
text ‹
Currently, the simplifier rules for ac-rewriting only work when
associativity groups to the right. Here, we define rules that work for
associativity grouping to the left. They are useful for operators where
syntax is parsed (and pretty-printed) left-associative.
›

locale ac_operator =
fixes f
assumes right_assoc: "f (f a b) c = f a (f b c)"
assumes commute: "f a b = f b a"
begin
lemmas left_assoc = right_assoc[symmetric]
lemma left_commute: "f a (f b c) = f b (f a c)"
done

lemmas right_ac = right_assoc left_commute commute

lemma right_commute: "f (f a b) c = f (f a c) b"

lemma safe_commute: "syntax_fo_nomatch (f x y) a ⟹ f a b = f b a"

lemmas left_ac = left_assoc right_commute safe_commute
end

interpretation mult: ac_operator "(*) ::'a::ab_semigroup_mult ⇒ _ ⇒ _"
apply unfold_locales
done

apply unfold_locales
done

text ‹Attention: ‹conj_assoc› is in standard simpset, it has to be
removed when using ‹conj.left_ac› !›
interpretation conj: ac_operator "(∧)"
by unfold_locales auto
interpretation disj: ac_operator "(∨)"
by unfold_locales auto

end


# Theory Run

section ‹Exception-Aware Relational Framework›
theory Run
imports "HOL-Imperative_HOL.Imperative_HOL"
begin

text ‹
With Imperative HOL comes a relational framework.
However, this can only be used if exception freeness is already assumed.
This results in some proof duplication, because exception freeness and
correctness need to be shown separately.

In this theory, we develop a relational framework that is aware of
exceptions, and makes it possible to show correctness and exception
freeness in one run.
›

text ‹
There are two types of states:
\begin{enumerate}
\item A normal (Some) state contains the current heap.
\item An exception state is None
\end{enumerate}
The two states exactly correspond to the option monad in Imperative HOL.
›

type_synonym state = "Heap.heap option"

primrec is_exn where
"is_exn (Some _) = False" |
"is_exn None = True"

primrec the_state where
"the_state (Some h) = h"

― ‹The exception-aware, relational semantics›

inductive run :: "'a Heap ⇒ state ⇒ state ⇒ 'a ⇒ bool" where
push_exn: "is_exn σ ⟹ run c σ σ r " |
new_exn:  "⟦¬ is_exn σ; execute c (the_state σ) = None⟧
⟹ run c σ None r" |
regular:  "⟦¬ is_exn σ; execute c (the_state σ) = Some (r, h')⟧
⟹ run c σ (Some h') r"

subsubsection "Link with ‹effect› and ‹success›"

lemma run_effectE:
assumes "run c σ σ' r"
assumes "¬is_exn σ'"
obtains h h' where
"σ=Some h" "σ' = Some h'"
"effect c h h' r"
using assms
unfolding effect_def
apply (cases σ)

lemma run_effectI:
assumes  "run c (Some h) (Some h') r"
shows  "effect c h h' r"
using run_effectE[OF assms] by auto

lemma effect_run:
assumes "effect c h h' r"
shows "run c (Some h) (Some h') r"
using assms
unfolding effect_def
by (auto intro: run.intros)

lemma success_run:
assumes "success f h"
obtains h' r where "run f (Some h) (Some h') r"
proof -
from assms obtain r h'
where "Heap_Monad.execute f h = Some (r, h')"
unfolding success_def by auto
then show thesis by (rule that[OF regular[of "Some h", simplified]])
qed

text ‹run always yields a result›
lemma run_complete:
obtains σ' r where "run c σ σ' r"
apply (cases "is_exn σ")
apply (auto intro: run.intros)
apply (cases "execute c (the_state σ)")
by (auto intro: run.intros)

lemma run_detE:
assumes "run c σ σ' r" "run c σ τ s"
"¬is_exn σ"
obtains "is_exn σ'" "σ' = τ" | "¬ is_exn σ'" "σ' = τ" "r = s"
using assms

lemma run_detI:
assumes "run c (Some h) (Some h') r" "run c (Some h) σ s"
shows "σ = Some h' ∧ r = s"
using assms

lemma run_exn:
assumes "run f σ σ' r"
"is_exn σ"
obtains "σ'=σ"
using assms
apply (cases σ)
apply (auto elim!: run.cases intro: that)
done

subsubsection ‹Elimination Rules for Basic Combinators›

named_theorems run_elims "elemination rules for run"

lemma runE[run_elims]:
assumes "run (f ⤜ g) σ σ'' r"
obtains σ' r' where
"run f σ σ' r'"
"run (g r') σ' σ'' r"
using assms
apply (cases "is_exn σ")
apply (cases "execute f (the_state σ)")
by (auto simp add: bind_def run.simps)

lemma runE'[run_elims]:
assumes "run (f ⪢ g) σ σ'' res"
obtains σt rt where
"run f σ σt rt"
"run g σt σ'' res"
using assms
by (rule_tac runE)

lemma run_return[run_elims]:
assumes "run (return x) σ σ' r"
obtains "r = x" "σ' = σ" "¬ is_exn σ" | "σ = None"
using assms  apply (cases σ) apply (simp add: run.simps)
by (auto simp add: run.simps execute_simps)

lemma run_raise_iff: "run (raise s) σ σ' r ⟷ (σ'=None)"
apply (cases σ)
by (auto simp add: run.simps execute_simps)

lemma run_raise[run_elims]:
assumes "run (raise s) σ σ' r"
obtains "σ' = None"
using assms by (simp add: run_raise_iff)

lemma run_raiseI:
"run (raise s) σ None r" by (simp add: run_raise_iff)

lemma run_if[run_elims]:
assumes "run (if c then t else e) h h' r"
obtains "c" "run t h h' r"
| "¬c" "run e h h' r"
using assms
by (auto split: if_split_asm)

lemma run_case_option[run_elims]:
assumes "run (case x of None ⇒ n | Some y ⇒ s y) σ σ' r"
"¬is_exn σ"
obtains "x = None" "run n σ σ' r"
| y where "x = Some y" "run (s y) σ σ' r"
using assms
by (cases x) simp_all

lemma run_heap[run_elims]:
assumes "run (Heap_Monad.heap f) σ σ' res"
"¬is_exn σ"
obtains "σ' = Some (snd (f (the_state σ)))"
and "res = (fst (f (the_state σ)))"
using assms
apply (cases σ)
apply simp

apply (simp only: execute_simps)
apply hypsubst_thin
subgoal premises prems for a h'
proof -
from prems(2) have "h' = snd (f a)" "res = fst (f a)" by simp_all
from prems(1)[OF this] show ?thesis .
qed
done

subsection ‹Array Commands›

lemma run_length[run_elims]:
assumes "run (Array.len a) σ σ' r"
"¬is_exn σ"
obtains "¬is_exn σ" "σ' = σ" "r = Array.length (the_state σ) a"
using assms
apply (cases σ)
by (auto simp add: run.simps execute_simps)

lemma run_new_array[run_elims]:
assumes "run (Array.new n x) σ σ' r"
"¬is_exn σ"
obtains "σ' = Some (snd (Array.alloc (replicate n x) (the_state σ)))"
and "r = fst (Array.alloc (replicate n x) (the_state σ))"
and "Array.get (the_state σ') r = replicate n x"
using assms
apply (cases σ)
apply simp
apply hypsubst_thin
subgoal premises prems for a h'
proof -
from prems(2) have "h' = snd (Array.alloc (replicate n x) a)"
"r = fst (Array.alloc (replicate n x) a)" by (auto simp add: execute_simps)
then show ?thesis by (rule prems(1))
qed
done

lemma run_make[run_elims]:
assumes "run (Array.make n f) σ σ' r"
"¬is_exn σ"
obtains "σ' = Some (snd (Array.alloc (map f [0 ..< n]) (the_state σ)))"
"r = fst (Array.alloc (map f [0 ..< n]) (the_state σ))"
"Array.get (the_state σ') r = (map f [0 ..< n])"
using assms
apply (cases σ)
subgoal by simp
subgoal by (simp add: run.simps execute_simps Array.get_alloc; fastforce)
done

lemma run_upd[run_elims]:
assumes "run (Array.upd i x a) σ σ' res"
"¬is_exn σ"
obtains "¬ i < Array.length (the_state σ) a"
"σ' = None"
|
"i < Array.length (the_state σ) a"
"σ' = Some (Array.update a i x (the_state σ))"
"res = a"
using assms
apply (cases σ)
apply simp
apply (cases "i < Array.length (the_state σ) a")
apply (simp_all only: execute_simps)
prefer 3
apply auto[2]
apply hypsubst_thin
subgoal premises prems for aa h'
proof -
from prems(3) have "h' = Array.update a i x aa" "res = a" by auto
then show ?thesis by (rule prems(1))
qed
done

lemma run_nth[run_elims]:
assumes "run (Array.nth a i) σ σ' r"
"¬is_exn σ"
obtains "¬is_exn σ"
"i < Array.length (the_state σ) a"
"r = (Array.get (the_state σ) a) ! i"
"σ' = σ"
|
"¬ i < Array.length (the_state σ) a"
"σ' = None"
using assms
apply (cases σ)
apply simp
apply (cases "i < Array.length (the_state σ) a")
apply (simp_all only: execute_simps)
prefer 3
apply auto[2]
apply hypsubst_thin
subgoal premises prems for aa h'
proof -
from prems(3) have "r = Array.get aa a ! i" "h' = aa" by auto
then show ?thesis by (rule prems(1))
qed
done

lemma run_of_list[run_elims]:
assumes "run (Array.of_list xs) σ σ' r"
"¬is_exn σ"
obtains "σ' = Some (snd (Array.alloc xs (the_state σ)))"
"r = fst (Array.alloc xs (the_state σ))"
"Array.get (the_state σ') r = xs"
using assms
apply (cases σ)
apply simp
apply hypsubst_thin
subgoal premises prems for a h'
proof -
from prems(2) have "h' = snd (Array.alloc xs a)"
"r = fst (Array.alloc xs a)" by (auto simp add: execute_simps)
then show ?thesis by (rule prems(1))
qed
done

lemma run_freeze[run_elims]:
assumes "run (Array.freeze a) σ σ' r"
"¬is_exn σ"
obtains "σ' = σ"
"r = Array.get (the_state σ) a"
using assms
apply (cases σ)
by (auto simp add: run.simps execute_simps)

subsection ‹Reference Commands›

lemma run_new_ref[run_elims]:
assumes "run (ref x) σ σ' r"
"¬is_exn σ"
obtains "σ' = Some (snd (Ref.alloc x (the_state σ)))"
"r = fst (Ref.alloc x (the_state σ))"
"Ref.get (the_state σ') r = x"
using assms
apply (cases σ)
apply simp
apply hypsubst_thin
subgoal premises prems for a h'
proof -
from prems(2) have
"h' = snd (Ref.alloc x a)"
"r = fst (Ref.alloc x a)"
then show ?thesis by (rule prems(1))
qed
done

lemma "fst (Ref.alloc x h) = Ref (lim h)"
unfolding alloc_def

lemma run_update[run_elims]:
assumes "run (p := x) σ σ' r"
"¬is_exn σ"
obtains "σ' = Some (Ref.set p x (the_state σ))" "r = ()"
using assms
unfolding Ref.update_def
by (auto elim: run_heap)

lemma run_lookup[run_elims]:
assumes "run (!p) σ σ' r"
"¬ is_exn σ"
obtains "¬is_exn σ" "σ' = σ" "r = Ref.get (the_state σ) p"
using assms
apply (cases σ)
by (auto simp add: run.simps execute_simps)

end


# Theory Assertions

section "Assertions"

theory Assertions
imports
"Tools/Syntax_Match"
Automatic_Refinement.Misc
begin

subsection ‹Partial Heaps›
text ‹
A partial heap is modeled by a heap and a set of valid addresses, with the
side condition that the valid addresses have to be within the limit of the
heap. This modeling is somewhat strange for separation logic, however, it
allows us to solve some technical problems related to definition of
Hoare triples, that will be detailed later.
›
type_synonym pheap = "heap × addr set"

text ‹Predicate that expresses that the address set of a partial heap is
within the heap's limit.
›
fun in_range :: "(heap × addr set) ⇒ bool"
where "in_range (h,as) ⟷ (∀a∈as. a < lim h)"

declare in_range.simps[simp del]

lemma in_range_empty[simp, intro!]: "in_range (h,{})"
by (auto simp: in_range.simps)

lemma in_range_dist_union[simp]:
"in_range (h,as ∪ as') ⟷ in_range (h,as) ∧ in_range (h,as')"
by (auto simp: in_range.simps)

lemma in_range_subset:
"⟦as ⊆ as'; in_range (h,as')⟧ ⟹ in_range (h,as)"
by (auto simp: in_range.simps)

text ‹Relation that holds if two heaps are identical on a given
definition relH :: "addr set ⇒ heap ⇒ heap ⇒ bool"
where "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_in_rangeI:
assumes "relH as h h'"
shows "in_range (h,as)" and "in_range (h',as)"
using assms unfolding relH_def by auto

text "Reflexivity"
lemma relH_refl: "in_range (h,as) ⟹ relH as h h"
unfolding relH_def by simp

text "Symmetry"
lemma relH_sym: "relH as h h' ⟹ relH as h' h"
unfolding relH_def
by auto

text "Transitivity"
lemma relH_trans[trans]: "⟦relH as h1 h2; relH as h2 h3⟧ ⟹ relH as h1 h3"
unfolding relH_def
by auto

lemma relH_dist_union[simp]:
"relH (as∪as') h h' ⟷ relH as h h' ∧ relH as' h h'"
unfolding relH_def
by auto

lemma relH_subset:
assumes "relH bs h h'"
assumes "as ⊆ bs"
shows "relH as h h'"
using assms unfolding relH_def by (auto intro: in_range_subset)

lemma relH_ref:
assumes "relH as h h'"
shows "Ref.get h r = Ref.get h' r"
using assms unfolding relH_def Ref.get_def by auto

lemma relH_array:
assumes "relH as h h'"
shows "Array.get h r = Array.get h' r"
using assms unfolding relH_def Array.get_def by auto

lemma relH_set_ref: "⟦ addr_of_ref r ∉ as; in_range (h,as)⟧
⟹ relH as h (Ref.set r x h)"
unfolding relH_def Ref.set_def
by (auto simp: in_range.simps)

lemma relH_set_array: "⟦addr_of_array r ∉ as; in_range (h,as)⟧
⟹ relH as h (Array.set r x h)"
unfolding relH_def Array.set_def
by (auto simp: in_range.simps)

subsection ‹Assertions›
text ‹
Assertions are predicates on partial heaps, that fulfill a well-formedness
condition called properness: They only depend on the part of the heap
by the address set, and must be false for partial heaps that are not in range.
›
type_synonym assn_raw = "pheap ⇒ bool"

definition proper :: "assn_raw ⇒ bool" where
"proper P ≡ ∀h h' as. (P (h,as) ⟶ in_range (h,as))
∧ (P (h,as) ∧ relH as h h' ∧ in_range (h',as) ⟶ P (h',as))"

lemma properI[intro?]:
assumes "⋀as h. P (h,as) ⟹ in_range (h,as)"
assumes "⋀as h h'.
⟦P (h,as); relH as h h'; in_range (h',as)⟧ ⟹ P (h',as)"
shows "proper P"
unfolding proper_def using assms by blast

lemma properD1:
assumes "proper P"
assumes "P (h,as)"
shows "in_range (h,as)"
using assms unfolding proper_def by blast

lemma properD2:
assumes "proper P"
assumes "P (h,as)"
assumes "relH as h h'"
assumes "in_range (h',as)"
shows "P (h',as)"
using assms unfolding proper_def by blast

lemmas properD = properD1 properD2

lemma proper_iff:
assumes "proper P"
assumes "relH as h h'"
assumes "in_range (h',as)"
shows "P (h,as) ⟷ P (h',as)"
using assms
by (metis properD2 relH_in_rangeI(1) relH_sym)

text ‹We encapsulate assertions in their own type›
typedef assn = "Collect proper"
apply simp
unfolding proper_def
by fastforce

lemmas [simp] = Rep_assn_inverse Rep_assn_inject
lemmas [simp, intro!] = Rep_assn[unfolded mem_Collect_eq]

lemma Abs_assn_eqI[intro?]:
"(⋀h. P h = Rep_assn Pr h) ⟹ Abs_assn P = Pr"
"(⋀h. P h = Rep_assn Pr h) ⟹ Pr = Abs_assn P"
by (metis Rep_assn_inverse predicate1I xt1(5))+

abbreviation models :: "pheap ⇒ assn ⇒ bool" (infix "⊨" 50)
where "h⊨P ≡ Rep_assn P h"

lemma models_in_range: "h⊨P ⟹ in_range h"
apply (cases h)
by (metis mem_Collect_eq Rep_assn properD1)

subsubsection ‹Empty Partial Heap›
text ‹The empty partial heap satisfies some special properties.
We set up a simplification that tries to rewrite it to the standard
empty partial heap ‹h⇩⊥››
abbreviation h_bot ("h⇩⊥") where "h⇩⊥ ≡ (undefined,{})"
lemma mod_h_bot_indep: "(h,{})⊨P ⟷ (h',{})⊨P"
by (metis mem_Collect_eq Rep_assn emptyE in_range_empty
proper_iff relH_def)

lemma mod_h_bot_normalize[simp]:
"syntax_fo_nomatch undefined h ⟹ (h,{})⊨P ⟷ h⇩⊥ ⊨ P"
using mod_h_bot_indep[where h'=undefined] by simp

text ‹Properness, lifted to the assertion type.›
lemma mod_relH: "relH as h h' ⟹ (h,as)⊨P ⟷ (h',as)⊨P"
by (metis mem_Collect_eq Rep_assn proper_iff relH_in_rangeI(2))

subsection ‹Connectives›
text ‹
We define several operations on assertions, and instantiate some type classes.
›

subsubsection ‹Empty Heap and Separation Conjunction›
text ‹The assertion that describes the empty heap, and the separation
conjunction form a commutative monoid:›
instantiation assn :: one begin
fun one_assn_raw :: "pheap ⇒ bool"
where "one_assn_raw (h,as) ⟷ as={}"

lemma one_assn_proper[intro!,simp]: "proper one_assn_raw"
by (auto intro!: properI)

definition one_assn :: assn where "1 ≡ Abs_assn one_assn_raw"
instance ..
end

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

instantiation assn :: times begin
fun times_assn_raw :: "assn_raw ⇒ assn_raw ⇒ assn_raw" where
"times_assn_raw P Q (h,as)
= (∃as1 as2. as=as1∪as2 ∧ as1∩as2={}
∧ P (h,as1) ∧ Q (h,as2))"

lemma times_assn_proper[intro!,simp]:
"proper P ⟹ proper Q ⟹ proper (times_assn_raw P Q)"
apply (rule properI)
apply (auto dest: properD1) []
apply clarsimp
apply (drule (3) properD2)
apply (drule (3) properD2)
apply blast
done

definition times_assn where "P*Q ≡
Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn Q))"

instance ..
end

lemma mod_star_conv: "h⊨A*B
⟷ (∃hr as1 as2. h=(hr,as1∪as2) ∧ as1∩as2={} ∧ (hr,as1)⊨A ∧ (hr,as2)⊨B)"
unfolding times_assn_def
apply (cases h)
by (auto simp: Abs_assn_inverse)

lemma mod_starD: "h⊨A*B ⟹ ∃h1 h2. h1⊨A ∧ h2⊨B"
by (auto simp: mod_star_conv)

lemma star_assnI:
assumes "(h,as)⊨P" and "(h,as')⊨Q" and "as∩as'={}"
shows "(h,as∪as')⊨P*Q"
using assms unfolding times_assn_def
by (auto simp: Abs_assn_inverse)

instantiation assn :: comm_monoid_mult begin
lemma assn_one_left: "1*P = (P::assn)"
unfolding one_assn_def times_assn_def
apply (rule)
apply (auto simp: Abs_assn_inverse)
done

lemma assn_times_comm: "P*Q = Q*(P::assn)"
unfolding times_assn_def
apply rule
apply (fastforce simp add: Abs_assn_inverse Un_ac)
done

lemma assn_times_assoc: "(P*Q)*R = P*(Q*(R::assn))"
unfolding times_assn_def
apply rule
apply (auto simp: Abs_assn_inverse)
apply (rule_tac x="as1∪as1a" in exI)
apply (rule_tac x="as2a" in exI)
apply (auto simp add: Un_ac) []

apply (rule_tac x="as1a" in exI)
apply (rule_tac x="as2a∪as2" in exI)
apply (fastforce simp add: Un_ac) []
done

instance
apply standard
apply (rule assn_times_assoc)
apply (rule assn_times_comm)
apply (rule assn_one_left)
done

end

subsubsection ‹Magic Wand›
fun wand_raw :: "assn_raw ⇒ assn_raw ⇒ assn_raw" where
"wand_raw P Q (h,as) ⟷ in_range (h,as)
∧ (∀h' as'. as∩as'={} ∧ relH as h h' ∧ in_range (h',as)
∧ P (h',as')
⟶ Q (h',as∪as'))"

lemma wand_proper[simp, intro!]: "proper (wand_raw P Q)"
apply (rule properI)
apply simp
apply (auto dest: relH_trans)
done

definition
wand_assn :: "assn ⇒ assn ⇒ assn" (infixl "-*" 56)
where "P-*Q ≡ Abs_assn (wand_raw (Rep_assn P) (Rep_assn Q))"

lemma wand_assnI:
assumes "in_range (h,as)"
assumes "⋀h' as'. ⟦
as ∩ as' = {};
relH as h h';
in_range (h',as);
(h',as')⊨Q
⟧ ⟹ (h',as∪as') ⊨ R"
shows "(h,as) ⊨ Q -* R"
using assms
unfolding wand_assn_def
apply (auto simp: Abs_assn_inverse)
done

subsubsection ‹Boolean Algebra on Assertions›
instantiation assn :: boolean_algebra begin
definition top_assn where "top ≡ Abs_assn in_range"
definition bot_assn where "bot ≡ Abs_assn (λ_. False)"
definition sup_assn where "sup P Q ≡ Abs_assn (λh. h⊨P ∨ h⊨Q)"
definition inf_assn where "inf P Q ≡ Abs_assn (λh. h⊨P ∧ h⊨Q)"
definition uminus_assn where
"-P ≡ Abs_assn (λh. in_range h ∧ ¬h⊨P)"

lemma bool_assn_proper[simp, intro!]:
"proper in_range"
"proper (λ_. False)"
"proper P ⟹ proper Q ⟹ proper (λh. P h ∨ Q h)"
"proper P ⟹ proper Q ⟹ proper (λh. P h ∧ Q h)"
"proper P ⟹ proper (λh. in_range h ∧ ¬P h)"
apply (auto
intro!: properI
intro: relH_in_rangeI
dest: properD1
simp: proper_iff)
done

text ‹(And, Or, True, False, Not) are a Boolean algebra.
Due to idiosyncrasies of the Isabelle/HOL class setup, we have to
also define a difference and an ordering:›
definition less_eq_assn where
[simp]: "(a::assn) ≤ b ≡ a = inf a b"

definition less_assn where
[simp]: "(a::assn) < b ≡ a ≤ b ∧ a≠b"

definition minus_assn where
[simp]: "(a::assn) - b ≡ inf a (-b)"

instance
apply standard
unfolding
top_assn_def bot_assn_def sup_assn_def inf_assn_def uminus_assn_def
less_eq_assn_def less_assn_def minus_assn_def
apply (auto
simp: Abs_assn_inverse conj_commute conj_ac
intro: Abs_assn_eqI models_in_range)
apply rule
apply (metis (mono_tags) Abs_assn_inverse[unfolded mem_Collect_eq]
Rep_assn[unfolded mem_Collect_eq] bool_assn_proper(4))
apply rule
apply (metis (mono_tags)
Abs_assn_inverse[unfolded mem_Collect_eq]
Rep_assn[unfolded mem_Collect_eq] bool_assn_proper(4))
apply rule
apply (metis (mono_tags)
Abs_assn_inverse[unfolded mem_Collect_eq]
Rep_assn[unfolded mem_Collect_eq] bool_assn_proper(4))
done

end

text ‹We give the operations some more standard names›
abbreviation top_assn::assn ("true") where "top_assn ≡ top"
abbreviation bot_assn::assn ("false") where "bot_assn ≡ bot"
abbreviation sup_assn::"assn⇒assn⇒assn" (infixr "∨⇩A" 61)
where "sup_assn ≡ sup"
abbreviation inf_assn::"assn⇒assn⇒assn" (infixr "∧⇩A" 62)
where "inf_assn ≡ inf"
abbreviation uminus_assn::"assn ⇒ assn" ("¬⇩A _" [81] 80)
where "uminus_assn ≡ uminus"

text ‹Now we prove some relations between the Boolean algebra operations
and the (empty heap,separation conjunction) monoid›

lemma star_false_left[simp]: "false * P = false"
unfolding times_assn_def bot_assn_def
apply rule
done

lemma star_false_right[simp]: "P * false = false"
using star_false_left by (simp add: assn_times_comm)

lemmas star_false = star_false_left star_false_right

lemma assn_basic_inequalities[simp, intro!]:
"true ≠ emp" "emp ≠ true"
"false ≠ emp" "emp ≠ false"
"true ≠ false" "false ≠ true"
subgoal
unfolding one_assn_def top_assn_def
proof (subst Abs_assn_inject; simp?)
have "in_range (⦇arrays = (λ_ _. []), refs = (λ_ _. 0), lim = 1⦈,{0})" (is "in_range ?h")
by (auto simp: in_range.simps)
moreover have "¬one_assn_raw ?h" by auto
ultimately show "in_range ≠ one_assn_raw" by auto
qed
subgoal
by (simp add: ‹true ≠ emp›)
subgoal
using star_false_left ‹true ≠ emp› by force
subgoal
by (simp add: ‹false ≠ emp›)
subgoal
by (metis inf_bot_right inf_top.right_neutral ‹true ≠ emp›)
subgoal
using ‹true ≠ false› by auto
done

subsubsection ‹Existential Quantification›
definition ex_assn :: "('a ⇒ assn) ⇒ assn" (binder "∃⇩A" 11)
where "(∃⇩Ax. P x) ≡ Abs_assn (λh. ∃x. h⊨P x)"

lemma ex_assn_proper[simp, intro!]:
"(⋀x. proper (P x)) ⟹ proper (λh. ∃x. P x h)"
by (auto intro!: properI dest: properD1 simp: proper_iff)

lemma ex_assn_const[simp]: "(∃⇩Ax. c) = c"
unfolding ex_assn_def by auto

lemma ex_one_point_gen:
"⟦⋀h x. h⊨P x ⟹ x=v⟧ ⟹ (∃⇩Ax. P x) = (P v)"
unfolding ex_assn_def
apply rule
apply auto
done

lemma ex_distrib_star: "(∃⇩Ax. P x * Q) = (∃⇩Ax. P x) * Q"
unfolding ex_assn_def times_assn_def
apply rule
apply fastforce
done

lemma ex_distrib_and: "(∃⇩Ax. P x ∧⇩A Q) = (∃⇩Ax. P x) ∧⇩A Q"
unfolding ex_assn_def inf_assn_def
apply rule
done

lemma ex_distrib_or: "(∃⇩Ax. P x ∨⇩A Q) = (∃⇩Ax. P x) ∨⇩A Q"
unfolding ex_assn_def sup_assn_def
apply rule
done

lemma ex_join_or: "(∃⇩Ax. P x ∨⇩A (∃⇩Ax. Q x)) = (∃⇩Ax. P x ∨⇩A Q x)"
unfolding ex_assn_def sup_assn_def
apply rule
done

subsubsection ‹Pure Assertions›
text ‹Pure assertions do not depend on any heap content.›
fun pure_assn_raw where "pure_assn_raw b (h,as) ⟷ as={} ∧ b"
definition pure_assn :: "bool ⇒ assn" ("↑") where
"↑b ≡ Abs_assn (pure_assn_raw b)"

lemma pure_assn_proper[simp, intro!]: "proper (pure_assn_raw b)"
by (auto intro!: properI intro: relH_in_rangeI)

lemma pure_true[simp]: "↑True = emp"
unfolding pure_assn_def one_assn_def
apply rule
apply (auto)
done

lemma pure_false[simp]: "↑False = false"
unfolding pure_assn_def bot_assn_def
apply rule
apply (auto simp: Abs_assn_inverse)
done

lemma pure_assn_eq_false_iff[simp]: "↑P = false ⟷ ¬P" by auto

lemma pure_assn_eq_emp_iff[simp]: "↑P = emp ⟷ P" by (cases P) auto

lemma merge_pure_star[simp]:
"↑a * ↑b = ↑(a∧b)"
unfolding times_assn_def
apply rule
unfolding pure_assn_def
apply fastforce
done

lemma merge_true_star[simp]: "true*true = true"
unfolding times_assn_def top_assn_def
apply rule
apply (fastforce simp: in_range.simps)
done

lemma merge_pure_and[simp]:
"↑a ∧⇩A ↑b = ↑(a∧b)"
unfolding inf_assn_def
apply rule
unfolding pure_assn_def
apply fastforce
done

lemma merge_pure_or[simp]:
"↑a ∨⇩A ↑b = ↑(a∨b)"
unfolding sup_assn_def
apply rule
unfolding pure_assn_def
apply fastforce
done

lemma pure_assn_eq_conv[simp]: "↑P = ↑Q ⟷ P=Q" by auto

definition "is_pure_assn a ≡ ∃P. a=↑P"
lemma is_pure_assnE: assumes "is_pure_assn a" obtains P where "a=↑P"
using assms
by (auto simp: is_pure_assn_def)

lemma is_pure_assn_pure[simp, intro!]: "is_pure_assn (↑P)"

lemma is_pure_assn_basic_simps[simp]:
"is_pure_assn false"
"is_pure_assn emp"
proof -
have "is_pure_assn (↑False)" by rule thus "is_pure_assn false" by simp
have "is_pure_assn (↑True)" by rule thus "is_pure_assn emp" by simp
qed

lemma is_pure_assn_starI[simp,intro!]:
"⟦is_pure_assn a; is_pure_assn b⟧ ⟹ is_pure_assn (a*b)"
by (auto elim!: is_pure_assnE)

subsubsection ‹Pointers›
text ‹In Imperative HOL, we have to distinguish between pointers to single
values and pointers to arrays. For both, we define assertions that
describe the part of the heap that a pointer points to.›
fun sngr_assn_raw :: "'a::heap ref ⇒ 'a ⇒ assn_raw" where
"sngr_assn_raw r x (h,as) ⟷ Ref.get h r = x ∧ as = {addr_of_ref r} ∧

lemma sngr_assn_proper[simp, intro!]: "proper (sngr_assn_raw r x)"
apply (auto intro!: properI simp: relH_ref)
apply (auto simp add: in_range.simps dest: relH_in_rangeI)
done

definition sngr_assn :: "'a::heap ref ⇒ 'a ⇒ assn" (infix "↦⇩r" 82)
where "r↦⇩rx ≡ Abs_assn (sngr_assn_raw r x)"

fun snga_assn_raw :: "'a::heap array ⇒ 'a list ⇒ assn_raw"
where "snga_assn_raw r x (h,as)
⟷ Array.get h r = x ∧ as = {addr_of_array r}
∧ addr_of_array r < lim h"

lemma snga_assn_proper[simp, intro!]: "proper (snga_assn_raw r x)"
apply (auto intro!: properI simp: relH_array)
apply (auto simp add: in_range.simps dest: relH_in_rangeI)
done

definition
snga_assn :: "'a::heap array ⇒ 'a list ⇒ assn" (infix "↦⇩a" 82)
where "r↦⇩aa ≡ Abs_assn (snga_assn_raw r a)"

text ‹Two disjoint parts of the heap cannot be pointed to by the
same pointer›
lemma sngr_same_false[simp]:
"p ↦⇩r x * p ↦⇩r y = false"
unfolding times_assn_def bot_assn_def sngr_assn_def
apply rule
apply (auto simp: Abs_assn_inverse)
done

lemma snga_same_false[simp]:
"p ↦⇩a x * p ↦⇩a y = false"
unfolding times_assn_def bot_assn_def snga_assn_def
apply rule
apply (auto simp: Abs_assn_inverse)
done

subsection ‹Properties of the Models-Predicate›
lemma mod_true[simp]: "h⊨true ⟷ in_range h"
unfolding top_assn_def by (simp add: Abs_assn_inverse)
lemma mod_false[simp]: "¬ h⊨false"
unfolding bot_assn_def by (simp add: Abs_assn_inverse)

lemma mod_emp: "h⊨emp ⟷ snd h = {}"
unfolding one_assn_def by (cases h) (simp add: Abs_assn_inverse)

lemma mod_emp_simp[simp]: "(h,{})⊨emp"

lemma mod_pure[simp]: "h⊨↑b ⟷ snd h = {} ∧ b"
unfolding pure_assn_def
apply (cases h)
done

lemma mod_ex_dist[simp]: "h⊨(∃⇩Ax. P x) ⟷ (∃x. h⊨P x)"
unfolding ex_assn_def by (auto simp: Abs_assn_inverse)

lemma mod_exI: "∃x. h⊨P x ⟹ h⊨(∃⇩Ax. P x)"
by (auto simp: mod_ex_dist)
lemma mod_exE: assumes "h⊨(∃⇩Ax. P x)" obtains x where "h⊨P x"
using assms by (auto simp: mod_ex_dist)

(* Not declared as simp, to not interfere with precision.
TODO: Perhaps define own connector for precision claims?
*)
lemma mod_and_dist: "h⊨P∧⇩AQ ⟷ h⊨P ∧ h⊨Q"
unfolding inf_assn_def by (simp add: Abs_assn_inverse)

lemma mod_or_dist[simp]: "h⊨P∨⇩AQ ⟷ h⊨P ∨ h⊨Q"
unfolding sup_assn_def by (simp add: Abs_assn_inverse)

lemma mod_not_dist[simp]: "h⊨(¬⇩AP) ⟷ in_range h ∧ ¬ h⊨P"
unfolding uminus_assn_def by (simp add: Abs_assn_inverse)

lemma mod_pure_star_dist[simp]: "h⊨P*↑b ⟷ h⊨P ∧ b"
by (metis (full_types) mod_false mult_1_right pure_false
pure_true star_false_right)

lemmas mod_dist = mod_pure mod_pure_star_dist mod_ex_dist mod_and_dist
mod_or_dist mod_not_dist

lemma mod_star_trueI: "h⊨P ⟹ h⊨P*true"
unfolding times_assn_def top_assn_def
apply (cases h)
apply auto
done

lemma mod_star_trueE': assumes "h⊨P*true" obtains h' where
"fst h' = fst h" and "snd h' ⊆ snd h" and "h'⊨P"
using assms
unfolding times_assn_def top_assn_def
apply (cases h)
done

lemma mod_star_trueE: assumes "h⊨P*true" obtains h' where "h'⊨P"
using assms by (blast elim: mod_star_trueE')

lemma mod_h_bot_iff[simp]:
"(h,{}) ⊨ ↑b ⟷ b"
"(h,{}) ⊨ true"
"(h,{}) ⊨ p↦⇩rx ⟷ False"
"(h,{}) ⊨ q↦⇩ay ⟷ False"
"(h,{}) ⊨ P*Q ⟷ ((h,{}) ⊨ P) ∧ ((h,{}) ⊨ Q)"
"(h,{}) ⊨ P∧⇩AQ ⟷ ((h,{}) ⊨ P) ∧ ((h,{}) ⊨ Q)"
"(h,{}) ⊨ P∨⇩AQ ⟷ ((h,{}) ⊨ P) ∨ ((h,{}) ⊨ Q)"
"(h,{}) ⊨ (∃⇩Ax. R x) ⟷ (∃x. (h,{}) ⊨ R x)"
apply simp
done

subsection ‹Entailment›
definition entails :: "assn ⇒ assn ⇒ bool" (infix "⟹⇩A" 10)
where "P ⟹⇩A Q ≡ ∀h. h⊨P ⟶ h⊨Q"

lemma entailsI:
assumes "⋀h. h⊨P ⟹ h⊨Q"
shows "P ⟹⇩A Q"
using assms unfolding entails_def by auto

lemma entailsD:
assumes "P ⟹⇩A Q"
assumes "h⊨P"
shows "h⊨Q"
using assms unfolding entails_def by blast

subsubsection ‹Properties›
lemma ent_fwd:
assumes "h⊨P"
assumes "P ⟹⇩A Q"
shows "h⊨Q" using assms(2,1) by (rule entailsD)

lemma ent_refl[simp]: "P ⟹⇩A P"
by (auto simp: entailsI)

lemma ent_trans[trans]: "⟦ P ⟹⇩A Q; Q ⟹⇩AR ⟧ ⟹ P ⟹⇩A R"
by (auto intro: entailsI dest: entailsD)

lemma ent_iffI:
assumes "A⟹⇩AB"
assumes "B⟹⇩AA"
shows "A=B"
apply (subst Rep_assn_inject[symmetric])
apply (rule ext)
using assms unfolding entails_def
by blast

lemma ent_false[simp]: "false ⟹⇩A P"
by (auto intro: entailsI)
lemma ent_true[simp]: "P ⟹⇩A true"
by (auto intro!: entailsI simp: models_in_range)

lemma ent_false_iff[simp]: "(P ⟹⇩A false) ⟷ (∀h. ¬h⊨P)"
unfolding entails_def
by auto

lemma ent_pure_pre_iff[simp]: "(P*↑b ⟹⇩A Q) ⟷ (b ⟶ (P ⟹⇩A Q))"
unfolding entails_def

lemma ent_pure_pre_iff_sng[simp]:
"(↑b ⟹⇩A Q) ⟷ (b ⟶ (emp ⟹⇩A Q))"
using ent_pure_pre_iff[where P=emp]
by simp

lemma ent_pure_post_iff[simp]:
"(P ⟹⇩A Q*↑b) ⟷ ((∀h. h⊨P ⟶ b) ∧ (P ⟹⇩A Q))"
unfolding entails_def

lemma ent_pure_post_iff_sng[simp]:
"(P ⟹⇩A ↑b) ⟷ ((∀h. h⊨P ⟶ b) ∧ (P ⟹⇩A emp))"
using ent_pure_post_iff[where Q=emp]
by simp

lemma ent_ex_preI: "(⋀x. P x ⟹⇩A Q) ⟹ ∃⇩Ax. P x ⟹⇩A Q"
unfolding entails_def ex_assn_def
by (auto simp: Abs_assn_inverse)

lemma ent_ex_postI: "(P ⟹⇩A Q x) ⟹ P ⟹⇩A ∃⇩Ax. Q x"
unfolding entails_def ex_assn_def
by (auto simp: Abs_assn_inverse)

lemma ent_mp: "(P * (P -* Q)) ⟹⇩A Q"
apply (rule entailsI)
unfolding times_assn_def wand_assn_def
apply (drule_tac x="a" in spec)
apply (drule_tac x="as1" in spec)
apply (auto simp: Un_ac relH_refl)
done

lemma ent_star_mono: "⟦ P ⟹⇩A P'; Q ⟹⇩A Q'⟧ ⟹ P*Q ⟹⇩A P'*Q'"
unfolding entails_def times_assn_def
apply metis
done

lemma ent_wandI:
assumes IMP: "Q*P ⟹⇩A R"
shows "P ⟹⇩A (Q -* R)"
unfolding entails_def
apply clarsimp
apply (rule wand_assnI)
apply (blast intro: models_in_range)
proof -
fix h as h' as'
assume "(h,as)⊨P"
and "as∩as'={}"
and "relH as h h'"
and "in_range (h',as)"
and "(h',as') ⊨ Q"

from ‹(h,as)⊨P› and ‹relH as h h'› have "(h',as)⊨P"
with ‹(h',as') ⊨ Q› and ‹as∩as'={}› have "(h',as∪as')⊨Q*P"
by (metis star_assnI Int_commute Un_commute)
with IMP show "(h',as∪as') ⊨ R" by (blast dest: ent_fwd)
qed

lemma ent_disjI1:
assumes "P ∨⇩A Q ⟹⇩A R"
shows "P ⟹⇩A R" using assms unfolding entails_def by simp

lemma ent_disjI2:
assumes "P ∨⇩A Q ⟹⇩A R"
shows "Q ⟹⇩A R" using assms unfolding entails_def by simp

lemma ent_disjI1_direct[simp]: "A ⟹⇩A A ∨⇩A B"

lemma ent_disjI2_direct[simp]: "B ⟹⇩A A ∨⇩A B"

lemma ent_disjE: "⟦ A⟹⇩AC; B⟹⇩AC ⟧ ⟹ A∨⇩AB ⟹⇩AC"
unfolding entails_def by auto

lemma ent_conjI: "⟦ A⟹⇩AB; A⟹⇩AC ⟧ ⟹ A ⟹⇩A B ∧⇩A C"
unfolding entails_def by (auto simp: mod_and_dist)

lemma ent_conjE1: "⟦A⟹⇩AC⟧ ⟹ A∧⇩AB⟹⇩AC"
unfolding entails_def by (auto simp: mod_and_dist)
lemma ent_conjE2: "⟦B⟹⇩AC⟧ ⟹ A∧⇩AB⟹⇩AC"
unfolding entails_def by (auto simp: mod_and_dist)

lemma star_or_dist1:
"(A ∨⇩A B)*C = (A*C ∨⇩A B*C)"
apply (rule ent_iffI)
unfolding entails_def

lemma star_or_dist2:
"C*(A ∨⇩A B) = (C*A ∨⇩A C*B)"
apply (rule ent_iffI)
unfolding entails_def

lemmas star_or_dist = star_or_dist1 star_or_dist2

lemma ent_disjI1': "A⟹⇩AB ⟹ A⟹⇩AB∨⇩AC"
by (auto simp: entails_def star_or_dist)

lemma ent_disjI2': "A⟹⇩AC ⟹ A⟹⇩AB∨⇩AC"
by (auto simp: entails_def star_or_dist)

lemma triv_exI[simp, intro!]: "Q x ⟹⇩A ∃⇩Ax. Q x"
by (meson ent_ex_postI ent_refl)

subsubsection ‹Weak Entails›
text ‹Weakening of entails to allow arbitrary unspecified memory in conclusion›
definition entailst :: "assn ⇒ assn ⇒ bool" (infix "⟹⇩t" 10)
where "entailst A B ≡ A ⟹⇩A B * true"

lemma enttI: "A⟹⇩AB*true ⟹ A⟹⇩tB" unfolding entailst_def .
lemma enttD: "A⟹⇩tB ⟹ A⟹⇩AB*true" unfolding entailst_def .

lemma entt_trans:
"entailst A B ⟹ entailst B C ⟹ entailst A C"
unfolding entailst_def
apply (erule ent_trans)
by (metis assn_times_assoc ent_star_mono ent_true merge_true_star)

lemma entt_refl[simp, intro!]: "entailst A A"
unfolding entailst_def

lemma entt_true[simp, intro!]:
"entailst A true"
unfolding entailst_def by simp

lemma entt_emp[simp, intro!]:
"entailst A emp"
unfolding entailst_def by simp

lemma entt_star_true_simp[simp]:
"entailst A (B*true) ⟷ entailst A B"
"entailst (A*true) B ⟷ entailst A B"
unfolding entailst_def
subgoal by (auto simp: assn_times_assoc)
subgoal
apply (intro iffI)
subgoal using entails_def mod_star_trueI by blast
subgoal by (metis assn_times_assoc ent_refl ent_star_mono merge_true_star)
done
done

lemma entt_star_mono: "⟦entailst A B; entailst C D⟧ ⟹ entailst (A*C) (B*D)"
unfolding entailst_def
proof -
assume a1: "A ⟹⇩A B * true"
assume "C ⟹⇩A D * true"
then have "A * C ⟹⇩A true * B * (true * D)"
using a1 assn_times_comm ent_star_mono by force
then show "A * C ⟹⇩A B * D * true"
qed

lemma entt_frame_fwd:
assumes "entailst P Q"
assumes "entailst A (P*F)"
assumes "entailst (Q*F) B"
shows "entailst A B"
using assms
by (metis entt_refl entt_star_mono entt_trans)

lemma enttI_true: "P*true ⟹⇩A Q*true ⟹ P⟹⇩tQ"
by (drule enttI) simp

lemma entt_def_true: "(P⟹⇩tQ) ≡ (P*true ⟹⇩A Q*true)"
unfolding entailst_def
apply (rule eq_reflection)
using entailst_def entt_star_true_simp(2) by auto

lemma ent_imp_entt: "P⟹⇩AQ ⟹ P⟹⇩tQ"
apply (rule enttI)
apply (erule ent_trans)

lemma entt_disjI1_direct[simp]: "A ⟹⇩t A ∨⇩A B"
by (rule ent_imp_entt[OF ent_disjI1_direct])

lemma entt_disjI2_direct[simp]: "B ⟹⇩t A ∨⇩A B"
by (rule ent_imp_entt[OF ent_disjI2_direct])

lemma entt_disjI1': "A⟹⇩tB ⟹ A⟹⇩tB∨⇩AC"
by (auto simp: entailst_def entails_def star_or_dist)

lemma entt_disjI2': "A⟹⇩tC ⟹ A⟹⇩tB∨⇩AC"
by (auto simp: entailst_def entails_def star_or_dist)

lemma entt_disjE: "⟦ A⟹⇩tM; B⟹⇩tM ⟧ ⟹ A∨⇩AB ⟹⇩t M"
using ent_disjE enttD enttI by blast

lemma entt_disjD1: "A∨⇩AB⟹⇩tC ⟹ A⟹⇩tC"
using entt_disjI1_direct entt_trans by blast

lemma entt_disjD2: "A∨⇩AB⟹⇩tC ⟹ B⟹⇩tC"
using entt_disjI2_direct entt_trans by blast

subsection ‹Precision›
text ‹
Precision rules describe that parts of an assertion may depend only on the
underlying heap. For example, the data where a pointer points to is the same
for the same heap.
›
text ‹Precision rules should have the form:
@{text [display] "∀x y. (h⊨(P x * F1) ∧⇩A (P y * F2)) ⟶ x=y"}›
definition "precise R ≡ ∀a a' h p F F'.
h ⊨ R a p * F ∧⇩A R a' p * F' ⟶ a = a'"

lemma preciseI[intro?]:
assumes "⋀a a' h p F F'. h ⊨ R a p * F ∧⇩A R a' p * F' ⟹ a = a'"
shows "precise R"
using assms unfolding precise_def by blast

lemma preciseD:
assumes "precise R"
assumes "h ⊨ R a p * F ∧⇩A R a' p * F'"
shows "a=a'"
using assms unfolding precise_def by blast

lemma preciseD':
assumes "precise R"
assumes "h ⊨ R a p * F"
assumes "h ⊨ R a' p * F'"
shows "a=a'"
apply (rule preciseD)
apply (rule assms)
apply (simp only: mod_and_dist)
apply (blast intro: assms)
done

lemma precise_extr_pure[simp]:
"precise (λx y. ↑P * R x y) ⟷ (P ⟶ precise R)"
"precise (λx y. R x y * ↑P) ⟷ (P ⟶ precise R)"
apply (cases P, (auto intro!: preciseI) [2])+
done

lemma sngr_prec: "precise (λx p. p↦⇩rx)"
apply rule
apply (clarsimp simp: mod_and_dist)
unfolding sngr_assn_def times_assn_def
apply auto
done

lemma snga_prec: "precise (λx p. p↦⇩ax)"
apply rule
apply (clarsimp simp: mod_and_dist)
unfolding snga_assn_def times_assn_def
apply auto
done

end


# Theory 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 ∧ 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]
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: "⟦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)

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


# Theory Automation

section ‹Automation›
theory Automation
imports Hoare_Triple (*"../Lib/Refine_Util"*)
begin

text ‹
In this theory, we provide a set of tactics and a simplifier setup for easy
reasoning with our separation logic.
›

subsection ‹Normalization of Assertions›
text ‹
In this section, we provide a set of lemmas and a simplifier
setup to bring assertions to a normal form. We provide a simproc that
detects pure parts of assertions and duplicate pointers. Moreover,
we provide ac-rules for assertions. See Section~\ref{sec:auto:overview}
for a short overview of the available proof methods.
›

lemmas assn_aci =
inf_aci[where 'a=assn]
sup_aci[where 'a=assn]
mult.left_ac[where 'a=assn]

lemmas star_assoc = mult.assoc[where 'a=assn]
lemmas assn_assoc =
mult.left_assoc inf_assoc[where 'a=assn] sup_assoc[where 'a=assn]

lemma merge_true_star_ctx: "true * (true * P) = true * P"

lemmas star_aci =
mult.assoc[where 'a=assn] mult.commute[where 'a=assn] mult.left_commute[where 'a=assn]
assn_one_left mult_1_right[where 'a=assn]
merge_true_star merge_true_star_ctx

text ‹Move existential quantifiers to the front of assertions›
lemma ex_assn_move_out[simp]:
"⋀Q R. (∃⇩Ax. Q x) * R = (∃⇩Ax. (Q x * R))"
"⋀Q R. R * (∃⇩Ax. Q x) = (∃⇩Ax. (R * Q x))"

"⋀P Q. (∃⇩Ax. Q x) ∧⇩A P = (∃⇩Ax. (Q x ∧⇩A P)) "
"⋀P Q. Q ∧⇩A (∃⇩Ax. P x) = (∃⇩Ax. (Q ∧⇩A P x))"

"⋀P Q. (∃⇩Ax. Q x) ∨⇩A P = (∃⇩Ax. (Q x ∨⇩A P))"
"⋀P Q. Q ∨⇩A (∃⇩Ax. P x) = (∃⇩Ax. (Q ∨⇩A P x))"
apply -
apply (subst mult.commute)
apply (subst (2) mult.commute)

apply (subst inf_commute)
apply (subst (2) inf_commute)

apply (subst sup_commute)
apply (subst (2) sup_commute)
done

text ‹Extract pure assertions from and-clauses›
lemma and_extract_pure_left_iff[simp]: "↑b ∧⇩A Q = (emp∧⇩AQ)*↑b"
by (cases b) auto

lemma and_extract_pure_left_ctx_iff[simp]: "P*↑b ∧⇩A Q = (P∧⇩AQ)*↑b"
by (cases b) auto

lemma and_extract_pure_right_iff[simp]: "P ∧⇩A ↑b = (emp∧⇩AP)*↑b"
by (cases b) (auto simp: assn_aci)

lemma and_extract_pure_right_ctx_iff[simp]: "P ∧⇩A Q*↑b = (P∧⇩AQ)*↑b"
by (cases b) auto

lemmas and_extract_pure_iff =
and_extract_pure_left_iff and_extract_pure_left_ctx_iff
and_extract_pure_right_iff and_extract_pure_right_ctx_iff

lemmas norm_assertion_simps =
(* Neutral elements *)
mult_1[where 'a=assn] mult_1_right[where 'a=assn]
inf_top_left[where 'a=assn] inf_top_right[where 'a=assn]
sup_bot_left[where 'a=assn] sup_bot_right[where 'a=assn]

(* Zero elements *)
star_false_left star_false_right
inf_bot_left[where 'a=assn] inf_bot_right[where 'a=assn]
sup_top_left[where 'a=assn] sup_top_right[where 'a=assn]

(* Associativity *)
mult.left_assoc[where 'a=assn]
inf_assoc[where 'a=assn]
sup_assoc[where 'a=assn]

(* Existential Quantifiers *)
ex_assn_move_out ex_assn_const

(* Extract pure assertions from conjunctions *)
and_extract_pure_iff

(* Merging *)
merge_pure_star merge_pure_and merge_pure_or
merge_true_star
inf_idem[where 'a=assn] sup_idem[where 'a=assn]

(* Duplicated References *)
sngr_same_false snga_same_false

subsubsection ‹Simplifier Setup Fine-Tuning›
text ‹Imperative HOL likes to simplify pointer inequations to this strange
operator. We do some additional simplifier setup here›
lemma not_same_noteqr[simp]: "¬ a=!=a"
by (metis Ref.unequal)
declare Ref.noteq_irrefl[dest!]

lemma not_same_noteqa[simp]: "¬ a=!!=a"
by (metis Array.unequal)
declare Array.noteq_irrefl[dest!]

text ‹However, it is safest to disable this rewriting, as there is
a working standard simplifier setup for ‹(≠)›
›
declare Ref.unequal[simp del]
declare Array.unequal[simp del]

subsection ‹Normalization of Entailments›

text ‹Used by existential quantifier extraction tactic›
lemma enorm_exI': (* Incomplete, as chosen x may depend on heap! *)
"(⋀x. Z x ⟶ (P ⟹⇩A Q x)) ⟹ (∃x. Z x) ⟶ (P ⟹⇩A (∃⇩Ax. Q x))"
by (metis ent_ex_postI)

text ‹Example of how to build an extraction lemma.›
thm enorm_exI'[OF enorm_exI'[OF imp_refl]]

lemmas ent_triv = ent_true ent_false

text ‹Dummy rule to detect Hoare triple goal›
lemma is_hoare_triple: "<P> c <Q> ⟹ <P> c <Q>" .
text ‹Dummy rule to detect entailment goal›
lemma is_entails: "P⟹⇩AQ ⟹ P ⟹⇩AQ" .

subsection ‹Frame Matcher›
text ‹Given star-lists P,Q and a frame F, this method tries to match
all elements of Q with corresponding elements of P. The result is a
partial match, that contains matching pairs and the unmatched content.›

text ‹The frame-matcher internally uses syntactic lists separated by
star, and delimited by the special symbol ‹SLN›, which is defined
to be ‹emp›.›
definition [simp]: "SLN ≡ emp"
lemma SLN_left: "SLN * P = P" by simp
lemma SLN_right: "P * SLN = P" by simp

lemmas SLN_normalize = SLN_right mult.left_assoc[where 'a=assn]
lemmas SLN_strip = SLN_right SLN_left mult.left_assoc[where 'a=assn]

text ‹A query to the frame matcher. Contains the assertions
P and Q that shall be matched, as well as a frame F, that is not
touched.›

definition [simp]: "FI_QUERY P Q F ≡ P ⟹⇩A Q*F"

abbreviation "fi_m_fst M ≡ foldr (*) (map fst M) emp"
abbreviation "fi_m_snd M ≡ foldr (*) (map snd M) emp"
abbreviation "fi_m_match M ≡ (∀(p,q)∈set M. p ⟹⇩A q)"

text ‹A result of the frame matcher. Contains a list of matching pairs,
as well as the unmatched parts of P and Q, and the frame F.
›
definition [simp]: "FI_RESULT M UP UQ F ≡
fi_m_match M ⟶ (fi_m_fst M * UP ⟹⇩A fi_m_snd M * UQ * F)"

text ‹Internal structure used by the frame matcher:
m contains the matched pairs; p,q the assertions that still needs to be
matched; up,uq the assertions that could not be matched; and f the frame.
p and q are SLN-delimited syntactic lists.
›

definition [simp]: "FI m p q up uq f ≡
fi_m_match m ⟶ (fi_m_fst m * p * up ⟹⇩A fi_m_snd m * q * uq * f)"

text ‹Initialize processing of query›
lemma FI_init:
assumes "FI [] (SLN*P) (SLN*Q) SLN SLN F"
shows "FI_QUERY P Q F"
using assms by simp

text ‹Construct result from internal representation›
lemma FI_finalize:
assumes "FI_RESULT m (p*up) (q*uq) f"
shows "FI m p q up uq f"
using assms by (simp add: assn_aci)

text ‹Auxiliary lemma to show that all matching pairs together form
an entailment. This is required for most applications.›
lemma fi_match_entails:
assumes "fi_m_match m"
shows "fi_m_fst m ⟹⇩A fi_m_snd m"
using assms apply (induct m)
apply (simp_all split: prod.split_asm add: ent_star_mono)
done

text ‹Internally, the frame matcher tries to match the first assertion
of q with the first assertion of p. If no match is found, the first
assertion of p is discarded. If no match for any assertion in p can be
found, the first assertion of q is discarded.›

text ‹Match›
lemma FI_match:
assumes "p ⟹⇩A q"
assumes "FI ((p,q)#m) (ps*up) (qs*uq) SLN SLN f"
shows "FI m (ps*p) (qs*q) up uq f"
using assms unfolding FI_def

text ‹No match›
lemma FI_p_nomatch:
assumes "FI m ps (qs*q) (p*up) uq f"
shows "FI m (ps*p) (qs*q) up uq f"
using assms unfolding FI_def

text ‹Head of q could not be matched›
lemma FI_q_nomatch:
assumes "FI m (SLN*up) qs SLN (q*uq) f"
shows "FI m SLN (qs*q) up uq f"
using assms unfolding FI_def

subsection ‹Frame Inference›
lemma frame_inference_init:
assumes "FI_QUERY P Q F"
shows "P ⟹⇩A Q * F"
using assms by simp

lemma frame_inference_finalize:
shows "FI_RESULT M F emp F"
apply simp
apply rule
apply (drule fi_match_entails)
apply (rule ent_star_mono[OF _ ent_refl])
apply assumption
done

subsection ‹Entailment Solver›
lemma entails_solve_init:
"FI_QUERY P Q true ⟹ P ⟹⇩A Q * true"
"FI_QUERY P Q emp ⟹ P ⟹⇩A Q"

lemma entails_solve_finalize:
"FI_RESULT M P emp true"
"FI_RESULT M emp emp emp"
by (auto simp add: fi_match_entails intro: ent_star_mono)

lemmas solve_ent_preprocess_simps =
ent_pure_post_iff ent_pure_post_iff_sng ent_pure_pre_iff ent_pure_pre_iff_sng

subsection ‹Verification Condition Generator›

lemmas normalize_rules = norm_pre_ex_rule norm_pre_pure_rule

(* Originally we introduced backwards-reasoning here, via
cons_pre_rule[OF _ return_wp_rule] (old name: complete_return_cons).
This only works, if the postcondition is not schematic! However, for
forward reasoning, one usually assumes a schematic postcondition!
*)
text ‹May be useful in simple, manual proofs, where the postcondition
is no schematic variable.›
lemmas return_cons_rule = cons_pre_rule[OF _ return_wp_rule]

text ‹Useful frame-rule variant for manual proof:›
lemma frame_rule_left:
"<P> c <Q> ⟹ <R * P> c <λx. R * Q x>"
using frame_rule by (simp add: assn_aci)

lemmas deconstruct_rules =
bind_rule if_rule false_rule return_sp_rule let_rule
case_prod_rule case_list_rule case_option_rule case_sum_rule

lemmas heap_rules =
ref_rule
lookup_rule
update_rule
new_rule
make_rule
of_list_rule
length_rule
nth_rule
upd_rule
freeze_rule

lemma fi_rule:
assumes CMD: "<P> c <Q>"
assumes FRAME: "Ps ⟹⇩A P * F"
shows "<Ps> c <λx. Q x * F>"
apply (rule cons_pre_rule[rotated])
apply (rule frame_rule)
apply (rule CMD)
apply (rule FRAME)
done

subsection ‹ML-setup›

named_theorems sep_dflt_simps "Seplogic: Default simplification rules for automated solvers"
named_theorems sep_eintros "Seplogic: Intro rules for entailment solver"
named_theorems sep_heap_rules "Seplogic: VCG heap rules"
named_theorems sep_decon_rules "Seplogic: VCG deconstruct rules"

ML ‹
infix 1 THEN_IGNORE_NEWGOALS

structure Seplogic_Auto =
struct

(***********************************)
(*             Tools               *)
(***********************************)

(* Repeat tac on subgoal. Determinize each step.
Stop if tac fails or subgoal is solved. *)
fun REPEAT_DETERM' tac i st = let
val n = Thm.nprems_of st
in
REPEAT_DETERM (COND (has_fewer_prems n) no_tac (tac i)) st
end

(***********************************)
(*             Debugging           *)
(***********************************)
fun tr_term t = Pretty.string_of (Syntax.pretty_term @{context} t);

(***********************************)
(*        Custom Tacticals         *)
(***********************************)

(* Apply tac1, and then tac2 with an offset such that anything left
over by tac1 is skipped.

The typical usage of this tactic is, if a theorem is instantiated
with another theorem that produces additional goals that should
be ignored first. Here, it is used in the vcg to ensure that
frame inference is done before additional premises (that may
depend on the frame) are discharged.
*)
fun (tac1 THEN_IGNORE_NEWGOALS tac2) i st = let
val np = Thm.nprems_of st
in
(tac1 i THEN (fn st' => let val np' = Thm.nprems_of st' in
if np'<np then tac2 i st'
else tac2 (i+(np'-np)+1) st'
end)) st
end;

(***********************************)
(*     Assertion Normalization     *)
(***********************************)
(* Find two terms in a list whose key is equal *)
fun find_similar (key_of:term -> term) (ts:term list) = let
fun frec _ [] = NONE
| frec tab (t::ts) = let val k=key_of t in
if Termtab.defined tab k then
SOME (the (Termtab.lookup tab k),t)
else frec (Termtab.update (k,t) tab) ts
end
in
frec Termtab.empty ts
end;

(* Perform DFS over term with binary operator opN, threading through
a state. Atomic terms are transformed by tr. Supports omission of
terms from the result structure by transforming them to NONE. *)
fun dfs_opr opN (tr:'state -> term -> ('state*term option))
d (t as ((op_t as Const (fN,_))$t1$t2)) =
if fN = opN then let
val (d1,t1') = dfs_opr opN tr d t1;
val (d2,t2') = dfs_opr opN tr d1 t2;
in
case (t1',t2') of
(NONE,NONE) => (d2,NONE)
| (SOME t1',NONE) => (d2,SOME t1')
| (NONE,SOME t2') => (d2,SOME t2')
| (SOME t1',SOME t2') => (d2,SOME (op_t$t1'$t2'))
end
else tr d t
| dfs_opr _ tr d t = tr d t;

(* Replace single occurrence of (atomic) ot in t by nt.
Returns new term or NONE if nothing was removed. *)
fun dfs_replace_atomic opN ot nt t = let
fun tr d t = if not d andalso t=ot then (true,SOME nt) else (d,SOME t);
val (success,SOME t') = dfs_opr opN tr false t;
in
if success then SOME t' else NONE
end;

fun assn_simproc_fun ctxt credex = let
val ([redex],ctxt') = Variable.import_terms true [Thm.term_of credex] ctxt;
(*val _ = tracing (tr_term redex);*)
val export = singleton (Variable.export ctxt' ctxt)

fun mk_star t1 t2 = @{term "(*)::assn ⇒ _ ⇒ _"}$t2$t1;

fun mk_star' NONE NONE = NONE
| mk_star' (SOME t1) NONE  = SOME t1
| mk_star' NONE (SOME t2) = SOME t2
| mk_star' (SOME t1) (SOME t2) = SOME (mk_star t1 t2);

fun ptrs_key (_$k$_) = k;

fun remove_term pt t = case
dfs_replace_atomic @{const_name "Groups.times_class.times"} pt
@{term emp} t
of
SOME t' => t';

fun normalize t = let

fun ep_tr (has_true,ps,ptrs) t = case t of
Const (@{const_name "Assertions.pure_assn"},_)$_ => ((has_true,t::ps,ptrs),NONE) | Const (@{const_name "Assertions.sngr_assn"},_)$_$_ => ((has_true,ps,t::ptrs),SOME t) | Const (@{const_name "Assertions.snga_assn"},_)$_$_ => ((has_true,ps,t::ptrs),SOME t) | Const (@{const_name "Orderings.top_class.top"},_) => ((true,ps,ptrs),NONE) | (inf_op as Const (@{const_name "Lattices.inf_class.inf"},_))$t1$t2 => ((has_true,ps,ptrs),SOME (inf_op$normalize t1$normalize t2)) | _ => ((has_true,ps,ptrs),SOME t); fun normalizer t = case dfs_opr @{const_name "Groups.times_class.times"} ep_tr (false,[],[]) t of ((has_true,ps,ptrs),rt) => ((has_true,rev ps,ptrs),rt); fun normalize_core t = let val ((has_true,pures,ptrs),rt) = normalizer t; val similar = find_similar ptrs_key ptrs; val true_t = if has_true then SOME @{term "Assertions.top_assn"} else NONE; val pures' = case pures of [] => NONE | p::ps => SOME (fold mk_star ps p); in case similar of NONE => the (mk_star' pures' (mk_star' true_t rt)) | SOME (t1,t2) => let val t_stripped = remove_term t1 (remove_term t2 t); in mk_star t_stripped (mk_star t1 t2) end end; fun skip_ex ((exq as Const (@{const_name "ex_assn"},_))$(Abs (n,ty,t))) =
exq$Abs (n,ty,skip_ex t) | skip_ex t = normalize_core t; val (bs,t') = strip_abs t; val ty = fastype_of1 (map #2 bs,t'); in if ty = @{typ assn} then Logic.rlist_abs (bs,skip_ex t') else t end; (*val _ = tracing (tr_term redex);*) val (f,terms) = strip_comb redex; val nterms = map (fn t => let (*val _ = tracing (tr_term t); *) val t'=normalize t; (*val _ = tracing (tr_term t');*) in t' end) terms; val new_form = list_comb (f,nterms); val res_ss = (put_simpset HOL_basic_ss ctxt addsimps @{thms star_aci}); val result = Option.map (export o mk_meta_eq) (Arith_Data.prove_conv_nohyps [simp_tac res_ss 1] ctxt' (redex,new_form) ); in result end handle exc => if Exn.is_interrupt exc then Exn.reraise exc else (tracing ("assn_simproc failed with exception\n:" ^ Runtime.exn_message exc); NONE) (* Fail silently *); val assn_simproc = Simplifier.make_simproc @{context} "assn_simproc" {lhss = [@{term "h ⊨ P"}, @{term "P ⟹⇩A Q"}, @{term "P ⟹⇩t Q"}, @{term "Hoare_Triple.hoare_triple P c Q"}, @{term "(P::assn) = Q"}], proc = K assn_simproc_fun}; (***********************************) (* Default Simplifications *) (***********************************) (* Default simplification. MUST contain assertion normalization! Tactic must not fail! *) fun dflt_tac ctxt = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimprocs [assn_simproc] addsimps @{thms norm_assertion_simps} addsimps (Named_Theorems.get ctxt @{named_theorems sep_dflt_simps}) |> fold Splitter.del_split @{thms if_split} ); (***********************************) (* Frame Matcher *) (***********************************) (* Do frame matching imp_solve_tac - tactic used to discharge first assumption of match-rule cf. lemma FI_match. *) fun match_frame_tac imp_solve_tac ctxt = let (* Normalize star-lists *) val norm_tac = simp_tac ( put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_normalize}); (* Strip star-lists *) val strip_tac = simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_strip}) THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_def}); (* Do a match step *) val match_tac = resolve_tac ctxt @{thms FI_match} (* Separate p,q*) THEN' SOLVED' imp_solve_tac (* Solve implication *) THEN' norm_tac; (* Do a no-match step *) val nomatch_tac = resolve_tac ctxt @{thms FI_p_nomatch} ORELSE' (resolve_tac ctxt @{thms FI_q_nomatch} THEN' norm_tac); in resolve_tac ctxt @{thms FI_init} THEN' norm_tac THEN' REPEAT_DETERM' (FIRST' [ CHANGED o dflt_tac ctxt, (match_tac ORELSE' nomatch_tac)]) THEN' resolve_tac ctxt @{thms FI_finalize} THEN' strip_tac end; (***********************************) (* Frame Inference *) (***********************************) fun frame_inference_tac ctxt = resolve_tac ctxt @{thms frame_inference_init} THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt THEN' resolve_tac ctxt @{thms frame_inference_finalize}; (***********************************) (* Entailment Solver *) (***********************************) (* Extract existential quantifiers from entailment goal *) fun extract_ex_tac ctxt i st = let fun count_ex (Const (@{const_name Assertions.entails},_)$_$c) = count_ex c RS @{thm HOL.mp} | count_ex (Const (@{const_name Assertions.ex_assn},_)$Abs (_,_,t))
= count_ex t RS @{thm enorm_exI'}
| count_ex _ = @{thm imp_refl};

val concl = Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop;
val thm = count_ex concl;
in
(TRY o REPEAT_ALL_NEW (match_tac ctxt @{thms ent_ex_preI}) THEN'
resolve_tac ctxt [thm]) i st
end;

(* Solve Entailment *)
fun solve_entails_tac ctxt = let
val preprocess_entails_tac =
dflt_tac ctxt
THEN' extract_ex_tac ctxt
THEN' simp_tac
(put_simpset HOL_ss ctxt addsimps @{thms solve_ent_preprocess_simps});

val match_entails_tac =
resolve_tac ctxt @{thms entails_solve_init}
THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt
THEN' resolve_tac ctxt @{thms entails_solve_finalize};
in
preprocess_entails_tac
THEN' (TRY o
REPEAT_ALL_NEW (match_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems sep_eintros}))))
THEN_ALL_NEW (dflt_tac ctxt THEN'
TRY o (match_tac ctxt @{thms ent_triv}
ORELSE' resolve_tac ctxt @{thms ent_refl}
ORELSE' match_entails_tac))
end;

(***********************************)
(* Verification Condition Generator*)
(***********************************)

fun heap_rule_tac ctxt h_thms =
resolve_tac ctxt h_thms ORELSE' (
resolve_tac ctxt @{thms fi_rule} THEN' (resolve_tac ctxt h_thms THEN_IGNORE_NEWGOALS
frame_inference_tac ctxt));

fun vcg_step_tac ctxt = let
val h_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules});
val d_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_decon_rules});
val heap_rule_tac = heap_rule_tac ctxt h_thms

(* Apply consequence rule if postcondition is not a schematic var *)
fun app_post_cons_tac i st =
case Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop of
Const (@{const_name Hoare_Triple.hoare_triple},_)$_$_$qt => if is_Var (head_of qt) then no_tac st else resolve_tac ctxt @{thms cons_post_rule} i st | _ => no_tac st; in CSUBGOAL (snd #> (FIRST' [ CHANGED o dflt_tac ctxt, REPEAT_ALL_NEW (resolve_tac ctxt @{thms normalize_rules}), CHANGED o (FIRST' [resolve_tac ctxt d_thms, heap_rule_tac] ORELSE' (app_post_cons_tac THEN' FIRST' [resolve_tac ctxt d_thms, heap_rule_tac])) ])) end; fun vcg_tac ctxt = REPEAT_DETERM' (vcg_step_tac ctxt) (***********************************) (* Automatic Solver *) (***********************************) fun sep_autosolve_tac do_pre do_post ctxt = let val pre_tacs = [ CHANGED o clarsimp_tac ctxt, CHANGED o REPEAT_ALL_NEW (match_tac ctxt @{thms ballI allI impI conjI}) ]; val main_tacs = [ match_tac ctxt @{thms is_hoare_triple} THEN' CHANGED o vcg_tac ctxt, match_tac ctxt @{thms is_entails} THEN' CHANGED o solve_entails_tac ctxt ]; val post_tacs = [SELECT_GOAL (auto_tac ctxt)]; val tacs = (if do_pre then pre_tacs else []) @ main_tacs @ (if do_post then post_tacs else []); in REPEAT_DETERM' (CHANGED o FIRST' tacs) end; (***********************************) (* Method Setup *) (***********************************) val dflt_simps_modifiers = [ Args.$$"dflt_simps" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_dflt_simps}) ⌂), Args.$$$ "dflt_simps" -- Scan.option Args.del -- Args.colon
>> K (Method.modifier (Named_Theorems.del @{named_theorems sep_dflt_simps}) ⌂)
];
val heap_modifiers = [
Args.$$"heap" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_heap_rules}) ⌂), Args.$$$"heap" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_heap_rules}) ⌂) ]; val decon_modifiers = [ Args.$$"decon" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_decon_rules}) ⌂), Args.$$$ "decon" -- Scan.option Args.del -- Args.colon
>> K (Method.modifier (Named_Theorems.del @{named_theorems sep_decon_rules}) ⌂)
];

val eintros_modifiers = [
Args.$$"eintros" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_eintros}) ⌂), Args.$$\$ "eintros" -- Scan.option Args.del -- Args.colon
>> K (Method.modifier (Named_Theorems.del @{named_theorems sep_eintros}) ⌂)
];

val solve_entails_modifiers = dflt_simps_modifiers @ eintros_modifiers;

val vcg_modifiers =
heap_modifiers @ decon_modifiers @ dflt_simps_modifiers;

val sep_auto_modifiers =
clasimp_modifiers @ vcg_modifiers @ eintros_modifiers;

end;
›

simproc_setup assn_simproc
("h⊨P" | "P⟹⇩AQ" | "P⟹⇩tQ" | "<P> c <R>" | "(P::assn) = Q")
= ‹K Seplogic_Auto.assn_simproc_fun›

method_setup assn_simp =‹Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
CHANGED o Seplogic_Auto.dflt_tac ctxt
)))› "Seplogic: Simplification of assertions"

method_setup frame_inference = ‹Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
CHANGED o Seplogic_Auto.frame_inference_tac ctxt
)))› "Seplogic: Frame inference"

method_setup solve_entails = ‹
Method.sections Seplogic_Auto.solve_entails_modifiers >>
(fn _ => fn ctxt => SIMPLE_METHOD' (
CHANGED o Seplogic_Auto.solve_entails_tac ctxt
))› "Seplogic: Entailment Solver"

method_setup heap_rule = ‹
Attrib.thms >>
(fn thms => fn ctxt => SIMPLE_METHOD' (
let
val thms = case thms of [] => rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules})
| _ => thms
in
CHANGED o Seplogic_Auto.heap_rule_tac ctxt thms
end
))› "Seplogic: Apply rule with frame inference"

method_setup vcg = ‹
Scan.lift (Args.mode "ss") --
Method.sections Seplogic_Auto.vcg_modifiers >>
(fn (ss,_) => fn ctxt => SIMPLE_METHOD' (
CHANGED o (
if ss then Seplogic_Auto.vcg_step_tac ctxt
else Seplogic_Auto.vcg_tac ctxt
)
))› "Seplogic: Verification Condition Generator"

method_setup sep_auto =
‹Scan.lift (Args.mode "nopre" -- Args.mode "nopost" -- Args.mode "plain")
--| Method.sections Seplogic_Auto.sep_auto_modifiers >>
(fn ((nopre,nopost),plain) => fn ctxt => SIMPLE_METHOD' (
CHANGED o Seplogic_Auto.sep_autosolve_tac
((not nopre) andalso (not plain))
((not nopost) andalso (not plain)) ctxt
))› "Seplogic: Automatic solver"

lemmas [sep_dflt_simps] = split

declare deconstruct_rules[sep_decon_rules]
declare heap_rules[sep_heap_rules]

lemmas [sep_eintros] = impI conjI exI

subsection ‹Semi-Automatic Reasoning›
text ‹In this section, we provide some lemmas for semi-automatic reasoning›

text ‹Forward reasoning with frame. Use ‹frame_inference›-method
to discharge second assumption.›
lemma ent_frame_fwd:
assumes R: "P ⟹⇩A R"
assumes F: "Ps ⟹⇩A P*F"
assumes I: "R*F ⟹⇩A Q"
shows "Ps ⟹⇩A Q"
using assms
by (metis ent_refl ent_star_mono ent_trans)

lemma mod_frame_fwd:
assumes M: "h⊨Ps"
assumes R: "P⟹⇩AR"
assumes F: "Ps ⟹⇩A P*F"
shows "h⊨R*F"
using assms
by (metis ent_star_mono entails_def)

text ‹Apply precision rule with frame inference.›
lemma prec_frame:
assumes PREC: "precise P"
assumes M1: "h⊨(R1 ∧⇩A R2)"
assumes F1: "R1 ⟹⇩A P x p * F1"
assumes F2: "R2 ⟹⇩A P y p * F2"
shows "x=y"
using preciseD[OF PREC] M1 F1 F2
by (metis entailsD mod_and_dist)

lemma prec_frame_expl:
assumes PREC: "∀x y. (h⊨(P x * F1) ∧⇩A (P y * F2)) ⟶ x=y"
assumes M1: "h⊨(R1 ∧⇩A R2)"
assumes F1: "R1 ⟹⇩A P x * F1"
assumes F2: "R2 ⟹⇩A P y * F2"
shows "x=y"
using assms
by (metis entailsD mod_and_dist)

text ‹Variant that is useful within induction proofs, where induction
goes over ‹x› or ‹y››
lemma prec_frame':
assumes PREC: "(h⊨(P x * F1) ∧⇩A (P y * F2)) ⟶ x=y"
assumes M1: "h⊨(R1 ∧⇩A R2)"
assumes F1: "R1 ⟹⇩A P x * F1"
assumes F2: "R2 ⟹⇩A P y * F2"
shows "x=y"
using assms
by (metis entailsD mod_and_dist)

lemma ent_wand_frameI:
assumes "(Q -* R) * F ⟹⇩A S"
assumes "P ⟹⇩A F * X"
assumes "Q*X ⟹⇩A R"
shows "P ⟹⇩A S"
using assms
by (metis ent_frame_fwd ent_wandI mult.commute)

subsubsection ‹Manual Frame Inference›

lemma ent_true_drop:
"P⟹⇩AQ*true ⟹ P*R⟹⇩AQ*true"
"P⟹⇩AQ ⟹ P⟹⇩AQ*true"
apply (metis assn_times_comm ent_star_mono ent_true merge_true_star_ctx)
apply (metis assn_one_left ent_star_mono ent_true star_aci(2))
done

lemma fr_refl: "A⟹⇩AB ⟹ A*C ⟹⇩AB*C"
by (blast intro: ent_star_mono ent_refl)

lemma fr_rot: "(A*B ⟹⇩A C) ⟹ (B*A ⟹⇩A C)"

lemma fr_rot_rhs: "(A ⟹⇩A B*C) ⟹ (A ⟹⇩A C*B)"

lemma ent_star_mono_true:
assumes "A ⟹⇩A A' * true"
assumes "B ⟹⇩A B' * true"
shows "A*B*true ⟹⇩A A'*B'*true"
using ent_star_mono[OF assms] apply simp
using ent_true_drop(1) by blast

lemma ent_refl_true: "A ⟹⇩A A * true"

lemma entt_fr_refl: "F⟹⇩tF' ⟹ F*A ⟹⇩t F'*A" by (rule entt_star_mono) auto
lemma entt_fr_drop: "F⟹⇩tF' ⟹ F*A ⟹⇩t F'"
using ent_true_drop(1) enttD enttI by blast

method_setup fr_rot = ‹
let
fun rot_tac ctxt =
resolve_tac ctxt @{thms fr_rot} THEN'
simp_tac (put_simpset HOL_basic_ss ctxt

in
Scan.lift Parse.nat >>
(fn n => fn ctxt => SIMPLE_METHOD' (
fn i => REPEAT_DETERM_N n (rot_tac ctxt i)))

end
›

method_setup fr_rot_rhs = ‹
let
fun rot_tac ctxt =
resolve_tac ctxt @{thms fr_rot_rhs} THEN'
simp_tac (put_simpset HOL_basic_ss ctxt

in
Scan.lift Parse.nat >>
(fn n => fn ctxt => SIMPLE_METHOD' (
fn i => REPEAT_DETERM_N n (rot_tac ctxt i)))

end
›

(*<*)
subsection ‹Test Cases›

lemma "⋀x. A x * true * Q x ⟹⇩A true * A x * Q x"
apply simp
done

lemma "A * (true * B) ⟹⇩A true * A * B"
apply (simp)
done

lemma "h⊨true*P*true ⟷ h⊨P*true"
by simp

lemma "A * true * ↑(b ∧ c) * true * B ⟹⇩A ↑b * ↑c * true *A * B"
by simp

lemma "∃y c. ∃⇩Ax. P x * (R x * Q y) * ↑ (b ∧ c) ⟹⇩A (∃⇩Ax. ↑b * (P x * (R x * Q y) * ↑c))"
apply simp
done

lemma "A * B * (↑c * B * C * D * ↑a * true * ↑d) * (∃⇩Ax. E x * F * ↑b) * true ⟹⇩A (∃⇩Ax. ↑ (c ∧ a ∧ d ∧ b) *
true * A * B * (true * B * C * D) * (E x * F))"
apply simp
done

lemma "<P> c <λr. Q r * true * ↑(b r) * true * ↑a>
⟷ <P> c <λr. Q r * true * ↑(b r ∧ a)>"
apply simp
done

lemma "(h⊨((A*B*↑b*true*↑c*true) ∧⇩A (↑(p=q)*P*Q)))
⟷ h ⊨ A * B * true ∧⇩A P * Q ∧ b ∧ c ∧ p = q"
apply simp
done

lemma assumes "FI_RESULT [(B, B), (A, A)] C D F"
shows "FI_QUERY (A*B*C) (D*B*A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

lemma
assumes "FI_RESULT [(B,B), (A,A)] C emp F"
shows "FI_QUERY (A*B*C) (B*A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

lemma
assumes "FI_RESULT [(B, B), (A, A)] emp emp F"
shows "FI_QUERY (A*B) (B*A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

lemma
assumes "FI_RESULT [(A, A)] emp emp F"
shows "FI_QUERY (A) (A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

lemma
assumes "FI_RESULT [(A, A)] (B * C * D) emp F"
shows "FI_QUERY (B*C*D*A) (A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

schematic_goal
"P1 * P2 * P3 * P4 ⟹⇩A P3 * ?R1"
"P1 * (P2 * (P3 * P4)) ⟹⇩A P1 * ?R2"
"P4 * (P2 * (P1 * P3)) ⟹⇩A P1 * ?R2'"
"P1 * P2 * P3 * P4 ⟹⇩A P4 * ?R3"
"P1 * P2 ⟹⇩A P1 * ?R4"
"P1 * P2 ⟹⇩A P2 * ?R5"
"P1 ⟹⇩A P1 * ?R6"
"P1 * P2 ⟹⇩A emp * ?R7"
by frame_inference+

lemma "⟦A; B; C; b 17⟧ ⟹
Q 1 5 3 ⟹⇩A (∃⇩Ax y z. ∃⇩Aa. Q x y z * ↑(b a) * ↑(y=5))"
by solve_entails

thm nth_rule
lemma "<P * x↦⇩a[1,2,3]>
do { v←Array.nth x 1; return v }
<λr. P * x↦⇩a[1,2,3] * ↑(r=2)>"
apply sep_auto
done

(*>*)

subsection ‹Quick Overview of Proof Methods›
text_raw ‹\label{sec:auto:overview}›
text ‹
In this section, we give a quick overview of the available proof methods
and options. The most versatile proof method that we provide is
‹sep_auto›. It tries to solve the first subgoal, invoking appropriate
proof methods as required. If it cannot solve the subgoal completely, it
stops at the intermediate state that it could not handle any more.

‹sep_auto› can be configured by
section-arguments for the simplifier, the classical reasoner, and all
section-arguments for the verification condition generator and
entailment solver. Moreover, it takes an optional mode argument (mode), where
valid modes are:
\begin{description}
\item[(nopre)] No preprocessing of goal. The preprocessor tries to clarify
and simplify the goal before the main method is invoked.
\item[(nopost)] No postprocessing of goal. The postprocessor tries to
solve or simplify goals left over by verification condition generation or
entailment solving.
\item[(plain)] Neither pre- nor postprocessing. Just applies vcg and
entailment solver.
\end{description}

\paragraph{Entailment Solver.} The entailment solver processes goals of the
form ‹P ⟹⇩A Q›. It is invoked by the method ‹solve_entails›.
It first tries to pull out pure parts of
‹P› and ‹Q›. This may introduce quantifiers, conjunction,
and implication into the goal, that are eliminated by resolving with rules
declared as ‹sep_eintros› (method argument: eintros[add/del]:).
Moreover, it simplifies with rules declared as ‹sep_dflt_simps›

Now, ‹P› and ‹Q› should have the form ‹X⇩1*…*X⇩n›.
Then, the frame-matcher is used to match all items of ‹P› with items
of ‹Q›, and thus solve the implication. Matching is currently done
syntactically, but can instantiate schematic variables.

Note that, by default, existential introduction is declared as
‹sep_eintros›-rule. This introduces schematic variables, that can
later be matched against. However, in some cases, the matching may instantiate
the schematic variables in an undesired way. In this case, the argument
‹eintros del: exI› should be passed to the entailment solver, and
the existential quantifier should be instantiated manually.

\paragraph{Frame Inference}
The method ‹frame_inference› tries to solve a goal of the
form ‹P⟹Q*?F›, by matching ‹Q› against the parts of
‹P›, and instantiating ‹?F› accordingly.
Matching is done syntactically, possibly
instantiating schematic variables. ‹P› and ‹Q› should be
assertions separated by ‹*›. Note that frame inference does no
simplification or other kinds of normalization.

The method ‹heap_rule› applies the specified heap rules, using
frame inference if necessary. If no rules are specified, the default
heap rules are used.

\paragraph{Verification Condition Generator}
The verification condition generator processes goals of the form
‹<P>c<Q>›. It is invoked by the method ‹vcg›.
First, it tries to pull out pure parts and simplifies with
the default simplification rules. Then, it tries to resolve the goal with
deconstruct rules (attribute: ‹sep_decon_rules›,
section argument: ‹decon[add/del]:›), and if this does not succeed,
it tries
to resolve the goal with heap rules (attribute: ‹sep_heap_rules›,
section argument: ‹heap[add/del]:›), using the frame rule and
frame inference.
If resolving is not possible, it also tries to apply the consequence rule to
make the postcondition a schematic variable.
›

(*<*)
subsection ‹Hiding of internal stuff›
hide_const (open) FI SLN
(*>*)

end


# Theory Sep_Main

section ‹Separation Logic Framework Entrypoint›
theory Sep_Main
imports Automation
begin
text ‹Import this theory to make available Imperative/HOL with
separation logic.›
end


# Theory Imp_List_Spec

section ‹Interface for Lists›
theory Imp_List_Spec
imports "../Sep_Main"
begin
text ‹
This file specifies an abstract interface for list data structures. It can
be implemented by concrete list data structures, as demonstrated in the open
and circular singly linked list examples.
›

locale imp_list =
fixes is_list :: "'a list ⇒ 'l ⇒ assn"
assumes precise: "precise is_list"
(*"∀l l'. h⊨(is_list l p * F1) ∧⇩A (is_list l' p * F2) ⟶ l=l'"*)

locale imp_list_empty = imp_list +
constrains is_list :: "'a list ⇒ 'l ⇒ assn"
fixes empty :: "'l Heap"
assumes empty_rule[sep_heap_rules]: "<emp> empty <is_list []>⇩t"

locale imp_list_is_empty = imp_list +
constrains is_list :: "'a list ⇒ 'l ⇒ assn"
fixes is_empty :: "'l ⇒ bool Heap"
assumes is_empty_rule[sep_heap_rules]:
"<is_list l p> is_empty p <λr. is_list l p * ↑(r ⟷ l=[])>⇩t"

locale imp_list_append = imp_list +
constrains is_list :: "'a list ⇒ 'l ⇒ assn"
fixes append :: "'a ⇒ 'l ⇒ 'l Heap"
assumes append_rule[sep_heap_rules]:
"<is_list l p> append a p <is_list (l@[a])>⇩t"

locale imp_list_prepend = imp_list +
constrains is_list :: "'a list ⇒ 'l ⇒ assn"
fixes prepend :: "'a ⇒ 'l ⇒ 'l Heap"
assumes prepend_rule[sep_heap_rules]:
"<is_list l p> prepend a p <is_list (a#l)>⇩t"

constrains is_list :: "'a list ⇒ 'l ⇒ assn"
fixes head :: "'l ⇒ 'a Heap"
"l≠[] ⟹ <is_list l p> head p <λr. is_list l p * ↑(r=hd l)>⇩t"

locale imp_list_pop = imp_list +
constrains is_list :: "'a list ⇒ 'l ⇒ assn"
fixes pop :: "'l ⇒ ('a×'l) Heap"
assumes pop_rule[sep_heap_rules]:
"l≠[] ⟹
<is_list l p>
pop p
<λ(r,p'). is_list (tl l) p' * ↑(r=hd l)>⇩t"

locale imp_list_rotate = imp_list +
constrains is_list :: "'a list ⇒ 'l ⇒ assn"
fixes rotate :: "'l ⇒ 'l Heap"
assumes rotate_rule[sep_heap_rules]:
"<is_list l p> rotate p <is_list (rotate1 l)>⇩t"

locale imp_list_reverse = imp_list +
constrains is_list :: "'a list ⇒ 'l ⇒ assn"
fixes reverse :: "'l ⇒ 'l Heap"
assumes reverse_rule[sep_heap_rules]:
"<is_list l p> reverse p <is_list (rev l)>⇩t"

locale imp_list_iterate = imp_list +
constrains is_list :: "'a list ⇒ 'l ⇒ assn"
fixes is_it :: "'a list ⇒ 'l ⇒ 'a list ⇒ 'it ⇒ assn"
fixes it_init :: "'l ⇒ ('it) Heap"
fixes it_has_next :: "'it ⇒ bool Heap"
fixes it_next :: "'it ⇒ ('a×'it) Heap"
assumes it_init_rule[sep_heap_rules]:
"<is_list l p> it_init p <is_it l p l>⇩t"
assumes it_next_rule[sep_heap_rules]: "l'≠[] ⟹
<is_it l p l' it>
it_next it
<λ(a,it'). is_it l p (tl l') it' * ↑(a=hd l')>"
assumes it_has_next_rule[sep_heap_rules]:
"<is_it l p l' it>
it_has_next it
<λr. is_it l p l' it * ↑(r⟷l'≠[])>"
assumes quit_iteration:
"is_it l p l' it ⟹⇩A is_list l p * true"

end


# Theory List_Seg

section ‹Singly Linked List Segments›
theory List_Seg
imports "../Sep_Main"
begin

subsection ‹Nodes›
text ‹
We define a node of a list to contain a data value and a next pointer.
As Imperative HOL does not support null-pointers, we make the next-pointer
an optional value, ‹None› representing a null pointer.

Unfortunately, Imperative HOL requires some boilerplate code to define
a datatype.
›
(@{const_name Ref}, SOME @{typ "nat ⇒ 'a::type ref"})›

datatype 'a node = Node "'a" "'a node ref option"

(@{const_name Ref}, SOME @{typ "nat ⇒ 'a::heap ref"})›

SOME @{typ "'a::heap ⇒ 'a node ref option ⇒ 'a node"})›

text ‹Selector Functions›
primrec val :: "'a::heap node ⇒ 'a" where
[sep_dflt_simps]: "val (Node x _) = x"

primrec "next" :: "'a::heap node ⇒ 'a node ref option" where
[sep_dflt_simps]: "next (Node _ r) = r"

text ‹Encoding to natural numbers, as required by Imperative/HOL›
fun
node_encode :: "'a::heap node ⇒ nat"
where
"node_encode (Node x r) = to_nat (x, r)"

instance node :: (heap) heap
apply (rule heap_class.intro)
apply (rule countable_classI [of "node_encode"])
apply (case_tac x, simp_all, case_tac y, simp_all)
..

subsection ‹List Segment Assertion›
text ‹
Intuitively, ‹lseg l p s› describes a list starting at ‹p› and
ending with a pointer ‹s›. The content of the list are ‹l›.
Note that the pointer ‹s› may also occur earlier in the list, in which
case it is handled as a usual next-pointer.
›
fun lseg
:: "'a::heap list ⇒ 'a node ref option ⇒ 'a node ref option ⇒ assn"
where
"lseg [] p s = ↑(p=s)"
| "lseg (x#l) (Some p) s = (∃⇩Aq. p ↦⇩r Node x q * lseg l q s)"
| "lseg (_#_) None _ = false"

lemma lseg_if_splitf1[simp, sep_dflt_simps]:
"lseg l None None = ↑(l=[])"
apply (cases l, simp_all)
done

lemma lseg_if_splitf2[simp, sep_dflt_simps]:
"lseg (x#xs) p q
= (∃⇩App n. pp ↦⇩r (Node x n) * lseg xs n q * ↑(p=Some pp))"
apply (cases p, simp_all)
(* TODO: One-point simproc for assertions! *)
apply (rule ent_iffI)
apply solve_entails
apply solve_entails
done

subsection ‹Lemmas›

subsubsection ‹Concatenation›
lemma lseg_prepend:
"p↦⇩rNode x q * lseg l q s ⟹⇩A lseg (x#l) (Some p) s"
by sep_auto

lemma lseg_append:
"lseg l p (Some s) * s↦⇩rNode x q ⟹⇩A lseg (l@[x]) p q"
proof (induction l arbitrary: p)
case Nil thus ?case by sep_auto
next
case (Cons y l)
show ?case
apply (cases p)
apply simp
apply (sep_auto)
apply (rule ent_frame_fwd[OF Cons.IH])
apply frame_inference
apply solve_entails
done
qed

lemma lseg_conc: "lseg l1 p q * lseg l2 q r ⟹⇩A lseg (l1@l2) p r"
proof (induct l1 arbitrary: p)
case Nil thus ?case by simp
next
case (Cons x l1)
show ?case
apply simp
apply sep_auto
apply (rule ent_frame_fwd[OF Cons.hyps])
apply frame_inference
apply solve_entails
done
qed

subsubsection ‹Splitting›
lemma lseg_split:
"lseg (l1@l2) p r ⟹⇩A ∃⇩Aq. lseg l1 p q * lseg l2 q r"
proof (induct l1 arbitrary: p)
case Nil thus ?case by sep_auto
next
case (Cons x l1)

have "lseg ((x # l1) @ l2) p r
⟹⇩A ∃⇩App n. pp ↦⇩r Node x n * lseg (l1 @ l2) n r * ↑ (p = Some pp)"
by simp
also have "… ⟹⇩A
∃⇩App n q. pp ↦⇩r Node x n
* lseg l1 n q
* lseg l2 q r
* ↑(p = Some pp)"
apply (intro ent_ex_preI)
apply clarsimp
apply (rule ent_frame_fwd[OF Cons.hyps])
apply frame_inference
apply sep_auto
done
also have "… ⟹⇩A ∃⇩Aq. lseg (x#l1) p q * lseg l2 q r"
by sep_auto
finally show ?case .
qed

subsubsection ‹Precision›
lemma lseg_prec1:
"∀l l'. (h⊨
(lseg l p (Some q) * q ↦⇩r x * F1)
∧⇩A (lseg l' p (Some q) * q ↦⇩r x * F2))
⟶ l=l'"
apply (intro allI)
subgoal for l l'
proof (induct l arbitrary: p l' F1 F2)
case Nil thus ?case
apply simp_all
apply (cases l')
apply simp
apply auto
done
next
case (Cons y l)
from Cons.prems show ?case
apply (cases l')
apply auto []
apply (cases p)
apply simp

apply (clarsimp)

apply (subgoal_tac "y=a ∧ na=n", simp)

using Cons.hyps apply (erule prec_frame')
apply frame_inference
apply frame_inference

apply (drule_tac p=aa in prec_frame[OF sngr_prec])
apply frame_inference
apply frame_inference
apply simp
done
qed
done

lemma lseg_prec2:
"∀l l'. (h⊨
(lseg l p None * F1) ∧⇩A (lseg l' p None * F2))
⟶ l=l'"
apply (intro allI)
subgoal for l l'
proof (induct l arbitrary: p l' F1 F2)
case Nil thus ?case
apply simp_all
apply (cases l')
apply simp
apply (cases p)
apply auto
done
next
case (Cons y l)
from Cons.prems show ?case
apply (cases p)
apply simp
apply (cases l')
apply (auto) []

apply (clarsimp)

apply (subgoal_tac "y=aa ∧ na=n", simp)

using Cons.hyps apply (erule prec_frame')
apply frame_inference
apply frame_inference

apply (drule_tac p=a in prec_frame[OF sngr_prec])
apply frame_inference
apply frame_inference
apply simp
done
qed
done

lemma lseg_prec3:
"∀q q'. h ⊨ (lseg l p q * F1) ∧⇩A (lseg l p q' * F2) ⟶ q=q'"
apply (intro allI)
proof (induct l arbitrary: p F1 F2)
case Nil thus ?case by auto
next
case (Cons x l)
show ?case
apply auto

apply (subgoal_tac "na=n")
using Cons.hyps apply (erule prec_frame')
apply frame_inference
apply frame_inference

apply (drule prec_frame[OF sngr_prec])
apply frame_inference
apply frame_inference
apply simp
done
qed

end


# Theory Open_List

section ‹Open Singly Linked Lists›
theory Open_List
imports List_Seg Imp_List_Spec
begin

subsection ‹Definitions›
type_synonym 'a os_list = "'a node ref option"

abbreviation os_list :: "'a list ⇒ ('a::heap) os_list ⇒ assn" where
"os_list l p ≡ lseg l p None"

subsection ‹Precision›
lemma os_prec:
"precise os_list"

lemma os_imp_list_impl: "imp_list os_list"
apply unfold_locales
apply (rule os_prec)
done
interpretation os: imp_list os_list by (rule os_imp_list_impl)

subsection ‹Operations›
subsubsection ‹Allocate Empty List›

definition os_empty :: "'a::heap os_list Heap" where
"os_empty ≡ return None"

lemma os_empty_rule: "<emp> os_empty <os_list []>"
unfolding os_empty_def
apply sep_auto
done

lemma os_empty_impl: "imp_list_empty os_list os_empty"
apply unfold_locales
done
interpretation os: imp_list_empty os_list os_empty by (rule os_empty_impl)

subsubsection ‹Emptiness check›
text ‹A linked list is empty, iff it is the null pointer.›

definition os_is_empty :: "'a::heap os_list ⇒ bool Heap" where
"os_is_empty b ≡ return (b = None)"

lemma os_is_empty_rule:
"<os_list xs b> os_is_empty b <λr. os_list xs b * ↑(r ⟷ xs = [])>"
unfolding os_is_empty_def
apply sep_auto
done

lemma os_is_empty_impl: "imp_list_is_empty os_list os_is_empty"
apply unfold_locales
done
interpretation os: imp_list_is_empty os_list os_is_empty
by (rule os_is_empty_impl)

subsubsection ‹Prepend›

text ‹To push an element to the front of a list we allocate a new node which
stores the element and the old list as successor. The new list is the new
allocated reference.›

definition os_prepend :: "'a ⇒ 'a::heap os_list ⇒ 'a os_list Heap" where
"os_prepend a n = do { p ← ref (Node a n); return (Some p) }"

lemma os_prepend_rule:
"<os_list xs n> os_prepend x n <os_list (x # xs)>"
unfolding os_prepend_def
apply sep_auto
done

lemma os_prepend_impl: "imp_list_prepend os_list os_prepend"
apply unfold_locales
done
interpretation os: imp_list_prepend os_list os_prepend
by (rule os_prepend_impl)

subsubsection‹Pop›
text ‹To pop the first element out of the list we look up the value and the
reference of the node and return the pair of those.›

fun os_pop :: "'a::heap os_list ⇒ ('a × 'a os_list) Heap" where
"os_pop None   = raise STR ''Empty Os_list''" |
"os_pop (Some p) = do {m ← !p; return (val m, next m)}"

declare os_pop.simps[simp del]

lemma os_pop_rule:
"xs ≠ [] ⟹ <os_list xs r>
os_pop r
<λ(x,r'). os_list (tl xs) r' * (the r) ↦⇩r (Node x r') * ↑(x = hd xs)>"

apply (cases r, simp_all)
apply (cases xs, simp_all)

apply (sep_auto simp: os_pop.simps)
done

lemma os_pop_impl: "imp_list_pop os_list os_pop"
apply unfold_locales
done
interpretation os: imp_list_pop os_list os_pop by (rule os_pop_impl)

subsubsection ‹Reverse›

text ‹The following reversal function is equivalent to the one from
Imperative HOL. And gives a more difficult example.›

partial_function (heap) os_reverse_aux
:: "'a::heap os_list ⇒ 'a os_list ⇒ 'a os_list Heap"
where [code]:
"os_reverse_aux q p = (case p of
None ⇒ return q |
Some r ⇒ do {
v ← !r;
r := Node (val v) q;
os_reverse_aux p (next v) })"

lemma [simp, sep_dflt_simps]:
"os_reverse_aux q None = return q"
"os_reverse_aux q (Some r) = do {
v ← !r;
r := Node (val v) q;
os_reverse_aux (Some r) (next v) }"
apply (subst os_reverse_aux.simps)
apply simp
apply (subst os_reverse_aux.simps)
apply simp
done

definition "os_reverse p = os_reverse_aux None p"

lemma os_reverse_aux_rule:
"<os_list xs p * os_list ys q>
os_reverse_aux q p
<os_list ((rev xs) @ ys) >"
proof (induct xs arbitrary: p q ys)
case Nil thus ?case
apply sep_auto
done
next
case (Cons x xs)
show ?case
apply (cases p, simp_all)
apply (sep_auto heap add: cons_pre_rule[OF _ Cons.hyps])
done
qed

lemma os_reverse_rule: "<os_list xs p> os_reverse p <os_list (rev xs)>"
unfolding os_reverse_def
apply (auto simp: os_reverse_aux_rule[where ys="[]", simplified, rule_format])
done

lemma os_reverse_impl: "imp_list_reverse os_list os_reverse"
apply unfold_locales
done
interpretation os: imp_list_reverse os_list os_reverse
by (rule os_reverse_impl)

subsubsection ‹Remove›

text ‹Remove all appearances of an element from a linked list.›

partial_function (heap) os_rem
:: "'a::heap ⇒ 'a node ref option ⇒ 'a node ref option Heap"
where [code]:
"os_rem x b = (case b of
None ⇒ return None |
Some p ⇒ do {
n ← !p;
q ← os_rem x (next n);
(if (val n = x)
then return q
else do {
p := Node (val n) q;
return (Some p) }) })"

lemma [simp, sep_dflt_simps]:
"os_rem x None = return None"
"os_rem x (Some p) = do {
n ← !p;
q ← os_rem x (next n);
(if (val n = x)
then return q
else do {
p := Node (val n) q;
return (Some p) }) }"
apply (subst os_rem.simps, simp)+
done

lemma os_rem_rule[sep_heap_rules]:
"<os_list xs b> os_rem x b <λr. os_list (removeAll x xs) r * true>"
proof (induct xs arbitrary: b x) (* Have to generalize over x, as
sep_auto preprocessor introduces a new variable. Alternative:
No preprocessing. (See alternative proof below) *)
case Nil show ?case
apply sep_auto
done
next
case (Cons y xs)
show ?case by (sep_auto heap add: Cons.hyps)
qed

lemma os_rem_rule_alt_proof:
"<os_list xs b> os_rem x b <λr. os_list (removeAll x xs) r * true>"
proof (induct xs arbitrary: b)
case Nil show ?case
apply sep_auto
done
next
case (Cons y xs)
show ?case
by (sep_auto (nopre) heap add: Cons.hyps) (* Switching off preprocessor *)
qed

subsubsection ‹Iterator›

type_synonym 'a os_list_it = "'a os_list"
definition "os_is_it l p l2 it
≡ ∃⇩Al1. ↑(l=l1@l2) * lseg l1 p it * os_list l2 it"

definition os_it_init :: "'a os_list ⇒ ('a os_list_it) Heap"
where "os_it_init l = return l"

fun os_it_next where
"os_it_next (Some p) = do {
n ← !p;
return (val n,next n)
}"

definition os_it_has_next :: "'a os_list_it ⇒ bool Heap" where
"os_it_has_next it ≡ return (it≠None)"

lemma os_iterate_impl:
"imp_list_iterate os_list os_is_it os_it_init os_it_has_next os_it_next"
apply unfold_locales
unfolding os_it_init_def os_is_it_def[abs_def]
apply sep_auto

apply (case_tac it, simp)
apply (case_tac l', simp)
apply sep_auto
apply (rule ent_frame_fwd[OF lseg_append])
apply frame_inference
apply simp

unfolding os_it_has_next_def
apply (sep_auto elim!: neq_NilE)

apply solve_entails
apply (rule ent_frame_fwd[OF lseg_conc])
apply frame_inference
apply solve_entails
done
interpretation os:
imp_list_iterate os_list os_is_it os_it_init os_it_has_next os_it_next
by (rule os_iterate_impl)

subsubsection ‹List-Sum›

partial_function (heap) os_sum' :: "int os_list_it ⇒ int ⇒ int Heap"
where [code]:
"os_sum' it s = do {
b ← os_it_has_next it;
if b then do {
(x,it') ← os_it_next it;
os_sum' it' (s+x)
} else return s
}"

lemma os_sum'_rule[sep_heap_rules]:
"<os_is_it l p l' it>
os_sum' it s
<λr. os_list l p * ↑(r = s + sum_list l')>⇩t"
proof (induct l' arbitrary: it s)
case Nil thus ?case
apply (subst os_sum'.simps)
apply (sep_auto intro: os.quit_iteration)
done
next
case (Cons x l')
show ?case
apply (subst os_sum'.simps)
apply (sep_auto heap: Cons.hyps)
done
qed

definition "os_sum p ≡ do {
it ← os_it_init p;
os_sum' it 0}"

lemma os_sum_rule[sep_heap_rules]:
"<os_list l p> os_sum p <λr. os_list l p * ↑(r=sum_list l)>⇩t"
unfolding os_sum_def
by sep_auto

end


# Theory Circ_List

section ‹Circular Singly Linked Lists›
theory Circ_List
imports List_Seg Imp_List_Spec
begin

text ‹
Example of circular lists, with efficient append, prepend, pop, and rotate
operations.
›

subsection ‹Datatype Definition›

type_synonym 'a cs_list = "'a node ref option"

text ‹A circular list is described by a list segment, with special
cases for the empty list:›
fun cs_list :: "'a::heap list ⇒ 'a node ref option ⇒ assn" where
"cs_list [] None = emp"
| "cs_list (x#l) (Some p) = lseg (x#l) (Some p) (Some p)"
| "cs_list _ _ = false"

lemma [simp]: "cs_list l None = ↑(l=[])"
by (cases l) auto

lemma [simp]:
"cs_list l (Some p)
= (∃⇩Ax ls. ↑(l=x#ls) * lseg (x#ls) (Some p) (Some p))"
apply (rule ent_iffI)
apply (cases l)
apply simp
apply sep_auto
apply (cases l)
apply simp
apply sep_auto
done

subsection ‹Precision›
lemma cs_prec:
"precise cs_list"
apply rule
apply (case_tac p)
apply clarsimp

apply clarsimp
apply (subgoal_tac "x=xa ∧ n=na", simp)

apply (erule prec_frame_expl[OF lseg_prec1])
apply frame_inference
apply frame_inference

apply (drule prec_frame[OF sngr_prec])
apply frame_inference
apply frame_inference
apply simp
done

lemma cs_imp_list_impl: "imp_list cs_list"
apply unfold_locales
apply (rule cs_prec)
done
interpretation cs: imp_list cs_list by (rule cs_imp_list_impl)

subsection ‹Operations›
subsubsection ‹Allocate Empty List›
definition cs_empty :: "'a::heap cs_list Heap" where
"cs_empty ≡ return None"

lemma cs_empty_rule: "<emp> cs_empty <cs_list []>"
unfolding cs_empty_def
by sep_auto

lemma cs_empty_impl: "imp_list_empty cs_list cs_empty"
by unfold_locales (sep_auto heap: cs_empty_rule)
interpretation cs: imp_list_empty cs_list cs_empty by (rule cs_empty_impl)

subsubsection ‹Prepend Element›
fun cs_prepend :: "'a ⇒ 'a::heap cs_list ⇒ 'a cs_list Heap" where
"cs_prepend x None = do {
p ← ref (Node x None);
p:=Node x (Some p);
return (Some p)
}"
| "cs_prepend x (Some p) = do {
n ← !p;
q ← ref (Node (val n) (next n));
p := Node x (Some q);
return (Some p)
}"

declare cs_prepend.simps [simp del]

lemma cs_prepend_rule:
"<cs_list l p> cs_prepend x p <cs_list (x#l)>"
apply (cases p)
apply simp_all
apply (sep_auto simp: cs_prepend.simps)

apply (sep_auto simp: cs_prepend.simps)
done

lemma cs_prepend_impl: "imp_list_prepend cs_list cs_prepend"
by unfold_locales (sep_auto heap: cs_prepend_rule)
interpretation cs: imp_list_prepend cs_list cs_prepend
by (rule cs_prepend_impl)

subsubsection ‹Append Element›
fun cs_append :: "'a ⇒ 'a::heap cs_list ⇒ 'a cs_list Heap" where
"cs_append x None = do {
p ← ref (Node x None);
p:=Node x (Some p);
return (Some p) }"
| "cs_append x (Some p) = do {
n ← !p;
q ← ref (Node (val n) (next n));
p := Node x (Some q);
return (Some q)
}"

declare cs_append.simps [simp del]

lemma cs_append_rule:
"<cs_list l p> cs_append x p <cs_list (l@[x])>"
apply (cases p)
apply simp_all
apply (sep_auto simp: cs_append.simps)

apply (sep_auto simp: cs_append.simps)
apply (rule ent_frame_fwd)
apply (rule_tac s=a in lseg_append) (* frame_inference does no backtracking
on instantiating schematics, hence we have to give it some help here. *)
apply frame_inference
apply (sep_auto)
done

lemma cs_append_impl: "imp_list_append cs_list cs_append"
by unfold_locales (sep_auto heap: cs_append_rule)
interpretation cs: imp_list_append cs_list cs_append
by (rule cs_append_impl)

subsubsection ‹Pop First Element›
fun cs_pop :: "'a::heap cs_list ⇒ ('a×'a cs_list) Heap" where
"cs_pop None = raise STR ''Pop from empty list''"
| "cs_pop (Some p) = do {
n1 ← !p;
if next n1 = Some p then
return (val n1,None) ― ‹Singleton list becomes empty list›
else do {
let p2 = the (next n1);
n2 ← !p2;
p := Node (val n2) (next n2);
return (val n1,Some p)
}
}"

declare cs_pop.simps[simp del]

lemma cs_pop_rule:
"<cs_list (x#l) p> cs_pop p <λ(y,p'). cs_list l p' * true * ↑(y=x)>"
apply (cases p)
apply (sep_auto simp: cs_pop.simps)

apply (cases l)
apply (sep_auto simp: cs_pop.simps dflt_simps: option.sel)

apply (sep_auto
simp: cs_pop.simps
dflt_simps: option.sel
eintros del: exI)
(* Some unfortunate quantifier fiddling :( *)
apply (rule_tac x=aa in exI)
apply (rule_tac x=list in exI)
apply (rule_tac x=a in exI)
apply clarsimp
apply (rule exI)
apply sep_auto
done

lemma cs_pop_impl: "imp_list_pop cs_list cs_pop"
apply unfold_locales
apply (sep_auto heap: cs_pop_rule elim!: neq_NilE)
done
interpretation cs: imp_list_pop cs_list cs_pop by (rule cs_pop_impl)

subsubsection ‹Rotate›
fun cs_rotate :: "'a::heap cs_list ⇒ 'a cs_list Heap" where
"cs_rotate None = return None"
| "cs_rotate (Some p) = do {
n ← !p;
return (next n)
}"

declare cs_rotate.simps [simp del]

lemma cs_rotate_rule:
"<cs_list l p> cs_rotate p <cs_list (rotate1 l)>"
apply (cases p)
apply (sep_auto simp: cs_rotate.simps)

apply (cases l)
apply simp

apply (case_tac list)
apply simp
apply (sep_auto simp: cs_rotate.simps)

apply (sep_auto simp: cs_rotate.simps)
apply (rule ent_frame_fwd)
apply (rule_tac s="a" in lseg_append)
apply frame_inference
apply sep_auto
done

lemma cs_rotate_impl: "imp_list_rotate cs_list cs_rotate"
apply unfold_locales
apply (sep_auto heap: cs_rotate_rule)
done
interpretation cs: imp_list_rotate cs_list cs_rotate by (rule cs_rotate_impl)

subsection ‹Test›
definition "test ≡ do {
l ← cs_empty;
l ← cs_append ''a'' l;
l ← cs_append ''b'' l;
l ← cs_append ''c'' l;
l ← cs_prepend ''0'' l;
l ← cs_rotate l;
(v1,l)←cs_pop l;
(v2,l)←cs_pop l;
(v3,l)←cs_pop l;
(v4,l)←cs_pop l;
return [v1,v2,v3,v4]
}"

definition "test_result ≡ [''a'', ''b'', ''c'', ''0'']"

lemma "<emp> test <λr. ↑(r=test_result) * true>"
unfolding test_def test_result_def
apply (sep_auto)
done

export_code test checking SML_imp

ML_val ‹
val res = @{code test} ();
if res = @{code test_result} then () else raise Match;
›

hide_const (open) test test_result

end


# Theory Imp_Map_Spec

section ‹Interface for Maps›
theory Imp_Map_Spec
imports "../Sep_Main"
begin
text ‹
This file specifies an abstract interface for map data structures. It can
be implemented by concrete map data structures, as demonstrated in the
hash map example.
›

locale imp_map =
fixes is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
assumes precise: "precise is_map"

locale imp_map_empty = imp_map +
constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
fixes empty :: "'m Heap"
assumes empty_rule[sep_heap_rules]: "<emp> empty <is_map Map.empty>⇩t"

locale imp_map_is_empty = imp_map +
constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
fixes is_empty :: "'m ⇒ bool Heap"
assumes is_empty_rule[sep_heap_rules]:
"<is_map m p> is_empty p <λr. is_map m p * ↑(r ⟷ m=Map.empty)>⇩t"

locale imp_map_lookup = imp_map +
constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
fixes lookup :: "'k ⇒ 'm ⇒ ('v option) Heap"
assumes lookup_rule[sep_heap_rules]:
"<is_map m p> lookup k p <λr. is_map m p * ↑(r = m k)>⇩t"

locale imp_map_update = imp_map +
constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
fixes update :: "'k ⇒ 'v ⇒ 'm ⇒ 'm Heap"
assumes update_rule[sep_heap_rules]:
"<is_map m p> update k v p <is_map (m(k ↦ v))>⇩t"

locale imp_map_delete = imp_map +
constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
fixes delete :: "'k ⇒ 'm ⇒ 'm Heap"
assumes delete_rule[sep_heap_rules]:
"<is_map m p> delete k p <is_map (m | (-{k}))>⇩t"

constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
fixes add :: "'m ⇒ 'm ⇒ 'm Heap"
"<is_map m p * is_map m' p'> add p p'
<λr. is_map m p * is_map m' p' * is_map (m ++ m') r>⇩t"

locale imp_map_size = imp_map +
constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
fixes size :: "'m ⇒ nat Heap"
assumes size_rule[sep_heap_rules]:
"<is_map m p> size p <λr. is_map m p * ↑(r = card (dom m))>⇩t"

locale imp_map_iterate = imp_map +
constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
fixes is_it :: "('k ⇀ 'v) ⇒ 'm ⇒ ('k ⇀ 'v) ⇒ 'it ⇒ assn"
fixes it_init :: "'m ⇒ ('it) Heap"
fixes it_has_next :: "'it ⇒ bool Heap"
fixes it_next :: "'it ⇒ (('k×'v)×'it) Heap"
assumes it_init_rule[sep_heap_rules]:
"<is_map s p> it_init p <is_it s p s>⇩t"
assumes it_next_rule[sep_heap_rules]: "m'≠Map.empty ⟹
<is_it m p m' it>
it_next it
<λ((k,v),it'). is_it m p (m' | (-{k})) it' * ↑(m' k = Some v)>"
assumes it_has_next_rule[sep_heap_rules]:
"<is_it m p m' it> it_has_next it <λr. is_it m p m' it * ↑(r⟷m'≠Map.empty)>"
assumes quit_iteration:
"is_it m p m' it ⟹⇩A is_map m p * true"

locale imp_map_iterate' = imp_map +
constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
fixes is_it :: "('k ⇀ 'v) ⇒ 'm ⇒ ('k×'v) list ⇒ 'it ⇒ assn"
fixes it_init :: "'m ⇒ ('it) Heap"
fixes it_has_next :: "'it ⇒ bool Heap"
fixes it_next :: "'it ⇒ (('k×'v)×'it) Heap"
assumes it_init_rule[sep_heap_rules]:
"<is_map s p> it_init p <λr. ∃⇩Al. ↑(map_of l = s) * is_it s p l r>⇩t"
assumes it_next_rule[sep_heap_rules]: "
<is_it m p (kv#l) it>
it_next it
<λ(kv',it'). is_it m p l it' * ↑(kv'=kv)>"
assumes it_has_next_rule[sep_heap_rules]:
"<is_it m p l it> it_has_next it <λr. is_it m p l it * ↑(r⟷l≠[])>"
assumes quit_iteration:
"is_it m p l it ⟹⇩A is_map m p * true"

end


# Theory Hash_Table

section "Hash-Tables"
theory Hash_Table
imports
Collections.HashCode
Collections.Code_Target_ICF
"../Sep_Main"
begin

subsection ‹Datatype›

subsubsection ‹Definition›

datatype ('k, 'v) hashtable = HashTable "('k × 'v) list array" nat

primrec the_array :: "('k, 'v) hashtable ⇒ ('k × 'v) list array"
where "the_array (HashTable a _) = a"

primrec the_size :: "('k, 'v) hashtable ⇒ nat"
where "the_size (HashTable _ n) = n"

subsubsection ‹Storable on Heap›

fun hs_encode :: "('k::countable, 'v::countable) hashtable ⇒ nat"
where "hs_encode (HashTable a n) = to_nat (n, a)"

instance hashtable :: (countable, countable) countable
proof (rule countable_classI[of "hs_encode"])
fix x y :: "('a, 'b) hashtable"
assume "hs_encode x = hs_encode y"
then show "x = y" by (cases x, cases y) auto
qed

instance hashtable :: (heap, heap) heap ..

subsection ‹Assertions›

subsubsection ‹Assertion for Hashtable›

definition ht_table :: "('k::heap × 'v::heap) list list ⇒ ('k, 'v) hashtable ⇒ assn"
where "ht_table l ht = (the_array ht) ↦⇩a l"

definition ht_size :: "'a list list ⇒ nat ⇒ bool"
where "ht_size l n ≡ n = sum_list (map length l)"

definition ht_hash :: "('k::hashable × 'v) list list ⇒ bool" where
"ht_hash l ≡ ∀i<length l. ∀x∈set (l!i).
bounded_hashcode_nat (length l) (fst x) = i"

definition ht_distinct :: "('k × 'v) list list ⇒ bool" where
"ht_distinct l ≡ ∀i<length l. distinct (map fst (l!i))"

definition is_hashtable :: "('k::{heap,hashable} × 'v::heap) list list
⇒ ('k, 'v) hashtable ⇒ assn"
where
"is_hashtable l ht =
(the_array ht ↦⇩a l) *
↑(ht_size l (the_size ht)
∧ ht_hash l
∧ ht_distinct l
∧ 1 < length l)"

lemma is_hashtable_prec: "precise is_hashtable"
apply (rule preciseI)
unfolding is_hashtable_def
apply (auto simp add: preciseD[OF snga_prec])
done

text ‹These rules are quite useful for automated methods, to avoid unfolding
of definitions, that might be used folded in other lemmas,
like induction hypothesis. However, they show in some sense a possibility for
modularization improvement, as it should be enough to show an implication
and know that the ‹nth› and ‹len› operations do not change
the heap.›
lemma ht_array_nth_rule[sep_heap_rules]:
"i<length l ⟹ <is_hashtable l ht>
Array.nth (the_array ht) i
<λr. is_hashtable l ht * ↑(r = l!i)>"
unfolding is_hashtable_def
by sep_auto

lemma ht_array_length_rule[sep_heap_rules]:
"<is_hashtable l ht>
Array.len (the_array ht)
<λr. is_hashtable l ht * ↑(r = length l)>"
unfolding is_hashtable_def
by sep_auto

subsection ‹New›

subsubsection ‹Definition›

definition ht_new_sz :: "nat ⇒ ('k::{heap,hashable}, 'v::heap) hashtable Heap"
where
"ht_new_sz n ≡ do { let l = replicate n [];
a ← Array.of_list l;
return (HashTable a 0) }"

definition ht_new :: "('k::{heap,hashable}, 'v::heap) hashtable Heap"
where "ht_new ≡ ht_new_sz (def_hashmap_size TYPE('k))"

subsubsection ‹Complete Correctness›

lemma ht_hash_replicate[simp, intro!]: "ht_hash (replicate n [])"
apply (induct n)
apply (case_tac i)
apply auto
done

lemma ht_distinct_replicate[simp, intro!]: "ht_distinct (replicate n [])"
apply (induct n)
apply (case_tac i)
apply auto
done

lemma ht_size_replicate[simp, intro!]: "ht_size (replicate n []) 0"

― ‹We can't create hash tables with a size of zero›
lemma complete_ht_new_sz: "1 < n ⟹ <emp> ht_new_sz n <is_hashtable (replicate n [])>"
apply (unfold ht_new_sz_def)
apply (simp del: replicate.simps)
apply (rule bind_rule)
apply (rule of_list_rule)
apply (rule return_cons_rule)
done

lemma complete_ht_new:
"<emp>
ht_new::('k::{heap,hashable}, 'v::heap) hashtable Heap
<is_hashtable (replicate (def_hashmap_size TYPE('k)) [])>"
unfolding ht_new_def

subsection ‹Lookup›

subsubsection ‹Definition›

fun ls_lookup :: "'k ⇒ ('k × 'v) list ⇒ 'v option"
where
"ls_lookup x [] = None" |
"ls_lookup x ((k, v) # l) = (if x = k then Some v else ls_lookup x l)"

definition ht_lookup :: "'k ⇒ ('k::{heap,hashable}, 'v::heap) hashtable ⇒ 'v option Heap"
where
"ht_lookup x ht = do {
m ← Array.len (the_array ht);
let i = bounded_hashcode_nat m x;
l ← Array.nth (the_array ht) i;
return (ls_lookup x l)
}"

subsubsection ‹Complete Correctness›

lemma complete_ht_lookup:
"<is_hashtable l ht> ht_lookup x ht
<λr. is_hashtable l ht *
↑(r = ls_lookup x (l!(bounded_hashcode_nat (length l) x))) >"
apply (cases ht)
apply (clarsimp simp: is_hashtable_def)
apply (rule bind_rule)
apply (rule length_rule)
apply (rule norm_pre_pure_rule)
apply (rule bind_rule)
apply (rule nth_rule)
apply (rule norm_pre_pure_rule)
apply (rule return_cons_rule)
apply simp
done

text ‹Alternative, more automatic proof›
lemma complete_ht_lookup_alt_proof:
"<is_hashtable l ht> ht_lookup x ht
<λr. is_hashtable l ht *
↑(r = ls_lookup x (l!(bounded_hashcode_nat (length l) x)))>"
unfolding is_hashtable_def ht_lookup_def
apply (cases ht)
apply (sep_auto simp: bounded_hashcode_nat_bounds)
done

subsection ‹Update›

subsubsection ‹Definition›

fun ls_update :: "'k ⇒ 'v ⇒ ('k × 'v) list ⇒ (('k × 'v) list × bool)"
where
"ls_update k v [] = ([(k, v)], False)" |
"ls_update k v ((l, w) # ls) = (
if k = l then
((k, v) # ls, True)
else
(let r = ls_update k v ls in ((l, w) # fst r, snd r))
)"

definition abs_update
:: "'k::hashable ⇒ 'v ⇒ ('k × 'v) list list ⇒ ('k × 'v) list list"
where
"abs_update k v l =
l[bounded_hashcode_nat (length l) k
:= fst (ls_update k v (l ! bounded_hashcode_nat (length l) k))]"

lemma ls_update_snd_set: "snd (ls_update k v l) ⟷ k ∈ set (map fst l)"
by (induct l rule: ls_update.induct) simp_all

lemma ls_update_fst_set: "set (fst (ls_update k v l)) ⊆ insert (k, v) (set l)"
apply (induct l rule: ls_update.induct)
apply simp
done

lemma ls_update_fst_map_set: "set (map fst (fst (ls_update k v l))) = insert k (set (map fst l))"
apply (induct l rule: ls_update.induct)
apply simp
done

lemma ls_update_distinct: "distinct (map fst l) ⟹ distinct (map fst (fst (ls_update k v l)))"
proof (induct l rule: ls_update.induct)
case 1 thus ?case by simp
next
case (2 k v l w ls) show ?case
proof (cases "k = l")
case True
with 2 show ?thesis by simp
next
case False
with 2 have d: "distinct (map fst (fst (ls_update k v ls)))"
by simp
from 2(2) have "l ∉ set (map fst ls)" by simp
with False have "l ∉ set (map fst (fst (ls_update k v ls)))"
by (simp only: ls_update_fst_map_set) simp
with d False show ?thesis by (simp add: Let_def)
qed
qed

lemma ls_update_length: "length (fst (ls_update k v l))
= (if (k ∈ set (map fst l)) then length l else Suc (length l))"
by (induct l rule: ls_update.induct) (auto simp add: Let_def)

lemma ls_update_length_snd_True:
"snd (ls_update k v l) ⟹ length (fst (ls_update k v l)) = length l"

lemma ls_update_length_snd_False:
"¬ snd (ls_update k v l) ⟹ length (fst (ls_update k v l)) = Suc (length l)"

definition ht_upd
:: "'k ⇒ 'v
⇒ ('k::{heap,hashable}, 'v::heap) hashtable
⇒ ('k, 'v) hashtable Heap"
where
"ht_upd k v ht = do {
m ← Array.len (the_array ht);
let i = bounded_hashcode_nat m k;
l ← Array.nth (the_array ht) i;
let l = ls_update k v l;
Array.upd i (fst l) (the_array ht);
let n = (if (snd l) then the_size ht else Suc (the_size ht));
return (HashTable (the_array ht) n)
}"

subsubsection ‹Complete Correctness›

lemma ht_hash_update:
assumes "ht_hash ls"
shows "ht_hash (abs_update k v ls)"
unfolding ht_hash_def abs_update_def
apply (intro allI ballI impI)
apply simp
subgoal premises prems for i x
proof (cases "i = bounded_hashcode_nat (length ls) k")
case True
note i = True
show ?thesis
proof (cases "fst x = k")
case True
with i show ?thesis by simp
next
case False
with prems i
have
"x ∈ set (fst (ls_update k v
(ls ! bounded_hashcode_nat (length ls) k)))"
by auto
with
ls_update_fst_set[
of k v "ls ! bounded_hashcode_nat (length ls) k"]
False
have "x ∈ insert (k, v)
(set (ls ! bounded_hashcode_nat (length ls) k))"
by auto
with False have "x ∈ set (ls ! bounded_hashcode_nat (length ls) k)"
by auto
with i prems assms[unfolded ht_hash_def] show ?thesis by simp
qed
next
case False
with prems have "x ∈ set (ls ! i)" by simp
with prems assms[unfolded ht_hash_def] show ?thesis by simp
qed
done

lemma ht_distinct_update:
assumes "ht_distinct l"
shows "ht_distinct (abs_update k v l)"
unfolding ht_distinct_def abs_update_def
apply (intro allI impI)
apply simp
subgoal premises prems for i
proof (cases "i = bounded_hashcode_nat (length l) k")
case True
with prems assms[unfolded ht_distinct_def]
have "distinct (map fst (l ! bounded_hashcode_nat (length l) k))"
by simp
from ls_update_distinct[OF this, of k v] True prems
show ?thesis by simp
next
case False
with prems assms[unfolded ht_distinct_def] show ?thesis by simp
qed
done

lemma length_update:
assumes "1 < length l"
shows "1 < length (abs_update k v l)"
using assms

lemma ht_size_update1:
assumes size: "ht_size l n"
assumes i: "i < length l"
assumes snd: "snd (ls_update k v (l ! i))"
shows "ht_size (l[i := fst (ls_update k v (l!i))]) n"
proof -
have "(map length (l[i := fst (ls_update k v (l ! i))]))
= (map length l)[i := length (fst (ls_update k v (l ! i)))]"
from sum_list_update[of i "map length l", simplified, OF i,
of "length (fst (ls_update k v (l ! i)))"]
ls_update_length_snd_True[OF snd]
have
"sum_list ((map length l)[i := length (fst (ls_update k v (l ! i)))])
= sum_list (map length l)" by simp
finally show ?thesis using assms by (simp add: ht_size_def assms)
qed

lemma ht_size_update2:
assumes size: "ht_size l n"
assumes i: "i < length l"
assumes snd: "¬ snd (ls_update k v (l ! i))"
shows "ht_size (l[i := fst (ls_update k v (l!i))]) (Suc n)"
proof -
have "(map length (l[i := fst (ls_update k v (l ! i))]))
= (map length l)[i := length (fst (ls_update k v (l ! i)))]"
from sum_list_update[of i "map length l", simplified, OF i,
of "length (fst (ls_update k v (l ! i)))"]
ls_update_length_snd_False[OF snd]
have
"sum_list ((map length l)[i := length (fst (ls_update k v (l ! i)))])
= Suc (sum_list (map length l))" by simp
finally show ?thesis using assms by (simp add: ht_size_def assms)
qed

lemma complete_ht_upd: "<is_hashtable l ht> ht_upd k v ht
<is_hashtable (abs_update k v l)>"
unfolding ht_upd_def is_hashtable_def
apply (rule norm_pre_pure_rule)
apply (rule bind_rule)
apply (rule length_rule)
apply (rule norm_pre_pure_rule)
apply (rule bind_rule)
apply (rule nth_rule)
apply (rule norm_pre_pure_rule)
apply (rule bind_rule)
apply (rule upd_rule)
apply (rule return_cons_rule)
apply (auto
is_hashtable_def ht_hash_update[unfolded abs_update_def]
ht_distinct_update[unfolded abs_update_def] abs_update_def)
done

text ‹Alternative, more automatic proof›
lemma complete_ht_upd_alt_proof:
"<is_hashtable l ht> ht_upd k v ht <is_hashtable (abs_update k v l)>"
unfolding ht_upd_def is_hashtable_def Let_def
(* TODO: Is this huge simp-step really necessary? *)
apply (sep_auto
simp: ht_size_update1 ht_size_update2 bounded_hashcode_nat_bounds
is_hashtable_def ht_hash_update[unfolded abs_update_def]
ht_distinct_update[unfolded abs_update_def] abs_update_def)
done

subsection ‹Delete›

subsubsection ‹Definition›

fun ls_delete :: "'k ⇒ ('k × 'v) list ⇒ (('k × 'v) list × bool)" where
"ls_delete k [] = ([], False)" |
"ls_delete k ((l, w) # ls) = (
if k = l then
(ls, True)
else
(let r = ls_delete k ls in ((l, w) # fst r, snd r)))"

lemma ls_delete_snd_set: "snd (ls_delete k l) ⟷ k ∈ set (map fst l)"
by (induct l rule: ls_delete.induct) simp_all

lemma ls_delete_fst_set: "set (fst (ls_delete k l)) ⊆ set l"
apply (induct l rule: ls_delete.induct)
apply simp
done

lemma ls_delete_fst_map_set:
"distinct (map fst l) ⟹
set (map fst (fst (ls_delete k l))) = (set (map fst l)) - {k}"
apply (induct l rule: ls_delete.induct)
apply simp
done

lemma ls_delete_distinct: "distinct (map fst l) ⟹ distinct (map fst (fst (ls_delete k l)))"
proof (induct l rule: ls_delete.induct)
case 1 thus ?case by simp
next
case (2 k l w ls) show ?case
proof (cases "k = l")
case True
with 2 show ?thesis by simp
next
case False
with 2 have d: "distinct (map fst (fst (ls_delete k ls)))"
by simp
from 2 have d2: "distinct (map fst ls)" by simp
from 2(2) have "l ∉ set (map fst ls)" by simp
with False 2 ls_delete_fst_map_set[OF d2, of k]
have "l ∉ set (map fst (fst (ls_delete k ls)))"
by simp
with d False show ?thesis by (simp add: Let_def)
qed
qed

lemma ls_delete_length:
"length (fst (ls_delete k l)) = (
if (k ∈ set (map fst l)) then
(length l - 1)
else
length l)"
proof (induct l rule: ls_delete.induct)
case 1
then show ?case by simp
next
case (2 k l w ls)
then show ?case by (cases ls) (auto simp add: Let_def)
qed

lemma ls_delete_length_snd_True:
"snd (ls_delete k l) ⟹ length (fst (ls_delete k l)) = length l - 1"

lemma ls_delete_length_snd_False:
"¬ snd (ls_delete k l) ⟹ length (fst (ls_delete k l)) = length l"

definition ht_delete
:: "'k
⇒ ('k::{heap,hashable}, 'v::heap) hashtable
⇒ ('k, 'v) hashtable Heap"
where
"ht_delete k ht = do {
m ← Array.len (the_array ht);
let i = bounded_hashcode_nat m k;
l ← Array.nth (the_array ht) i;
let l = ls_delete k l;
Array.upd i (fst l) (the_array ht);
let n = (if (snd l) then (the_size ht - 1) else the_size ht);
return (HashTable (the_array ht) n)
}"

subsubsection ‹Complete Correctness›

lemma ht_hash_delete:
assumes "ht_hash ls"
shows "ht_hash (
ls[bounded_hashcode_nat (length ls) k
:= fst (ls_delete k
(ls ! bounded_hashcode_nat (length ls) k)
)
]
)"
unfolding ht_hash_def
apply (intro allI ballI impI)
apply simp
subgoal premises prems for i x
proof (cases "i = bounded_hashcode_nat (length ls) k")
case i: True
show ?thesis
proof (cases "fst x = k")
case True
with i show ?thesis by simp
next
case False
with prems i
have
"x ∈ set (fst (ls_delete k
(ls ! bounded_hashcode_nat (length ls) k)))"
by auto
with
ls_delete_fst_set[
of k "ls ! bounded_hashcode_nat (length ls) k"]
False
have "x ∈ (set (ls ! bounded_hashcode_nat (length ls) k))" by auto
with i prems assms[unfolded ht_hash_def] show ?thesis by simp
qed
next
case False
with prems have "x ∈ set (ls ! i)" by simp
with prems assms[unfolded ht_hash_def] show ?thesis by simp
qed
done

lemma ht_distinct_delete:
assumes "ht_distinct l"
shows "ht_distinct (
l[bounded_hashcode_nat (length l) k
:= fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])"
unfolding ht_distinct_def
apply (intro allI impI)
apply simp
subgoal premises prems for i
proof (cases "i = bounded_hashcode_nat (length l) k")
case True
with prems assms[unfolded ht_distinct_def]
have "distinct (map fst (l ! bounded_hashcode_nat (length l) k))"
by simp
from ls_delete_distinct[OF this, of k] True prems
show ?thesis by simp
next
case False
with prems assms[unfolded ht_distinct_def] show ?thesis by simp
qed
done

lemma ht_size_delete1:
assumes size: "ht_size l n"
assumes i: "i < length l"
assumes snd: "snd (ls_delete k (l ! i))"
shows "ht_size (l[i := fst (ls_delete k (l!i))]) (n - 1)"
proof -
have "(map length (l[i := fst (ls_delete k (l ! i))]))
= (map length l)[i := length (fst (ls_delete k (l ! i)))]"
from sum_list_update[of i "map length l", simplified, OF i,
of "length (fst (ls_delete k (l ! i)))"]
ls_delete_length_snd_True[OF snd] snd
have "sum_list ((map length l)[i := length (fst (ls_delete k (l ! i)))])
= sum_list (map length l) - 1"
by (cases "length (l ! i)") (simp_all add: ls_delete_snd_set)
finally show ?thesis using assms by (simp add: ht_size_def assms)
qed

lemma ht_size_delete2:
assumes size: "ht_size l n"
assumes i: "i < length l"
assumes snd: "¬ snd (ls_delete k (l ! i))"
shows "ht_size (l[i := fst (ls_delete k (l!i))]) n"
proof -
have "(map length (l[i := fst (ls_delete k (l ! i))]))
= (map length l)[i := length (fst (ls_delete k (l ! i)))]"
from sum_list_update[of i "map length l", simplified, OF i,
of "length (fst (ls_delete k (l ! i)))"]
ls_delete_length_snd_False[OF snd]
have "sum_list ((map length l)[i := length (fst (ls_delete k (l ! i)))])
= sum_list (map length l)" by simp
finally show ?thesis using assms by (simp add: ht_size_def assms)
qed

lemma complete_ht_delete: "<is_hashtable l ht> ht_delete k ht
<is_hashtable (l[bounded_hashcode_nat (length l) k
:= fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])>"
unfolding ht_delete_def is_hashtable_def
apply (rule norm_pre_pure_rule)
apply (rule bind_rule)
apply (rule length_rule)
apply (rule norm_pre_pure_rule)
apply (rule bind_rule)
apply (rule nth_rule)
apply (rule norm_pre_pure_rule)
apply (rule bind_rule)
apply (rule upd_rule)
apply (rule return_cons_rule)
apply (auto
is_hashtable_def ht_hash_delete ht_distinct_delete)
using ht_size_delete1[OF _ bounded_hashcode_nat_bounds[of "length l" k], of "the_size ht"]
apply simp
done

text ‹Alternative, more automatic proof›
lemma "<is_hashtable l ht> ht_delete k ht
<is_hashtable (l[bounded_hashcode_nat (length l)
k := fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])>"
unfolding ht_delete_def is_hashtable_def Let_def
using ht_size_delete1[OF _ bounded_hashcode_nat_bounds[of "length l" k],
of "the_size ht"]
apply (sep_auto simp:
ht_size_delete1 ht_size_delete2 bounded_hashcode_nat_bounds
is_hashtable_def ht_hash_delete ht_distinct_delete)
done

subsection ‹Re-Hashing›

subsubsection ‹Auxiliary Functions›

text ‹\paragraph{Insert List}›
fun ht_insls
:: "('k × 'v) list
⇒ ('k::{heap,hashable}, 'v::heap) hashtable
⇒ ('k, 'v::heap) hashtable Heap"
where
"ht_insls [] ht = return ht" |
"ht_insls ((k, v) # l) ht = do { h ← ht_upd k v ht; ht_insls l h }"

text "Abstract version"
fun ls_insls :: "('k::hashable × 'v) list
⇒ ('k × 'v) list list ⇒ ('k × 'v) list list"
where
"ls_insls [] l = l" |
"ls_insls ((k, v) # ls) l =
ls_insls ls (abs_update k v l)"

lemma ht_hash_ls_insls:
assumes "ht_hash l"
shows "ht_hash (ls_insls ls l)"
using assms
apply (induct l rule: ls_insls.induct)
apply simp
done

lemma ht_distinct_ls_insls:
assumes "ht_distinct l"
shows "ht_distinct (ls_insls ls l)"
using assms
apply (induct l rule: ls_insls.induct)
apply simp
done

lemma length_ls_insls:
assumes "1 < length l"
shows "1 < length (ls_insls ls l)"
using assms
proof (induct l rule: ls_insls.induct)
case 1
then show ?case by simp
next
case (2 k v ls l)
from 2(1)[OF length_update[OF 2(2), of k v]] show ?case
by simp
qed

lemma complete_ht_insls:
"<is_hashtable ls ht> ht_insls xs ht <is_hashtable (ls_insls xs ls)>"
proof (induct xs arbitrary: ls ht)
case Nil
show ?case by (auto intro: return_cons_rule)
next
case (Cons x xs)
show ?case
proof (cases x)
case (Pair k v)
then show ?thesis
apply simp
apply (rule bind_rule)
apply (rule complete_ht_upd)
done
qed
qed

text ‹\paragraph{Copy}›
fun ht_copy :: "nat ⇒ ('k::{heap,hashable}, 'v::heap) hashtable
⇒ ('k, 'v) hashtable ⇒ ('k, 'v) hashtable Heap"
where
"ht_copy 0 src dst = return dst" |
"ht_copy (Suc n) src dst = do {
l ← Array.nth (the_array src) n;
ht ← ht_insls l dst;
ht_copy n src ht
}"

text "Abstract version"
fun ls_copy :: "nat ⇒ ('k::hashable × 'v) list list
⇒ ('k × 'v) list list ⇒ ('k × 'v) list list"
where
"ls_copy 0 ss ds = ds" |
"ls_copy (Suc n) ss ds = ls_copy n ss (ls_insls (ss ! n) ds)"

lemma ht_hash_ls_copy:
assumes "ht_hash l"
shows "ht_hash (ls_copy n ss l)"
using assms
apply (induct n arbitrary: l)
apply simp
done

lemma ht_distinct_ls_copy:
assumes "ht_distinct l"
shows "ht_distinct (ls_copy n ss l)"
using assms
apply (induct n arbitrary: l)
apply simp
done

lemma length_ls_copy:
assumes "1 < length l"
shows "1 < length (ls_copy n ss l)"
using assms
proof (induct n arbitrary: l)
case 0
then show ?case by simp
next
case (Suc n)
from Suc(1)[OF length_ls_insls[OF Suc(2)]] show ?case by simp
qed

lemma complete_ht_copy: "n ≤ List.length ss ⟹
<is_hashtable ss src * is_hashtable ds dst>
ht_copy n src dst
<λr. is_hashtable ss src * is_hashtable (ls_copy n ss ds) r>"
proof (induct n arbitrary: ds dst)
case 0
show ?case by (auto intro!: return_cons_rule)
next
case (Suc n)
then have n: "n < length ss" by simp
then have "n ≤ length ss" by simp
note IH = Suc(1)[OF this]
show ?case
apply simp
apply (rule bind_rule)
apply (rule frame_rule)
apply (subgoal_tac "<is_hashtable ss src>
Array.nth (the_array src) n
<λr. is_hashtable ss src * ↑(r = ss ! n)>")
apply simp
apply (auto intro!: nth_rule simp add: n)[]
apply clarsimp
apply (rule bind_rule)
apply (rule frame_rule_left)
apply (rule complete_ht_insls)
done
qed

text ‹Alternative, more automatic proof›
lemma complete_ht_copy_alt_proof: "n ≤ List.length ss ⟹
<is_hashtable ss src * is_hashtable ds dst>
ht_copy n src dst
<λr. is_hashtable ss src * is_hashtable (ls_copy n ss ds) r>"
proof (induct n arbitrary: ds dst)
case 0
show ?case by (sep_auto)
next
case (Suc n)
then have N_LESS: "n < length ss" by simp
then have N_LE: "n ≤ length ss" by simp
note IH = Suc(1)[OF this]
show ?case
by (sep_auto simp: N_LESS N_LE heap: complete_ht_insls IH)
qed

definition ht_rehash
:: "('k::{heap,hashable}, 'v::heap) hashtable ⇒ ('k, 'v) hashtable Heap"
where
"ht_rehash ht = do {
n ← Array.len (the_array ht);
h ← ht_new_sz (2 * n);
ht_copy n ht h
}"

text "Operation on Abstraction"
definition ls_rehash :: "('k::hashable × 'v) list list ⇒ ('k × 'v) list list"
where "ls_rehash l = ls_copy (List.length l) l (replicate (2 * length l) [])"

lemma ht_hash_ls_rehash: "ht_hash (ls_rehash l)"

lemma ht_distinct_ls_rehash: "ht_distinct (ls_rehash l)"

lemma length_ls_rehash:
assumes "1 < length l"
shows "1 < length (ls_rehash l)"
proof -
from assms have "1 < length (replicate (2 * length l) [])" by simp
from length_ls_copy[OF this, of "length l" l] show ?thesis
qed

lemma ht_imp_len: "is_hashtable l ht ⟹⇩A is_hashtable l ht * ↑(length l > 0)"
unfolding is_hashtable_def
by sep_auto

lemma complete_ht_rehash:
"<is_hashtable l ht> ht_rehash ht
<λr. is_hashtable l ht * is_hashtable (ls_rehash l) r>"
apply (rule cons_pre_rule[OF ht_imp_len])
unfolding ht_rehash_def
apply (sep_auto heap: complete_ht_new_sz)
apply (cases l; simp)
apply (sep_auto heap: complete_ht_copy simp: ls_rehash_def)
done

definition load_factor :: nat ― ‹in percent›
"ht_update k v ht