kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_S

lemma bisim_validE_R2:
  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 validE_def validE_R_def by (fastforce simp: split_def split: sum.splits)

(* 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 (=) 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). case r of Inl e \<Rightarrow> True | Inr r \<Rightarrow> S r s')

goal (1 subgoal):
 1. \<forall>s. (P and P' and Q) s \<longrightarrow> (\<forall>(r, s')\<in>fst (a s). case r of Inl e \<Rightarrow> True | Inr r \<Rightarrow> S r s')
theory Syscall_S

lemma get_cap_wp':
  "\<lbrace>\<lambda>s. \<forall>cap. caps_of_state s p = Some cap \<longrightarrow> Q cap s\<rbrace> get_cap p \<lbrace>Q\<rbrace>" apply (wp get_cap_wp) apply (simp add: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap. caps_of_state s p = Some cap \<longrightarrow> Q cap s\<rbrace> get_cap p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>cap. caps_of_state s p = Some cap \<longrightarrow> Q cap s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> Q cap s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma lc_sep [wp]:
  "\<lbrace>separate_state and valid_objs \<rbrace> lookup_cap tcb cptr \<lbrace>\<lambda>cap _. separate_cap cap\<rbrace>, -" unfolding lookup_cap_def apply (simp add: split_def) apply (rule hoare_pre) apply (wp get_cap_wp' lsft_sep) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and valid_objs\<rbrace> lookup_cap tcb cptr \<lbrace>\<lambda>cap _. separate_cap cap\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and valid_objs\<rbrace> doE (ref', uu_) <- lookup_slot_for_thread tcb cptr;
liftE $ get_cap ref'
odE \<lbrace>\<lambda>cap _. separate_cap cap\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and valid_objs\<rbrace> doE p <- lookup_slot_for_thread tcb cptr;
liftE (get_cap (fst p))
odE \<lbrace>\<lambda>cap _. separate_cap cap\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE p <- lookup_slot_for_thread tcb cptr;
liftE (get_cap (fst p))
odE \<lbrace>\<lambda>cap _. separate_cap cap\<rbrace>, -
 2. \<And>s. (separate_state and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (separate_state and valid_objs) s \<Longrightarrow> True \<and> (separate_state and valid_objs) s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma not_empty_thread_get [wp]:
  "not_empty (tcb_at p) (thread_get f p)" unfolding thread_get_def apply (rule not_empty_guard_imp) apply (simp add: gets_the_def bind_assoc) apply wp apply (simp add: tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at p) (thread_get f p) proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at p) (do tcb <- gets_the $ get_tcb p;
return $ f tcb
od) proof (prove)
goal (2 subgoals):
 1. not_empty ?P' (do tcb <- gets_the $ get_tcb p;
return $ f tcb
od)
 2. \<And>s. tcb_at p s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. not_empty ?P' (do x <- gets (get_tcb p);
tcb <- assert_opt x;
return (f tcb)
od)
 2. \<And>s. tcb_at p s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at p s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. get_tcb p s \<noteq> None) and (\<lambda>sa. get_tcb p s \<noteq> None \<longrightarrow> True)) s)) s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma not_empty_throwError [wp]:
  "not_empty \<top> (throwError e)" unfolding not_empty_def throwError_def by (fastforce simp: return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>_. True) (throwError e) proof (prove)
goal (1 subgoal):
 1. \<forall>s. True \<longrightarrow> fst ((return \<circ> Inl) e s) \<noteq> {}
theory Syscall_S

lemma not_empty_cap_fault_on_failure [wp]:
  assumes d: "not_empty P m"
  shows "not_empty P (cap_fault_on_failure a b m)" unfolding cap_fault_on_failure_def apply (simp add: handleE_def handleE'_def) apply (rule not_empty_guard_imp) apply (wp d | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty P (cap_fault_on_failure a b m) proof (prove)
goal (1 subgoal):
 1. not_empty P (m <handle2> throwError \<circ> CapFault a b) proof (prove)
goal (1 subgoal):
 1. not_empty P (do v <- m;
case v of Inl e \<Rightarrow> (throwError \<circ> CapFault a b) e | Inr v' \<Rightarrow> return (Inr v')
od) proof (prove)
goal (2 subgoals):
 1. not_empty ?P' (do v <- m;
