|
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 "Equivalence between Separation Algebra Formulations" |
|
7 |
|
8 theory Sep_Eq |
|
9 imports Separation_Algebra Separation_Algebra_Alt |
|
10 begin |
|
11 |
|
12 text {* |
|
13 In this theory we show that our total formulation of separation algebra is |
|
14 equivalent in strength to Calcagno et al's original partial one. |
|
15 |
|
16 This theory is not intended to be included in own developments. |
|
17 *} |
|
18 |
|
19 no_notation map_add (infixl "++" 100) |
|
20 |
|
21 section "Total implies Partial" |
|
22 |
|
23 definition add2 :: "'a::sep_algebra => 'a => 'a option" where |
|
24 "add2 x y \<equiv> if x ## y then Some (x + y) else None" |
|
25 |
|
26 lemma add2_zero: "add2 x 0 = Some x" |
|
27 by (simp add: add2_def) |
|
28 |
|
29 lemma add2_comm: "add2 x y = add2 y x" |
|
30 by (auto simp: add2_def sep_add_commute sep_disj_commute) |
|
31 |
|
32 lemma add2_assoc: |
|
33 "lift2 add2 a (lift2 add2 b c) = lift2 add2 (lift2 add2 a b) c" |
|
34 by (auto simp: add2_def lift2_def sep_add_assoc |
|
35 dest: sep_disj_addD sep_disj_addI3 |
|
36 sep_add_disjD sep_disj_addI2 sep_disj_commuteI |
|
37 split: option.splits) |
|
38 |
|
39 interpretation total_partial: sep_algebra_alt 0 add2 |
|
40 by (unfold_locales) (auto intro: add2_zero add2_comm add2_assoc) |
|
41 |
|
42 |
|
43 section "Partial implies Total" |
|
44 |
|
45 definition |
|
46 sep_add' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a :: sep_algebra_alt" where |
|
47 "sep_add' x y \<equiv> if disjoint x y then the (add x y) else undefined" |
|
48 |
|
49 lemma sep_disj_zero': |
|
50 "disjoint x 0" |
|
51 by simp |
|
52 |
|
53 lemma sep_disj_commuteI': |
|
54 "disjoint x y \<Longrightarrow> disjoint y x" |
|
55 by (clarsimp simp: disjoint_def add_comm) |
|
56 |
|
57 lemma sep_add_zero': |
|
58 "sep_add' x 0 = x" |
|
59 by (simp add: sep_add'_def) |
|
60 |
|
61 lemma sep_add_commute': |
|
62 "disjoint x y \<Longrightarrow> sep_add' x y = sep_add' y x" |
|
63 by (clarsimp simp: sep_add'_def disjoint_def add_comm) |
|
64 |
|
65 lemma sep_add_assoc': |
|
66 "\<lbrakk> disjoint x y; disjoint y z; disjoint x z \<rbrakk> \<Longrightarrow> |
|
67 sep_add' (sep_add' x y) z = sep_add' x (sep_add' y z)" |
|
68 using add_assoc [of "Some x" "Some y" "Some z"] |
|
69 by (clarsimp simp: disjoint_def sep_add'_def lift2_def |
|
70 split: option.splits) |
|
71 |
|
72 lemma sep_disj_addD1': |
|
73 "disjoint x (sep_add' y z) \<Longrightarrow> disjoint y z \<Longrightarrow> disjoint x y" |
|
74 proof (clarsimp simp: disjoint_def sep_add'_def) |
|
75 fix a assume a: "y \<oplus> z = Some a" |
|
76 fix b assume b: "x \<oplus> a = Some b" |
|
77 with a have "Some x ++ (Some y ++ Some z) = Some b" by (simp add: lift2_def) |
|
78 hence "(Some x ++ Some y) ++ Some z = Some b" by (simp add: add_assoc) |
|
79 thus "\<exists>b. x \<oplus> y = Some b" by (simp add: lift2_def split: option.splits) |
|
80 qed |
|
81 |
|
82 lemma sep_disj_addI1': |
|
83 "disjoint x (sep_add' y z) \<Longrightarrow> disjoint y z \<Longrightarrow> disjoint (sep_add' x y) z" |
|
84 apply (clarsimp simp: disjoint_def sep_add'_def) |
|
85 apply (rule conjI) |
|
86 apply clarsimp |
|
87 apply (frule lift_to_add2, assumption) |
|
88 apply (simp add: add_assoc) |
|
89 apply (clarsimp simp: lift2_def add_comm) |
|
90 apply clarsimp |
|
91 apply (frule lift_to_add2, assumption) |
|
92 apply (simp add: add_assoc) |
|
93 apply (clarsimp simp: lift2_def) |
|
94 done |
|
95 |
|
96 interpretation partial_total: sep_algebra sep_add' 0 disjoint |
|
97 apply (unfold_locales) |
|
98 apply (rule sep_disj_zero') |
|
99 apply (erule sep_disj_commuteI') |
|
100 apply (rule sep_add_zero') |
|
101 apply (erule sep_add_commute') |
|
102 apply (erule (2) sep_add_assoc') |
|
103 apply (erule (1) sep_disj_addD1') |
|
104 apply (erule (1) sep_disj_addI1') |
|
105 done |
|
106 |
|
107 end |
|
108 |