Merge branch 'master' into simpl-update

lib/Monads/nondet/Nondet_No_Fail.thy

@@ -54,39 +54,43 @@ lemma no_failD:
   "\<lbrakk> no_fail P m; P s \<rbrakk> \<Longrightarrow> \<not>(snd (m s))"
   by (simp add: no_fail_def)
 
+lemma no_fail_return[simp, wp]:
+  "no_fail \<top> (return x)"
+  by (simp add: return_def no_fail_def)
+
+lemma no_fail_bind[wp]:
+  "\<lbrakk> \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
+  unfolding no_fail_def bind_def
+  using post_by_hoare by fastforce
+
+lemma no_fail_get[simp, wp]:
+  "no_fail \<top> get"
+  by (simp add: get_def no_fail_def)
+
+lemma no_fail_put[simp, wp]:
+  "no_fail \<top> (put s)"
+  by (simp add: put_def no_fail_def)
+
 lemma no_fail_modify[wp,simp]:
   "no_fail \<top> (modify f)"
-  by (simp add: no_fail_def modify_def get_def put_def bind_def)
+  by (wpsimp simp: modify_def)
 
 lemma no_fail_gets_simp[simp]:
   "no_fail P (gets f)"
-  unfolding no_fail_def gets_def get_def return_def bind_def
-  by simp
+  by (wpsimp simp: gets_def)
 
 lemma no_fail_gets[wp]:
   "no_fail \<top> (gets f)"
   by simp
 
-lemma no_fail_select[simp]:
+lemma no_fail_select[wp,simp]:
   "no_fail \<top> (select S)"
   by (simp add: no_fail_def select_def)
 
 lemma no_fail_alt[wp]:
   "\<lbrakk> no_fail P f; no_fail Q g \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f \<sqinter> g)"
   by (simp add: no_fail_def alternative_def)
 
-lemma no_fail_return[simp, wp]:
-  "no_fail \<top> (return x)"
-  by (simp add: return_def no_fail_def)
-
-lemma no_fail_get[simp, wp]:
-  "no_fail \<top> get"
-  by (simp add: get_def no_fail_def)
-
-lemma no_fail_put[simp, wp]:
-  "no_fail \<top> (put s)"
-  by (simp add: put_def no_fail_def)
-
 lemma no_fail_when[wp]:
   "(P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then Q else \<top>) (when P f)"
   by (simp add: when_def)
@@ -129,11 +133,6 @@ lemma no_fail_returnOK[simp, wp]:
   "no_fail \<top> (returnOk x)"
   by (simp add: returnOk_def)
 
-lemma no_fail_bind[wp]:
-  "\<lbrakk> \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
-  unfolding no_fail_def bind_def
-  using post_by_hoare by fastforce
-
 lemma no_fail_assume_pre:
   "(\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f"
   by (simp add: no_fail_def)
@@ -220,7 +219,7 @@ lemma no_fail_state_assert[wp]:
   unfolding state_assert_def
   by wpsimp
 
-lemma no_fail_condition:
+lemma no_fail_condition[wp]:
   "\<lbrakk>no_fail Q A; no_fail R B\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s)) (condition C A B)"
   unfolding condition_def no_fail_def
   by clarsimp
@@ -231,6 +230,6 @@ lemma no_fail_ex_lift:
 
 lemma no_fail_grab_asm:
   "(G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. G \<and> P s) f"
-  by (cases G, simp+)
+  by (cases G; clarsimp)
 
 end

lib/Monads/nondet/Nondet_Total.thy

@@ -202,7 +202,7 @@ lemma validNF_gets[wp]:
 lemma validNF_condition[wp]:
   "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>!"
   by (erule validNFE)+
-     (rule validNF; wpsimp wp: no_fail_condition)
+     (rule validNF; wpsimp)
 
 lemma validNF_assert[wp]:
   "\<lbrace> (\<lambda>s. P) and (R ()) \<rbrace> assert P \<lbrace> R \<rbrace>!"
@@ -344,7 +344,7 @@ lemma validE_NF_handleE[wp]:
 lemma validE_NF_condition[wp]:
   "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow>
    \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!"
-  by (erule validE_NFE)+ (wpsimp wp: no_fail_condition validE_NF)
+  by (erule validE_NFE)+ (wpsimp wp: validE_NF)
 
 lemma hoare_assume_preNF:
   "(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!"

lib/Monads/trace/Trace_Empty_Fail.thy

@@ -18,7 +18,7 @@ text \<open>
   following property: if they return an empty set of completed results, there exists a trace
   corresponding to a failed result.\<close>
 definition empty_fail :: "('s,'a) tmonad \<Rightarrow> bool" where
