Merge branch 'master' into ioapic

lib/CorresK_Method.thy

@@ -969,9 +969,9 @@ method corresKwp uses wp =
       \<open>use in \<open>wp add: wp | wpc\<close>\<close>))\<close>)
 
 lemmas [corresKwp_wp_comb_del] =
-  hoare_vcg_precond_imp
-  hoare_vcg_precond_impE
-  hoare_vcg_precond_impE_R
+  hoare_weaken_pre
+  hoare_weaken_preE
+  hoare_weaken_preE_R
 
 lemma corres_inst_conj_lift[corresKwp_wp_comb]:
   "\<lbrakk>\<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. corres_inst_eq (R s) (P s)\<rbrakk> \<Longrightarrow>

lib/EquivValid.thy

@@ -513,7 +513,7 @@ lemma liftME_ev:
   shows "equiv_valid_inv I A P (liftME f g)"
   apply(simp add: liftME_def)
   apply (rule bindE_ev_pre[OF returnOk_ev reads_res])
-  apply (rule hoare_True_E_R)
+  apply (rule hoareE_R_TrueI)
   apply fast
   done
 
@@ -645,7 +645,7 @@ lemma mapME_ev_pre:
    apply(subst mapME_Cons)
    apply wp
    apply fastforce
-   apply (rule hoare_True_E_R[where P="\<top>"])
+   apply (rule wp_post_tautE_R)
    apply fastforce+
   done
 

lib/ExtraCorres.thy

