1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Generic_Separation_Algebras 8imports Sep_Algebra_L4v 9begin 10 11 12instantiation "prod" :: (stronger_sep_algebra,stronger_sep_algebra) zero 13begin 14 definition "zero_prod \<equiv> (0,0)" 15 instance .. 16end 17 18instantiation "prod" :: (stronger_sep_algebra,stronger_sep_algebra) stronger_sep_algebra 19begin 20 21definition "sep_disj_prod x y \<equiv> sep_disj (fst x) (fst y) \<and> sep_disj (snd x) (snd y)" 22definition "plus_prod x y \<equiv> ( (fst x) + (fst y) , (snd x) + (snd y))" 23 24instance 25 apply intro_classes 26 apply (metis fst_conv sep_disj_prod_def sep_disj_zero snd_conv zero_prod_def) 27 apply (metis (full_types) sep_disj_commuteI sep_disj_prod_def) 28 apply (clarsimp simp: plus_prod_def zero_prod_def) 29 apply (clarsimp simp: plus_prod_def sep_disj_prod_def) 30 apply safe 31 apply (metis sep_add_commute) 32 apply (metis sep_add_commute) 33 apply (clarsimp simp: plus_prod_def sep_disj_prod_def) 34 apply (metis sep_add_assoc) 35 apply (clarsimp simp: plus_prod_def sep_disj_prod_def) 36 apply (clarsimp simp: plus_prod_def sep_disj_prod_def) 37 apply (clarsimp simp: plus_prod_def sep_disj_prod_def) 38 done 39 40end 41 42 43instantiation "option" :: (type) zero 44begin 45 definition "zero_option \<equiv> None" 46 instance .. 47end 48 49definition 50 orelse :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" 51where 52 "orelse x y \<equiv> case x of Some x' => Some x' | None => y" 53 54definition 55 onlyone :: "'a option => 'a option => bool" 56where 57 "onlyone x y \<equiv> case x of 58 Some x' => (case y of Some y' => False | _ => True) 59 | None => True" 60 61 62instantiation "option" :: (type) stronger_sep_algebra 63begin 64 65definition "sep_disj_option \<equiv> onlyone " 66definition "plus_option \<equiv> orelse" 67 68instance 69 by intro_classes 70 (clarsimp simp: sep_disj_option_def zero_option_def plus_option_def onlyone_def orelse_def 71 split: option.splits)+ 72end 73 74 75record 'a generic_heap_record = 76 heap :: "'a " 77 78instantiation "generic_heap_record_ext" :: (stronger_sep_algebra, stronger_sep_algebra) stronger_sep_algebra 79begin 80 81definition "zero_generic_heap_record_ext \<equiv> Abs_generic_heap_record_ext 0" 82definition "plus_generic_heap_record_ext h1 h2 \<equiv> 83 Abs_generic_heap_record_ext (Rep_generic_heap_record_ext h1 + Rep_generic_heap_record_ext h2)" 84definition "sep_disj_generic_heap_record_ext h1 h2 \<equiv> Rep_generic_heap_record_ext h1 ## Rep_generic_heap_record_ext h2" 85 86instance 87 apply intro_classes 88 apply (fastforce simp: sep_add_left_commute sep_disj_commute Rep_generic_heap_record_ext_inverse 89 sep_disj_commuteI sep_add_assoc sep_add_commute Abs_generic_heap_record_ext_inverse 90 zero_generic_heap_record_ext_def sep_disj_generic_heap_record_ext_def 91 plus_generic_heap_record_ext_def)+ 92 done 93 94end 95 96 97 98end 99