-  "empty_fail m \<equiv> \<forall>s. mres (m s) = {} \<longrightarrow> Failed \<in> snd ` (m s)"
+  "empty_fail m \<equiv> \<forall>s. mres (m s) = {} \<longrightarrow> failed (m s)"
 
 text \<open>Useful in forcing otherwise unknown executions to have the @{const empty_fail} property.\<close>
 definition mk_ef ::
@@ -38,28 +38,28 @@ wpc_setup "\<lambda>m. empty_fail m" wpc_helper_empty_fail_final
 subsection \<open>@{const empty_fail} intro/dest rules\<close>
 
 lemma empty_failI:
-  "(\<And>s. mres (m s) = {} \<Longrightarrow> Failed \<in> snd ` (m s)) \<Longrightarrow> empty_fail m"
+  "(\<And>s. mres (m s) = {} \<Longrightarrow> failed (m s)) \<Longrightarrow> empty_fail m"
   by (simp add: empty_fail_def)
 
 lemma empty_failD:
-  "\<lbrakk> empty_fail m; mres (m s) = {} \<rbrakk> \<Longrightarrow> Failed \<in> snd ` (m s)"
+  "\<lbrakk> empty_fail m; mres (m s) = {} \<rbrakk> \<Longrightarrow> failed (m s)"
   by (simp add: empty_fail_def)
 
 lemma empty_fail_not_snd:
-  "\<lbrakk> Failed \<notin> snd ` (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> mres (m s)"
+  "\<lbrakk> \<not> failed (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> mres (m s)"
   by (fastforce simp: empty_fail_def)
 
 lemmas empty_failD2 = empty_fail_not_snd[rotated]
 
 lemma empty_failD3:
-  "\<lbrakk> empty_fail f; Failed \<notin> snd ` (f s) \<rbrakk> \<Longrightarrow> mres (f s) \<noteq> {}"
+  "\<lbrakk> empty_fail f; \<not> failed (f s) \<rbrakk> \<Longrightarrow> mres (f s) \<noteq> {}"
   by (drule(1) empty_failD2, clarsimp)
 
 lemma empty_fail_bindD1:
   "empty_fail (a >>= b) \<Longrightarrow> empty_fail a"
   unfolding empty_fail_def bind_def
   apply (erule all_reg[rotated])
-  by (force simp: split_def mres_def vimage_def split: tmres.splits)
+  by (force simp: split_def mres_def vimage_def failed_def split: tmres.splits)
 
 
 subsection \<open>Wellformed monads\<close>
@@ -116,23 +116,23 @@ lemma mres_bind_empty:
   apply fastforce
   done
 
-lemma bind_FailedI1:
-  "Failed \<in> snd ` f s \<Longrightarrow> Failed \<in> snd ` (f >>= g) s"
-  by (force simp: bind_def vimage_def)
+lemma bind_failedI1:
+  "failed (f s) \<Longrightarrow> failed ((f >>= g) s)"
+  by (force simp: bind_def vimage_def failed_def)
 
