diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Hoare.thy | 4 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 3 |
2 files changed, 5 insertions, 2 deletions
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index afa953be..88807c7c 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -13,7 +13,7 @@ subsection \<open>Hoare triples\<close> type_synonym 'regs predS = "'regs sequential_state \<Rightarrow> bool" -definition PrePost :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> (('a, 'e) result \<Rightarrow> 'regs predS) \<Rightarrow> bool" +definition PrePost :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> (('a, 'e) result \<Rightarrow> 'regs predS) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<lbrace>_\<rbrace>") where "PrePost P f Q \<equiv> (\<forall>s. P s \<longrightarrow> (\<forall>(r, s') \<in> f s. Q r s'))" lemma PrePostI: @@ -211,7 +211,7 @@ there is an exception. [1] D. Cock, G. Klein, and T. Sewell, ‘Secure Microkernels, State Monads and Scalable Refinement’, in Theorem Proving in Higher Order Logics, 2008, pp. 167–182.\<close> -definition PrePostE :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> ('a \<Rightarrow> 'regs predS) \<Rightarrow> ('e ex \<Rightarrow> 'regs predS) \<Rightarrow> bool" +definition PrePostE :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> ('a \<Rightarrow> 'regs predS) \<Rightarrow> ('e ex \<Rightarrow> 'regs predS) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<lbrace>_ \<bar> _\<rbrace>") where "PrePostE P f Q E \<equiv> PrePost P f (\<lambda>v. case v of Value a \<Rightarrow> Q a | Ex e \<Rightarrow> E e)" lemmas PrePost_defs = PrePost_def PrePostE_def diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index 91e4c17e..3a286c10 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -8,6 +8,9 @@ begin notes returnS_def[simp] and failS_def[simp] and throwS_def[simp] and readS_def[simp] and updateS_def[simp] begin*) +notation bindS (infixr "\<bind>\<^sub>S" 54) +notation seqS (infixr "\<then>\<^sub>S" 54) + lemma bindS_ext_cong[fundef_cong]: assumes m: "m1 s = m2 s" and f: "\<And>a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" |