# Theory Separation_Logic_Imperative_HOL.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
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
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