case v of Inl e \<Rightarrow> (throwError \<circ> CapFault a b) e | Inr v' \<Rightarrow> return (Inr v')
od)
 2. \<And>s. P s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma not_empty_splitE [wp_split]:
  assumes da: "not_empty Pa a"
  and     db: "\<And>x. not_empty (Pb x) (b x)"
  and      v: "\<lbrace>Pb'\<rbrace> a \<lbrace>Pb\<rbrace>, -"
  shows "not_empty (Pa and Pb') (a >>=E b)" using v apply (clarsimp simp: bindE_def validE_R_def validE_def) apply (rule not_empty_split [OF da]) apply (rule not_empty_lift [OF db]) apply (erule hoare_post_imp [rotated]) apply (clarsimp split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (Pa and Pb') (a >>=E b) proof (prove)
using this:
\<lbrace>Pb'\<rbrace> a \<lbrace>Pb\<rbrace>, -

goal (1 subgoal):
 1. not_empty (Pa and Pb') (a >>=E b) proof (prove)
goal (1 subgoal):
 1. \<lbrace>Pb'\<rbrace> a \<lbrace>\<lambda>v s. \<forall>r. v = Inr r \<longrightarrow> Pb r s\<rbrace> \<Longrightarrow> not_empty (Pa and Pb') (a >>= lift b) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>Pb'\<rbrace> a \<lbrace>\<lambda>v s. \<forall>r. v = Inr r \<longrightarrow> Pb r s\<rbrace> \<Longrightarrow> not_empty (?Pb4 x) (lift b x)
 2. \<lbrace>Pb'\<rbrace> a \<lbrace>\<lambda>v s. \<forall>r. v = Inr r \<longrightarrow> Pb r s\<rbrace> \<Longrightarrow> \<lbrace>Pb'\<rbrace> a \<lbrace>?Pb4\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Pb'\<rbrace> a \<lbrace>\<lambda>v s. \<forall>r. v = Inr r \<longrightarrow> Pb r s\<rbrace> \<Longrightarrow> \<lbrace>Pb'\<rbrace> a \<lbrace>\<lambda>x. case x of Inl uu_ \<Rightarrow> \<lambda>_. True | Inr y \<Rightarrow> Pb y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>r. rv = Inr r \<longrightarrow> Pb r s \<Longrightarrow> (case rv of Inl uu_ \<Rightarrow> \<lambda>_. True | Inr y \<Rightarrow> Pb y) s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma not_empty_whenE_throwError [wp]:
  "not_empty \<top> (whenE P (throwError e))" by (simp add: whenE_def throwError_def return_def not_empty_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>_. True) (whenE P (throwError e))
theory Syscall_S

lemma not_empty_returnOk [wp]:
  "not_empty \<top> (returnOk v)" by (simp add: return_def not_empty_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>_. True) (returnOk v)
theory Syscall_S

lemma not_empty_if [wp_split]:
  "\<lbrakk> not_empty Pt m; not_empty Pf m' \<rbrakk> \<Longrightarrow> not_empty (\<lambda>s. (b \<longrightarrow> Pt s) \<and> ( \<not> b \<longrightarrow> Pf s)) (if b then m else m')" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>not_empty Pt m; not_empty Pf m'\<rbrakk> \<Longrightarrow> not_empty (\<lambda>s. (b \<longrightarrow> Pt s) \<and> (\<not> b \<longrightarrow> Pf s)) (if b then m else m')
theory Syscall_S

lemma not_empty_lsft:
  shows "not_empty (tcb_at t and valid_objs and separate_state) (lookup_slot_for_thread t cptr)" unfolding lookup_slot_for_thread_def apply (simp add: gets_the_def bind_assoc) apply (rule not_empty_guard_imp) apply (wp bisim_not_empty [OF bisim_rab] | wpc)+ apply (fastforce simp: tcb_at_def elim: separate_cnode_capE dest: separate_state_get_tcbD objs_valid_tcb_ctable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at t and valid_objs and separate_state) (lookup_slot_for_thread t cptr) proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at t and valid_objs and separate_state) (doE tcb <- liftE $ gets_the $ get_tcb t;
resolve_address_bits (tcb_ctable tcb, cptr)
odE) proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at t and valid_objs and separate_state) (doE tcb <- liftE (gets (get_tcb t) >>= assert_opt);
resolve_address_bits (tcb_ctable tcb, cptr)
odE) proof (prove)
goal (2 subgoals):
 1. not_empty ?P' (doE tcb <- liftE (gets (get_tcb t) >>= assert_opt);
