kings-crown/FVELER_Isabelle huggingface dataset:
theory IRQ_DP

lemma validE_R_gen_asm_conj:
  "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<and> P\<rbrace> f \<lbrace>Q\<rbrace>, -" by (fastforce simp: validE_R_def validE_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<and> P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory IRQ_DP

lemma decode_irq_control_issue_irq_rv:
"\<lbrace>\<lambda>s. P (IssueIrqHandler irq target_ref (cap_object root_cap, offset index r)) s \<and>
        caps = (root_cap, root_ptr)#xs \<and> (unat depth) \<le> word_bits \<and> 0 < (unat depth) \<and>
         <\<box> (r, (unat depth)) : root_cap index \<mapsto>u cap \<and>* R> s\<rbrace>
           decode_irq_control_invocation target target_ref caps (IrqControlIssueIrqHandlerIntent irq index depth) \<lbrace>P\<rbrace>, -" apply (clarsimp simp: decode_irq_control_invocation_def) apply (wp lookup_slot_for_cnode_op_rvu'[where cap=cap and r=r] throw_on_none_rv) apply (clarsimp simp: get_index_def) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (IssueIrqHandler irq target_ref (cap_object root_cap, offset index r)) s \<and> caps = (root_cap, root_ptr) # xs \<and> unat depth \<le> word_bits \<and> 0 < unat depth \<and> cdl.lift (\<box> (r, unat depth) : root_cap index \<mapsto>u cap \<and>* R) s\<rbrace> decode_irq_control_invocation target target_ref caps (IrqControlIssueIrqHandlerIntent irq index depth) \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (IssueIrqHandler irq target_ref (cap_object root_cap, offset index r)) s \<and> caps = (root_cap, root_ptr) # xs \<and> unat depth \<le> word_bits \<and> 0 < unat depth \<and> cdl.lift (\<box> (r, unat depth) : root_cap index \<mapsto>u cap \<and>* R) s\<rbrace> doE root <- throw_on_none (get_index caps 0);
dest_slot_cap_ref <- lookup_slot_for_cnode_op (fst root) index (unat depth);
returnOk (IssueIrqHandler irq target_ref dest_slot_cap_ref)
odE \<sqinter> throw \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. P (IssueIrqHandler irq target_ref (cap_object root_cap, offset index r)) s \<and> caps = (root_cap, root_ptr) # xs \<and> unat depth \<le> word_bits \<and> 0 < unat depth \<and> cdl.lift (\<box> (r, unat depth) : root_cap index \<mapsto>u cap \<and>* R) s \<Longrightarrow> ((\<lambda>s. True \<and> (case get_index caps 0 of None \<Rightarrow> False | Some y \<Rightarrow> P (IssueIrqHandler irq target_ref (cap_object (fst y), offset index r)) s \<and> unat depth \<le> word_bits \<and> 0 < unat depth \<and> cdl.lift (\<box> (r, unat depth) : fst y index \<mapsto>u cap \<and>* ?R9 y) s)) and (\<lambda>s. True \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P (IssueIrqHandler irq target_ref (cap_object root_cap, offset index r)) s; caps = (root_cap, root_ptr) # xs; unat depth \<le> word_bits; 0 < unat depth; cdl.lift (\<box> (r, unat depth) : root_cap index \<mapsto>u cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (r, unat depth) : root_cap index \<mapsto>u cap \<and>* ?R9 (root_cap, root_ptr)) s proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma reset_cap_cdl_cap_irq: "reset_cap_asid c = IrqHandlerCap irq \<Longrightarrow> the (cdl_cap_irq c) = irq" apply (clarsimp simp: reset_cap_asid_def cdl_cap_irq_def the_def split: cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid c = IrqHandlerCap irq \<Longrightarrow> the (cdl_cap_irq c) = irq proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma not_memory_reset: "\<not> is_memory_cap (reset_cap_asid cap) \<Longrightarrow> reset_cap_asid cap = cap " apply (clarsimp simp: is_memory_cap_def reset_cap_asid_def split:cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_memory_cap (reset_cap_asid cap) \<Longrightarrow> reset_cap_asid cap = cap proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma not_ep_related_reset_cap_asid: "reset_cap_asid c = IrqControlCap \<Longrightarrow> \<not>ep_related_cap c" apply (clarsimp simp: reset_cap_asid_def ep_related_cap_def split: cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid c = IrqControlCap \<Longrightarrow> \<not> ep_related_cap c proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma reset_cap_asid_control: "reset_cap_asid c = reset_cap_asid cap \<Longrightarrow> is_irqcontrol_cap cap \<Longrightarrow> is_irqcontrol_cap c" apply (clarsimp simp: reset_cap_asid_def is_irqcontrol_cap_def split: cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reset_cap_asid c = reset_cap_asid cap; is_irqcontrol_cap cap\<rbrakk> \<Longrightarrow> is_irqcontrol_cap c proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma obj_tcb_simp [simp]:
  "is_tcb tcb \<Longrightarrow> Tcb (obj_tcb tcb) = tcb" by (clarsimp simp: obj_tcb_def is_tcb_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb tcb \<Longrightarrow> Tcb (obj_tcb tcb) = tcb
theory Bisim_UL

lemma bisim_valid:
  assumes ac: "bisim_underlying (=)  (=) 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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P' and Q\<rbrace> a' \<lbrace>S\<rbrace> proof (prove)
using this:
bisim_underlying (=) (=) P P' a a'
\<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P and P' and Q\<rbrace> a' \<lbrace>S\<rbrace> proof (prove)
using this:
\<forall>s s'. s = s' \<and> P s \<and> P' s' \<longrightarrow> (\<forall>(r, t)\<in>fst (a s). \<exists>(r', t')\<in>fst (a' s'). r = r' \<and> t = t') \<and> (\<forall>(r', t')\<in>fst (a' s'). \<exists>(r, t)\<in>fst (a s). r = r' \<and> t = t')
\<forall>s. Q s \<longrightarrow> (\<forall>(r, s')\<in>fst (a s). S r s')

goal (1 subgoal):
 1. \<forall>s. (P and P' and Q) s \<longrightarrow> (\<forall>(r, s')\<in>fst (a' s). S r s')
theory Bisim_UL

lemma bisim_valid2:
  assumes ac: "bisim_underlying (=) (=) 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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P' and Q\<rbrace> a \<lbrace>S\<rbrace> proof (prove)
using this:
bisim_underlying (=) (=) P P' a a'
\<lbrace>Q\<rbrace> a' \<lbrace>S\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P and P' and Q\<rbrace> a \<lbrace>S\<rbrace> proof (prove)
using this:
\<forall>s s'. s = s' \<and> P s \<and> P' s' \<longrightarrow> (\<forall>(r, t)\<in>fst (a s). \<exists>(r', t')\<in>fst (a' s'). r = r' \<and> t = t') \<and> (\<forall>(r', t')\<in>fst (a' s'). \<exists>(r, t)\<in>fst (a s). r = r' \<and> t = t')
\<forall>s. Q s \<longrightarrow> (\<forall>(r, s')\<in>fst (a' s). S r s')

goal (1 subgoal):
 1. \<forall>s. (P and P' and Q) s \<longrightarrow> (\<forall>(r, s')\<in>fst (a s). S r s')
theory Bisim_UL

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR R P P' m m' proof (prove)
goal (1 subgoal):
 1. \<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')
theory Bisim_UL

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. X proof (prove)
using this:
bisim_underlying SR R P P' m m'
SR s s'
P s
P' s'
(r, t) \<in> fst (m s)

goal (1 subgoal):
 1. X proof (prove)
using this:
\<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')
SR s s'
P s
P' s'
(r, t) \<in> fst (m s)

goal (1 subgoal):
 1. X
theory Bisim_UL

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. X proof (prove)
using this:
bisim_underlying SR R P P' m m'
SR s s'
P s
P' s'
(r', t') \<in> fst (m' s')

goal (1 subgoal):
 1. X proof (prove)
using this:
\<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')
SR s s'
P s
P' s'
(r', t') \<in> fst (m' s')

goal (1 subgoal):
 1. X
theory Bisim_UL

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim R P P' m m proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>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> t = t'
 2. \<And>s s' r' t'. \<lbrakk>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> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t. \<lbrakk>P s'; P' s'; (r, t) \<in> fst (m s')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m s'). R r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>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> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t. \<lbrakk>P s'; P' s'\<rbrakk> \<Longrightarrow> R r (fst (r, t)) \<and> t = snd (r, t)
 2. \<And>s s' r' t'. \<lbrakk>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> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>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> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t'. \<lbrakk>P s'; P' s'; (r', t') \<in> fst (m s')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t'. \<lbrakk>P s'; P' s'\<rbrakk> \<Longrightarrow> R (fst (r', t')) r' \<and> snd (r', t') = t' proof (prove)
goal:
No subgoals!
theory Bisim_UL

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR R P P' m m' proof (prove)
using this:
bisim_underlying SR R Q Q' m m'
P ?s \<Longrightarrow> Q ?s
P' ?s \<Longrightarrow> Q' ?s

goal (1 subgoal):
 1. bisim_underlying SR R P P' m m'
theory Bisim_UL

lemma bisim_return':
  assumes Rxx: "R x x'"
  shows "bisim_underlying SR R P P' (return x) (return x')" apply (rule bisim_underlyingI) apply (clarsimp simp: in_monad split_def Bex_def Rxx) apply (clarsimp simp: in_monad split_def Bex_def Rxx) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR R P P' (return x) (return x') proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>SR s s'; P s; P' s'; (r, t) \<in> fst (return x s)\<rbrakk> \<Longrightarrow> \<exists>(r', t')\<in>fst (return x' s'). R r r' \<and> SR t t'
 2. \<And>s s' r' t'. \<lbrakk>SR s s'; P s; P' s'; (r', t') \<in> fst (return x' s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (return x s). R r r' \<and> SR t t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>SR s s'; P s; P' s'; (r', t') \<in> fst (return x' s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (return x s). R r r' \<and> SR t t' proof (prove)
goal:
No subgoals!
theory Bisim_UL

lemma wpc_helper_bisim:
  "bisim_underlying SR r Q Q' f f' \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (bisim_underlying SR r P P' f f')" apply (clarsimp simp: wpc_helper_def) apply (erule bisim_guard_imp) apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR r Q Q' f f' \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (bisim_underlying SR r P P' f f') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bisim_underlying SR r Q Q' f f'; \<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''\<rbrakk> \<Longrightarrow> bisim_underlying SR r P P' f f' proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''; P s\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''; P' s\<rbrakk> \<Longrightarrow> Q' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''; P' s\<rbrakk> \<Longrightarrow> Q' s proof (prove)
goal:
No subgoals!
theory Bisim_UL

lemma bisim_split_refl:
  assumes bs: "\<And>r. bisim R (Q r) (Q' r) (b r) (d r)"
  and    v1: "\<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>"
  and   v2: "\<lbrace>S'\<rbrace> a \<lbrace>Q'\<rbrace>"
  shows "bisim R S S' (a >>= b) (a >>= d)" apply (rule bisim_guard_imp) apply (rule bisim_split [OF _ _ v1 v2]) apply (rule bisim_refl [where P = \<top> and P' = \<top> and R = "(=)", OF refl]) apply simp apply (rule bs) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim R S S' (a >>= b) (a >>= d) proof (prove)
goal (3 subgoals):
 1. bisim R ?Q ?Q' (a >>= b) (a >>= d)
 2. \<And>s. S s \<Longrightarrow> ?Q s
 3. \<And>s. S' s \<Longrightarrow> ?Q' s proof (prove)
goal (4 subgoals):
 1. bisim ?R'4 ?P4 ?P'4 a a
 2. \<And>r r'. ?R'4 r r' \<Longrightarrow> bisim R (Q r) (Q' r') (b r) (d r')
 3. \<And>s. S s \<Longrightarrow> (?P4 and S) s
 4. \<And>s. S' s \<Longrightarrow> (?P'4 and S') s proof (prove)
goal (3 subgoals):
 1. \<And>r r'. r = r' \<Longrightarrow> bisim R (Q r) (Q' r') (b r) (d r')
 2. \<And>s. S s \<Longrightarrow> ((\<lambda>_. True) and S) s
 3. \<And>s. S' s \<Longrightarrow> ((\<lambda>_. True) and S') s proof (prove)
goal (3 subgoals):
 1. \<And>r. bisim R (Q r) (Q' r) (b r) (d r)
 2. \<And>s. S s \<Longrightarrow> ((\<lambda>_. True) and S) s
 3. \<And>s. S' s \<Longrightarrow> ((\<lambda>_. True) and S') s proof (prove)
goal (2 subgoals):
 1. \<And>s. S s \<Longrightarrow> ((\<lambda>_. True) and S) s
 2. \<And>s. S' s \<Longrightarrow> ((\<lambda>_. True) and S') s proof (prove)
goal:
No subgoals!
theory Bisim_UL

lemma bisim_throwError':
  "f e e' \<Longrightarrow> bisim_underlying SR (f \<oplus> R') P P' (throwError e) (throwError e')" apply (rule bisim_underlyingI) apply (clarsimp simp: in_monad Bex_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f e e' \<Longrightarrow> bisim_underlying SR (f \<oplus> R') P P' (throwError e) (throwError e') proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>f e e'; SR s s'; P s; P' s'; (r, t) \<in> fst (throwError e s)\<rbrakk> \<Longrightarrow> \<exists>(r', t')\<in>fst (throwError e' s'). (f \<oplus> R') r r' \<and> SR t t'
 2. \<And>s s' r' t'. \<lbrakk>f e e'; SR s s'; P s; P' s'; (r', t') \<in> fst (throwError e' s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (throwError e s). (f \<oplus> R') r r' \<and> SR t t' proof (prove)
goal:
No subgoals!
theory Bisim_UL

lemma bisim_liftE [simp]:
  "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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR (f \<oplus> R) P P' (liftE a) (liftE b) = bisim_underlying SR R P P' a b
theory Bisim_UL

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR R (\<lambda>s. b \<longrightarrow> P s) (\<lambda>s. b \<longrightarrow> P' s) (when b m) (when b m') proof (prove)
using this:
b \<Longrightarrow> bisim_underlying SR R P P' m m'
R () ()

goal (1 subgoal):
 1. bisim_underlying SR R (\<lambda>s. b \<longrightarrow> P s) (\<lambda>s. b \<longrightarrow> P' s) (when b m) (when b m') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> b; R () ()\<rbrakk> \<Longrightarrow> bisim_underlying SR R (\<lambda>s. True) (\<lambda>s. True) (return ()) (return ()) proof (prove)
goal:
No subgoals!
theory Bisim_UL

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<exists>r. f s = ({r}, False)); P s; \<And>r s'. \<lbrakk>(r, s') \<in> fst (f s); \<not> snd (f s)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Bisim_UL

lemma det_on_gets:
  "det_on \<top> (gets f)" unfolding det_on_def by (clarsimp simp: gets_def return_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_on (\<lambda>_. True) (gets f) proof (prove)
goal (1 subgoal):
 1. \<forall>s. True \<longrightarrow> (\<exists>r. gets f s = ({r}, False))
theory Bisim_UL

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (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> proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R e s | Inr r \<Rightarrow> Q r s\<rbrace>) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R e s | Inr r \<Rightarrow> Q r s\<rbrace>
theory Bisim_UL

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det_on P f; P s; \<And>r s'. f s = ({(r, s')}, False) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<exists>r. f s = ({r}, False)); P s; \<And>r s'. f s = ({(r, s')}, False) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Bisim_UL

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>"
  shows "det_on (Pa and Pb') (a >>= b)" unfolding det_on_def using da apply - apply clarsimp apply (erule (1) det_onE) apply (frule (1) use_valid [OF _ v]) apply (erule det_onE' [OF da]) apply (erule det_onE' [OF db]) apply (clarsimp simp: bind_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_on (Pa and Pb') (a >>= b) proof (prove)
goal (1 subgoal):
 1. \<forall>s. (Pa and Pb') s \<longrightarrow> (\<exists>r. (a >>= b) s = ({r}, False)) proof (prove)
using this:
det_on Pa a

goal (1 subgoal):
 1. \<forall>s. (Pa and Pb') s \<longrightarrow> (\<exists>r. (a >>= b) s = ({r}, False)) proof (prove)
goal (1 subgoal):
 1. det_on Pa a \<Longrightarrow> \<forall>s. (Pa and Pb') s \<longrightarrow> (\<exists>r. (a >>= b) s = ({r}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>det_on Pa a; Pa s; Pb' s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (a >>= b) s = ({(aa, ba)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s r s'. \<lbrakk>Pa s; Pb' s; (r, s') \<in> fst (a s); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>aa ba. (a >>= b) s = ({(aa, ba)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s r s'. \<lbrakk>Pa s; Pb' s; (r, s') \<in> fst (a s); \<not> snd (a s); Pb r s'\<rbrakk> \<Longrightarrow> \<exists>aa ba. (a >>= b) s = ({(aa, ba)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s r s' ra s'a. \<lbrakk>Pb' s; (r, s') \<in> fst (a s); \<not> snd (a s); Pb r s'; a s = ({(ra, s'a)}, False)\<rbrakk> \<Longrightarrow> \<exists>aa ba. (a >>= b) s = ({(aa, ba)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s r s' ra s'a rb s'b. \<lbrakk>Pb' s; (r, s') \<in> fst (a s); \<not> snd (a s); a s = ({(ra, s'a)}, False); b r s' = ({(rb, s'b)}, False)\<rbrakk> \<Longrightarrow> \<exists>aa ba. (a >>= b) s = ({(aa, ba)}, False) proof (prove)
goal:
No subgoals!
theory Bisim_UL

lemma det_on_liftE [wp]:
  "det_on P m \<Longrightarrow> det_on P (liftE m)" unfolding liftE_def apply (rule det_on_guard_imp) apply (erule det_on_split [OF _ det_det_on]) apply simp apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_on P m \<Longrightarrow> det_on P (liftE m) proof (prove)
goal (1 subgoal):
 1. det_on P m \<Longrightarrow> det_on P (do r <- m;
return (Inr r)
od) proof (prove)
goal (2 subgoals):
 1. det_on P m \<Longrightarrow> det_on ?P' (do r <- m;
return (Inr r)
od)
 2. \<And>s. \<lbrakk>det_on P m; P s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>x. det (return (Inr x))
 2. \<lbrace>?Pb'3\<rbrace> m \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s. \<lbrakk>det_on P m; P s\<rbrakk> \<Longrightarrow> (P and ?Pb'3) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Pb'3\<rbrace> m \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>s. \<lbrakk>det_on P m; P s\<rbrakk> \<Longrightarrow> (P and ?Pb'3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>det_on P m; P s\<rbrakk> \<Longrightarrow> (P and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!