Theory Simple_Separation_Example

(* Title: Adaptation of example from HOL/Hoare/Separation
   Author: Gerwin Klein, 2012
   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
                Rafal Kolanski <rafal.kolanski at nicta.com.au>
*)

section "Example from HOL/Hoare/Separation"

theory Simple_Separation_Example
  imports "HOL-Hoare.Hoare_Logic_Abort" "../Sep_Heap_Instance"
          "../Sep_Tactics"
begin

declare [[syntax_ambiguity_warning = false]]

type_synonym heap = "(nat ⇒ nat option)"

(* This syntax isn't ideal, but this is what is used in the original *)
definition maps_to:: "nat ⇒ nat ⇒ heap ⇒ bool" ("_ ↦ _" [56,51] 56)
  where "x ↦ y ≡ λh. h = [x ↦ y]"

(* If you don't mind syntax ambiguity: *)
notation pred_ex  (binder "∃" 10)

(* could be generated automatically *)
definition maps_to_ex :: "nat ⇒ heap ⇒ bool" ("_ ↦ -" [56] 56)
  where "x ↦ - ≡ ∃y. x ↦ y"


(* could be generated automatically *)
lemma maps_to_maps_to_ex [elim!]:
  "(p ↦ v) s ⟹ (p ↦ -) s"
  by (auto simp: maps_to_ex_def)

(* The basic properties of maps_to: *)
lemma maps_to_write:
  "(p ↦ - ** P) H ⟹ (p ↦ v ** P) (H (p ↦ v))"
  apply (clarsimp simp: sep_conj_def maps_to_def maps_to_ex_def split: option.splits)
  apply (rule_tac x=y in exI)
  apply (auto simp: sep_disj_fun_def map_convs map_add_def split: option.splits)
  done

lemma points_to:
  "(p ↦ v ** P) H ⟹ the (H p) = v"
  by (auto elim!: sep_conjE
           simp: sep_disj_fun_def maps_to_def map_convs map_add_def
           split: option.splits)


(* This differs from the original and uses separation logic for the definition. *)
primrec
  list :: "nat ⇒ nat list ⇒ heap ⇒ bool"
where
  "list i [] = (⟨i=0⟩ and □)"
| "list i (x#xs) = (⟨i=x ∧ i≠0⟩ and (EXS j. i ↦ j ** list j xs))"

lemma list_empty [simp]:
  shows "list 0 xs = (λs. xs = [] ∧ □ s)"
  by (cases xs) auto

(* The examples from Hoare/Separation.thy *)
lemma "VARS x y z w h
 {(x ↦ y ** z ↦ w) h}
 SKIP
 {x ≠ z}"
  apply vcg
  apply(auto elim!: sep_conjE simp: maps_to_def sep_disj_fun_def domain_conv)
done

lemma "VARS H x y z w
 {(P ** Q) H}
 SKIP
 {(Q ** P) H}"
  apply vcg
  apply(simp add: sep_conj_commute)
done

lemma "VARS H
 {p≠0 ∧ (p ↦ - ** list q qs) H}
 H := H(p ↦ q)
 {list p (p#qs) H}"
  apply vcg
  apply (auto intro: maps_to_write)
done

lemma "VARS H p q r
  {(list p Ps ** list q Qs) H}
  WHILE p ≠ 0
  INV {∃ps qs. (list p ps ** list q qs) H ∧ rev ps @ qs = rev Ps @ Qs}
  DO r := p; p := the(H p); H := H(r ↦ q); q := r OD
  {list q (rev Ps @ Qs) H}"
  supply [[simproc del: defined_all]]
  apply vcg
    apply fastforce
   apply clarsimp
   apply (case_tac ps, simp)
   apply (rename_tac p ps')
   apply (clarsimp simp: sep_conj_exists sep_conj_ac)
   apply (sep_subst points_to)
   apply (rule_tac x = "ps'" in exI)
   apply (rule_tac x = "p # qs" in exI)
   apply (simp add: sep_conj_exists sep_conj_ac)
   apply (rule exI)
   apply (sep_rule maps_to_write)
   apply ((sep_cancel add: maps_to_maps_to_ex)+)[1]
  apply clarsimp
  done

end