* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*)
(* A theory of guarded monadic bisimulation. *)
theory Bisim_UL
imports
"wp/NonDetMonadVCG"
Corres_UL
EmptyFailLib
begin
(* This still looks a bit wrong to me, although it is more or less what I want \<emdash> we want to be
able to move hoare triples across bisimulations, and this allows guards to be left behind, more or less
definition
"bisim_underlying SR R P P' m m' \<equiv>
\<forall>s s'. SR s s' \<longrightarrow> (P s \<longrightarrow> (\<forall>(r, t) \<in> fst (m s). \<exists>(r', t') \<in> fst (m' s'). R r r' \<and> SR t t')) \<and>
(P' s' \<longrightarrow> (\<forall>(r', t') \<in> fst (m' s'). \<exists>(r, t) \<in> fst (m s). R r r' \<and> SR t t'))"
\<forall>s s'. SR s s' \<and> P s \<and> P' s' \<longrightarrow> ((\<forall>(r, t) \<in> fst (m s). \<exists>(r', t') \<in> fst (m' s'). R r r' \<and> SR t t') \<and>
(\<forall>(r', t') \<in> fst (m' s'). \<exists>(r, t) \<in> fst (m s). R r r' \<and> SR t t'))"
(*
lemma bisim_is_corres_both_ways:
"bisim_underlying SR R P P' m m' = (corres_underlying SR False R P P' m m' \<and> corres_underlying (converse SR) False (swp R) P' P m' m)"
assumes ac: "bisim_underlying (op =) (op =) P P' a a'"
and rl: "\<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>"
shows "\<lbrace>P and P' and Q\<rbrace> a' \<lbrace>S\<rbrace>"
using ac rl
unfolding bisim_underlying_def valid_def
by (fastforce simp: split_def)
lemma bisim_valid2:
assumes ac: "bisim_underlying (op =) (op =) P P' a a'"
and rl: "\<lbrace>Q\<rbrace> a' \<lbrace>S\<rbrace>"
shows "\<lbrace>P and P' and Q\<rbrace> a \<lbrace>S\<rbrace>"
using ac rl
unfolding bisim_underlying_def valid_def
by (fastforce simp: split_def)
lemma bisim_underlyingI [consumes 0, case_names Left Right]:
assumes r1: "\<And>s s' r t. \<lbrakk>SR s s'; P s; P' s'; (r, t) \<in> fst (m s) \<rbrakk> \<Longrightarrow> \<exists>(r', t') \<in> fst (m' s'). R r r' \<and> SR t t'"
and r2: "\<And>s s' r' t'. \<lbrakk>SR s s'; P s; P' s'; (r', t') \<in> fst (m' s') \<rbrakk> \<Longrightarrow> \<exists>(r, t) \<in> fst (m s). R r r' \<and> SR t t'"
shows "bisim_underlying SR R P P' m m'"
unfolding bisim_underlying_def
by (fastforce dest: r1 r2 simp: split_def)
lemma bisim_underlyingE1:
assumes bs: "bisim_underlying SR R P P' m m'"
and sr: "SR s s'"
and ps: "P s" "P' s'"
and ms: "(r, t) \<in> fst (m s)"
and rl: "\<And>r' t'. \<lbrakk> (r', t') \<in> fst (m' s'); R r r'; SR t t' \<rbrakk> \<Longrightarrow> X"
shows X
using bs sr ps ms unfolding bisim_underlying_def
by (fastforce intro: rl)
lemma bisim_underlyingE2:
assumes bs: "bisim_underlying SR R P P' m m'"
and sr: "SR s s'"
and ps: "P s" "P' s'"
and ms: "(r', t') \<in> fst (m' s')"
and rl: "\<And>r t. \<lbrakk> (r, t) \<in> fst (m s); R r r'; SR t t' \<rbrakk> \<Longrightarrow> X"
shows X
using bs sr ps ms unfolding bisim_underlying_def
by (fastforce intro: rl)
lemma bisim_split:
assumes ac: "bisim_underlying SR R' P P' a c"
and bd: "\<And>r r'. R' r r' \<Longrightarrow> bisim_underlying SR R (Q r) (Q' r') (b r) (d r')"
and v1: "\<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>"
and v2: "\<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>"
shows "bisim_underlying SR R (P and S) (P' and S') (a >>= b) (c >>= d)"
using ac
apply -
apply (rule bisim_underlyingI)
apply (clarsimp simp: in_monad split_def)
apply (erule (4) bisim_underlyingE1)
apply (frule (1) use_valid [OF _ v1])
apply (frule (1) use_valid [OF _ v2])
apply (erule (4) bisim_underlyingE1 [OF bd])
apply (rename_tac r'' t'')
apply (rule_tac x = "(r'', t'')" in bexI)
apply clarsimp
apply (fastforce simp: in_monad)
apply (clarsimp simp: in_monad split_def)
apply (erule (4) bisim_underlyingE2)
apply (frule (1) use_valid [OF _ v1])
apply (frule (1) use_valid [OF _ v2])
apply (erule (4) bisim_underlyingE2 [OF bd])
apply (rename_tac r'' t'')
apply (rule_tac x = "(r'', t'')" in bexI)
apply clarsimp
apply (fastforce simp: in_monad)
done
abbreviation
"bisim \<equiv> bisim_underlying (op =)"
lemma bisim_refl:
assumes rrefl: "\<And>r. R r r"
shows "bisim R P P' m m"
apply (rule bisim_underlyingI)
apply (clarsimp simp: split_def)
apply (erule bexI [rotated])
apply (simp add: rrefl)
apply (clarsimp simp: split_def)
apply (erule bexI [rotated])
apply (simp add: rrefl)
done
lemma bisim_guard_imp:
assumes bs: "bisim_underlying SR R Q Q' m m'"
and rls: "\<And>s. P s \<Longrightarrow> Q s" "\<And>s. P' s \<Longrightarrow> Q' s"
shows "bisim_underlying SR R P P' m m'"
using bs rls
by (fastforce intro!: bisim_underlyingI elim: bisim_underlyingE1 bisim_underlyingE2)
lemma bisim_return':
assumes Rxx: "R x x'"
shows "bisim_underlying SR R P P' (return x) (return x')"
"\<lbrakk>bisim_underlying sr (lr \<oplus> rr) P P' a d;
\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv');
\<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk>
\<Longrightarrow> bisim_underlying sr r (P and Q) (P' and Q') (a >>= case_sum b c) (d >>= case_sum e f)"
apply (erule bisim_split [where Q = "\<lambda>rv s. case_sum (\<lambda>l. R l s) (\<lambda>r. S r s) rv" and Q' = "\<lambda>rv s. case_sum (\<lambda>l. R' l s) (\<lambda>r. S' r s) rv", folded validE_def])
"bisim_underlying SR (f \<oplus> R) P P' (liftE a) (liftE b) = bisim_underlying SR R P P' a b"
by (fastforce simp: in_monad intro: bisim_underlyingI elim: bisim_underlyingE1 bisim_underlyingE2)
lemma bisim_when:
assumes bs: "b \<Longrightarrow> bisim_underlying SR R P P' m m'"
and rr: "R () ()"
shows "bisim_underlying SR R (\<lambda>s. b \<longrightarrow> P s) (\<lambda>s. b \<longrightarrow> P' s) (when b m) (when b m')"
using assms
apply (cases b, simp_all add: when_def)
apply (erule bisim_return)
done
(* not really used *)
definition
"det_on P f \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>r. f s = ({r}, False))"
lemma det_onE:
"\<lbrakk>det_on P f; P s; \<And>r s'. \<lbrakk> (r, s') \<in> fst (f s); \<not> snd (f s)\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
unfolding det_on_def by fastforce
lemma bisim_noop_det_on:
assumes a: "\<And>s. \<lbrace>Pa and op = s\<rbrace> a \<lbrace>\<lambda>_. op = s\<rbrace>"
and b: "\<And>s. \<lbrace>Pb and op = s\<rbrace> b \<lbrace>\<lambda>_. op = s\<rbrace>"
and da: "det_on P a"
and db: "det_on P' b"
shows "bisim_underlying sr dc (Pa and P) (Pb and P') a b"
using da db
apply -
apply (rule bisim_underlyingI)
apply clarsimp
apply (erule (1) det_onE)+
apply (frule use_valid [OF _ a], fastforce)
apply (frule use_valid [OF _ b], fastforce)
apply fastforce
apply clarsimp
apply (erule (1) det_onE)+
apply (frule use_valid [OF _ a], fastforce)
apply (frule use_valid [OF _ b], fastforce)
apply fastforce
done
lemma det_on_gets:
"det_on \<top> (gets f)" unfolding det_on_def
by (clarsimp simp: gets_def return_def bind_def get_def)
lemma hoare_gen_asmE':
"(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>"
unfolding validE_def
by (erule hoare_gen_asm)
lemma det_onE':
"\<lbrakk>det_on P f; P s; \<And>r s'. \<lbrakk> f s = ({(r, s')}, False)\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
unfolding det_on_def by fastforce
(* ugh *)
lemma det_on_guard_imp [wp_comb]:
assumes da: "det_on P' a"
and "\<And>s. P s \<Longrightarrow> P' s"
shows "det_on P a"
using assms unfolding det_on_def by auto
lemma det_on_split [wp_split]:
assumes da: "det_on Pa a"
and db: "\<And>x. det_on (Pb x) (b x)"
and v: "\<lbrace>Pb'\<rbrace> a \<lbrace>Pb\<rbrace>"