resolve_address_bits (tcb_ctable tcb, cptr)
odE)
 2. \<And>s. (tcb_at t and valid_objs and separate_state) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at t and valid_objs and separate_state) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. get_tcb t s \<noteq> None) and (\<lambda>s. get_tcb t s \<noteq> None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>sa. separate_cnode_cap (caps_of_state sa) (tcb_ctable (the (get_tcb t s))) \<and> sa \<turnstile> tcb_ctable (the (get_tcb t s))) and ((\<lambda>_. True) and (\<lambda>sa. (tcb_ctable (the (get_tcb t s)) = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. tcb_ctable (the (get_tcb t s)) = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb t s)) = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb t s)) = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb t s)) = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb t s)) = CNodeCap x xa xb \<longrightarrow> (xb \<le> cptr \<longrightarrow> True) \<and> (\<not> xb \<le> cptr \<longrightarrow> True)) \<and> (\<forall>x. tcb_ctable (the (get_tcb t s)) = ThreadCap x \<longrightarrow> True) \<and> (tcb_ctable (the (get_tcb t s)) = DomainCap \<longrightarrow> True) \<and> (tcb_ctable (the (get_tcb t s)) = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. tcb_ctable (the (get_tcb t s)) = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb t s)) = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. tcb_ctable (the (get_tcb t s)) = ArchObjectCap x \<longrightarrow> True)))) s)) s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma not_empty_get_cap [wp]:
  "not_empty (cte_at p) (get_cap p)" unfolding not_empty_def by (clarsimp simp: cte_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (cte_wp_at (\<lambda>_. True) p) (get_cap p) proof (prove)
goal (1 subgoal):
 1. \<forall>s. cte_wp_at (\<lambda>_. True) p s \<longrightarrow> fst (get_cap p s) \<noteq> {}
theory Syscall_S

lemma not_empty_lc:
  shows "not_empty (tcb_at t and valid_objs and separate_state) (lookup_cap t cptr)" unfolding lookup_cap_def apply (simp add: split_def) apply (rule not_empty_guard_imp) apply (wp not_empty_lsft) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at t and valid_objs and separate_state) (lookup_cap t cptr) proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at t and valid_objs and separate_state) (doE (ref', uu_) <- lookup_slot_for_thread t cptr;
liftE $ get_cap ref'
odE) proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at t and valid_objs and separate_state) (doE p <- lookup_slot_for_thread t cptr;
liftE (get_cap (fst p))
odE) proof (prove)
goal (2 subgoals):
 1. not_empty ?P' (doE p <- lookup_slot_for_thread t cptr;
liftE (get_cap (fst p))
odE)
 2. \<And>s. (tcb_at t and valid_objs and separate_state) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at t and valid_objs and separate_state) s \<Longrightarrow> (tcb_at t and valid_objs and separate_state and valid_objs) s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma not_empty_get [wp]:
  "not_empty \<top> get" unfolding not_empty_def get_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>_. True) get proof (prove)
goal (1 subgoal):
 1. \<forall>s. True \<longrightarrow> fst ({(s, s)}, False) \<noteq> {}
theory Syscall_S

lemma not_empty_put [wp]:
  "not_empty \<top> (put s)" unfolding not_empty_def put_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>_. True) (put s) proof (prove)
