Commit 37ae9abd authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

trival

parent b41e4757c02f
......@@ -318,7 +318,7 @@ definition
subsubsection \<open>Properties\<close>
text \<open>Here we present some trival properties of {\em mean} and {\em gmean}.\<close>
text \<open>Here we present some trivial properties of {\em mean} and {\em gmean}.\<close>
lemma list_sum_mean:
fixes xs::"real list"
......
......@@ -746,7 +746,7 @@ lemma hbexE [elim!]: "\<exists>x\<^bold>\<in>A. P x \<Longrightarrow> (\<And>x.
by (unfold HBex_def) blast
lemma hball_triv [simp]: "(\<forall>x\<^bold>\<in>A. P) = ((\<exists>x. x\<^bold>\<in>A) \<longrightarrow> P)"
\<comment> \<open>Trival rewrite rule.\<close>
\<comment> \<open>trivial rewrite rule.\<close>
by (simp add: HBall_def)
lemma hbex_triv [simp]: "(\<exists>x\<^bold>\<in>A. P) = ((\<exists>x. x\<^bold>\<in>A) \<and> P)"
......
......@@ -176,7 +176,7 @@ proof -
thus ?thesis
using assms unfolding cong_def
using int_mod_pos_eq large_mod_0 zless_imp_add1_zle
by (metis abs_of_nonneg le_less not_less zabs_less_one_iff zmod_trival_iff)
by (metis abs_of_nonneg le_less not_less zabs_less_one_iff zmod_trivial_iff)
qed
(* an intro version of sum_list_0 *)
......
......@@ -936,7 +936,7 @@ Moreover, the coupling relation as well as the invariants become trivial for a i
\end{enumerate}
Step \ref{sim:sb-sbh} is trivial since the bookkeeping within the additional ghost and history state does not affect the control flow of the transition systems and can be easily removed. Similar the additional @{term \<R>} ghost component can be ignored in Step \ref{sim:delayed-free-flowing}. However, to apply Theorem \ref{thm:simulation} in Step \ref{sim:sbh-delayed} we have to convert from @{term [names_short] "safe_reach_virtual_free_flowing (ts, m, \<S>)"} provided by the preconditions of Theorem \ref{thm:reduction} to the required @{term [names_short] "safe_reach_direct_delayed (ts, m, \<S>)"}. This argument is more involved and we only give a short sketch here.
The other direction is trival as every single case for delayed releases (cf. Figure \ref{fig:safe-delayed}) immediately implies the corresponding case for free flowing releases (cf. Figure \ref{fig:safe-virtual-memory}).
The other direction is trivial as every single case for delayed releases (cf. Figure \ref{fig:safe-delayed}) immediately implies the corresponding case for free flowing releases (cf. Figure \ref{fig:safe-virtual-memory}).
First keep in mind that the predicates ensure that \emph{all} reachable configurations starting from @{term "(ts,m,\<S>)"} are safe, according to the rules for free flowing releases or delayed releases respectively. We show the theorem by contraposition and start with a computation which reaches a configuration @{term c} that is unsafe according to the rules for delayed releases and want to show that there has to be a (potentially other) computation (starting from the same initial state) that leads to an unsafe configuration @{term c'} accroding to free flowing releases.
If @{term c} is already unsafe according to free flowing releases we have @{term "c'=c"} and are finished.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment