diff options
Diffstat (limited to 'lib/isabelle/manual/Manual.thy')
| -rw-r--r-- | lib/isabelle/manual/Manual.thy | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy index 51591531..0c83ebea 100644 --- a/lib/isabelle/manual/Manual.thy +++ b/lib/isabelle/manual/Manual.thy @@ -412,7 +412,9 @@ case, defined as @{thm [display, names_short] PrePostE_def} The theory includes standard proof rules for both of these variants, in particular rules giving weakest preconditions of the predefined primitives of the monad, collected under the names -@{attribute PrePost_intro} and @{attribute PrePostE_intro}, respectively. +@{attribute PrePost_atomI} for atoms such as @{term return} and @{attribute PrePost_compositeI} +for composites such as @{term bind} (or @{attribute PrePostE_atomI} and +@{attribute PrePostE_compositeI}, respectively, for the quadruple variant). The instruction we are considering is defined as @{thm [display] execute_ITYPE.simps[of _ rs for rs]} @@ -448,16 +450,17 @@ lemma shows "PrePostE pre (liftS instr) post (\<lambda>_ _. False)" unfolding pre_def instr_def post_def - by (simp add: rX_def wX_def cong: bindS_cong if_cong split del: if_split) - (rule PrePostE_strengthen_pre, (rule PrePostE_intro)+, auto simp: uint_0_iff) + by (simp add: rX_def wX_def liftState_simp cong: bindS_cong if_cong split del: if_split) + (rule PrePostE_strengthen_pre, (rule PrePostE_atomI PrePostE_compositeI)+, auto simp: uint_0_iff) text \<open>The proof begins with a simplification step, which not only unfolds the definitions of the auxiliary functions @{term rX} and @{term wX}, but also performs the lifting from the free monad to the state monad. We apply the rule @{thm [source] PrePostE_strengthen_pre} (in a -backward manner) to allow a weaker precondition, then use the rules in @{attribute PrePostE_intro} -to derive a weakest precondition, and then use @{method auto} to show that it is implied by -the given precondition. For more serious proofs, one will want to set up specialised proof -tactics. This example uses only basic proof methods, to make the reasoning steps more explicit.\<close> +backward manner) to allow a weaker precondition, then use the rules in +@{attribute PrePostE_compositeI} and @{attribute PrePostE_atomI} to derive a weakest precondition, +and then use @{method auto} to show that it is implied by the given precondition. For more serious +proofs, one will want to set up specialised proof tactics. This example uses only basic proof +methods, to make the reasoning steps more explicit.\<close> (*<*) end |