goal (1 subgoal):
 1. \<forall>sa. True \<longrightarrow> fst ({((), s)}, False) \<noteq> {}
theory Syscall_S

lemma not_empty_assert [wp]:
  "not_empty (\<lambda>s. C) (assert C)" by (clarsimp simp: assert_def not_empty_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>s. C) (assert C)
theory Syscall_S

lemma not_empty_get_object [wp]:
  "not_empty (\<lambda>s. kheap s p \<noteq> None) (get_object p)" unfolding get_object_def apply (rule not_empty_guard_imp) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>s. kheap s p \<noteq> None) (get_object p) proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>s. kheap s p \<noteq> None) (do kh <- gets kheap;
assert (kh p \<noteq> None);
return $ the $ kh p
od) proof (prove)
goal (2 subgoals):
 1. not_empty ?P' (do kh <- gets kheap;
assert (kh p \<noteq> None);
return $ the $ kh p
od)
 2. \<And>s. kheap s p \<noteq> None \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma not_empty_assert_opt [wp]:
  "not_empty (\<lambda>_. v \<noteq> None) (assert_opt v)" unfolding not_empty_def assert_opt_def by (clarsimp simp: return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>_. v \<noteq> None) (assert_opt v) proof (prove)
goal (1 subgoal):
 1. \<forall>s. v \<noteq> None \<longrightarrow> fst ((case v of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) \<noteq> {}
theory Syscall_S

lemma not_empty_thread_set [wp]:
  "not_empty (tcb_at p) (thread_set f p)" unfolding thread_set_def apply (simp add: gets_the_def bind_assoc) apply (rule not_empty_guard_imp) apply wp apply (clarsimp simp: tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at p) (thread_set f p) proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at p) (do tcb <- gets_the $ get_tcb p;
set_object p $ TCB $ f tcb
od) proof (prove)
goal (1 subgoal):
 1. not_empty (tcb_at p) (do x <- gets (get_tcb p);
tcb <- assert_opt x;
set_object p (TCB (f tcb))
od) proof (prove)
goal (2 subgoals):
 1. not_empty ?P' (do x <- gets (get_tcb p);
tcb <- assert_opt x;
set_object p (TCB (f tcb))
od)
 2. \<And>s. tcb_at p s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at p s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. get_tcb p s \<noteq> None) and (\<lambda>sa. get_tcb p s \<noteq> None \<longrightarrow> typ_at (a_type (TCB (f (the (get_tcb p s))))) p sa)) s)) s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma not_empty_False:
  "not_empty (\<lambda>_. False) m" unfolding not_empty_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (\<lambda>_. False) m proof (prove)
goal (1 subgoal):
 1. \<forall>s. False \<longrightarrow> fst (m s) \<noteq> {}
theory Syscall_S

lemma not_empty_gen_asm:
  assumes ne: "P \<Longrightarrow> not_empty R m"
  shows "not_empty (R and (\<lambda>_. P)) m" using ne unfolding not_empty_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (R and (\<lambda>_. P)) m proof (prove)
using this:
P \<Longrightarrow> not_empty R m

goal (1 subgoal):
 1. not_empty (R and (\<lambda>_. P)) m proof (prove)
using this:
P \<Longrightarrow> \<forall>s. R s \<longrightarrow> fst (m s) \<noteq> {}

goal (1 subgoal):
 1. \<forall>s. (R and (\<lambda>_. P)) s \<longrightarrow> fst (m s) \<noteq> {}
theory Syscall_S

