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