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 σ)
  by (auto simp add: run.simps)


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
  by (auto simp add: run.simps)
   
lemma run_detI:
  assumes "run c (Some h) (Some h') r" "run c (Some h) σ s"
  shows "σ = Some h' ∧ r = s"
  using assms
  by (auto simp add: run.simps)

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 (simp add: run.simps)
apply (cases "execute f (the_state σ)")
apply (simp add: run.simps bind_def)
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 (auto simp add: run.simps)
  apply (simp add: execute_simps)
  
  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 (auto simp add: run.simps)
  apply (simp add: execute_simps)
  apply (simp add: Array.get_alloc)
  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 (auto simp add: run.simps)
  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 (auto simp add: run.simps)
  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 (auto simp add: run.simps)
  apply (simp add: execute_simps)
  apply (simp add: Array.get_alloc)
  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 (auto simp add: run.simps)
  apply (simp add: execute_simps)
  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)"
      by (auto simp add: execute_simps)
    then show ?thesis by (rule prems(1))
  qed
  done

lemma "fst (Ref.alloc x h) = Ref (lim h)"
  unfolding alloc_def
  by (simp add: Let_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