1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(* Author: Gerwin Klein, 2012
8   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
9                Rafal Kolanski <rafal.kolanski at nicta.com.au>
10*)
11
12chapter "Standard Heaps as an Instance of Separation Algebra"
13
14theory Sep_Heap_Instance
15imports Separation_Algebra
16begin
17
18text \<open>
19  Example instantiation of a the separation algebra to a map, i.e.\ a
20  function from any type to @{typ "'a option"}.
21\<close>
22
23class opt =
24  fixes none :: 'a
25begin
26  definition "domain f \<equiv> {x. f x \<noteq> none}"
27end
28
29instantiation option :: (type) opt
30begin
31  definition none_def [simp]: "none \<equiv> None"
32  instance ..
33end
34
35instantiation "fun" :: (type, opt) zero
36begin
37  definition zero_fun_def: "0 \<equiv> \<lambda>s. none"
38  instance ..
39end
40
41instantiation "fun" :: (type, opt) sep_algebra
42begin
43
44definition
45  plus_fun_def: "m1 + m2 \<equiv> \<lambda>x. if m2 x = none then m1 x else m2 x"
46
47definition
48  sep_disj_fun_def: "sep_disj m1 m2 \<equiv> domain m1 \<inter> domain m2 = {}"
49
50instance
51  apply intro_classes
52        apply (simp add: sep_disj_fun_def domain_def zero_fun_def)
53       apply (fastforce simp: sep_disj_fun_def)
54      apply (simp add: plus_fun_def zero_fun_def)
55     apply (simp add: plus_fun_def sep_disj_fun_def domain_def)
56     apply (rule ext)
57     apply fastforce
58    apply (rule ext)
59    apply (simp add: plus_fun_def)
60   apply (simp add: sep_disj_fun_def domain_def plus_fun_def)
61   apply fastforce
62  apply (simp add: sep_disj_fun_def domain_def plus_fun_def)
63  apply fastforce
64  done
65
66end
67
68text \<open>
69  For the actual option type @{const domain} and @{text "+"} are
70  just @{const dom} and @{text "++"}:
71\<close>
72
73lemma domain_conv: "domain = dom"
74  by (rule ext) (simp add: domain_def dom_def)
75
76lemma plus_fun_conv: "a + b = a ++ b"
77  by (auto simp: plus_fun_def map_add_def split: option.splits)
78
79lemmas map_convs = domain_conv plus_fun_conv
80
81text \<open>
82  Any map can now act as a separation heap without further work:
83\<close>
84lemma
85  fixes h :: "(nat => nat) => 'foo option"
86  shows "(P ** Q ** H) h = (Q ** H ** P) h"
87  by (simp add: sep_conj_ac)
88
89section \<open>@{typ unit} Instantiation\<close>
90
91text \<open>
92  The @{typ unit} type also forms a separation algebra. Although
93  typically not useful as a state space by itself, it may be
94  a type parameter to more complex state space.
95\<close>
96
97instantiation "unit" :: stronger_sep_algebra
98begin
99  definition "plus_unit (a :: unit) (b :: unit) \<equiv> ()"
100  definition "sep_disj_unit  (a :: unit) (b :: unit) \<equiv> True"
101  instance
102    apply intro_classes
103    apply (simp add: plus_unit_def sep_disj_unit_def)+
104    done
105end
106
107lemma unit_disj_sep_unit [simp]: "(a :: unit) ## b"
108  by (clarsimp simp: sep_disj_unit_def)
109
110lemma unit_plus_unit [simp]: "(a :: unit) + b = ()"
111  by (rule unit_eq)
112
113section \<open>@{typ "'a option"} Instantiation\<close>
114
115text \<open>
116  The @{typ "'a option"} is a seperation algebra, with @{term None}
117  indicating emptyness.
118\<close>
119
120instantiation option :: (type) stronger_sep_algebra
121begin
122  definition
123    "zero_option \<equiv> None"
124  definition
125    "plus_option (a :: 'a option) (b :: 'a option) \<equiv> (case b of None \<Rightarrow> a | Some x \<Rightarrow> b)"
126  definition
127    "sep_disj_option  (a :: 'a option) (b :: 'a option) \<equiv> a = None \<or> b = None"
128
129  instance
130    by intro_classes
131       (auto simp: zero_option_def sep_disj_option_def plus_option_def split: option.splits)
132end
133
134lemma disj_sep_None [simp]:
135  "a ## None"
136  "None ## a"
137  by (auto simp: sep_disj_option_def)
138
139lemma disj_sep_Some_Some [simp]:
140  "\<not> (Some a ## Some b)"
141  by (auto simp: sep_disj_option_def)
142
143lemma None_plus [simp]:
144  "a + None = a"
145  "None + a = a"
146  by (auto simp: plus_option_def split: option.splits)
147
148lemma None_plus_distrib:
149  "(a :: 'a option) + (b + c) = (a + b) + c"
150  by (clarsimp simp: plus_option_def split: option.splits)
151
152end
153