lib/monads: improve style of nondet and trace
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis
Corey Lewis
parent
293b97cb17
commit
3333395cc3
|
|
@ -277,7 +277,8 @@ lemma monad_state_eqI [intro]:
|
|||
subsection \<open>General @{const whileLoop} reasoning\<close>
|
||||
|
||||
definition whileLoop_terminatesE ::
|
||||
"('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('s, 'e + 'a) nondet_monad) \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" where
|
||||
"('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('s, 'e + 'a) nondet_monad) \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
|
||||
where
|
||||
"whileLoop_terminatesE C B \<equiv>
|
||||
\<lambda>r. whileLoop_terminates (\<lambda>r s. case r of Inr v \<Rightarrow> C v s | _ \<Rightarrow> False) (lift B) (Inr r)"
|
||||
|
||||
|
|
|
|||
|
|
@ -71,16 +71,15 @@ text \<open>
|
|||
operation may have failed, if @{text f} may have failed or @{text g} may
|
||||
have failed on any of the results of @{text f}.\<close>
|
||||
definition bind ::
|
||||
"('s, 'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> ('s, 'b) nondet_monad) \<Rightarrow> ('s, 'b) nondet_monad"
|
||||
(infixl ">>=" 60) where
|
||||
"('s, 'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> ('s, 'b) nondet_monad) \<Rightarrow> ('s, 'b) nondet_monad" (infixl ">>=" 60)
|
||||
where
|
||||
"bind f g \<equiv> \<lambda>s. (\<Union>(fst ` case_prod g ` fst (f s)),
|
||||
True \<in> snd ` case_prod g ` fst (f s) \<or> snd (f s))"
|
||||
|
||||
text \<open>
|
||||
Sometimes it is convenient to write @{text bind} in reverse order.\<close>
|
||||
text \<open>Sometimes it is convenient to write @{text bind} in reverse order.\<close>
|
||||
abbreviation (input) bind_rev ::
|
||||
"('c \<Rightarrow> ('a, 'b) nondet_monad) \<Rightarrow> ('a, 'c) nondet_monad \<Rightarrow> ('a, 'b) nondet_monad"
|
||||
(infixl "=<<" 60) where
|
||||
"('c \<Rightarrow> ('a, 'b) nondet_monad) \<Rightarrow> ('a, 'c) nondet_monad \<Rightarrow> ('a, 'b) nondet_monad" (infixl "=<<" 60)
|
||||
where
|
||||
"g =<< f \<equiv> f >>= g"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -107,7 +106,8 @@ definition select :: "'a set \<Rightarrow> ('s,'a) nondet_monad" where
|
|||
"select A \<equiv> \<lambda>s. (A \<times> {s}, False)"
|
||||
|
||||
definition alternative ::
|
||||
"('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad" (infixl "\<sqinter>" 20) where
|
||||
"('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad" (infixl "\<sqinter>" 20)
|
||||
where
|
||||
"f \<sqinter> g \<equiv> \<lambda>s. (fst (f s) \<union> fst (g s), snd (f s) \<or> snd (g s))"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -125,20 +125,21 @@ text \<open>
|
|||
definition state_select :: "('s \<times> 's) set \<Rightarrow> ('s, unit) nondet_monad" where
|
||||
"state_select r \<equiv> \<lambda>s. ((\<lambda>x. ((), x)) ` {s'. (s, s') \<in> r}, \<not> (\<exists>s'. (s, s') \<in> r))"
|
||||
|
||||
|
||||
subsection "Failure"
|
||||
|
||||
text \<open>
|
||||
The monad function that always fails. Returns an empty set of results and sets the failure flag.\<close>
|
||||
definition fail :: "('s, 'a) nondet_monad" where
|
||||
"fail \<equiv> \<lambda>s. ({}, True)"
|
||||
"fail \<equiv> \<lambda>s. ({}, True)"
|
||||
|
||||
text \<open>Assertions: fail if the property @{text P} is not true\<close>
|
||||
definition assert :: "bool \<Rightarrow> ('a, unit) nondet_monad" where
|
||||
"assert P \<equiv> if P then return () else fail"
|
||||
"assert P \<equiv> if P then return () else fail"
|
||||
|
||||
text \<open>Fail if the value is @{const None}, return result @{text v} for @{term "Some v"}\<close>
|
||||
definition assert_opt :: "'a option \<Rightarrow> ('b, 'a) nondet_monad" where
|
||||
"assert_opt v \<equiv> case v of None \<Rightarrow> fail | Some v \<Rightarrow> return v"
|
||||
"assert_opt v \<equiv> case v of None \<Rightarrow> fail | Some v \<Rightarrow> return v"
|
||||
|
||||
text \<open>An assertion that also can introspect the current state.\<close>
|
||||
definition state_assert :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, unit) nondet_monad" where
|
||||
|
|
@ -148,11 +149,11 @@ subsection "Generic functions on top of the state monad"
|
|||
|
||||
text \<open>Apply a function to the current state and return the result without changing the state.\<close>
|
||||
definition gets :: "('s \<Rightarrow> 'a) \<Rightarrow> ('s, 'a) nondet_monad" where
|
||||
"gets f \<equiv> get >>= (\<lambda>s. return (f s))"
|
||||
"gets f \<equiv> get >>= (\<lambda>s. return (f s))"
|
||||
|
||||
text \<open>Modify the current state using the function passed in.\<close>
|
||||
definition modify :: "('s \<Rightarrow> 's) \<Rightarrow> ('s, unit) nondet_monad" where
|
||||
"modify f \<equiv> get >>= (\<lambda>s. put (f s))"
|
||||
"modify f \<equiv> get >>= (\<lambda>s. put (f s))"
|
||||
|
||||
lemma simpler_gets_def:
|
||||
"gets f = (\<lambda>s. ({(f s, s)}, False))"
|
||||
|
|
@ -174,7 +175,8 @@ text \<open>
|
|||
Perform a test on the current state, performing the left monad if
|
||||
the result is true or the right monad if the result is false. \<close>
|
||||
definition condition ::
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s, 'r) nondet_monad \<Rightarrow> ('s, 'r) nondet_monad \<Rightarrow> ('s, 'r) nondet_monad" where
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s, 'r) nondet_monad \<Rightarrow> ('s, 'r) nondet_monad \<Rightarrow> ('s, 'r) nondet_monad"
|
||||
where
|
||||
"condition P L R \<equiv> \<lambda>s. if (P s) then (L s) else (R s)"
|
||||
|
||||
notation (output)
|
||||
|
|
@ -189,14 +191,13 @@ definition gets_the :: "('s \<Rightarrow> 'a option) \<Rightarrow> ('s, 'a) nond
|
|||
text \<open>
|
||||
Get a map (such as a heap) from the current state and apply an argument to the map.
|
||||
Fail if the map returns @{const None}, otherwise return the value.\<close>
|
||||
definition
|
||||
gets_map :: "('s \<Rightarrow> 'a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> ('s, 'b) nondet_monad" where
|
||||
definition gets_map :: "('s \<Rightarrow> 'a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> ('s, 'b) nondet_monad" where
|
||||
"gets_map f p \<equiv> gets f >>= (\<lambda>m. assert_opt (m p))"
|
||||
|
||||
|
||||
subsection \<open>The Monad Laws\<close>
|
||||
|
||||
text \<open>A more expanded definition of @{text bind}\<close>
|
||||
text \<open>An alternative definition of @{term bind}, sometimes more convenient.\<close>
|
||||
lemma bind_def':
|
||||
"(f >>= g) \<equiv>
|
||||
\<lambda>s. ({(r'', s''). \<exists>(r', s') \<in> fst (f s). (r'', s'') \<in> fst (g r' s') },
|
||||
|
|
@ -212,7 +213,8 @@ lemma return_bind[simp]:
|
|||
by (simp add: return_def bind_def)
|
||||
|
||||
text \<open>@{term return} is absorbed on the right of a @{term bind}\<close>
|
||||
lemma bind_return[simp]: "(m >>= return) = m"
|
||||
lemma bind_return[simp]:
|
||||
"(m >>= return) = m"
|
||||
by (simp add: bind_def return_def split_def)
|
||||
|
||||
text \<open>@{term bind} is associative\<close>
|
||||
|
|
@ -264,7 +266,6 @@ definition bindE ::
|
|||
(infixl ">>=E" 60) where
|
||||
"f >>=E g \<equiv> f >>= lift g"
|
||||
|
||||
|
||||
text \<open>
|
||||
Lifting a normal nondeterministic monad into the
|
||||
exception monad is achieved by always returning its
|
||||
|
|
@ -272,7 +273,6 @@ text \<open>
|
|||
definition liftE :: "('s,'a) nondet_monad \<Rightarrow> ('s, 'e+'a) nondet_monad" where
|
||||
"liftE f \<equiv> f >>= (\<lambda>r. return (Inr r))"
|
||||
|
||||
|
||||
text \<open>
|
||||
Since the underlying type and @{text return} function changed,
|
||||
we need new definitions for when and unless:\<close>
|
||||
|
|
@ -282,13 +282,11 @@ definition whenE :: "bool \<Rightarrow> ('s, 'e + unit) nondet_monad \<Rightarro
|
|||
definition unlessE :: "bool \<Rightarrow> ('s, 'e + unit) nondet_monad \<Rightarrow> ('s, 'e + unit) nondet_monad" where
|
||||
"unlessE P f \<equiv> if P then returnOk () else f"
|
||||
|
||||
|
||||
text \<open>
|
||||
Throwing an exception when the parameter is @{term None}, otherwise
|
||||
returning @{term "v"} for @{term "Some v"}.\<close>
|
||||
definition throw_opt :: "'e \<Rightarrow> 'a option \<Rightarrow> ('s, 'e + 'a) nondet_monad" where
|
||||
"throw_opt ex x \<equiv> case x of None \<Rightarrow> throwError ex | Some v \<Rightarrow> returnOk v"
|
||||
|
||||
"throw_opt ex x \<equiv> case x of None \<Rightarrow> throwError ex | Some v \<Rightarrow> returnOk v"
|
||||
|
||||
text \<open>
|
||||
Failure in the exception monad is redefined in the same way
|
||||
|
|
@ -297,6 +295,7 @@ text \<open>
|
|||
definition assertE :: "bool \<Rightarrow> ('a, 'e + unit) nondet_monad" where
|
||||
"assertE P \<equiv> if P then returnOk () else fail"
|
||||
|
||||
|
||||
subsection "Monad Laws for the Exception Monad"
|
||||
|
||||
text \<open>More direct definition of @{const liftE}:\<close>
|
||||
|
|
@ -415,9 +414,7 @@ lemma "doE x \<leftarrow> returnOk 1;
|
|||
by simp
|
||||
|
||||
|
||||
|
||||
section "Library of Monadic Functions and Combinators"
|
||||
|
||||
section "Library of additional Monadic Functions and Combinators"
|
||||
|
||||
text \<open>Lifting a normal function into the monad type:\<close>
|
||||
definition liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('s, 'b) nondet_monad" where
|
||||
|
|
@ -427,12 +424,11 @@ text \<open>The same for the exception monad:\<close>
|
|||
definition liftME :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'e+'a) nondet_monad \<Rightarrow> ('s,'e+'b) nondet_monad" where
|
||||
"liftME f m \<equiv> doE x \<leftarrow> m; returnOk (f x) odE"
|
||||
|
||||
text \<open> Execute @{term f} for @{term "Some x"}, otherwise do nothing. \<close>
|
||||
text \<open>Execute @{term f} for @{term "Some x"}, otherwise do nothing.\<close>
|
||||
definition maybeM :: "('a \<Rightarrow> ('s, unit) nondet_monad) \<Rightarrow> 'a option \<Rightarrow> ('s, unit) nondet_monad" where
|
||||
"maybeM f y \<equiv> case y of Some x \<Rightarrow> f x | None \<Rightarrow> return ()"
|
||||
|
||||
text \<open>
|
||||
Run a sequence of monads from left to right, ignoring return values.\<close>
|
||||
text \<open>Run a sequence of monads from left to right, ignoring return values.\<close>
|
||||
definition sequence_x :: "('s, 'a) nondet_monad list \<Rightarrow> ('s, unit) nondet_monad" where
|
||||
"sequence_x xs \<equiv> foldr (\<lambda>x y. x >>= (\<lambda>_. y)) xs (return ())"
|
||||
|
||||
|
|
@ -447,10 +443,10 @@ text \<open>
|
|||
going through both lists simultaneously, left to right, ignoring
|
||||
return values.\<close>
|
||||
definition zipWithM_x ::
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, unit) nondet_monad" where
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, unit) nondet_monad"
|
||||
where
|
||||
"zipWithM_x f xs ys \<equiv> sequence_x (zipWith f xs ys)"
|
||||
|
||||
|
||||
text \<open>
|
||||
The same three functions as above, but returning a list of
|
||||
return values instead of @{text unit}\<close>
|
||||
|
|
@ -462,15 +458,18 @@ definition mapM :: "('a \<Rightarrow> ('s,'b) nondet_monad) \<Rightarrow> 'a lis
|
|||
"mapM f xs \<equiv> sequence (map f xs)"
|
||||
|
||||
definition zipWithM ::
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, 'c list) nondet_monad" where
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, 'c list) nondet_monad"
|
||||
where
|
||||
"zipWithM f xs ys \<equiv> sequence (zipWith f xs ys)"
|
||||
|
||||
definition foldM :: "('b \<Rightarrow> 'a \<Rightarrow> ('s, 'a) nondet_monad) \<Rightarrow> 'b list \<Rightarrow> 'a \<Rightarrow> ('s, 'a) nondet_monad"
|
||||
definition foldM ::
|
||||
"('b \<Rightarrow> 'a \<Rightarrow> ('s, 'a) nondet_monad) \<Rightarrow> 'b list \<Rightarrow> 'a \<Rightarrow> ('s, 'a) nondet_monad"
|
||||
where
|
||||
"foldM m xs a \<equiv> foldr (\<lambda>p q. q >>= m p) xs (return a) "
|
||||
|
||||
definition foldME ::
|
||||
"('b \<Rightarrow> 'a \<Rightarrow> ('s,('e + 'b)) nondet_monad) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> ('s, ('e + 'b)) nondet_monad" where
|
||||
"('b \<Rightarrow> 'a \<Rightarrow> ('s,('e + 'b)) nondet_monad) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> ('s, ('e + 'b)) nondet_monad"
|
||||
where
|
||||
"foldME m a xs \<equiv> foldr (\<lambda>p q. q >>=E swp m p) xs (returnOk a)"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -486,11 +485,11 @@ definition sequenceE :: "('s, 'e+'a) nondet_monad list \<Rightarrow> ('s, 'e+'a
|
|||
"sequenceE xs \<equiv> let mcons = (\<lambda>p q. p >>=E (\<lambda>x. q >>=E (\<lambda>y. returnOk (x#y))))
|
||||
in foldr mcons xs (returnOk [])"
|
||||
|
||||
definition mapME :: "('a \<Rightarrow> ('s,'e+'b) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> ('s,'e+'b list) nondet_monad"
|
||||
definition mapME ::
|
||||
"('a \<Rightarrow> ('s,'e+'b) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> ('s,'e+'b list) nondet_monad"
|
||||
where
|
||||
"mapME f xs \<equiv> sequenceE (map f xs)"
|
||||
|
||||
|
||||
text \<open>Filtering a list using a monadic function as predicate:\<close>
|
||||
primrec filterM :: "('a \<Rightarrow> ('s, bool) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> ('s, 'a list) nondet_monad" where
|
||||
"filterM P [] = return []"
|
||||
|
|
@ -536,8 +535,7 @@ text \<open>
|
|||
The handler may throw a type of exceptions different from
|
||||
the left side.\<close>
|
||||
definition handleE' ::
|
||||
"('s, 'e1 + 'a) nondet_monad \<Rightarrow> ('e1 \<Rightarrow> ('s, 'e2 + 'a) nondet_monad) \<Rightarrow>
|
||||
('s, 'e2 + 'a) nondet_monad"
|
||||
"('s, 'e1 + 'a) nondet_monad \<Rightarrow> ('e1 \<Rightarrow> ('s, 'e2 + 'a) nondet_monad) \<Rightarrow> ('s, 'e2 + 'a) nondet_monad"
|
||||
(infix "<handle2>" 10) where
|
||||
"f <handle2> handler \<equiv>
|
||||
do
|
||||
|
|
@ -556,15 +554,13 @@ definition handleE ::
|
|||
(infix "<handle>" 10) where
|
||||
"handleE \<equiv> handleE'"
|
||||
|
||||
|
||||
text \<open>
|
||||
Handling exceptions, and additionally providing a continuation
|
||||
if the left-hand side throws no exception:\<close>
|
||||
definition
|
||||
handle_elseE ::
|
||||
definition handle_elseE ::
|
||||
"('s, 'e + 'a) nondet_monad \<Rightarrow> ('e \<Rightarrow> ('s, 'ee + 'b) nondet_monad) \<Rightarrow>
|
||||
('a \<Rightarrow> ('s, 'ee + 'b) nondet_monad) \<Rightarrow> ('s, 'ee + 'b) nondet_monad"
|
||||
("_ <handle> _ <else> _" 10) where
|
||||
('a \<Rightarrow> ('s, 'ee + 'b) nondet_monad) \<Rightarrow> ('s, 'ee + 'b) nondet_monad" ("_ <handle> _ <else> _" 10)
|
||||
where
|
||||
"f <handle> handler <else> continue \<equiv>
|
||||
do v \<leftarrow> f;
|
||||
case v of Inl e \<Rightarrow> handler e
|
||||
|
|
@ -593,7 +589,8 @@ inductive_simps whileLoop_results_simps_valid: "(Some x, Some y) \<in> whileLoop
|
|||
inductive_simps whileLoop_results_simps_start_fail[simp]: "(None, x) \<in> whileLoop_results C B"
|
||||
|
||||
inductive whileLoop_terminates ::
|
||||
"('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) nondet_monad) \<Rightarrow> 'r \<Rightarrow> 's \<Rightarrow> bool" for C B where
|
||||
"('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) nondet_monad) \<Rightarrow> 'r \<Rightarrow> 's \<Rightarrow> bool"
|
||||
for C B where
|
||||
"\<not> C r s \<Longrightarrow> whileLoop_terminates C B r s"
|
||||
| "\<lbrakk> C r s; \<forall>(r', s') \<in> fst (B r s). whileLoop_terminates C B r' s' \<rbrakk>
|
||||
\<Longrightarrow> whileLoop_terminates C B r s"
|
||||
|
|
@ -602,7 +599,8 @@ inductive_cases whileLoop_terminates_cases: "whileLoop_terminates C B r s"
|
|||
inductive_simps whileLoop_terminates_simps: "whileLoop_terminates C B r s"
|
||||
|
||||
definition whileLoop ::
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b, 'a) nondet_monad) \<Rightarrow> 'a \<Rightarrow> ('b, 'a) nondet_monad" where
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b, 'a) nondet_monad) \<Rightarrow> 'a \<Rightarrow> ('b, 'a) nondet_monad"
|
||||
where
|
||||
"whileLoop C B \<equiv> \<lambda>r s.
|
||||
({(r',s'). (Some (r, s), Some (r', s')) \<in> whileLoop_results C B},
|
||||
(Some (r, s), None) \<in> whileLoop_results C B \<or> \<not>whileLoop_terminates C B r s)"
|
||||
|
|
@ -626,7 +624,8 @@ definition notM :: "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_mona
|
|||
"notM m = do c \<leftarrow> m; return (\<not> c) od"
|
||||
|
||||
definition whileM ::
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, unit) nondet_monad" where
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, unit) nondet_monad"
|
||||
where
|
||||
"whileM C B \<equiv> do
|
||||
c \<leftarrow> C;
|
||||
whileLoop (\<lambda>c s. c) (\<lambda>_. do B; C od) c;
|
||||
|
|
@ -634,8 +633,8 @@ definition whileM ::
|
|||
od"
|
||||
|
||||
definition ifM ::
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow>
|
||||
('s, 'a) nondet_monad" where
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad"
|
||||
where
|
||||
"ifM test t f = do
|
||||
c \<leftarrow> test;
|
||||
if c then t else f
|
||||
|
|
@ -643,22 +642,26 @@ definition ifM ::
|
|||
|
||||
definition ifME ::
|
||||
"('a, 'b + bool) nondet_monad \<Rightarrow> ('a, 'b + 'c) nondet_monad \<Rightarrow> ('a, 'b + 'c) nondet_monad
|
||||
\<Rightarrow> ('a, 'b + 'c) nondet_monad" where
|
||||
\<Rightarrow> ('a, 'b + 'c) nondet_monad"
|
||||
where
|
||||
"ifME test t f = doE
|
||||
c \<leftarrow> test;
|
||||
if c then t else f
|
||||
odE"
|
||||
|
||||
definition whenM ::
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, unit) nondet_monad \<Rightarrow> ('s, unit) nondet_monad" where
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, unit) nondet_monad \<Rightarrow> ('s, unit) nondet_monad"
|
||||
where
|
||||
"whenM t m = ifM t m (return ())"
|
||||
|
||||
definition orM ::
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad"
|
||||
where
|
||||
"orM a b = ifM a (return True) b"
|
||||
|
||||
definition andM ::
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
|
||||
"('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad"
|
||||
where
|
||||
"andM a b = ifM a b (return False)"
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -160,7 +160,7 @@ lemma no_fail_spec:
|
|||
|
||||
lemma no_fail_assertE[wp]:
|
||||
"no_fail (\<lambda>_. P) (assertE P)"
|
||||
by (simp add: assertE_def split: if_split)
|
||||
by (simp add: assertE_def)
|
||||
|
||||
lemma no_fail_spec_pre:
|
||||
"\<lbrakk> no_fail (((=) s) and P') f; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> no_fail (((=) s) and P) f"
|
||||
|
|
@ -168,7 +168,7 @@ lemma no_fail_spec_pre:
|
|||
|
||||
lemma no_fail_whenE[wp]:
|
||||
"\<lbrakk> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. G \<longrightarrow> P s) (whenE G f)"
|
||||
by (simp add: whenE_def split: if_split)
|
||||
by (simp add: whenE_def)
|
||||
|
||||
lemma no_fail_unlessE[wp]:
|
||||
"\<lbrakk> \<not> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<not> G \<longrightarrow> P s) (unlessE G f)"
|
||||
|
|
|
|||
|
|
@ -17,7 +17,8 @@ text \<open>
|
|||
The dual to validity: an existential instead of a universal quantifier for the post condition.
|
||||
In refinement, it is often sufficient to know that there is one state that satisfies a condition.\<close>
|
||||
definition exs_valid ::
|
||||
"('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) nondet_monad \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>") where
|
||||
"('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) nondet_monad \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>") where
|
||||
"\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>(rv, s') \<in> fst (f s). Q rv s')"
|
||||
|
||||
text \<open>The above for the exception monad\<close>
|
||||
|
|
|
|||
|
|
@ -20,7 +20,8 @@ text \<open>
|
|||
is often similar. The following definitions allow such reasoning to take place.\<close>
|
||||
|
||||
definition validNF ::
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>!") where
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>!") where
|
||||
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! \<equiv> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<and> no_fail P f"
|
||||
|
||||
lemma validNF_alt_def:
|
||||
|
|
@ -304,7 +305,8 @@ lemma validNF_nobindE[wp]:
|
|||
text \<open>
|
||||
Set up triple rules for @{term validE_NF} so that we can use @{method wp} combinator rules.\<close>
|
||||
definition validE_NF_property ::
|
||||
"('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> ('s, 'c+'a) nondet_monad \<Rightarrow> bool" where
|
||||
"('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> ('s, 'c+'a) nondet_monad \<Rightarrow> bool"
|
||||
where
|
||||
"validE_NF_property Q E s b \<equiv>
|
||||
\<not> snd (b s) \<and> (\<forall>(r', s') \<in> fst (b s). case r' of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> Q x s')"
|
||||
|
||||
|
|
|
|||
|
|
@ -35,14 +35,16 @@ text \<open>
|
|||
to assume @{term P}! Proving non-failure is done via a separate predicate and
|
||||
calculus (see Nondet_No_Fail).\<close>
|
||||
definition valid ::
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>") where
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>") where
|
||||
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r,s') \<in> fst (f s). Q r s')"
|
||||
|
||||
text \<open>
|
||||
We often reason about invariant predicates. The following provides shorthand syntax
|
||||
that avoids repeating potentially long predicates.\<close>
|
||||
abbreviation (input) invariant ::
|
||||
"('s,'a) nondet_monad \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<lbrace>_\<rbrace>" [59,0] 60) where
|
||||
"('s,'a) nondet_monad \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
("_ \<lbrace>_\<rbrace>" [59,0] 60) where
|
||||
"invariant f P \<equiv> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -708,7 +710,7 @@ lemma hoare_vcg_if_lift:
|
|||
by (auto simp: valid_def split_def)
|
||||
|
||||
lemma hoare_vcg_disj_lift_R:
|
||||
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
|
||||
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
|
||||
assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
|
||||
shows "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>,-"
|
||||
using assms
|
||||
|
|
|
|||
|
|
@ -47,12 +47,14 @@ text \<open>
|
|||
\<close>
|
||||
definition whileLoop_inv ::
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b, 'a) nondet_monad) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow>
|
||||
(('a \<times> 'b) \<times> 'a \<times> 'b) set \<Rightarrow> ('b, 'a) nondet_monad" where
|
||||
(('a \<times> 'b) \<times> 'a \<times> 'b) set \<Rightarrow> ('b, 'a) nondet_monad"
|
||||
where
|
||||
"whileLoop_inv C B x I R \<equiv> whileLoop C B x"
|
||||
|
||||
definition whileLoopE_inv ::
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b, 'c + 'a) nondet_monad) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow>
|
||||
(('a \<times> 'b) \<times> 'a \<times> 'b) set \<Rightarrow> ('b, 'c + 'a) nondet_monad" where
|
||||
(('a \<times> 'b) \<times> 'a \<times> 'b) set \<Rightarrow> ('b, 'c + 'a) nondet_monad"
|
||||
where
|
||||
"whileLoopE_inv C B x I R \<equiv> whileLoopE C B x"
|
||||
|
||||
lemma whileLoop_add_inv:
|
||||
|
|
@ -287,7 +289,7 @@ lemma fst_whileLoop_cond_false:
|
|||
lemma snd_whileLoop:
|
||||
assumes init_I: "I r s"
|
||||
and cond_I: "C r s"
|
||||
and non_term: "\<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<rbrace> B r \<exists>\<lbrace> \<lambda>r' s'. C r' s' \<and> I r' s' \<rbrace>"
|
||||
and non_term: "\<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<rbrace> B r \<exists>\<lbrace> \<lambda>r' s'. C r' s' \<and> I r' s' \<rbrace>"
|
||||
shows "snd (whileLoop C B r s)"
|
||||
apply (clarsimp simp: whileLoop_def)
|
||||
apply (rotate_tac)
|
||||
|
|
|
|||
|
|
@ -38,14 +38,13 @@ datatype ('s, 'a) tmres = Failed | Incomplete | Result "('a \<times> 's)"
|
|||
abbreviation map_tmres_rv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s, 'a) tmres \<Rightarrow> ('s, 'b) tmres" where
|
||||
"map_tmres_rv f \<equiv> map_tmres id f"
|
||||
|
||||
section "The Monad"
|
||||
|
||||
text \<open>
|
||||
tmonad returns a set of non-deterministic computations, including
|
||||
a trace as a list of "thread identifier" \<times> state, and an optional
|
||||
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
|
||||
|
|
@ -64,6 +63,7 @@ print_ast_translation \<open>
|
|||
else raise Match
|
||||
in [(@{type_syntax "fun"}, tmonad_tr)] end\<close>
|
||||
|
||||
|
||||
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)"
|
||||
|
|
@ -98,7 +98,7 @@ definition bind ::
|
|||
| Result (rv, s) \<Rightarrow> fst_upd (\<lambda>ys. ys @ xs) ` g rv s"
|
||||
|
||||
text \<open>Sometimes it is convenient to write @{text bind} in reverse order.\<close>
|
||||
abbreviation(input) bind_rev ::
|
||||
abbreviation (input) bind_rev ::
|
||||
"('c \<Rightarrow> ('a, 'b) tmonad) \<Rightarrow> ('a, 'c) tmonad \<Rightarrow> ('a, 'b) tmonad" (infixl "=<<" 60)
|
||||
where
|
||||
"g =<< f \<equiv> f >>= g"
|
||||
|
|
@ -123,6 +123,7 @@ primrec put_trace :: "(tmid \<times> 's) list \<Rightarrow> ('s, unit) tmonad" w
|
|||
"put_trace [] = return ()"
|
||||
| "put_trace (x # xs) = (put_trace xs >>= (\<lambda>_. put_trace_elem x))"
|
||||
|
||||
|
||||
subsection "Nondeterminism"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -134,8 +135,9 @@ text \<open>
|
|||
definition select :: "'a set \<Rightarrow> ('s, 'a) tmonad" where
|
||||
"select A \<equiv> \<lambda>s. (Pair [] ` Result ` (A \<times> {s}))"
|
||||
|
||||
definition alternative :: "('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad"
|
||||
(infixl "\<sqinter>" 20) where
|
||||
definition alternative ::
|
||||
"('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad" (infixl "\<sqinter>" 20)
|
||||
where
|
||||
"f \<sqinter> g \<equiv> \<lambda>s. (f s \<union> g s)"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -153,6 +155,7 @@ definition state_select :: "('s \<times> 's) set \<Rightarrow> ('s, unit) tmonad
|
|||
"state_select r \<equiv>
|
||||
\<lambda>s. (Pair [] ` default_elem Failed (Result ` (\<lambda>x. ((), x)) ` {s'. (s, s') \<in> r}))"
|
||||
|
||||
|
||||
subsection "Failure"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -202,7 +205,8 @@ text \<open>
|
|||
Perform a test on the current state, performing the left monad if
|
||||
the result is true or the right monad if the result is false.\<close>
|
||||
definition condition ::
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s, 'r) tmonad \<Rightarrow> ('s, 'r) tmonad \<Rightarrow> ('s, 'r) tmonad" where
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s, 'r) tmonad \<Rightarrow> ('s, 'r) tmonad \<Rightarrow> ('s, 'r) tmonad"
|
||||
where
|
||||
"condition P L R \<equiv> \<lambda>s. if (P s) then (L s) else (R s)"
|
||||
|
||||
notation (output)
|
||||
|
|
@ -217,15 +221,14 @@ definition gets_the :: "('s \<Rightarrow> 'a option) \<Rightarrow> ('s, 'a) tmon
|
|||
text \<open>
|
||||
Get a map (such as a heap) from the current state and apply an argument to the map.
|
||||
Fail if the map returns @{const None}, otherwise return the value.\<close>
|
||||
definition
|
||||
gets_map :: "('s \<Rightarrow> 'a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> ('s, 'b) tmonad" where
|
||||
definition gets_map :: "('s \<Rightarrow> 'a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> ('s, 'b) tmonad" where
|
||||
"gets_map f p \<equiv> gets f >>= (\<lambda>m. assert_opt (m p))"
|
||||
|
||||
|
||||
subsection \<open>The Monad Laws\<close>
|
||||
|
||||
text \<open>An alternative definition of bind, sometimes more convenient.\<close>
|
||||
lemma bind_def2:
|
||||
text \<open>An alternative definition of @{term bind}, sometimes more convenient.\<close>
|
||||
lemma bind_def':
|
||||
"bind f g \<equiv>
|
||||
\<lambda>s. ((\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> f s})
|
||||
\<union> ((\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> f s})
|
||||
|
|
@ -242,7 +245,7 @@ lemma elem_bindE:
|
|||
\<lbrakk>res = Incomplete \<or> res = Failed; (tr, map_tmres undefined undefined res) \<in> f s\<rbrakk> \<Longrightarrow> P;
|
||||
\<And>tr' tr'' x s'. \<lbrakk>(tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> P\<rbrakk>
|
||||
\<Longrightarrow> P"
|
||||
by (auto simp: bind_def2)
|
||||
by (auto simp: bind_def')
|
||||
|
||||
text \<open>Each monad satisfies at least the following three laws.\<close>
|
||||
|
||||
|
|
@ -277,6 +280,7 @@ lemma bind_assoc:
|
|||
apply (simp add: image_image)
|
||||
done
|
||||
|
||||
|
||||
section \<open>Adding Exceptions\<close>
|
||||
|
||||
text \<open>
|
||||
|
|
@ -312,8 +316,8 @@ text \<open>
|
|||
the right-hand side is skipped if the left-hand side
|
||||
produced an exception.\<close>
|
||||
definition bindE ::
|
||||
"('s, 'e + 'a) tmonad \<Rightarrow> ('a \<Rightarrow> ('s, 'e + 'b) tmonad) \<Rightarrow> ('s, 'e + 'b) tmonad"
|
||||
(infixl ">>=E" 60) where
|
||||
"('s, 'e + 'a) tmonad \<Rightarrow> ('a \<Rightarrow> ('s, 'e + 'b) tmonad) \<Rightarrow> ('s, 'e + 'b) tmonad" (infixl ">>=E" 60)
|
||||
where
|
||||
"f >>=E g \<equiv> f >>= lift g"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -345,6 +349,7 @@ text \<open>
|
|||
definition assertE :: "bool \<Rightarrow> ('a, 'e + unit) tmonad" where
|
||||
"assertE P \<equiv> if P then returnOk () else fail"
|
||||
|
||||
|
||||
subsection "Monad Laws for the Exception Monad"
|
||||
|
||||
text \<open>More direct definition of @{const liftE}:\<close>
|
||||
|
|
@ -545,7 +550,8 @@ text \<open>
|
|||
going through both lists simultaneously, left to right, ignoring
|
||||
return values.\<close>
|
||||
definition zipWithM_x ::
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) tmonad) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, unit) tmonad" where
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) tmonad) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, unit) tmonad"
|
||||
where
|
||||
"zipWithM_x f xs ys \<equiv> sequence_x (zipWith f xs ys)"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -559,14 +565,16 @@ definition mapM :: "('a \<Rightarrow> ('s,'b) tmonad) \<Rightarrow> 'a list \<Ri
|
|||
"mapM f xs \<equiv> sequence (map f xs)"
|
||||
|
||||
definition zipWithM ::
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) tmonad) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, 'c list) tmonad" where
|
||||
"('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) tmonad) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, 'c list) tmonad"
|
||||
where
|
||||
"zipWithM f xs ys \<equiv> sequence (zipWith f xs ys)"
|
||||
|
||||
definition foldM :: "('b \<Rightarrow> 'a \<Rightarrow> ('s, 'a) tmonad) \<Rightarrow> 'b list \<Rightarrow> 'a \<Rightarrow> ('s, 'a) tmonad" where
|
||||
"foldM m xs a \<equiv> foldr (\<lambda>p q. q >>= m p) xs (return a) "
|
||||
|
||||
definition foldME ::
|
||||
"('b \<Rightarrow> 'a \<Rightarrow> ('s,('e + 'b)) tmonad) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> ('s, ('e + 'b)) tmonad" where
|
||||
"('b \<Rightarrow> 'a \<Rightarrow> ('s,('e + 'b)) tmonad) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> ('s, ('e + 'b)) tmonad"
|
||||
where
|
||||
"foldME m a xs \<equiv> foldr (\<lambda>p q. q >>=E swp m p) xs (returnOk a)"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -585,7 +593,6 @@ definition sequenceE :: "('s, 'e+'a) tmonad list \<Rightarrow> ('s, 'e+'a list)
|
|||
definition mapME :: "('a \<Rightarrow> ('s,'e+'b) tmonad) \<Rightarrow> 'a list \<Rightarrow> ('s,'e+'b list) tmonad" where
|
||||
"mapME f xs \<equiv> sequenceE (map f xs)"
|
||||
|
||||
|
||||
text \<open>Filtering a list using a monadic function as predicate:\<close>
|
||||
primrec filterM :: "('a \<Rightarrow> ('s, bool) tmonad) \<Rightarrow> 'a list \<Rightarrow> ('s, 'a list) tmonad" where
|
||||
"filterM P [] = return []"
|
||||
|
|
@ -617,7 +624,8 @@ text \<open>
|
|||
Turning an exception monad into a normal state monad
|
||||
by catching and handling any potential exceptions:\<close>
|
||||
definition catch ::
|
||||
"('s, 'e + 'a) tmonad \<Rightarrow> ('e \<Rightarrow> ('s, 'a) tmonad) \<Rightarrow> ('s, 'a) tmonad" (infix "<catch>" 10) where
|
||||
"('s, 'e + 'a) tmonad \<Rightarrow> ('e \<Rightarrow> ('s, 'a) tmonad) \<Rightarrow> ('s, 'a) tmonad" (infix "<catch>" 10)
|
||||
where
|
||||
"f <catch> handler \<equiv>
|
||||
do x \<leftarrow> f;
|
||||
case x of
|
||||
|
|
@ -645,8 +653,8 @@ text \<open>
|
|||
practice: the exception handle (potentially) throws exception
|
||||
of the same type as the left-hand side.\<close>
|
||||
definition handleE ::
|
||||
"('s, 'x + 'a) tmonad \<Rightarrow> ('x \<Rightarrow> ('s, 'x + 'a) tmonad) \<Rightarrow> ('s, 'x + 'a) tmonad"
|
||||
(infix "<handle>" 10) where
|
||||
"('s, 'x + 'a) tmonad \<Rightarrow> ('x \<Rightarrow> ('s, 'x + 'a) tmonad) \<Rightarrow> ('s, 'x + 'a) tmonad" (infix "<handle>" 10)
|
||||
where
|
||||
"handleE \<equiv> handleE'"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -654,8 +662,8 @@ text \<open>
|
|||
if the left-hand side throws no exception:\<close>
|
||||
definition handle_elseE ::
|
||||
"('s, 'e + 'a) tmonad \<Rightarrow> ('e \<Rightarrow> ('s, 'ee + 'b) tmonad) \<Rightarrow> ('a \<Rightarrow> ('s, 'ee + 'b) tmonad) \<Rightarrow>
|
||||
('s, 'ee + 'b) tmonad"
|
||||
("_ <handle> _ <else> _" 10) where
|
||||
('s, 'ee + 'b) tmonad" ("_ <handle> _ <else> _" 10)
|
||||
where
|
||||
"f <handle> handler <else> continue \<equiv>
|
||||
do v \<leftarrow> f;
|
||||
case v of Inl e \<Rightarrow> handler e
|
||||
|
|
@ -698,7 +706,8 @@ inductive_cases whileLoop_terminates_cases: "whileLoop_terminates C B r s"
|
|||
inductive_simps whileLoop_terminates_simps: "whileLoop_terminates C B r s"
|
||||
|
||||
definition whileLoop ::
|
||||
"('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> 'r \<Rightarrow> ('s, 'r) tmonad" where
|
||||
"('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> 'r \<Rightarrow> ('s, 'r) tmonad"
|
||||
where
|
||||
"whileLoop C B \<equiv> (\<lambda>r s. {(ts, res). ((r,s), ts,res) \<in> whileLoop_results C B})"
|
||||
|
||||
notation (output)
|
||||
|
|
@ -706,7 +715,8 @@ notation (output)
|
|||
|
||||
\<comment> \<open>FIXME: why does this differ to Nondet_Monad?\<close>
|
||||
definition whileLoopT ::
|
||||
"('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> 'r \<Rightarrow> ('s, 'r) tmonad" where
|
||||
"('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> 'r \<Rightarrow> ('s, 'r) tmonad"
|
||||
where
|
||||
"whileLoopT C B \<equiv> (\<lambda>r s. {(ts, res). ((r,s), ts,res) \<in> whileLoop_results C B
|
||||
\<and> whileLoop_terminates C B r s})"
|
||||
|
||||
|
|
@ -714,7 +724,8 @@ notation (output)
|
|||
whileLoopT ("(whileLoopT (_)// (_))" [1000, 1000] 1000)
|
||||
|
||||
definition whileLoopE ::
|
||||
"('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'e + 'r) tmonad) \<Rightarrow> 'r \<Rightarrow> ('s, ('e + 'r)) tmonad" where
|
||||
"('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'e + 'r) tmonad) \<Rightarrow> 'r \<Rightarrow> ('s, ('e + 'r)) tmonad"
|
||||
where
|
||||
"whileLoopE C body \<equiv>
|
||||
\<lambda>r. whileLoop (\<lambda>r s. (case r of Inr v \<Rightarrow> C v s | _ \<Rightarrow> False)) (lift body) (Inr r)"
|
||||
|
||||
|
|
@ -727,44 +738,38 @@ section "Combinators that have conditions with side effects"
|
|||
definition notM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
|
||||
"notM m = do c \<leftarrow> m; return (\<not> c) od"
|
||||
|
||||
definition whileM ::
|
||||
"('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, unit) tmonad" where
|
||||
definition whileM :: "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, unit) tmonad" where
|
||||
"whileM C B \<equiv> do
|
||||
c \<leftarrow> C;
|
||||
whileLoop (\<lambda>c s. c) (\<lambda>_. do B; C od) c;
|
||||
return ()
|
||||
od"
|
||||
|
||||
definition ifM ::
|
||||
"('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow>
|
||||
('s, 'a) tmonad" where
|
||||
definition ifM :: "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, 'a) tmonad" where
|
||||
"ifM test t f = do
|
||||
c \<leftarrow> test;
|
||||
if c then t else f
|
||||
od"
|
||||
|
||||
definition ifME ::
|
||||
"('a, 'b + bool) tmonad \<Rightarrow> ('a, 'b + 'c) tmonad \<Rightarrow> ('a, 'b + 'c) tmonad
|
||||
\<Rightarrow> ('a, 'b + 'c) tmonad" where
|
||||
"('a, 'b + bool) tmonad \<Rightarrow> ('a, 'b + 'c) tmonad \<Rightarrow> ('a, 'b + 'c) tmonad \<Rightarrow> ('a, 'b + 'c) tmonad"
|
||||
where
|
||||
"ifME test t f = doE
|
||||
c \<leftarrow> test;
|
||||
if c then t else f
|
||||
odE"
|
||||
|
||||
definition whenM ::
|
||||
"('s, bool) tmonad \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
|
||||
definition whenM :: "('s, bool) tmonad \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
|
||||
"whenM t m = ifM t m (return ())"
|
||||
|
||||
definition orM ::
|
||||
"('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
|
||||
definition orM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
|
||||
"orM a b = ifM a (return True) b"
|
||||
|
||||
definition
|
||||
andM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
|
||||
definition andM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
|
||||
"andM a b = ifM a b (return False)"
|
||||
|
||||
|
||||
subsection "Await command"
|
||||
section "Await command"
|
||||
|
||||
text \<open>@{term "Await c f"} blocks the execution until @{term "c"} is true,
|
||||
and then atomically executes @{term "f"}.\<close>
|
||||
|
|
@ -782,7 +787,7 @@ definition Await :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,unit) tmonad" whe
|
|||
od"
|
||||
|
||||
|
||||
section "Trace monad Parallel"
|
||||
section "Parallel combinator"
|
||||
|
||||
definition parallel :: "('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad" where
|
||||
"parallel f g = (\<lambda>s. {(xs, rv). \<exists>f_steps. length f_steps = length xs
|
||||
|
|
|
|||
|
|
@ -286,6 +286,14 @@ lemma gets_fold_into_modify:
|
|||
by (simp_all add: fun_eq_iff modify_def bind_assoc exec_gets
|
||||
exec_get exec_put)
|
||||
|
||||
lemma gets_return_gets_eq:
|
||||
"gets f >>= (\<lambda>g. return (h g)) = gets (\<lambda>s. h (f s))"
|
||||
by (simp add: simpler_gets_def bind_def return_def)
|
||||
|
||||
lemma gets_prod_comp:
|
||||
"gets (case x of (a, b) \<Rightarrow> f a b) = (case x of (a, b) \<Rightarrow> gets (f a b))"
|
||||
by (auto simp: split_def)
|
||||
|
||||
lemma bind_assoc2:
|
||||
"(do x \<leftarrow> a; _ \<leftarrow> b; c x od) = (do x \<leftarrow> (do x' \<leftarrow> a; _ \<leftarrow> b; return x' od); c x od)"
|
||||
by (simp add: bind_assoc)
|
||||
|
|
|
|||
|
|
@ -45,14 +45,6 @@ lemma hoare_name_pre_stateE:
|
|||
"\<lbrakk>\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
|
||||
by (clarsimp simp: validE_def2)
|
||||
|
||||
lemma hoare_vcg_if_lift:
|
||||
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
|
||||
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P then X rv s else Y rv s\<rbrace>"
|
||||
|
||||
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
|
||||
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P then X rv else Y rv\<rbrace>"
|
||||
by (auto simp: valid_def split_def)
|
||||
|
||||
lemma hoare_vcg_if_lift_strong:
|
||||
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>P\<rbrace>; \<lbrace>\<lambda>s. \<not> P' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>R'\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow>
|
||||
\<lbrace>\<lambda>s. if P' s then Q' s else R' s\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then Q rv s else R rv s\<rbrace>"
|
||||
|
|
@ -240,13 +232,6 @@ lemma hoare_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules *
|
|||
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>, -"
|
||||
by (auto simp: valid_def validE_R_def validE_def split_def)
|
||||
|
||||
lemma hoare_vcg_imp_liftE:
|
||||
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, \<lbrace>A\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>A\<rbrace> \<rbrakk>
|
||||
\<Longrightarrow> \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, \<lbrace>A\<rbrace>"
|
||||
apply (simp only: imp_conv_disj)
|
||||
apply (clarsimp simp: validE_def valid_def split_def sum.case_eq_if)
|
||||
done
|
||||
|
||||
lemma hoare_list_all_lift:
|
||||
"(\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace> f \<lbrace>\<lambda>rv. Q r\<rbrace>)
|
||||
\<Longrightarrow> \<lbrace>\<lambda>s. list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. list_all (\<lambda>r. Q r s) xs\<rbrace>"
|
||||
|
|
@ -394,13 +379,6 @@ lemma hoare_validE_R_conj:
|
|||
"\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q and R\<rbrace>, -"
|
||||
by (simp add: valid_def validE_def validE_R_def Let_def split_def split: sum.splits)
|
||||
|
||||
lemma hoare_vcg_disj_lift_R:
|
||||
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
|
||||
assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
|
||||
shows "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>,-"
|
||||
using assms
|
||||
by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
|
||||
|
||||
lemmas throwError_validE_R = throwError_wp [where E="\<top>\<top>", folded validE_R_def]
|
||||
|
||||
lemma valid_case_option_post_wp:
|
||||
|
|
@ -552,10 +530,6 @@ lemma wp_split_const_if_R:
|
|||
shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>,-"
|
||||
by (case_tac G, simp_all add: x y)
|
||||
|
||||
lemma hoare_vcg_imp_lift_R:
|
||||
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -"
|
||||
by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
|
||||
|
||||
lemma hoare_disj_division:
|
||||
"\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk>
|
||||
\<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>"
|
||||
|
|
|
|||
|
|
@ -131,7 +131,7 @@ lemma no_fail_returnOK[simp, wp]:
|
|||
|
||||
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_def2 image_Un image_image
|
||||
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)
|
||||
|
|
|
|||
|
|
@ -17,7 +17,8 @@ text \<open>
|
|||
The dual to validity: an existential instead of a universal quantifier for the post condition.
|
||||
In refinement, it is often sufficient to know that there is one state that satisfies a condition.\<close>
|
||||
definition exs_valid ::
|
||||
"('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) tmonad \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>") where
|
||||
"('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) tmonad \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>") where
|
||||
"\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>(rv, s') \<in> mres (f s). Q rv s')"
|
||||
|
||||
text \<open>The above for the exception monad\<close>
|
||||
|
|
@ -86,7 +87,7 @@ lemma exs_valid_assume_pre:
|
|||
lemma exs_valid_bind[wp_split]:
|
||||
"\<lbrakk> \<And>rv. \<lbrace>B rv\<rbrace> g rv \<exists>\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<exists>\<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= (\<lambda>rv. g rv) \<exists>\<lbrace>C\<rbrace>"
|
||||
apply atomize
|
||||
apply (clarsimp simp: exs_valid_def bind_def2 mres_def)
|
||||
apply (clarsimp simp: exs_valid_def bind_def' mres_def)
|
||||
apply (drule spec, drule(1) mp, clarsimp)
|
||||
apply (drule spec2, drule(1) mp, clarsimp)
|
||||
apply (simp add: image_def bex_Un)
|
||||
|
|
|
|||
|
|
@ -20,7 +20,8 @@ text \<open>
|
|||
is often similar. The following definitions allow such reasoning to take place.\<close>
|
||||
|
||||
definition validNF ::
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>!") where
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>!") where
|
||||
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! \<equiv> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<and> no_fail P f"
|
||||
|
||||
lemma validNF_alt_def:
|
||||
|
|
@ -304,7 +305,8 @@ lemma validNF_nobindE[wp]:
|
|||
text \<open>
|
||||
Set up triple rules for @{term validE_NF} so that we can use @{method wp} combinator rules.\<close>
|
||||
definition validE_NF_property ::
|
||||
"('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> ('s, 'c+'a) tmonad \<Rightarrow> bool" where
|
||||
"('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> ('s, 'c+'a) tmonad \<Rightarrow> bool"
|
||||
where
|
||||
"validE_NF_property Q E s b \<equiv>
|
||||
Failed \<notin> snd ` (b s) \<and> (\<forall>(r', s') \<in> mres (b s). case r' of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> Q x s')"
|
||||
|
||||
|
|
|
|||
|
|
@ -34,15 +34,15 @@ text \<open>
|
|||
@{term "assert P"} does not require us to prove that @{term P} holds, but
|
||||
rather allows us to assume @{term P}! Proving non-failure is done via a
|
||||
separate predicate and calculus (see Trace_No_Fail).\<close>
|
||||
definition valid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
definition valid ::
|
||||
"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>") where
|
||||
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r,s') \<in> mres (f s). Q r s')"
|
||||
|
||||
text \<open>
|
||||
We often reason about invariant predicates. The following provides shorthand syntax
|
||||
that avoids repeating potentially long predicates.\<close>
|
||||
abbreviation (input) invariant ::
|
||||
"('s,'a) tmonad \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<lbrace>_\<rbrace>" [59,0] 60) where
|
||||
abbreviation (input) invariant :: "('s,'a) tmonad \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<lbrace>_\<rbrace>" [59,0] 60) where
|
||||
"invariant f P \<equiv> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -143,7 +143,7 @@ subsection "Hoare Logic Rules"
|
|||
|
||||
lemma bind_wp[wp_split]:
|
||||
"\<lbrakk> \<And>r. \<lbrace>Q' r\<rbrace> g r \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= (\<lambda>rv. g rv) \<lbrace>Q\<rbrace>"
|
||||
by (fastforce simp: valid_def bind_def2 mres_def intro: image_eqI[rotated])
|
||||
by (fastforce simp: valid_def bind_def' mres_def intro: image_eqI[rotated])
|
||||
|
||||
lemma seq':
|
||||
"\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<forall>x. P x \<longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; \<forall>x s. B x s \<longrightarrow> P x \<and> C s \<rbrakk> \<Longrightarrow>
|
||||
|
|
@ -467,7 +467,7 @@ lemma in_image_constant:
|
|||
|
||||
lemma hoare_liftM_subst:
|
||||
"\<lbrace>P\<rbrace> liftM f m \<lbrace>Q\<rbrace> = \<lbrace>P\<rbrace> m \<lbrace>Q \<circ> f\<rbrace>"
|
||||
apply (simp add: liftM_def bind_def2 return_def split_def)
|
||||
apply (simp add: liftM_def bind_def' return_def split_def)
|
||||
apply (simp add: valid_def Ball_def mres_def image_Un)
|
||||
apply (simp add: image_image in_image_constant)
|
||||
apply force
|
||||
|
|
@ -554,6 +554,15 @@ lemma hoare_vcg_conj_liftE1:
|
|||
unfolding valid_def validE_R_def validE_def
|
||||
by (fastforce simp: split_def split: sum.splits)
|
||||
|
||||
lemma hoare_vcg_conj_liftE_weaker:
|
||||
assumes "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
|
||||
assumes "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>"
|
||||
shows "\<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E\<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (fastforce intro: assms hoare_vcg_conj_liftE1 validE_validE_R hoare_post_impErr)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma hoare_vcg_disj_lift:
|
||||
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>"
|
||||
unfolding valid_def
|
||||
|
|
@ -585,6 +594,19 @@ lemma hoare_vcg_imp_lift':
|
|||
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
|
||||
by (wpsimp wp: hoare_vcg_imp_lift)
|
||||
|
||||
lemma hoare_vcg_imp_liftE:
|
||||
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, \<lbrace>A\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>A\<rbrace> \<rbrakk>
|
||||
\<Longrightarrow> \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, \<lbrace>A\<rbrace>"
|
||||
by (fastforce simp: validE_def valid_def split: sum.splits)
|
||||
|
||||
lemma hoare_vcg_imp_lift_R:
|
||||
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -"
|
||||
by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
|
||||
|
||||
lemma hoare_vcg_imp_lift_R':
|
||||
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not>P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -"
|
||||
by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
|
||||
|
||||
lemma hoare_vcg_imp_conj_lift[wp_comb]:
|
||||
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> Q' rv s\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace> \<rbrakk> \<Longrightarrow>
|
||||
\<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>"
|
||||
|
|
@ -605,6 +627,10 @@ lemma hoare_vcg_const_imp_lift:
|
|||
"\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>"
|
||||
by (cases P, simp_all add: hoare_vcg_prop)
|
||||
|
||||
lemma hoare_vcg_const_imp_lift_E:
|
||||
"(P \<Longrightarrow> \<lbrace>Q\<rbrace> f -, \<lbrace>R\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> f -, \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>"
|
||||
by (fastforce simp: validE_E_def validE_def valid_def split_def split: sum.splits)
|
||||
|
||||
lemma hoare_vcg_const_imp_lift_R:
|
||||
"(P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,-) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
|
||||
by (fastforce simp: validE_R_def validE_def valid_def split_def split: sum.splits)
|
||||
|
|
@ -708,6 +734,58 @@ lemma hoare_post_comb_imp_conj:
|
|||
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
|
||||
by (wpsimp wp: hoare_vcg_conj_lift)
|
||||
|
||||
lemma hoare_vcg_if_lift:
|
||||
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
|
||||
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P then X rv s else Y rv s\<rbrace>"
|
||||
|
||||
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
|
||||
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P then X rv else Y rv\<rbrace>"
|
||||
by (auto simp: valid_def split_def)
|
||||
|
||||
lemma hoare_vcg_disj_lift_R:
|
||||
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
|
||||
assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
|
||||
shows "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>,-"
|
||||
using assms
|
||||
by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
|
||||
|
||||
lemma hoare_vcg_all_liftE:
|
||||
"\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>"
|
||||
by (fastforce simp: validE_def valid_def split: sum.splits)
|
||||
|
||||
lemma hoare_vcg_const_Ball_liftE:
|
||||
"\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>r s. True\<rbrace>, \<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>S. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>"
|
||||
by (fastforce simp: validE_def valid_def split: sum.splits)
|
||||
|
||||
lemma hoare_vcg_split_lift[wp]:
|
||||
"\<lbrace>P\<rbrace> f x y \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> case (x, y) of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>"
|
||||
by simp
|
||||
|
||||
named_theorems hoare_vcg_op_lift
|
||||
lemmas [hoare_vcg_op_lift] =
|
||||
hoare_vcg_const_imp_lift
|
||||
hoare_vcg_const_imp_lift_E
|
||||
hoare_vcg_const_imp_lift_R
|
||||
(* leaving out hoare_vcg_conj_lift*, because that is built into wp *)
|
||||
hoare_vcg_disj_lift
|
||||
hoare_vcg_disj_lift_R
|
||||
hoare_vcg_ex_lift
|
||||
hoare_vcg_ex_liftE
|
||||
hoare_vcg_ex_liftE_E
|
||||
hoare_vcg_all_lift
|
||||
hoare_vcg_all_liftE
|
||||
hoare_vcg_all_liftE_E
|
||||
hoare_vcg_all_lift_R
|
||||
hoare_vcg_const_Ball_lift
|
||||
hoare_vcg_const_Ball_lift_R
|
||||
hoare_vcg_const_Ball_lift_E_E
|
||||
hoare_vcg_split_lift
|
||||
hoare_vcg_if_lift
|
||||
hoare_vcg_imp_lift'
|
||||
hoare_vcg_imp_liftE
|
||||
hoare_vcg_imp_lift_R
|
||||
hoare_vcg_imp_liftE_E
|
||||
|
||||
|
||||
subsection \<open>Weakest Precondition Rules\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ lemma triv_refinement_mono_bind:
|
|||
"(\<forall>x. triv_refinement (b x) (d x)) \<Longrightarrow> triv_refinement (a >>= b) (a >>= d)"
|
||||
apply (simp add: triv_refinement_def bind_def)
|
||||
apply (intro allI UN_mono; simp)
|
||||
apply (simp only: triv_refinement_def bind_def2 split_def)
|
||||
apply (simp only: triv_refinement_def bind_def' split_def)
|
||||
apply (intro Un_mono allI order_refl UN_mono image_mono)
|
||||
apply simp
|
||||
done
|
||||
|
|
|
|||
Loading…
Reference in New Issue