1(*
2 * Copyright 2017, Data61, CSIRO
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(DATA61_BSD)
9 *)
10
11theory ModifiesProofs
12imports CLanguage
13begin
14
15(* Rules for breaking down modifies goals before feeding them to the VCG.
16   Helps avoid some pathological performance issues. *)
17
18definition
19  modifies_inv_refl :: "('a \<Rightarrow> 'a set) \<Rightarrow> bool"
20where
21  "modifies_inv_refl P \<equiv> \<forall>x. x \<in> P x"
22
23definition
24  modifies_inv_incl :: "('a \<Rightarrow> 'a set) \<Rightarrow> bool"
25where
26  "modifies_inv_incl P \<equiv> \<forall>x y. y \<in> P x \<longrightarrow> P y \<subseteq> P x"
27
28definition
29  modifies_inv_prop :: "('a \<Rightarrow> 'a set) \<Rightarrow> bool"
30where
31  "modifies_inv_prop P \<equiv> modifies_inv_refl P \<and> modifies_inv_incl P"
32
33lemma modifies_inv_prop:
34  "modifies_inv_refl P \<Longrightarrow> modifies_inv_incl P \<Longrightarrow> modifies_inv_prop P"
35  by (simp add: modifies_inv_prop_def)
36
37named_theorems modifies_inv_intros
38
39context
40  fixes P :: "'a \<Rightarrow> 'a set"
41  assumes p: "modifies_inv_prop P"
42begin
43
44private lemmas modifies_inv_prop' =
45  p[unfolded modifies_inv_prop_def modifies_inv_refl_def modifies_inv_incl_def]
46
47private lemma modifies_inv_prop_lift:
48  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c (P \<sigma>),(P \<sigma>)"
49  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> (P \<sigma>) c (P \<sigma>),(P \<sigma>)"
50  using modifies_inv_prop' by (fastforce intro: c hoarep.Conseq)
51
52private lemma modifies_inv_prop_lower:
53  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> (P \<sigma>) c (P \<sigma>),(P \<sigma>)"
54  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c (P \<sigma>),(P \<sigma>)"
55  using modifies_inv_prop' by (fastforce intro: c hoarep.Conseq)
56
57private lemma modifies_inv_Seq [modifies_inv_intros]:
58  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c1 (P \<sigma>),(P \<sigma>)" "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c2 (P \<sigma>),(P \<sigma>)"
59  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c1 ;; c2 (P \<sigma>),(P \<sigma>)"
60  by (intro modifies_inv_prop_lower HoarePartial.Seq[OF c[THEN modifies_inv_prop_lift]])
61
62private lemma modifies_inv_Cond [modifies_inv_intros]:
63  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c1 (P \<sigma>),(P \<sigma>)" "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c2 (P \<sigma>),(P \<sigma>)"
64  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Cond b c1 c2 (P \<sigma>),(P \<sigma>)"
65  by (auto intro: HoarePartial.Cond c)
66
67private lemma modifies_inv_Guard_strip [modifies_inv_intros]:
68  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} c (P \<sigma>),(P \<sigma>)"
69  shows "\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Guard f b c (P \<sigma>),(P \<sigma>)"
70  by (rule HoarePartial.GuardStrip[OF subset_refl c UNIV_I])
71
72private lemma modifies_inv_Skip [modifies_inv_intros]:
73  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} SKIP (P \<sigma>),(P \<sigma>)"
74  using modifies_inv_prop' by (auto intro: modifies_inv_prop_lift HoarePartial.Skip)
75
76private lemma modifies_inv_Skip' [modifies_inv_intros]:
77  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} SKIP (P \<sigma>)"
78  using modifies_inv_prop' by (auto intro: modifies_inv_prop_lift HoarePartial.Skip)
79
80private lemma modifies_inv_whileAnno [modifies_inv_intros]:
81  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c (P \<sigma>),(P \<sigma>)"
82  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} whileAnno b I V c (P \<sigma>),(P \<sigma>)"
83  apply (rule HoarePartial.reannotateWhileNoGuard[where I="P \<sigma>"])
84  by (intro HoarePartial.While hoarep.Conseq;
85      fastforce simp: modifies_inv_prop' intro: modifies_inv_prop_lift c)
86
87private lemma modifies_inv_While [modifies_inv_intros]:
88  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c (P \<sigma>),(P \<sigma>)"
89  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} While b c (P \<sigma>),(P \<sigma>)"
90  by (intro modifies_inv_whileAnno[unfolded whileAnno_def] c)
91
92private lemma modifies_inv_Throw [modifies_inv_intros]:
93  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} THROW (P \<sigma>),(P \<sigma>)"
94  using modifies_inv_prop' by (auto intro: modifies_inv_prop_lift HoarePartial.Throw)
95
96private lemma modifies_inv_Catch [modifies_inv_intros]:
97  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c1 (P \<sigma>),(P \<sigma>)"
98             "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c2 (P \<sigma>),(P \<sigma>)"
99  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} TRY c1 CATCH c2 END (P \<sigma>),(P \<sigma>)"
100  by (intro modifies_inv_prop_lower HoarePartial.Catch[OF c[THEN modifies_inv_prop_lift]])
101
102private lemma modifies_inv_Catch_all [modifies_inv_intros]:
103  assumes 1: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c1 (P \<sigma>),(P \<sigma>)"
104  assumes 2: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c2 (P \<sigma>)"
105  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} TRY c1 CATCH c2 END (P \<sigma>)"
106  apply (intro HoarePartial.Catch[OF 1] hoarep.Conseq, clarsimp)
107  apply (metis modifies_inv_prop' 2 singletonI)
108  done
109
110private lemma modifies_inv_switch_Nil [modifies_inv_intros]:
111  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} switch v [] (P \<sigma>),(P \<sigma>)"
112  by (auto intro: modifies_inv_Skip)
113
114private lemma modifies_inv_switch_Cons [modifies_inv_intros]:
115  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} c (P \<sigma>),(P \<sigma>)"
116             "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} switch p vcs (P \<sigma>),(P \<sigma>)"
117  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} switch p ((v,c) # vcs) (P \<sigma>),(P \<sigma>)"
118  by (auto intro: c modifies_inv_Cond)
119
120end
121
122context
123  fixes P :: "('c, 'd) state_scheme \<Rightarrow> ('c, 'd) state_scheme set"
124  assumes p: "modifies_inv_prop P"
125begin
126
127private lemma modifies_inv_creturn [modifies_inv_intros]:
128  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Basic (\<lambda>s. xfu (\<lambda>_. v s) s) (P \<sigma>),(P \<sigma>)"
129             "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Basic (rtu (\<lambda>_. Return)) (P \<sigma>),(P \<sigma>)"
130  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} creturn rtu xfu v (P \<sigma>),(P \<sigma>)"
131  unfolding creturn_def by (intro p c modifies_inv_intros)
132
133private lemma modifies_inv_creturn_void [modifies_inv_intros]:
134  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Basic (rtu (\<lambda>_. Return)) (P \<sigma>),(P \<sigma>)"
135  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} creturn_void rtu (P \<sigma>),(P \<sigma>)"
136  unfolding creturn_void_def by (intro p c modifies_inv_intros)
137
138private lemma modifies_inv_cbreak [modifies_inv_intros]:
139  assumes c: "\<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Basic (rtu (\<lambda>_. Break)) (P \<sigma>),(P \<sigma>)"
140  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} cbreak rtu (P \<sigma>),(P \<sigma>)"
141  unfolding cbreak_def by (intro p c modifies_inv_intros)
142
143private lemma modifies_inv_ccatchbrk [modifies_inv_intros]:
144  shows "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} ccatchbrk rt (P \<sigma>),(P \<sigma>)"
145  unfolding ccatchbrk_def by (intro p modifies_inv_intros)
146
147end
148
149end
150