Merge branch 'master' into gicv3

lib/Corres_UL.thy

@@ -104,6 +104,17 @@ lemma corres_gets[simp, corres_no_simp]:
   (\<forall> s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (a s) (b s'))"
   by (simp add: simpler_gets_def corres_singleton)
 
+lemma corres_gets_return:
+  "corres_underlying sr nf nf' r P P' (gets f) (return v)
+   = (\<forall>s s'. ((s, s') \<in> sr \<and> P s \<and> P' s') \<longrightarrow> r (f s) v)"
+  by (fastforce simp: corres_underlying_def gets_def get_def return_def bind_def)
+
+text \<open>A safer non-rewrite version of @{thm corres_gets_return} \<close>
+lemma corres_gets_return_trivial:
+  "(\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> r (f s) v)
+   \<Longrightarrow> corres_underlying sr nf nf' r P P' (gets f) (return v)"
+  by (fastforce simp: corres_gets_return)
+
 lemma corres_throwError[simp, corres_no_simp]:
   "corres_underlying sr nf nf' r P P' (throwError a) (throwError b) =
    ((\<exists>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr) \<longrightarrow> r (Inl a) (Inl b))"
@@ -894,11 +905,24 @@ qed
 lemma corres_inst: "corres_underlying sr nf nf' r P P' f g \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" .
 
 lemma corres_assert_opt_assume:
-  assumes "\<And>x. P' = Some x \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g x)"
-  assumes "\<And>s. Q s \<Longrightarrow> P' \<noteq> None"
-  shows "corres_underlying sr nf nf' r P Q f (assert_opt P' >>= g)" using assms
-  by (auto simp: bind_def assert_opt_def assert_def fail_def return_def
-                 corres_underlying_def split: option.splits)
+  "\<lbrakk>\<And>x. opt = Some x \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g x); \<And>s. Q s \<Longrightarrow> opt \<noteq> None\<rbrakk>
+   \<Longrightarrow> corres_underlying sr nf nf' r P Q f (assert_opt opt >>= g)"
+  by (fastforce simp: bind_def return_def corres_underlying_def)
+
+lemma corres_assert_opt_assume':
+  "(\<And>x. opt = Some x \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g x))
+   \<Longrightarrow> corres_underlying sr nf nf' r P (Q and K (opt \<noteq> None)) f (assert_opt opt >>= g)"
+  by (fastforce intro: corres_gen_asm2 stronger_corres_guard_imp corres_assert_opt_assume)
+
+lemma corres_assert_opt_assume_lhs:
+  "\<lbrakk>\<And>x. opt = Some x \<Longrightarrow> corres_underlying sr nf nf' r P Q (f x) g; \<And>s. P s \<Longrightarrow> opt \<noteq> None\<rbrakk>
+   \<Longrightarrow> corres_underlying sr nf nf' r P Q (assert_opt opt >>= f) g"
+  by (fastforce simp: bind_def return_def corres_underlying_def)
+
+lemma corres_assert_opt_assume_lhs':
+  "(\<And>x. opt = Some x \<Longrightarrow> corres_underlying sr nf nf' r P Q (f x) g)
+   \<Longrightarrow> corres_underlying sr nf nf' r (P and K (opt \<noteq> None)) Q (assert_opt opt >>= f) g"
+  by (fastforce intro: corres_gen_asm stronger_corres_guard_imp corres_assert_opt_assume_lhs)
 
 lemma corres_assert_opt[corres]:
   "r x x' \<Longrightarrow>

lib/Monads/nondet/Nondet_VCG.thy

@@ -1019,6 +1019,10 @@ lemma gets_the_wp': (* FIXME: should prefer this one in [wp] *)
   unfolding gets_the_def
   by (wpsimp wp: bind_wp_fwd gets_wp assert_opt_wp)
 