lemma handle_fault_bisim:
  "bisim (=) \<top> (separate_state and tcb_at tcb and valid_objs) (handle_fault tcb flt) (Ipc_A.handle_fault tcb flt')" unfolding handle_fault_def Ipc_A.handle_fault_def apply (rule bisim_guard_imp) apply (rule bisim_symb_exec_r [where Pe = \<top>]) apply simp apply (rule send_fault_ipc_bisim) apply (wpsimp simp: gets_the_def tcb_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (separate_state and tcb_at tcb and valid_objs) (Ipc_SA.handle_fault tcb flt) (Ipc_A.handle_fault tcb flt') proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (separate_state and tcb_at tcb and valid_objs) (set_thread_state tcb Inactive) (do _ <- gets_the $ get_tcb tcb;
send_fault_ipc tcb flt' <catch> handle_double_fault tcb flt';
return ()
od) proof (prove)
goal (3 subgoals):
 1. bisim (=) ?Q ?Q' (set_thread_state tcb Inactive) (do _ <- gets_the $ get_tcb tcb;
send_fault_ipc tcb flt' <catch> handle_double_fault tcb flt';
return ()
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (separate_state and tcb_at tcb and valid_objs) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>uu_. bisim (=) ?Q (?Q'4 uu_) (set_thread_state tcb Inactive) (do send_fault_ipc tcb flt' <catch> handle_double_fault tcb flt';
return ()
od)
 2. \<lbrace>?P'4\<rbrace> gets_the $ get_tcb tcb \<lbrace>?Q'4\<rbrace>
 3. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> gets_the $ get_tcb tcb \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. not_empty ?Pd4 (gets_the $ get_tcb tcb)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. (separate_state and tcb_at tcb and valid_objs) s \<Longrightarrow> (?P'4 and (\<lambda>_. True) and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. \<And>uu_. bisim (=) ?Q (?Q'4 uu_) (set_thread_state tcb Inactive) (send_fault_ipc tcb flt' <catch> handle_double_fault tcb flt')
 2. \<lbrace>?P'4\<rbrace> gets_the $ get_tcb tcb \<lbrace>?Q'4\<rbrace>
 3. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> gets_the $ get_tcb tcb \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. not_empty ?Pd4 (gets_the $ get_tcb tcb)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. (separate_state and tcb_at tcb and valid_objs) s \<Longrightarrow> (?P'4 and (\<lambda>_. True) and ?Pd4) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'4\<rbrace> gets_the $ get_tcb tcb \<lbrace>\<lambda>_. tcb_at tcb and valid_objs and separate_state\<rbrace>
 2. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> gets_the $ get_tcb tcb \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. not_empty ?Pd4 (gets_the $ get_tcb tcb)
 4. \<And>s. True \<Longrightarrow> True
 5. \<And>s. (separate_state and tcb_at tcb and valid_objs) s \<Longrightarrow> (?P'4 and (\<lambda>_. True) and ?Pd4) s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma bisim_returnOk:
  "R a b \<Longrightarrow> bisim (f \<oplus> R) \<top> \<top> (returnOk a) (returnOk b)" apply (simp add: returnOk_def) apply (rule bisim_return) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R a b \<Longrightarrow> bisim (f \<oplus> R) (\<lambda>_. True) (\<lambda>_. True) (returnOk a) (returnOk b) proof (prove)
goal (1 subgoal):
 1. R a b \<Longrightarrow> bisim (f \<oplus> R) (\<lambda>_. True) (\<lambda>_. True) (return (Inr a)) (return (Inr b)) proof (prove)
goal (1 subgoal):
 1. R a b \<Longrightarrow> (f \<oplus> R) (Inr a) (Inr b) proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma bisim_liftME_same:
  assumes bs: "bisim (f \<oplus> (=)) P P' m m'"
  shows "bisim (f \<oplus> (=)) P P' (liftME g m) (liftME g m')" unfolding liftME_def apply (rule bisim_guard_imp) apply (rule bisim_splitE [OF bs]) apply simp apply (rule bisim_returnOk) apply simp apply wp apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (f \<oplus> (=)) P P' (liftME g m) (liftME g m') proof (prove)
goal (1 subgoal):
 1. bisim (f \<oplus> (=)) P P' (doE x <- m;
returnOk (g x)
odE) (doE x <- m';
returnOk (g x)
odE) proof (prove)
goal (3 subgoals):
 1. bisim (f \<oplus> (=)) ?Q ?Q' (doE x <- m;
returnOk (g x)
odE) (doE x <- m';
returnOk (g x)
odE)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. P' s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>r r'. r = r' \<Longrightarrow> bisim (f \<oplus> (=)) (?Q4 r) (?Q'4 r') (returnOk (g r)) (returnOk (g r'))
 2. \<lbrace>?S4\<rbrace> m \<lbrace>?Q4\<rbrace>, -
 3. \<lbrace>?S'4\<rbrace> m' \<lbrace>?Q'4\<rbrace>, -
 4. \<And>s. P s \<Longrightarrow> (P and ?S4) s
 5. \<And>s. P' s \<Longrightarrow> (P' and ?S'4) s proof (prove)
