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