@@ -72,7 +72,7 @@ next
   show ?case
     apply (simp add: mapM_Cons)
     apply (rule corres_underlying_split [OF corr' _ ha [OF Cons(2)] hc [OF Cons(2)]])
-    apply (rule corres_underlying_split [OF Cons(3) _ hoare_post_taut hoare_post_taut])
+    apply (rule corres_underlying_split [OF Cons(3) _ hoare_TrueI hoare_TrueI])
     apply (simp add: rc)
     apply (rule Cons.hyps)+
     done

lib/HaskellLemmaBucket.thy

@@ -225,15 +225,15 @@ lemma findM_on_outcome':
 lemma findM_on_outcome:
   assumes x: "\<And>x ys. x \<in> set xs \<Longrightarrow> \<lbrace>Q None and I\<rbrace> f x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> I s)\<rbrace>"
   shows      "\<lbrace>Q None and I\<rbrace> findM f xs \<lbrace>Q\<rbrace>"
-  apply (rule hoare_vcg_precond_imp)
+  apply (rule hoare_weaken_pre)
    apply (rule findM_on_outcome' [where fn="\<lambda>s. if I s then set xs else {}"])
    apply (case_tac "x \<notin> set xs")
     apply simp
    apply (simp cong: rev_conj_cong)
    apply (case_tac "\<not> set xsa \<subseteq> set xs")
     apply simp
    apply simp
-   apply (rule hoare_vcg_precond_imp)
+   apply (rule hoare_weaken_pre)
     apply (rule hoare_post_imp [OF _ x])
      apply clarsimp
     apply assumption

lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy

@@ -31,10 +31,10 @@ lemma hoare_eq_post: " \<lbrakk> \<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace
   by (rule hoare_strengthen_post, assumption, clarsimp)
 
 lemma hoare_eq_postE: " \<lbrakk> \<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>E\<rbrace>"
-  by (metis (full_types) hoare_post_impErr')
+  by (metis (full_types) hoare_strengthen_postE)
 
 lemma hoare_eq_postE_R: " \<lbrakk> \<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>, -"
-  by (metis hoare_post_imp_R)
+  by (metis hoare_strengthen_postE_R)
 
 ML \<open>
 val sep_select_post_method =  sep_select_generic_method false [@{thm hoare_eq_post},

lib/Monad_Lists.thy

@@ -469,8 +469,8 @@ lemma filterM_distinct1:
   apply (rule rev_induct [where xs=xs])
    apply (clarsimp | wp)+
   apply (simp add: filterM_append)
-  apply (erule hoare_seq_ext[rotated])
-  apply (rule hoare_seq_ext[rotated], rule hoare_vcg_prop)
+  apply (erule bind_wp_fwd)
+  apply (rule bind_wp_fwd, rule hoare_vcg_prop)
   apply (wp, clarsimp)
   apply blast
   done
@@ -601,15 +601,15 @@ lemma mapME_set:
   and     invp: "\<And>x y. \<lbrace>R and P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>, -"
   and     invr: "\<And>x. \<lbrace>R\<rbrace> f x \<lbrace>\<lambda>_. R\<rbrace>, -"
   shows "\<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. P x s\<rbrace>, -"
-proof (rule hoare_post_imp_R [where Q' = "\<lambda>rv s. R s \<and> (\<forall>x \<in> set rv. P x s)"], induct xs)
+proof (rule hoare_strengthen_postE_R [where Q' = "\<lambda>rv s. R s \<and> (\<forall>x \<in> set rv. P x s)"], induct xs)
   case Nil
   thus ?case by (simp add: mapME_Nil | wp returnOKE_R_wp)+
 next
   case (Cons y ys)
 
   have minvp: "\<And>x. \<lbrace>R and P x\<rbrace> mapME f ys \<lbrace>\<lambda>_. P x\<rbrace>, -"
     apply (rule hoare_pre)
-     apply (rule_tac Q' = "\<lambda>_ s. R s \<and> P x s" in hoare_post_imp_R)
+     apply (rule_tac Q' = "\<lambda>_ s. R s \<and> P x s" in hoare_strengthen_postE_R)
       apply (wp mapME_wp' invr invp)+
       apply simp
      apply simp
@@ -619,7 +619,7 @@ next
   show ?case
     apply (simp add: mapME_Cons)
     apply (wp)
-     apply (rule_tac Q' = "\<lambda>xs s. (R s \<and> (\<forall>x \<in> set xs. P x s)) \<and> P x s" in hoare_post_imp_R)
+     apply (rule_tac Q' = "\<lambda>xs s. (R s \<and> (\<forall>x \<in> set xs. P x s)) \<and> P rv s" in hoare_strengthen_postE_R)
       apply (wp Cons.hyps minvp)
      apply simp
     apply (fold validE_R_def)

lib/Monads/nondet/Nondet_Monad_Equations.thy

@@ -278,7 +278,7 @@ lemma bind_return_unit:
   by simp
 
 lemma modify_id_return:
- "modify id = return ()"
+  "modify id = return ()"
   by (simp add: simpler_modify_def return_def)
 
 lemma liftE_bind_return_bindE_returnOk:
@@ -496,20 +496,24 @@ lemma bind_inv_inv_comm_weak:
   apply (fastforce simp: bind_def valid_def empty_fail_def split_def image_def)
   done
 
-lemma state_assert_false[simp]: "state_assert (\<lambda>_. False) = fail"
+lemma state_assert_false[simp]:
+  "state_assert (\<lambda>_. False) = fail"
   by monad_eq
 
-lemma condition_fail_rhs: "condition C X fail = (state_assert C >>= (\<lambda>_. X))"
+lemma condition_fail_rhs:
+  "condition C X fail = (state_assert C >>= (\<lambda>_. X))"
   by (monad_eq simp: Bex_def)
 
-lemma condition_swap: "condition C A B = condition (\<lambda>s. \<not> C s) B A"
+lemma condition_swap:
+  "condition C A B = condition (\<lambda>s. \<not> C s) B A"
   by monad_eq auto
 
-lemma condition_fail_lhs: "condition C fail X = (state_assert (\<lambda>s. \<not> C s) >>= (\<lambda>_. X))"
+lemma condition_fail_lhs:
+  "condition C fail X = (state_assert (\<lambda>s. \<not> C s) >>= (\<lambda>_. X))"
   by (metis condition_fail_rhs condition_swap)
 
 lemma condition_bind_fail[simp]:
-    "(condition C A B >>= (\<lambda>_. fail)) = condition C (A >>= (\<lambda>_. fail)) (B >>= (\<lambda>_. fail))"
+  "(condition C A B >>= (\<lambda>_. fail)) = condition C (A >>= (\<lambda>_. fail)) (B >>= (\<lambda>_. fail))"
   by monad_eq blast
 
 lemma bind_fail_propagates:

lib/Monads/nondet/Nondet_More_VCG.thy

@@ -25,7 +25,7 @@ lemma hoare_post_add:
 
 lemma hoare_post_addE:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. R s \<and> Q s\<rbrace>, \<lbrace>T\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. Q s\<rbrace>, \<lbrace>T\<rbrace>"
-  by (erule hoare_post_impErr'; simp)
+  by (erule hoare_strengthen_postE; simp)
 
 lemma hoare_pre_add:
   "(\<forall>s. P s \<longrightarrow> R s) \<Longrightarrow> (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<longleftrightarrow> \<lbrace>P and R\<rbrace> f \<lbrace>Q\<rbrace>)"
@@ -137,7 +137,7 @@ lemma hoare_split_bind_case_sum:
              "\<And>rv. \<lbrace>S rv\<rbrace> h rv \<lbrace>Q\<rbrace>"
   assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>"
   shows      "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>"
-  apply (rule hoare_seq_ext[OF _ y[unfolded validE_def]])
+  apply (rule bind_wp[OF _ y[unfolded validE_def]])
   apply (wpsimp wp: x split: sum.splits)
   done
 
@@ -147,7 +147,7 @@ lemma hoare_split_bind_case_sumE:
   assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>"
   shows      "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   apply (unfold validE_def)
-  apply (rule hoare_seq_ext[OF _ y[unfolded validE_def]])
+  apply (rule bind_wp[OF _ y[unfolded validE_def]])
   apply (wpsimp wp: x[unfolded validE_def] split: sum.splits)
   done
 
@@ -509,7 +509,7 @@ lemma weaker_hoare_ifE:
   assumes x: "\<lbrace>P \<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   assumes y: "\<lbrace>P'\<rbrace> b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   shows      "\<lbrace>P and P'\<rbrace> if test then a else b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
-  apply (rule hoare_vcg_precond_impE)
+  apply (rule hoare_weaken_preE)
    apply (wp x y)
   apply simp
   done
@@ -635,7 +635,7 @@ lemma bindE_split_recursive_asm:
 
 lemma validE_R_abstract_rv:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. Q rv' s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
-  by (erule hoare_post_imp_R, simp)
+  by (erule hoare_strengthen_postE_R, simp)
 
 lemma validE_cases_valid:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (Inr rv) s\<rbrace>,\<lbrace>\<lambda>rv s. Q (Inl rv) s\<rbrace>
@@ -649,10 +649,9 @@ lemma liftM_pre:
   assumes rl: "\<lbrace>\<lambda>s. \<not> P s \<rbrace> a \<lbrace> \<lambda>_ _. False \<rbrace>"
   shows "\<lbrace>\<lambda>s. \<not> P s \<rbrace> liftM f a \<lbrace> \<lambda>_ _. False \<rbrace>"
   unfolding liftM_def
-  apply (rule seq)
-  apply (rule rl)
+  apply (rule bind_wp_fwd)
+   apply (rule rl)
   apply wp
-  apply simp
   done
 
 lemma hoare_gen_asm':

lib/Monads/nondet/Nondet_No_Throw.thy

@@ -47,7 +47,7 @@ lemma no_throw_bindE:
   "\<lbrakk> no_throw A X; \<And>a. no_throw B (Y a); \<lbrace> A \<rbrace> X \<lbrace> \<lambda>_. B \<rbrace>,\<lbrace> \<lambda>_ _. True \<rbrace> \<rbrakk>
    \<Longrightarrow> no_throw A (X >>=E Y)"
   unfolding no_throw_def
-  using hoare_validE_cases seqE by blast
+  using hoare_validE_cases bindE_wp_fwd by blast
 
 lemma no_throw_bindE_simple:
   "\<lbrakk> no_throw \<top> L; \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L >>=E R)"
@@ -81,7 +81,7 @@ lemma bindE_fail_propagates:
 lemma whileLoopE_nothrow:
   "\<lbrakk> \<And>x. no_throw \<top> (B x) \<rbrakk> \<Longrightarrow> no_throw \<top> (whileLoopE C B x)"
   unfolding no_throw_def
-  by (fastforce intro!: validE_whileLoopE intro: validE_weaken)
+  by (fastforce intro!: validE_whileLoopE intro: hoare_chainE)
 
 lemma handleE'_nothrow_lhs:
   "no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle2> R)"

lib/Monads/nondet/Nondet_Strengthen_Setup.thy

@@ -24,17 +24,17 @@ lemma strengthen_hoare [strg]:
 lemma strengthen_validE_R_cong[strg]:
   "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)\<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -)"
-  by (cases F, auto intro: hoare_post_imp_R)
+  by (cases F, auto intro: hoare_strengthen_postE_R)
 
 lemma strengthen_validE_cong[strg]:
   "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)"
-  by (cases F, auto elim: hoare_post_impErr)
+  by (cases F, auto elim: hoare_strengthen_postE)
 
 lemma strengthen_validE_E_cong[strg]:
   "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f -, \<lbrace>T\<rbrace>)"
-  by (cases F, auto elim: hoare_post_impErr simp: validE_E_def)
+  by (cases F, auto elim: hoare_strengthen_postE simp: validE_E_def)
 
 lemma wpfix_strengthen_hoare:
   "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk>

lib/Monads/nondet/Nondet_Total.thy

@@ -43,7 +43,7 @@ subsection \<open>@{method wpc} setup\<close>
 lemma wpc_helper_validNF:
   "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!"
   unfolding wpc_helper_def
-  by clarsimp (metis hoare_vcg_precond_imp no_fail_pre validNF_def)
+  by clarsimp (metis hoare_weaken_pre no_fail_pre validNF_def)
 
 wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>!" wpc_helper_validNF
 
@@ -177,12 +177,12 @@ lemma validNF_vcg_all_lift[wp]:
   "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>!"
   by (auto simp: validNF_def no_fail_def intro!: hoare_vcg_all_lift)
 
-lemma validNF_bind[wp_split]:
+lemma validNF_bind_wp[wp_split]:
   "\<lbrakk> \<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>!"
   unfolding validNF_def
-  by (auto intro: hoare_seq_ext no_fail_bind[where P=Q and Q=Q for Q, simplified])
+  by (auto intro: bind_wp no_fail_bind[where P=Q and Q=Q for Q, simplified])
 
-lemmas validNF_seq_ext = validNF_bind
+lemmas validNF_bind_wp_fwd = validNF_bind_wp[rotated]
 
 
 subsection "validNF compound rules"
@@ -278,13 +278,13 @@ lemma validE_NF_chain:
 
 lemma validE_NF_bind_wp[wp]:
   "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!"
-  by (blast intro: validE_NF hoare_vcg_seqE no_fail_pre no_fail_bindE validE_validE_R validE_weaken
+  by (blast intro: validE_NF bindE_wp no_fail_pre no_fail_bindE validE_validE_R hoare_chainE
             elim!: validE_NFE)
 
 lemma validNF_catch[wp]:
   "\<lbrakk>\<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <catch> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>!"
   unfolding validE_NF_alt_def catch_def lift_def throwError_def
-  by (clarsimp simp: validNF_return split: sum.splits elim!: validNF_bind[rotated])
+  by (clarsimp simp: validNF_return split: sum.splits elim!: validNF_bind_wp_fwd)
 
 lemma validNF_throwError[wp]:
   "\<lbrace>E e\<rbrace> throwError e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!"
@@ -330,7 +330,7 @@ lemma validE_NF_handleE'[wp]:
   "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>! \<rbrakk> \<Longrightarrow>
    \<lbrace>P\<rbrace> f <handle2> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!"
   unfolding validE_NF_alt_def handleE'_def
-  apply (erule validNF_bind[rotated])
+  apply (erule validNF_bind_wp_fwd)
   apply (clarsimp split: sum.splits)
   apply wpsimp
   done