goal (5 subgoals):
 1. \<And>r. bisim (f \<oplus> (=)) (?Q4 r) (?Q'4 r) (returnOk (g r)) (returnOk (g r))
 2. \<lbrace>?S4\<rbrace> m \<lbrace>?Q4\<rbrace>, -
 3. \<lbrace>?S'4\<rbrace> m' \<lbrace>?Q'4\<rbrace>, -
 4. \<And>s. P s \<Longrightarrow> (P and ?S4) s
 5. \<And>s. P' s \<Longrightarrow> (P' and ?S'4) s proof (prove)
goal (5 subgoals):
 1. \<And>r. g r = g r
 2. \<lbrace>?S4\<rbrace> m \<lbrace>\<lambda>r _. True\<rbrace>, -
 3. \<lbrace>?S'4\<rbrace> m' \<lbrace>\<lambda>r _. True\<rbrace>, -
 4. \<And>s. P s \<Longrightarrow> (P and ?S4) s
 5. \<And>s. P' s \<Longrightarrow> (P' and ?S'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?S4\<rbrace> m \<lbrace>\<lambda>r _. True\<rbrace>, -
 2. \<lbrace>?S'4\<rbrace> m' \<lbrace>\<lambda>r _. True\<rbrace>, -
 3. \<And>s. P s \<Longrightarrow> (P and ?S4) s
 4. \<And>s. P' s \<Longrightarrow> (P' and ?S'4) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?S'4\<rbrace> m' \<lbrace>\<lambda>r _. True\<rbrace>, -
 2. \<And>s. P s \<Longrightarrow> (P and (\<lambda>_. True)) s
 3. \<And>s. P' s \<Longrightarrow> (P' and ?S'4) s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma bisim_split_if:
  "\<lbrakk> P \<Longrightarrow> bisim R Pt Pt' a a'; \<not> P \<Longrightarrow> bisim R Pf Pf' b b' \<rbrakk> \<Longrightarrow>
     bisim R (\<lambda>s. (P \<longrightarrow> Pt s) \<and> (\<not> P \<longrightarrow> Pf s)) (\<lambda>s. (P \<longrightarrow> Pt' s) \<and> (\<not> P \<longrightarrow> Pf' s))
                                               (if P then a else b) (if P then a' else b')" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> bisim R Pt Pt' a a'; \<not> P \<Longrightarrow> bisim R Pf Pf' b b'\<rbrakk> \<Longrightarrow> bisim R (\<lambda>s. (P \<longrightarrow> Pt s) \<and> (\<not> P \<longrightarrow> Pf s)) (\<lambda>s. (P \<longrightarrow> Pt' s) \<and> (\<not> P \<longrightarrow> Pf' s)) (if P then a else b) (if P then a' else b')
theory Syscall_S

lemma bisim_reflE:
  "bisim ((=) \<oplus> (=)) \<top> \<top> a a" apply (rule bisim_underlyingI) apply (case_tac r, fastforce+)[1] apply (case_tac r', fastforce+)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim ((=) \<oplus> (=)) (\<lambda>_. True) (\<lambda>_. True) a a proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>s = s'; True; True; (r, t) \<in> fst (a s)\<rbrakk> \<Longrightarrow> \<exists>(r', t')\<in>fst (a s'). ((=) \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s s' r' t'. \<lbrakk>s = s'; True; True; (r', t') \<in> fst (a s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). ((=) \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>s = s'; True; True; (r', t') \<in> fst (a s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). ((=) \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal:
No subgoals!