1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(* Title: Adaptation of example from HOL/Hoare/Separation
8   Author: Gerwin Klein, 2012
9   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
10                Rafal Kolanski <rafal.kolanski at nicta.com.au>
11*)
12
13chapter "Example from HOL/Hoare/Separation"
14
15theory Simple_Separation_Example
16imports
17  "HOL-Hoare.Hoare_Logic_Abort"
18  Sep_Heap_Instance
19  Sep_Tactics
20begin
21
22declare [[syntax_ambiguity_warning = false]]
23
24type_synonym heap = "(nat \<Rightarrow> nat option)"
25
26(* This syntax isn't ideal, but this is what is used in the original *)
27definition maps_to:: "nat \<Rightarrow> nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> _" [56,51] 56)
28  where "x \<mapsto> y \<equiv> \<lambda>h. h = [x \<mapsto> y]"
29
30(* If you don't mind syntax ambiguity: *)
31notation pred_ex  (binder "\<exists>" 10)
32
33(* could be generated automatically *)
34definition maps_to_ex :: "nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> -" [56] 56)
35  where "x \<mapsto> - \<equiv> \<exists>y. x \<mapsto> y"
36
37
38(* could be generated automatically *)
39lemma maps_to_maps_to_ex [elim!]:
40  "(p \<mapsto> v) s \<Longrightarrow> (p \<mapsto> -) s"
41  by (auto simp: maps_to_ex_def)
42
43(* The basic properties of maps_to: *)
44lemma maps_to_write:
45  "(p \<mapsto> - ** P) H \<Longrightarrow> (p \<mapsto> v ** P) (H (p \<mapsto> v))"
46  apply (clarsimp simp: sep_conj_def maps_to_def maps_to_ex_def split: option.splits)
47  apply (rule_tac x=y in exI)
48  apply (auto simp: sep_disj_fun_def map_convs map_add_def split: option.splits)
49  done
50
51lemma points_to:
52  "(p \<mapsto> v ** P) H \<Longrightarrow> the (H p) = v"
53  by (auto elim!: sep_conjE
54           simp: sep_disj_fun_def maps_to_def map_convs map_add_def
55           split: option.splits)
56
57
58(* This differs from the original and uses separation logic for the definition. *)
59primrec
60  list :: "nat \<Rightarrow> nat list \<Rightarrow> heap \<Rightarrow> bool"
61where
62  "list i [] = (\<langle>i=0\<rangle> and \<box>)"
63| "list i (x#xs) = (\<langle>i=x \<and> i\<noteq>0\<rangle> and (EXS j. i \<mapsto> j ** list j xs))"
64
65lemma list_empty [simp]:
66  shows "list 0 xs = (\<lambda>s. xs = [] \<and> \<box> s)"
67  by (cases xs) auto
68
69(* The examples from Hoare/Separation.thy *)
70lemma "VARS x y z w h
71 {(x \<mapsto> y ** z \<mapsto> w) h}
72 SKIP
73 {x \<noteq> z}"
74  apply vcg
75  apply(auto elim!: sep_conjE simp: maps_to_def sep_disj_fun_def domain_conv)
76done
77
78lemma "VARS H x y z w
79 {(P ** Q) H}
80 SKIP
81 {(Q ** P) H}"
82  apply vcg
83  apply(simp add: sep_conj_commute)
84done
85
86lemma "VARS H
87 {p\<noteq>0 \<and> (p \<mapsto> - ** list q qs) H}
88 H := H(p \<mapsto> q)
89 {list p (p#qs) H}"
90  apply vcg
91  apply (auto intro: maps_to_write)
92done
93
94text \<open>First a proof without using tactics\<close>
95lemma "VARS H p q r
96  {(list p Ps ** list q Qs) H}
97  WHILE p \<noteq> 0
98  INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs}
99  DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
100  {list q (rev Ps @ Qs) H}"
101  apply vcg
102    apply fastforce
103   apply clarsimp
104   apply (case_tac ps, simp)
105   apply (rename_tac p ps')
106   apply (rule_tac x = "ps'" in exI)
107   apply (rule_tac x = "p # qs" in exI)
108   apply clarsimp
109   apply (clarsimp simp: sep_conj_exists sep_conj_ac)
110   apply (rule_tac x = "q" in exI)
111   thm points_to
112   apply (subst (asm) sep_conj_ac)
113   apply (subst (asm) sep_conj_commute)
114   apply (simp add: sep_conj_assoc)
115   apply (frule points_to)
116   apply simp
117   thm maps_to_write
118   apply (subst sep_conj_assoc[symmetric])
119   apply (subst sep_conj_commute)
120   apply (simp add: sep_conj_assoc)
121   apply (rule maps_to_write)
122   thm maps_to_maps_to_ex
123   apply (drule sep_conj_impl1[rotated])
124    apply (erule maps_to_maps_to_ex)
125   apply (rule sep_conj_impl1[rotated])
126    apply (subst sep_conj_ac, assumption)
127   apply assumption
128  apply clarsimp
129  done
130
131text \<open>Now with tactics\<close>
132lemma "VARS H p q r
133  {(list p Ps ** list q Qs) H}
134  WHILE p \<noteq> 0
135  INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs}
136  DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
137  {list q (rev Ps @ Qs) H}"
138  apply vcg
139    apply fastforce
140   apply clarsimp
141   apply (case_tac ps, simp)
142   apply (rename_tac p ps')
143   apply (clarsimp simp: sep_conj_exists sep_conj_ac)
144   apply (subst points_to, sep_solve)
145   apply (rule_tac x = "ps'" in exI)
146   apply (rule_tac x = "p # qs" in exI)
147   apply (simp add: sep_conj_exists sep_conj_ac)
148   apply (rule exI)
149   apply (sep_rule (direct) maps_to_write) \<comment> \<open>note: demonstrates computation\<close>
150   apply (sep_solve add: maps_to_maps_to_ex)
151  apply clarsimp
152  done
153
154end
155