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