|
1 (* Title: Adaptation of example from HOL/Hoare/Separation |
|
2 Author: Gerwin Klein, 2012 |
|
3 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> |
|
4 Rafal Kolanski <rafal.kolanski at nicta.com.au> |
|
5 *) |
|
6 |
|
7 header "Example from HOL/Hoare/Separation" |
|
8 |
|
9 theory Simple_Separation_Example |
|
10 imports "~~/src/HOL/Hoare/Hoare_Logic_Abort" "../Sep_Heap_Instance" |
|
11 "../Sep_Tactics" |
|
12 begin |
|
13 |
|
14 declare [[syntax_ambiguity_warning = false]] |
|
15 |
|
16 type_synonym heap = "(nat \<Rightarrow> nat option)" |
|
17 |
|
18 (* This syntax isn't ideal, but this is what is used in the original *) |
|
19 definition maps_to:: "nat \<Rightarrow> nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> _" [56,51] 56) |
|
20 where "x \<mapsto> y \<equiv> \<lambda>h. h = [x \<mapsto> y]" |
|
21 |
|
22 (* If you don't mind syntax ambiguity: *) |
|
23 notation pred_ex (binder "\<exists>" 10) |
|
24 |
|
25 (* could be generated automatically *) |
|
26 definition maps_to_ex :: "nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> -" [56] 56) |
|
27 where "x \<mapsto> - \<equiv> \<exists>y. x \<mapsto> y" |
|
28 |
|
29 |
|
30 (* could be generated automatically *) |
|
31 lemma maps_to_maps_to_ex [elim!]: |
|
32 "(p \<mapsto> v) s \<Longrightarrow> (p \<mapsto> -) s" |
|
33 by (auto simp: maps_to_ex_def) |
|
34 |
|
35 (* The basic properties of maps_to: *) |
|
36 lemma maps_to_write: |
|
37 "(p \<mapsto> - ** P) H \<Longrightarrow> (p \<mapsto> v ** P) (H (p \<mapsto> v))" |
|
38 apply (clarsimp simp: sep_conj_def maps_to_def maps_to_ex_def split: option.splits) |
|
39 apply (rule_tac x=y in exI) |
|
40 apply (auto simp: sep_disj_fun_def map_convs map_add_def split: option.splits) |
|
41 done |
|
42 |
|
43 lemma points_to: |
|
44 "(p \<mapsto> v ** P) H \<Longrightarrow> the (H p) = v" |
|
45 by (auto elim!: sep_conjE |
|
46 simp: sep_disj_fun_def maps_to_def map_convs map_add_def |
|
47 split: option.splits) |
|
48 |
|
49 |
|
50 (* This differs from the original and uses separation logic for the definition. *) |
|
51 primrec |
|
52 list :: "nat \<Rightarrow> nat list \<Rightarrow> heap \<Rightarrow> bool" |
|
53 where |
|
54 "list i [] = (\<langle>i=0\<rangle> and \<box>)" |
|
55 | "list i (x#xs) = (\<langle>i=x \<and> i\<noteq>0\<rangle> and (EXS j. i \<mapsto> j ** list j xs))" |
|
56 |
|
57 lemma list_empty [simp]: |
|
58 shows "list 0 xs = (\<lambda>s. xs = [] \<and> \<box> s)" |
|
59 by (cases xs) auto |
|
60 |
|
61 (* The examples from Hoare/Separation.thy *) |
|
62 lemma "VARS x y z w h |
|
63 {(x \<mapsto> y ** z \<mapsto> w) h} |
|
64 SKIP |
|
65 {x \<noteq> z}" |
|
66 apply vcg |
|
67 apply(auto elim!: sep_conjE simp: maps_to_def sep_disj_fun_def domain_conv) |
|
68 done |
|
69 |
|
70 lemma "VARS H x y z w |
|
71 {(P ** Q) H} |
|
72 SKIP |
|
73 {(Q ** P) H}" |
|
74 apply vcg |
|
75 apply(simp add: sep_conj_commute) |
|
76 done |
|
77 |
|
78 lemma "VARS H |
|
79 {p\<noteq>0 \<and> (p \<mapsto> - ** list q qs) H} |
|
80 H := H(p \<mapsto> q) |
|
81 {list p (p#qs) H}" |
|
82 apply vcg |
|
83 apply (auto intro: maps_to_write) |
|
84 done |
|
85 |
|
86 lemma "VARS H p q r |
|
87 {(list p Ps ** list q Qs) H} |
|
88 WHILE p \<noteq> 0 |
|
89 INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs} |
|
90 DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD |
|
91 {list q (rev Ps @ Qs) H}" |
|
92 apply vcg |
|
93 apply fastforce |
|
94 apply clarsimp |
|
95 apply (case_tac ps, simp) |
|
96 apply (rename_tac p ps') |
|
97 apply (clarsimp simp: sep_conj_exists sep_conj_ac) |
|
98 apply (sep_subst points_to) |
|
99 apply (rule_tac x = "ps'" in exI) |
|
100 apply (rule_tac x = "p # qs" in exI) |
|
101 apply (simp add: sep_conj_exists sep_conj_ac) |
|
102 apply (rule exI) |
|
103 apply (sep_rule maps_to_write) |
|
104 apply (sep_cancel)+ |
|
105 apply ((sep_cancel add: maps_to_maps_to_ex)+)[1] |
|
106 apply clarsimp |
|
107 done |
|
108 |
|
109 end |