(* 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>

*)

header "Example from HOL/Hoare/Separation"

theory Simple_Separation_Example

  imports "~~/src/HOL/Hoare/Hoare_Logic_Abort" "../Sep_Heap_Instance"

          "../Sep_Tactics"

begin

declare [[syntax_ambiguity_warning = false]]

type_synonym heap = "(nat \<Rightarrow> nat option)"

(* This syntax isn't ideal, but this is what is used in the original *)

definition maps_to:: "nat \<Rightarrow> nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> _" [56,51] 56)

  where "x \<mapsto> y \<equiv> \<lambda>h. h = [x \<mapsto> y]"

(* If you don't mind syntax ambiguity: *)

notation pred_ex  (binder "\<exists>" 10)

(* could be generated automatically *)

definition maps_to_ex :: "nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> -" [56] 56)

  where "x \<mapsto> - \<equiv> \<exists>y. x \<mapsto> y"

(* could be generated automatically *)

lemma maps_to_maps_to_ex [elim!]:

  "(p \<mapsto> v) s \<Longrightarrow> (p \<mapsto> -) s"

  by (auto simp: maps_to_ex_def)

(* The basic properties of maps_to: *)

lemma maps_to_write:

  "(p \<mapsto> - ** P) H \<Longrightarrow> (p \<mapsto> v ** P) (H (p \<mapsto> 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 \<mapsto> v ** P) H \<Longrightarrow> 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 \<Rightarrow> nat list \<Rightarrow> heap \<Rightarrow> bool"

where

  "list i [] = (\<langle>i=0\<rangle> and \<box>)"

| "list i (x#xs) = (\<langle>i=x \<and> i\<noteq>0\<rangle> and (EXS j. i \<mapsto> j ** list j xs))"

lemma list_empty [simp]:

  shows "list 0 xs = (\<lambda>s. xs = [] \<and> \<box> s)"

  by (cases xs) auto

(* The examples from Hoare/Separation.thy *)

lemma "VARS x y z w h

 {(x \<mapsto> y ** z \<mapsto> w) h}

 SKIP

 {x \<noteq> 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\<noteq>0 \<and> (p \<mapsto> - ** list q qs) H}

 H := H(p \<mapsto> 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 \<noteq> 0

  INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs}

  DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD

  {list q (rev Ps @ Qs) H}"

  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)+

   apply ((sep_cancel add: maps_to_maps_to_ex)+)[1]

  apply clarsimp

  done

end