-lemma bind_FailedI2:
-  "\<lbrakk>\<forall>res\<in>mres (f s). Failed \<in> snd ` (g (fst res) (snd res)); mres (f s) \<noteq> {}\<rbrakk>
-   \<Longrightarrow> Failed \<in> snd ` (f >>= g) s"
-  by (force simp: bind_def mres_def image_def split_def)
+lemma bind_failedI2:
+  "\<lbrakk>\<forall>res\<in>mres (f s). failed (g (fst res) (snd res)); mres (f s) \<noteq> {}\<rbrakk>
+   \<Longrightarrow> failed ((f >>= g) s)"
+  by (force simp: bind_def mres_def image_def split_def failed_def)
 
 lemma empty_fail_bind[empty_fail_cond]:
   "\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)"
   unfolding empty_fail_def
   apply clarsimp
   apply (drule mres_bind_empty)
   apply (erule context_disjE)
-   apply (fastforce intro: bind_FailedI1)
-  apply (fastforce intro!: bind_FailedI2)
+   apply (fastforce intro: bind_failedI1)
+  apply (fastforce intro!: bind_failedI2)
   done
 
 lemma empty_fail_return[empty_fail_term]:
@@ -189,7 +189,7 @@ lemma empty_fail_assert_opt[empty_fail_term]:
 
 lemma empty_fail_mk_ef[empty_fail_term]:
   "empty_fail (mk_ef o m)"
-  by (simp add: empty_fail_def mk_ef_def)
+  by (simp add: empty_fail_def mk_ef_def failed_def)
 
 lemma empty_fail_gets_the[empty_fail_term]:
   "empty_fail (gets_the f)"
@@ -224,7 +224,7 @@ lemma empty_fail_guard[empty_fail_term]:
 
 lemma empty_fail_spec[empty_fail_term]:
   "empty_fail (state_select F)"
-  by (clarsimp simp: state_select_def empty_fail_def default_elem_def mres_def image_def)
+  by (clarsimp simp: state_select_def empty_fail_def default_elem_def mres_def image_def failed_def)
 
 lemma empty_fail_when[empty_fail_cond]:
   "(P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (when P x)"
@@ -333,6 +333,31 @@ lemma empty_fail_notM[empty_fail_cond]:
   "empty_fail A \<Longrightarrow> empty_fail (notM A)"
   by (simp add: notM_def empty_fail_term empty_fail_cond)
 
+lemma empty_fail_put_trace_elem[empty_fail_term]:
+  "empty_fail (put_trace_elem x)"
+  by (clarsimp simp: put_trace_elem_def empty_fail_def mres_def vimage_def)
+
+lemma empty_fail_put_trace[empty_fail_term]:
+  "empty_fail (put_trace xs)"
+  apply (induct xs)
+   apply (clarsimp simp: empty_fail_term)
+  apply (clarsimp simp: empty_fail_term empty_fail_cond)
+  done
+
+lemma empty_fail_interference[empty_fail_term]:
+  "empty_fail interference"
+  by (simp add: interference_def commit_step_def env_steps_def empty_fail_term empty_fail_cond)
+
+lemma last_st_tr_not_empty:
+  "P s \<Longrightarrow> \<exists>xs. P (last_st_tr (map (Pair Env) xs) s')"
+  apply (rule exI[where x="[s]"])
+  apply (auto simp: last_st_tr_def)
+  done
+
+lemma empty_fail_Await[empty_fail_term]:
+  "\<exists>s. c s \<Longrightarrow> empty_fail (Await c)"
+  by (clarsimp simp: Await_def last_st_tr_not_empty empty_fail_term empty_fail_cond)
+
 (* not everything [simp] by default, because side conditions can slow down simp a lot *)
 lemmas empty_fail[wp, intro!] = empty_fail_term empty_fail_cond
 lemmas [simp] = empty_fail_term

lib/Monads/trace/Trace_Monad.thy

@@ -44,7 +44,6 @@ text \<open>
   pair of result and state when the computation did not fail.\<close>
 type_synonym ('s, 'a) tmonad = "'s \<Rightarrow> ((tmid \<times> 's) list \<times> ('s, 'a) tmres) set"
 
-
 text \<open>
   Print the type @{typ "('s,'a) tmonad"} instead of its unwieldy expansion.
   Needs an AST translation in code, because it needs to check that the state variable
@@ -68,6 +67,17 @@ text \<open>Returns monad results, ignoring failures and traces.\<close>
 definition mres :: "((tmid \<times> 's) list \<times> ('s, 'a) tmres) set \<Rightarrow> ('a \<times> 's) set" where
   "mres r = Result -` (snd ` r)"
 
+text \<open>True if the monad has a computation resulting in Failed.\<close>
+definition failed :: "((tmid \<times> 's) list \<times> ('s, 'a) tmres) set \<Rightarrow> bool" where
+  "failed r \<equiv> Failed \<in> snd ` r"
+
+lemma failed_simps[simp]:
+  "failed {(x, y)} = (y = Failed)"
+  "failed (r \<union> r') = (failed r \<or> failed r')"
+  "\<not> failed {}"
+  by (auto simp: failed_def)
+
+
 text \<open>
   The definition of fundamental monad functions @{text return} and
   @{text bind}. The monad function @{text "return x"} does not change

lib/Monads/trace/Trace_No_Fail.thy

@@ -22,7 +22,7 @@ text \<open>
   state that satisfies the precondition it returns a @{term Failed} result.
 \<close>
 definition no_fail :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> bool" where
-  "no_fail P m \<equiv> \<forall>s. P s \<longrightarrow> Failed \<notin> snd ` (m s)"
+  "no_fail P m \<equiv> \<forall>s. P s \<longrightarrow> \<not> failed (m s)"
 
 
 subsection \<open>@{method wpc} setup\<close>
@@ -51,42 +51,52 @@ bundle classic_wp_pre =
 subsection \<open>Lemmas\<close>
 
 lemma no_failD:
-  "\<lbrakk> no_fail P m; P s \<rbrakk> \<Longrightarrow> Failed \<notin> snd ` m s"
+  "\<lbrakk> no_fail P m; P s \<rbrakk> \<Longrightarrow> \<not> failed (m s)"
   by (simp add: no_fail_def)
 
+lemma no_fail_return[simp, wp]:
+  "no_fail \<top> (return x)"
+  by (simp add: return_def no_fail_def)
+
+lemma no_fail_bind[wp]:
+  "\<lbrakk> no_fail P f; \<And>x. no_fail (R x) (g x); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
+  apply (simp add: no_fail_def bind_def' image_Un image_image
+                   in_image_constant failed_def)
+  apply (intro allI conjI impI)
+   apply (fastforce simp: image_def)
+  apply clarsimp
+  apply (drule(1) post_by_hoare, erule in_mres)
+  apply (fastforce simp: image_def)
+  done
+
+lemma no_fail_get[simp, wp]:
+  "no_fail \<top> get"
+  by (simp add: get_def no_fail_def)
+
+lemma no_fail_put[simp, wp]:
+  "no_fail \<top> (put s)"
+  by (simp add: put_def no_fail_def)
+
 lemma no_fail_modify[wp,simp]:
   "no_fail \<top> (modify f)"
-  by (simp add: no_fail_def modify_def get_def put_def bind_def)
+  by (wpsimp simp: modify_def)
 
 lemma no_fail_gets_simp[simp]:
   "no_fail P (gets f)"
-  unfolding no_fail_def gets_def get_def return_def bind_def
-  by simp
+  by (wpsimp simp: gets_def)
 
 lemma no_fail_gets[wp]:
   "no_fail \<top> (gets f)"
   by simp
 
-lemma no_fail_select[simp]:
+lemma no_fail_select[wp,simp]:
   "no_fail \<top> (select S)"
-  by (simp add: no_fail_def select_def image_def)
+  by (simp add: no_fail_def select_def image_def failed_def)
 
 lemma no_fail_alt[wp]:
   "\<lbrakk> no_fail P f; no_fail Q g \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f \<sqinter> g)"
   by (auto simp: no_fail_def alternative_def)
 
-lemma no_fail_return[simp, wp]:
-  "no_fail \<top> (return x)"
-  by (simp add: return_def no_fail_def)
-
-lemma no_fail_get[simp, wp]:
-  "no_fail \<top> get"
-  by (simp add: get_def no_fail_def)
-
-lemma no_fail_put[simp, wp]:
-  "no_fail \<top> (put s)"
-  by (simp add: put_def no_fail_def)
-
 lemma no_fail_when[wp]:
   "(P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then Q else \<top>) (when P f)"
   by (simp add: when_def)
@@ -129,17 +139,6 @@ lemma no_fail_returnOK[simp, wp]:
   "no_fail \<top> (returnOk x)"
   by (simp add: returnOk_def)
 
-lemma no_fail_bind[wp]:
-  "\<lbrakk> no_fail P f; \<And>x. no_fail (R x) (g x); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
-  apply (simp add: no_fail_def bind_def' image_Un image_image
-                   in_image_constant)
-  apply (intro allI conjI impI)
-   apply (fastforce simp: image_def)
-  apply clarsimp
-  apply (drule(1) post_by_hoare, erule in_mres)
-  apply (fastforce simp: image_def)
-  done
-
 lemma no_fail_assume_pre:
   "(\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f"
   by (simp add: no_fail_def)
@@ -223,9 +222,41 @@ lemma no_fail_state_assert[wp]:
   unfolding state_assert_def
   by wpsimp
 
-lemma no_fail_condition:
+lemma no_fail_condition[wp]:
   "\<lbrakk>no_fail Q A; no_fail R B\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s)) (condition C A B)"
   unfolding condition_def no_fail_def
   by clarsimp
 
+lemma no_fail_ex_lift:
+  "(\<And>x. no_fail (P x) f) \<Longrightarrow> no_fail (\<lambda>s. \<exists>x. P x s) f"
+  by (fastforce simp: no_fail_def)
+
+lemma no_fail_grab_asm:
+  "(G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. G \<and> P s) f"
+  by (cases G; clarsimp)
+
+lemma no_fail_put_trace_elem[wp]:
+  "no_fail \<top> (put_trace_elem x)"
+  by (clarsimp simp: put_trace_elem_def no_fail_def failed_def)
+
+lemma no_fail_put_trace[wp]:
+  "no_fail \<top> (put_trace xs)"
+  by (induct xs; wpsimp)
+
+lemma no_fail_interference[wp]:
+  "no_fail \<top> interference"
+  by (wpsimp simp: interference_def commit_step_def env_steps_def)
+
+lemma no_fail_Await[wp]:
+  "\<exists>s. c s \<Longrightarrow> no_fail \<top> (Await c)"
+  by (wpsimp simp: Await_def)
+
+lemma parallel_failed:
+  "failed (parallel f g s) \<Longrightarrow> failed (f s) \<and> failed (g s)"
+  by (auto simp: parallel_def2 failed_def image_def intro!: bexI)
+
+lemma no_fail_parallel[wp]:
+  "\<lbrakk> no_fail P f \<or> no_fail Q g \<rbrakk> \<Longrightarrow> no_fail (P and Q) (parallel f g)"
+  by (auto simp: no_fail_def dest!: parallel_failed)
+
 end