+lemma gets_the_sp:
+  "\<lbrace>Q\<rbrace> gets_the f \<lbrace>\<lambda>rv s. f s = Some rv \<and> Q s\<rbrace>"
+  by (wpsimp wp: gets_the_wp')
+
 lemma gets_map_wp:
   "\<lbrace>\<lambda>s. f s p \<noteq> None \<longrightarrow> Q (the (f s p)) s\<rbrace> gets_map f p \<lbrace>Q\<rbrace>"
   unfolding gets_map_def

lib/Monads/reader_option/Reader_Option_VCG.thy

@@ -140,6 +140,13 @@ lemma ovalid_if_split:
   "\<lbrakk> P \<Longrightarrow> \<lblot>Q\<rblot> f \<lblot>S\<rblot>; \<not>P \<Longrightarrow> \<lblot>R\<rblot> g \<lblot>S\<rblot> \<rbrakk> \<Longrightarrow> \<lblot>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rblot> if P then f else g \<lblot>S\<rblot>"
   by simp
 
+lemma ovalid_if_lift2:
+  "\<lblot>P\<rblot> f \<lblot>\<lambda>rv s. (Q rv s \<longrightarrow> X rv s) \<and> (\<not> Q rv s \<longrightarrow> Y rv s)\<rblot> \<Longrightarrow>
+   \<lblot>P\<rblot> f \<lblot>\<lambda>rv s. if Q rv s then X rv s else Y rv s\<rblot>"
+  "\<lblot>P\<rblot> f \<lblot>\<lambda>rv s. (Q' rv \<longrightarrow> X rv s) \<and> (\<not> Q' rv \<longrightarrow> Y rv s)\<rblot> \<Longrightarrow>
+   \<lblot>P\<rblot> f \<lblot>\<lambda>rv. if Q' rv then X rv else Y rv\<rblot>"
+  by (auto simp: ovalid_def split_def)
+
 lemma reader_case_option_wp[wp]:
   "\<lbrakk>\<And>x. \<lblot>P x\<rblot> m x \<lblot>Q\<rblot>; \<lblot>P'\<rblot> m' \<lblot>Q\<rblot>\<rbrakk>
    \<Longrightarrow> \<lblot>\<lambda>s. (x = None \<longrightarrow> P' s) \<and> (\<forall>y. x = Some y \<longrightarrow> P y s)\<rblot> case_option m' m x \<lblot>Q\<rblot>"

lib/clib/CCorresLemmas.thy

@@ -990,6 +990,29 @@ lemma ccorres_cond2':
   apply clarsimp
   done
 
+text \<open>
+  A stronger version of @{thm ccorres_cond_both}, which allows specifying a C state predicate
+  when showing equality of the conditionals' guards, and which supplies the relevant @{term If}
+  guard truth to the @{term ccorres_underlying} assumptions.\<close>
+lemma ccorres_cond_both':
+  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
+  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
+  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
+  shows  "ccorres_underlying sr G r xf arrel axf
+          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
+          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
+          hs
+          (if P then a else b) (Cond P' c d)"
+  apply (rule ccorres_guard_imp2)
+   apply (rule ccorres_if_lhs)
+    apply (rule ccorres_cond_true)
+    apply (erule ac)
+   apply (rule ccorres_cond_false)
+   apply (erule bd)
+  apply clarsimp
+  apply (frule abs[rule_format, OF conjI], simp+)
+  done
+
 lemmas ccorres_handlers_weaken2 = ccorres_nohs
 
 lemma ccorres_abstract_cleanup:

proof/crefine/AARCH64/SyscallArgs_C.thy

@@ -707,25 +707,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_64 [simp]:
   "pageBitsForSize sz < 64"
   by (cases sz, auto simp: bit_simps)

proof/crefine/ARM/SyscallArgs_C.thy

@@ -688,25 +688,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_32 [simp]:
   "pageBitsForSize sz < 32"
   by (cases sz, auto)

proof/crefine/ARM_HYP/SyscallArgs_C.thy

@@ -711,25 +711,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_32 [simp]:
   "pageBitsForSize sz < 32"
   by (cases sz, auto)

proof/crefine/RISCV64/SyscallArgs_C.thy

@@ -707,25 +707,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_32 [simp]:
   "pageBitsForSize sz < 64"
   by (cases sz, auto simp: bit_simps)

proof/crefine/X64/SyscallArgs_C.thy

@@ -713,25 +713,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_32 [simp]:
   "pageBitsForSize sz < 64"
   by (cases sz, auto simp: bit_simps)

proof/invariant-abstract/CSpaceInv_AI.thy

@@ -76,10 +76,6 @@ lemma get_bound_notification_inv[simp]:
   apply (wp, simp)
   done
 
-lemma gets_the_sp:
-  "\<lbrace> Q \<rbrace> gets_the f \<lbrace>\<lambda>rv s. f s = Some rv \<and> Q s\<rbrace>"
-  by wpsimp
-
 lemma gets_the_get_tcb_sp:
   "\<lbrace> Q \<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>t. Q and ko_at (TCB t) thread\<rbrace>"
   by wpsimp