|
1 (* Author: Gerwin Klein, 2012 |
|
2 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> |
|
3 Rafal Kolanski <rafal.kolanski at nicta.com.au> |
|
4 *) |
|
5 |
|
6 header "Standard Heaps as an Instance of Separation Algebra" |
|
7 |
|
8 theory Sep_Heap_Instance |
|
9 imports Separation_Algebra |
|
10 begin |
|
11 |
|
12 text {* |
|
13 Example instantiation of a the separation algebra to a map, i.e.\ a |
|
14 function from any type to @{typ "'a option"}. |
|
15 *} |
|
16 |
|
17 class opt = |
|
18 fixes none :: 'a |
|
19 begin |
|
20 definition "domain f \<equiv> {x. f x \<noteq> none}" |
|
21 end |
|
22 |
|
23 instantiation option :: (type) opt |
|
24 begin |
|
25 definition none_def [simp]: "none \<equiv> None" |
|
26 instance .. |
|
27 end |
|
28 |
|
29 instantiation "fun" :: (type, opt) zero |
|
30 begin |
|
31 definition zero_fun_def: "0 \<equiv> \<lambda>s. none" |
|
32 instance .. |
|
33 end |
|
34 |
|
35 instantiation "fun" :: (type, opt) sep_algebra |
|
36 begin |
|
37 |
|
38 definition |
|
39 plus_fun_def: "m1 + m2 \<equiv> \<lambda>x. if m2 x = none then m1 x else m2 x" |
|
40 |
|
41 definition |
|
42 sep_disj_fun_def: "sep_disj m1 m2 \<equiv> domain m1 \<inter> domain m2 = {}" |
|
43 |
|
44 instance |
|
45 apply default |
|
46 apply (simp add: sep_disj_fun_def domain_def zero_fun_def) |
|
47 apply (fastforce simp: sep_disj_fun_def) |
|
48 apply (simp add: plus_fun_def zero_fun_def) |
|
49 apply (simp add: plus_fun_def sep_disj_fun_def domain_def) |
|
50 apply (rule ext) |
|
51 apply fastforce |
|
52 apply (rule ext) |
|
53 apply (simp add: plus_fun_def) |
|
54 apply (simp add: sep_disj_fun_def domain_def plus_fun_def) |
|
55 apply fastforce |
|
56 apply (simp add: sep_disj_fun_def domain_def plus_fun_def) |
|
57 apply fastforce |
|
58 done |
|
59 |
|
60 end |
|
61 |
|
62 text {* |
|
63 For the actual option type @{const domain} and @{text "+"} are |
|
64 just @{const dom} and @{text "++"}: |
|
65 *} |
|
66 |
|
67 lemma domain_conv: "domain = dom" |
|
68 by (rule ext) (simp add: domain_def dom_def) |
|
69 |
|
70 lemma plus_fun_conv: "a + b = a ++ b" |
|
71 by (auto simp: plus_fun_def map_add_def split: option.splits) |
|
72 |
|
73 lemmas map_convs = domain_conv plus_fun_conv |
|
74 |
|
75 text {* |
|
76 Any map can now act as a separation heap without further work: |
|
77 *} |
|
78 lemma |
|
79 fixes h :: "(nat => nat) => 'foo option" |
|
80 shows "(P ** Q ** H) h = (Q ** H ** P) h" |
|
81 by (simp add: sep_conj_ac) |
|
82 |
|
83 end |
|
84 |