add experiment section, some minor adjustments too squash

Signed-off-by: Michael McInerney <[email protected]>

Author: michaelmcinerney

lib/RCorres.thy

@@ -33,11 +33,12 @@ text \<open>
   for the usual Boolean connectives, but will also wish to lift an rcorres goal to a @{term valid}
   goal when the postcondition of the rcorres goal mentions only the return value and state from
   one of the two monads. These lifting rules often require @{term no_fail} assumptions, and so when
-  lifting an rcorres goal with concrete function that is a @{term Nondet_Monad.bind} of other
+  lifting an rcorres goal with a concrete function that is a @{term Nondet_Monad.bind} of other
   functions, we will immediately be required to show @{term no_fail} for the composite function
   anyway. Therefore, we have chosen to keep failure separate. The section below regarding
   interactions with @{term no_fail} includes a rule that allows us to show @{term no_fail} for
-  composite functions by transforming complex predicates with rcorres.\<close>
+  composite functions by transforming complex predicates with rcorres. The section below regarding
+  @{term corres_underlying} shows the relation between rcorres and @{term corres_underlying}.\<close>
 
 definition rcorres ::
   "('s \<Rightarrow> 't \<Rightarrow> bool) \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('t, 'b) nondet_monad
@@ -47,7 +48,7 @@ definition rcorres ::
      \<forall>s s'. R s s' \<longrightarrow> (\<forall>(rv', t') \<in> fst (f' s'). \<exists>(rv, t) \<in> fst (f s). R' rv rv' t t')"
 
 
-chapter \<open>Interactions with @{term valid}\<close>
+section \<open>Interactions with @{term valid}\<close>
 
 lemma rcorres_as_valid:
   "rcorres R f f' R' \<longleftrightarrow> (\<forall>s. \<lbrace>\<lambda>s'. R s s'\<rbrace> f' \<lbrace>\<lambda>rv' t'. \<exists>(rv, t) \<in> fst (f s). R' rv rv' t t'\<rbrace>)"
@@ -73,7 +74,7 @@ lemma rcorres_from_valid_det:
   by (force simp: rcorres_def det_wp_def valid_def)
 
 
-chapter \<open>Manipulating the precondition and the postcondition\<close>
+section \<open>Manipulating the precondition and the postcondition\<close>
 
 lemma rcorres_weaken_pre:
   "\<lbrakk>rcorres Q' f f' R; \<And>s s'. Q s s' \<Longrightarrow> Q' s s'\<rbrakk> \<Longrightarrow> rcorres Q f f' R"
@@ -109,7 +110,7 @@ lemma rcorres_assume_name_pre:
   by (fastforce simp: rcorres_def)
 
 
-chapter \<open>Interactions with @{term Nondet_Monad.bind}\<close>
+section \<open>Interactions with @{term Nondet_Monad.bind}\<close>
 
 lemma rcorres_split:
   "\<lbrakk>\<And>rv rv'. rcorres (Q rv rv') (b rv) (d rv') R; rcorres P a c Q\<rbrakk>
@@ -135,7 +136,7 @@ lemma rcorres_add_return_r:
   by (simp add: rcorres_def)
 
 
-chapter \<open>Symbolic execution and assertions\<close>
+section \<open>Symbolic execution and assertions\<close>
 
 lemma rcorres_symb_exec_l:
   "\<lbrakk>\<And>s'. \<lbrace>\<lambda>s. R s s'\<rbrace> a \<lbrace>\<lambda>rv s. Q rv s s'\<rbrace>; \<And>s s'. R s s' \<Longrightarrow> \<lbrace>(=) s\<rbrace> a \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>;
@@ -287,7 +288,7 @@ lemma rcorres_split_gets_the_fwd:
   by (fastforce intro: rcorres_weaken_pre[OF rcorres_split_gets_the])
 
 
-chapter \<open>if\<close>
+section \<open>if\<close>
 
 lemma rcorres_if_l:
   "\<lbrakk>b \<Longrightarrow> rcorres T f f' R'; \<not> b \<Longrightarrow> rcorres F g f' R'\<rbrakk>
@@ -304,7 +305,7 @@ lemma rcorres_if_r:
 lemmas rcorres_if_r_fwd = rcorres_if_r[where T=R and F=R for R, simplified]
 
 
-chapter \<open>Lifting rules\<close>
+section \<open>Lifting rules\<close>
 
 text \<open>
   We would like a lifting rule for conjunctions, and so a rule with assumptions including
@@ -326,9 +327,8 @@ text \<open>
   assumption does allow us to make this inference, and so we include this assumption in our rule.
 
   It does not seem possible for us to state an adequate lifting rule for conjunction for
-  @{term rcorres}, and so for an abstract monadic function that is not deterministic,
-  it may be necessary to unfold the definition of @{term rcorres} in order to show a postcondition
-  that is a conjunction.\<close>
+  @{term rcorres} with a nondeterministic abstract monadic function, and so in such a situation,
+  it may be necessary to unfold the definition of @{term rcorres}.\<close>
 lemma rcorres_conj_lift:
   "\<lbrakk>\<And>s'. det_wp (\<lambda>s. P s s') f; rcorres Q f f' R'; rcorres R f f' Q'\<rbrakk>
    \<Longrightarrow> rcorres
@@ -417,7 +417,7 @@ lemma rcorres_lift_conc_only:
 lemmas rcorres_lift_conc_only_fwd = rcorres_lift_conc_only[where P=P and R=P for P, simplified]
 
 
-chapter \<open>Interactions with @{term corres_underlying}\<close>
+section \<open>Interactions with @{term corres_underlying}\<close>
 
 lemma corres_underlying_from_rcorres:
   "\<lbrakk>nf' \<Longrightarrow> no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> srel \<and> P s \<and> P' s') f';
@@ -431,7 +431,7 @@ lemma rcorres_from_corres_underlying:
   by (fastforce simp: corres_underlying_def rcorres_def no_fail_def)
 
 
-chapter \<open>Interactions with @{term no_fail}\<close>
+section \<open>Interactions with @{term no_fail}\<close>
 
 lemma no_fail_rcorres_bind:
   "\<lbrakk>\<And>rv rv'. no_fail (\<lambda>s'. \<exists>s. R rv rv' s s') (g' rv'); rcorres Q f f' R;
@@ -444,23 +444,24 @@ lemma no_fail_rcorres_bind:
   done
 
 
-chapter \<open>Automation\<close>
+section \<open>Automation\<close>
 
 named_theorems rcorres
 named_theorems rcorres_lift
 
-method rcorres_step uses rcorres_del wp simp declares rcorres rcorres_lift =
-  declaring rcorres_del[rcorres del] in
+method rcorres_step uses rcorres_del rcorres_lift_del wp simp declares rcorres rcorres_lift =
+  declaring rcorres_del[rcorres del] rcorres_lift_del[rcorres_lift del] in
   \<open>rule rcorres
    | rule rcorres_split rcorres_conj_lift
    | rule rcorres_lift rcorres_lift_abs_only rcorres_lift_conc_only
    | wpsimp wp: wp simp: simp\<close>
 
 declare rcorres_weaken_pre[wp_pre]
 
-method rcorres uses rcorres_del wp simp declares rcorres rcorres_lift =
+method rcorres uses rcorres_del rcorres_lift_del wp simp declares rcorres rcorres_lift =
   wp_pre,
-  ((rcorres_step rcorres: rcorres rcorres_del: rcorres_del rcorres_lift: rcorres_lift
+  ((rcorres_step rcorres: rcorres rcorres_del: rcorres_del
+                 rcorres_lift: rcorres_lift rcorres_lift_del: rcorres_lift_del
                  wp: wp simp: simp)+)[1]
 
 text \<open>
@@ -473,4 +474,63 @@ method rcorres_conj_lift methods solve uses rule simp wp =
   (rule rcorres_lift, (solves \<open>rule rule\<close> | solves \<open>wpsimp wp: wp simp: simp\<close>)+)[1],
   solves solve
 
+experiment
+  fixes f f' :: "('s, 'r) nondet_monad"
+  fixes g g' h :: "'r \<Rightarrow> ('s, 'r) nondet_monad"
+
+  fixes P Q :: "'s \<Rightarrow> bool"
+  fixes R V :: "'s \<Rightarrow> 's \<Rightarrow> bool"
+  fixes S T U :: "'r \<Rightarrow> 'r \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> bool"
+
+  assumes [wp]: "f \<lbrace>P\<rbrace>" "\<And>rv. g rv \<lbrace>P\<rbrace>" "f \<lbrace>Q\<rbrace>" "\<And>rv. g rv \<lbrace>Q\<rbrace>"
+  assumes [wp]: "no_fail P f" "\<And>rv. no_fail P (g rv)"
+  assumes [wp]: "det_wp P f"
+  assumes [wp]: "empty_fail f" "\<And>rv. empty_fail (g rv)"
+
+  assumes [rcorres]: "rcorres R f f' S"
+  assumes [rcorres]: "\<And>rv rv'. rcorres (S rv rv') (g rv) (g' rv') T"
+  assumes [rcorres]: "\<And>rv rv'. rcorres (T rv rv') (h rv) (return rv') U"
+
+  assumes
+    lift[rcorres_lift]:
+      "\<And>(f :: ('s, 'r) nondet_monad) (f' :: ('s, 'r) nondet_monad).
+         \<lbrakk>no_fail P f; empty_fail f; f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> rcorres V f f' (\<lambda>_ _. V)"
+begin
+
+text \<open>The rcorres method works very similarly to wpsimp in straightforward cases.\<close>
+lemma "rcorres R (do rv \<leftarrow> f; g rv od) (do rv \<leftarrow> f'; g' rv od) T"
+  apply rcorres
+  by simp
+
+text \<open>
+  It may help to add a @{term return} on one side in order to balance the abstract and concrete
+  functions, so that splitting occurs in the desired way.\<close>
+lemma "rcorres R (do x \<leftarrow> f; y \<leftarrow> g x; h y od) (do x \<leftarrow> f'; g' x od) U"
+  apply (rule rcorres_add_return_r)
+  apply (simp only: bind_assoc) \<comment> \<open>now @{term h} will be lined up with @{term return}\<close>
+  apply rcorres
+  by simp
+
+text \<open>
+  Although the rule @{thm lift} is in the set rcorres_lift, in this instance, we can give the rule
+  directly to the rcorres argument for it to be applied before the method attempts to split the
+  functions.\<close>
+lemma "rcorres V (do rv \<leftarrow> f; g rv od) (do rv \<leftarrow> f'; g' rv od) (\<lambda>_ _. V)"
+  apply (rcorres rcorres: lift)
+  by simp
+
+text
+  \<open>When the postcondition refers to the return value and state from only one of the monads, then
+   the rules @{thm rcorres_lift_abs_only} or @{thm rcorres_lift_conc_only} will be applied.\<close>
+lemma "rcorres (\<lambda>s _. P s) f f' (\<lambda>_ _ s _. P s)"
+  apply rcorres
+  by simp
+
+text \<open>A typical example of the rcorres_conj_lift method.\<close>
+lemma "rcorres (\<lambda>s s'. V s s' \<and> P s) f f' (\<lambda>_ _ s s'. V s s' \<and> W s s')"
+  apply (rcorres_conj_lift \<open>clarsimp\<close>) \<comment> \<open>breaks off the first conjunct and solves it with @{thm lift}\<close>
+  oops \<comment> \<open>leaves the goal with the same precondition, and the second conjunct as the postcondition\<close>
+
+end
+
 end