# Theory Separation

Up to index of Isabelle/HOL/Hoare

theory Separation
imports HoareAbort SepLogHeap
begin

    (*  Title:      HOL/Hoare/Separation.thy
        ID:         $Id: Separation.thy,v 1.7 2005/06/17 14:13:07 haftmann Exp $
        Author:     Tobias Nipkow
        Copyright   2003 TUM

    A first attempt at a nice syntactic embedding of separation logic.
    Already builds on the theory for list abstractions.

    If we suppress the H parameter for "List", we have to hardwired this
    into parser and pretty printer, which is not very modular.
    Alternative: some syntax like <P> which stands for P H. No more
    compact, but avoids the funny H.

    *)

    theory Separation imports HoareAbort SepLogHeap begin

    text{* The semantic definition of a few connectives: *}

    constdefs
     ortho:: "heap => heap => bool" (infix "⊥" 55)
    "h1 ⊥ h2 == dom h1 ∩ dom h2 = {}"

     is_empty :: "heap => bool"
    "is_empty h == h = empty"

     singl:: "heap => nat => nat => bool"
    "singl h x y == dom h = {x} & h x = Some y"

     star:: "(heap => bool) => (heap => bool) => (heap => bool)"
    "star P Q == λh. ∃h1 h2. h = h1++h2 ∧ h1 ⊥ h2 ∧ P h1 ∧ Q h2"

     wand:: "(heap => bool) => (heap => bool) => (heap => bool)"
    "wand P Q == λh. ∀h'. h' ⊥ h ∧ P h' --> Q(h++h')"

    text{*This is what assertions look like without any syntactic sugar: *}

    lemma "VARS x y z w h
     {star (%h. singl h x y) (%h. singl h z w) h}
     SKIP
     {x ≠ z}"
    apply vcg
    apply(auto simp:star_def ortho_def singl_def)
    done

    text{* Now we add nice input syntax.  To suppress the heap parameter
    of the connectives, we assume it is always called H and add/remove it
    upon parsing/printing. Thus every pointer program needs to have a
    program variable H, and assertions should not contain any locally
    bound Hs - otherwise they may bind the implicit H. *}

    syntax
     "@emp" :: "bool" ("emp")
     "@singl" :: "nat => nat => bool" ("[_ \<mapsto> _]")
     "@star" :: "bool => bool => bool" (infixl "**" 60)
     "@wand" :: "bool => bool => bool" (infixl "-*" 60)

    ML{*
    (* free_tr takes care of free vars in the scope of sep. logic connectives:
       they are implicitly applied to the heap *)
    fun free_tr(t as Free _) = t $ Syntax.free "H"
    (*
      | free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps
    *)
      | free_tr t = t

    fun emp_tr [] = Syntax.const "is_empty" $ Syntax.free "H"
      | emp_tr ts = raise TERM ("emp_tr", ts);
    fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
      | singl_tr ts = raise TERM ("singl_tr", ts);
    fun star_tr [P,Q] = Syntax.const "star" $
          absfree("H",dummyT,free_tr P) $ absfree("H",dummyT,free_tr Q) $
          Syntax.free "H"
      | star_tr ts = raise TERM ("star_tr", ts);
    fun wand_tr [P,Q] = Syntax.const "wand" $
          absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
      | wand_tr ts = raise TERM ("wand_tr", ts);
    *}

    parse_translation
     {* [("@emp", emp_tr), ("@singl", singl_tr),
         ("@star", star_tr), ("@wand", wand_tr)] *}

    text{* Now it looks much better: *}

    lemma "VARS H x y z w
     {[x\<mapsto>y] ** [z\<mapsto>w]}
     SKIP
     {x ≠ z}"
    apply vcg
    apply(auto simp:star_def ortho_def singl_def)
    done

    lemma "VARS H x y z w
     {emp ** emp}
     SKIP
     {emp}"
    apply vcg
    apply(auto simp:star_def ortho_def is_empty_def)
    done

    text{* But the output is still unreadable. Thus we also strip the heap
    parameters upon output: *}

    (* debugging code:
    fun sot(Free(s,_)) = s
      | sot(Var((s,i),_)) = "?" ^ s ^ string_of_int i
      | sot(Const(s,_)) = s
      | sot(Bound i) = "B." ^ string_of_int i
      | sot(s $ t) = "(" ^ sot s ^ " " ^ sot t ^ ")"
      | sot(Abs(_,_,t)) = "(% " ^ sot t ^ ")";
    *)

    ML{*
    local
    fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t
      | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
    (*
      | strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps
    *)
      | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
      | strip (Abs(_,_,P)) = P
      | strip (Const("is_empty",_)) = Syntax.const "@emp"
      | strip t = t;
    in
    fun is_empty_tr' [_] = Syntax.const "@emp"
    fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
    fun star_tr' [P,Q,_] = Syntax.const "@star" $ strip P $ strip Q
    fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q
    end
    *}

    print_translation
     {* [("is_empty", is_empty_tr'),("singl", singl_tr'),
         ("star", star_tr'),("wand", wand_tr')] *}

    text{* Now the intermediate proof states are also readable: *}

    lemma "VARS H x y z w
     {[x\<mapsto>y] ** [z\<mapsto>w]}
     y := w
     {x ≠ z}"
    apply vcg
    apply(auto simp:star_def ortho_def singl_def)
    done

    lemma "VARS H x y z w
     {emp ** emp}
     SKIP
     {emp}"
    apply vcg
    apply(auto simp:star_def ortho_def is_empty_def)
    done

    text{* So far we have unfolded the separation logic connectives in
    proofs. Here comes a simple example of a program proof that uses a law
    of separation logic instead. *}

    (* a law of separation logic *)
    lemma star_comm: "P ** Q = Q ** P"
    apply(simp add:star_def ortho_def)
    apply(blast intro:map_add_comm)
    done

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

    lemma "VARS H
     {p≠0 ∧ [p \<mapsto> x] ** List H q qs}
     H := H(p \<mapsto> q)
     {List H p (p#qs)}"
    apply vcg
    apply(simp add: star_def ortho_def singl_def)
    apply clarify
    apply(subgoal_tac "p ∉ set qs")
     prefer 2
     apply(blast dest:list_in_heap)
    apply simp
    done

    lemma "VARS H p q r
      {List H p Ps ** List H q Qs}
      WHILE p ≠ 0
      INV {∃ps qs. (List H p ps ** List H q qs) ∧ rev ps @ qs = rev Ps @ Qs}
      DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
      {List H q (rev Ps @ Qs)}"
    apply vcg
    apply(simp_all add: star_def ortho_def singl_def)

    apply fastsimp

    apply (clarsimp simp add:List_non_null)
    apply(rename_tac ps')
    apply(rule_tac x = ps' in exI)
    apply(rule_tac x = "p#qs" in exI)
    apply simp
    apply(rule_tac x = "h1(p:=None)" in exI)
    apply(rule_tac x = "h2(p\<mapsto>q)" in exI)
    apply simp
    apply(rule conjI)
     apply(rule ext)
     apply(simp add:map_add_def split:option.split)
    apply(rule conjI)
     apply blast
    apply(simp add:map_add_def split:option.split)
    apply(rule conjI)
    apply(subgoal_tac "p ∉ set qs")
     prefer 2
     apply(blast dest:list_in_heap)
    apply(simp)
    apply fast

    apply(fastsimp)
    done

    end

lemma

      {star (%h. singl h x y) (%h. singl h z w) h}
       SKIP
       {x ≠ z}

lemma

      {star (%H. singl H x y) (%H. singl H z w) H}
       SKIP
       {x ≠ z}

lemma

      {star is_empty is_empty H}
       SKIP
       {is_empty H}

lemma

      {[x \<mapsto> y] ** [z \<mapsto> w]}
       y := w
       {x ≠ z}

lemma

      {emp ** emp}
       SKIP
       {emp}

lemma star_comm:

      P ** Q = Q ** P

lemma

      {P ** Q}
       SKIP
       {Q ** P}

lemma

      {p ≠ 0 ∧ [p \<mapsto> x] ** List B.0 q qs}
       H := H(p |-> q)
       {List H p (p # qs)}

lemma

      {List B.0 p Ps ** List B.0 q Qs}
       WHILE p ≠ 0
        INV {∃ps qs. List B.0 p ps ** List B.0 q qs ∧ rev ps @ qs = rev Ps @ Qs}
        DO r := p; p := the (H p); H := H(r |-> q); q := r OD
       {List H q (rev Ps @ Qs)}