kings-crown/FVELER_Isabelle huggingface dataset:
theory Bisim_UL

lemma det_on_lift [wp]:
  "(\<And>y. det_on (P y) (m y)) \<Longrightarrow> det_on (case_sum (\<lambda>_. \<top>) P x) (lift m x)" unfolding lift_def by (auto simp: det_on_def throwError_def return_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>y. det_on (P y) (m y)) \<Longrightarrow> det_on (case x of Inl uu_ \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> P x) (lift m x) proof (prove)
goal (1 subgoal):
 1. (\<And>y. det_on (P y) (m y)) \<Longrightarrow> det_on (case x of Inl uu_ \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> P x) (case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> m v')
theory Bisim_UL

lemma det_on_assert_opt [wp]:
  "det_on (\<lambda>_. x \<noteq> None) (assert_opt x)" unfolding det_on_def assert_opt_def by (fastforce split: option.splits simp: fail_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_on (\<lambda>_. x \<noteq> None) (assert_opt x) proof (prove)
goal (1 subgoal):
 1. \<forall>s. x \<noteq> None \<longrightarrow> (\<exists>r. (case x of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s = ({r}, False))
theory Bisim_UL

lemma wpc_helper_det_on:
  "det_on Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (det_on P f)" apply (clarsimp simp: wpc_helper_def det_on_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_on Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (det_on P f) proof (prove)
goal:
No subgoals!
theory Bisim_UL

lemma not_emptyE:
  "\<lbrakk> not_empty P f; P s; \<And>r s'. \<lbrakk> (r, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" unfolding not_empty_def by fastforce

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

lemma not_empty_guard_imp [wp_comb]:
  assumes da: "not_empty P' a"
  and   "\<And>s. P s \<Longrightarrow> P' s"
  shows "not_empty P a" using assms unfolding not_empty_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty P a proof (prove)
using this:
not_empty P' a
P ?s \<Longrightarrow> P' ?s

goal (1 subgoal):
 1. not_empty P a proof (prove)
using this:
\<forall>s. P' s \<longrightarrow> fst (a s) \<noteq> {}
P ?s \<Longrightarrow> P' ?s

goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> fst (a s) \<noteq> {}
theory Bisim_UL

lemma not_empty_split [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 >>= b)" unfolding not_empty_def using da apply - apply clarsimp apply (erule (1) not_emptyE) apply (frule (1) use_valid [OF _ v]) apply (erule not_emptyE [OF da]) apply (erule not_emptyE [OF db]) apply (fastforce simp: bind_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (Pa and Pb') (a >>= b) proof (prove)
goal (1 subgoal):
 1. \<forall>s. (Pa and Pb') s \<longrightarrow> fst ((a >>= b) s) \<noteq> {} proof (prove)
using this:
not_empty Pa a

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

lemma not_empty_return [wp]:
  "not_empty \<top> (return x)" unfolding not_empty_def by (simp add: return_def)

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

lemma not_empty_liftE [wp]:
  assumes ne: "not_empty P m"
  shows "not_empty P (liftE m)" unfolding liftE_def apply (rule not_empty_guard_imp) apply (wp ne) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty P (liftE m) proof (prove)
goal (1 subgoal):
 1. not_empty P (do r <- m;
return (Inr r)
od) proof (prove)
goal (2 subgoals):
 1. not_empty ?P' (do r <- m;
return (Inr r)
od)
 2. \<And>s. P s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (P and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!
theory Bisim_UL

lemma not_empty_lift [wp]:
  "(\<And>y. not_empty (P y) (m y)) \<Longrightarrow> not_empty (case_sum (\<lambda>_. \<top>) P x) (lift m x)" unfolding lift_def by (auto simp: not_empty_def throwError_def return_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>y. not_empty (P y) (m y)) \<Longrightarrow> not_empty (case x of Inl uu_ \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> P x) (lift m x) proof (prove)
goal (1 subgoal):
 1. (\<And>y. not_empty (P y) (m y)) \<Longrightarrow> not_empty (case x of Inl uu_ \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> P x) (case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> m v')
theory Bisim_UL

lemma not_empty_assert_opt [wp]:
  "not_empty (\<lambda>_. x \<noteq> None) (assert_opt x)" unfolding not_empty_def assert_opt_def by (fastforce split: option.splits simp: fail_def return_def)

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

lemma not_empty_gets [wp]:
  "not_empty \<top> (gets f)" unfolding not_empty_def by (clarsimp simp: gets_def return_def bind_def get_def)

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

lemma wpc_helper_not_empty:
  "not_empty Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (not_empty P f)" apply (clarsimp simp: wpc_helper_def not_empty_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (not_empty P f) proof (prove)
goal:
No subgoals!
theory Bisim_UL

lemma bisim_not_empty:
  assumes bs: "bisim r P P' m m'"
  and     ne: "not_empty R m"
  shows   "not_empty (P and P' and R) m'" unfolding not_empty_def using bs ne apply clarsimp apply (erule (1) not_emptyE) apply (erule_tac s=s and s'=s in bisim_underlyingE1 [where SR = "(=)"]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_empty (P and P' and R) m' proof (prove)
goal (1 subgoal):
 1. \<forall>s. (P and P' and R) s \<longrightarrow> fst (m' s) \<noteq> {} proof (prove)
using this:
bisim r P P' m m'
not_empty R m

goal (1 subgoal):
 1. \<forall>s. (P and P' and R) s \<longrightarrow> fst (m' s) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>bisim r P P' m m'; not_empty R m; P s; P' s; R s; fst (m' s) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ra s'. \<lbrakk>bisim r P P' m m'; P s; P' s; R s; fst (m' s) = {}; (ra, s') \<in> fst (m s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s r s'. \<lbrakk>P s; P' s; R s; fst (m' s) = {}; (r, s') \<in> fst (m s)\<rbrakk> \<Longrightarrow> s = s
 2. \<And>s r s'. \<lbrakk>P s; P' s; R s; fst (m' s) = {}; (r, s') \<in> fst (m s)\<rbrakk> \<Longrightarrow> P s
 3. \<And>s r s'. \<lbrakk>P s; P' s; R s; fst (m' s) = {}; (r, s') \<in> fst (m s)\<rbrakk> \<Longrightarrow> P' s
 4. \<And>s r s'. \<lbrakk>P s; P' s; R s; fst (m' s) = {}; (r, s') \<in> fst (m s)\<rbrakk> \<Longrightarrow> (?r11 s r s', ?t11 s r s') \<in> fst (m s)
 5. \<And>s ra s' r' t'. \<lbrakk>P s; P' s; R s; fst (m' s) = {}; (ra, s') \<in> fst (m s); (r', t') \<in> fst (m' s); r (?r11 s ra s') r'; ?t11 s ra s' = t'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Bisim_UL

lemma bisim_symb_exec_r_bs:
  assumes bs: "bisim (=) R R' (return ()) m"
  and      z: "\<And>rv. bisim r P P' x (y rv)"
  shows      "bisim r (P and R and P') R' x (m >>= (\<lambda>rv. y rv))" apply (rule bisim_guard_imp) apply (subst return_bind [symmetric, where f = "\<lambda>(_ :: unit).x"],  rule bisim_split_req) apply (rule bs) apply (rule z) apply wp apply simp apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim r (P and R and P') R' x (m >>= y) proof (prove)
goal (3 subgoals):
 1. bisim r ?Q ?Q' x (m >>= y)
 2. \<And>s. (P and R and P') s \<Longrightarrow> ?Q s
 3. \<And>s. R' s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. bisim (=) ?P7 ?Q' (return ?x5) m
 2. \<And>ra. bisim r (?Q7 ra) (?Q'7 ra) x (y ra)
 3. \<lbrace>?S7\<rbrace> return ?x5 \<lbrace>\<lambda>r. ?Q7 r and ?Q'7 r\<rbrace>
 4. \<And>s. (P and R and P') s \<Longrightarrow> (?P7 and ?S7) s
 5. \<And>s. R' s \<Longrightarrow> ?Q' s proof (prove)
goal (4 subgoals):
 1. \<And>ra. bisim r (?Q7 ra) (?Q'7 ra) x (y ra)
 2. \<lbrace>?S7\<rbrace> return () \<lbrace>\<lambda>r. ?Q7 r and ?Q'7 r\<rbrace>
 3. \<And>s. (P and R and P') s \<Longrightarrow> (R and ?S7) s
 4. \<And>s. R' s \<Longrightarrow> R' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?S7\<rbrace> return () \<lbrace>\<lambda>r. P and P'\<rbrace>
 2. \<And>s. (P and R and P') s \<Longrightarrow> (R and ?S7) s
 3. \<And>s. R' s \<Longrightarrow> R' s proof (prove)
goal (2 subgoals):
 1. \<And>s. (P and R and P') s \<Longrightarrow> (R and (P and P')) s
 2. \<And>s. R' s \<Longrightarrow> R' s proof (prove)
goal (1 subgoal):
 1. \<And>s. R' s \<Longrightarrow> R' s proof (prove)
goal:
No subgoals!
theory Separation

lemma separate_capE:
  "\<lbrakk> separate_cap cap; cap = NullCap \<Longrightarrow> R; \<And>ptr badge rights. \<lbrakk> cap = NotificationCap ptr badge rights \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" unfolding separate_cap_def by (fastforce split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>separate_cap cap; cap = NullCap \<Longrightarrow> R; \<And>ptr badge rights. cap = NotificationCap ptr badge rights \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case cap of NullCap \<Rightarrow> True | NotificationCap ptr badge rights \<Rightarrow> rights \<subseteq> {AllowRecv, AllowSend} | _ \<Rightarrow> False; cap = NullCap \<Longrightarrow> R; \<And>ptr badge rights. cap = NotificationCap ptr badge rights \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Separation

lemma separate_cnode_cap_rab:
  "\<lbrakk> separate_cnode_cap cs cap; length cref = word_bits \<rbrakk> \<Longrightarrow>
  resolve_address_bits (cap, cref) = (case cap of
                                         CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then
                                                                     returnOk ((p, drop (length guard) cref), [])
                                                                 else
                                                                     (throwError (GuardMismatch (length cref) guard))
                                       | _ \<Rightarrow> throwError InvalidRoot)" unfolding separate_cnode_cap_def resolve_address_bits_def by (auto simp: word_bits_def resolve_address_bits'.simps split: cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>separate_cnode_cap cs cap; length cref = word_bits\<rbrakk> \<Longrightarrow> resolve_address_bits (cap, cref) = (case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, drop (length guard) cref), []) else throwError (GuardMismatch (length cref) guard) | _ \<Rightarrow> throwError InvalidRoot) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case cap of NullCap \<Rightarrow> True | CNodeCap p bits guard \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case cs (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | _ \<Rightarrow> False; length cref = word_bits\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('b) (cap, cref) = (case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, drop (length guard) cref), []) else throwError (GuardMismatch (length cref) guard) | _ \<Rightarrow> throwError InvalidRoot)
theory Separation

lemma valid_sep_cap_not_cnode:
  "\<lbrakk> s \<turnstile> cap; \<forall>off cap'. caps_of_state s (p, off) = Some cap' \<longrightarrow> separate_cap cap'; cap = CNodeCap p bits guard; bits \<le> length cref - length guard \<rbrakk>
  \<Longrightarrow> \<exists>cap'. caps_of_state s (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap'" apply (clarsimp simp: valid_cap_simps not_less in_monad) apply (drule_tac offset = "take bits (drop (length guard) cref)" in cap_table_at_cte_at) apply simp apply (fastforce simp: cte_wp_at_caps_of_state separate_cap_def is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> cap; \<forall>off cap'. caps_of_state s (p, off) = Some cap' \<longrightarrow> separate_cap cap'; cap = CNodeCap p bits guard; bits \<le> length cref - length guard\<rbrakk> \<Longrightarrow> \<exists>cap'. caps_of_state s (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>off cap'. caps_of_state s (p, off) = Some cap' \<longrightarrow> separate_cap cap'; cap = CNodeCap p bits guard; bits \<le> length cref - length guard; cap_aligned (CNodeCap p bits guard); cap_table_at bits p s; 0 < bits; length guard \<le> word_bits\<rbrakk> \<Longrightarrow> \<exists>cap'. caps_of_state s (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>off cap'. caps_of_state s (p, off) = Some cap' \<longrightarrow> separate_cap cap'; cap = CNodeCap p bits guard; bits \<le> length cref - length guard; cap_aligned (CNodeCap p bits guard); 0 < bits; length guard \<le> word_bits\<rbrakk> \<Longrightarrow> length (take bits (drop (length guard) cref)) = bits
 2. \<lbrakk>\<forall>off cap'. caps_of_state s (p, off) = Some cap' \<longrightarrow> separate_cap cap'; cap = CNodeCap p bits guard; bits \<le> length cref - length guard; cap_aligned (CNodeCap p bits guard); 0 < bits; length guard \<le> word_bits; cte_wp_at (\<lambda>_. True) (p, take bits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> \<exists>cap'. caps_of_state s (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>off cap'. caps_of_state s (p, off) = Some cap' \<longrightarrow> separate_cap cap'; cap = CNodeCap p bits guard; bits \<le> length cref - length guard; cap_aligned (CNodeCap p bits guard); 0 < bits; length guard \<le> word_bits; cte_wp_at (\<lambda>_. True) (p, take bits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> \<exists>cap'. caps_of_state s (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap' proof (prove)
goal:
No subgoals!
theory Separation

lemma caps_of_state_tcb:
  "\<lbrakk> get_tcb p s = Some tcb; option_map fst (tcb_cap_cases idx) = Some getF \<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb)" apply (drule get_tcb_SomeD) apply clarsimp apply (drule (1) cte_wp_at_tcbI [where t = "(p, idx)" and P = "(=) (getF tcb)", simplified]) apply simp apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb p s = Some tcb; map_option fst (tcb_cap_cases idx) = Some getF\<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_option fst (tcb_cap_cases idx) = Some getF; kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>kheap s p = Some (TCB tcb); tcb_cap_cases idx = Some (getF, a, b)\<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb) proof (prove)
goal (2 subgoals):
 1. \<And>a b. tcb_cap_cases idx = Some (getF, a, b) \<Longrightarrow> getF tcb = getF tcb
 2. \<And>a b. \<lbrakk>tcb_cap_cases idx = Some (getF, a, b); cte_wp_at ((=) (getF tcb)) (p, idx) s\<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>tcb_cap_cases idx = Some (getF, a, b); cte_wp_at ((=) (getF tcb)) (p, idx) s\<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb) proof (prove)
goal:
No subgoals!
theory Separation

lemma caps_of_state_tcb_cap_cases:
  "\<lbrakk> get_tcb p s = Some tcb; idx \<in> dom tcb_cap_cases \<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some ((the (option_map fst (tcb_cap_cases idx))) tcb)" apply (clarsimp simp: dom_def) apply (erule caps_of_state_tcb) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb p s = Some tcb; idx \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (the (map_option fst (tcb_cap_cases idx)) tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>get_tcb p s = Some tcb; tcb_cap_cases idx = Some (a, aa, b)\<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (a tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. tcb_cap_cases idx = Some (a, aa, b) \<Longrightarrow> map_option fst (tcb_cap_cases idx) = Some a proof (prove)
goal:
No subgoals!
theory Separation

lemma separate_state_get_tcbD:
  "\<lbrakk>separate_state s; get_tcb p s = Some tcb \<rbrakk> \<Longrightarrow>
  separate_cnode_cap (caps_of_state s) (tcb_ctable tcb) \<and> tcb_caller tcb = NullCap" unfolding separate_state_def apply (drule spec [where x = p]) apply (simp add: tcb_at_def separate_tcb_def caps_of_state_tcb_cap_cases dom_tcb_cap_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>separate_state s; get_tcb p s = Some tcb\<rbrakk> \<Longrightarrow> separate_cnode_cap (caps_of_state s) (tcb_ctable tcb) \<and> tcb_caller tcb = NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s); get_tcb p s = Some tcb\<rbrakk> \<Longrightarrow> separate_cnode_cap (caps_of_state s) (tcb_ctable tcb) \<and> tcb_caller tcb = NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb p s = Some tcb; tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s)\<rbrakk> \<Longrightarrow> separate_cnode_cap (caps_of_state s) (tcb_ctable tcb) \<and> tcb_caller tcb = NullCap proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma dc_refl: "dc r r" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dc r r
theory Syscall_S

lemma bisim_catch_faults_r:
  assumes bs: "\<And>x. bisim_underlying sr r P (P' x) a (m x)"
  and    flt: "\<lbrace>S\<rbrace> b \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>P'\<rbrace>"
  and   pure: "\<And>s. \<lbrace>S' and (=) s\<rbrace> b \<lbrace>\<lambda>_. (=) s\<rbrace>"
  and     db: "not_empty Pd b"
  shows "bisim_underlying sr r P (S and S' and Pd) a (b <catch> m)" unfolding catch_def apply (rule bisim_symb_exec_r [OF _ flt [unfolded validE_def] pure db] ) apply (case_tac x) apply simp apply (rule bs) apply simp apply (rule bisim_underlyingI, simp_all)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying sr r P (S and S' and Pd) a (b <catch> m) proof (prove)
goal (1 subgoal):
 1. bisim_underlying sr r P (S and S' and Pd) a (do x <- b;
case x of Inl e \<Rightarrow> m e | Inr b \<Rightarrow> return b
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. bisim_underlying sr r P (\<lambda>s. case x of Inl e \<Rightarrow> P' e s | Inr r \<Rightarrow> False) a (case x of Inl e \<Rightarrow> m e | Inr b \<Rightarrow> return b) proof (prove)
goal (2 subgoals):
 1. \<And>x aa. x = Inl aa \<Longrightarrow> bisim_underlying sr r P (\<lambda>s. case x of Inl e \<Rightarrow> P' e s | Inr r \<Rightarrow> False) a (case x of Inl e \<Rightarrow> m e | Inr b \<Rightarrow> return b)
 2. \<And>x b. x = Inr b \<Longrightarrow> bisim_underlying sr r P (\<lambda>s. case x of Inl e \<Rightarrow> P' e s | Inr r \<Rightarrow> False) a (case x of Inl e \<Rightarrow> m e | Inr b \<Rightarrow> return b) proof (prove)
goal (2 subgoals):
 1. \<And>x aa. x = Inl aa \<Longrightarrow> bisim_underlying sr r P (P' aa) a (m aa)
 2. \<And>x b. x = Inr b \<Longrightarrow> bisim_underlying sr r P (\<lambda>s. case x of Inl e \<Rightarrow> P' e s | Inr r \<Rightarrow> False) a (case x of Inl e \<Rightarrow> m e | Inr b \<Rightarrow> return b) proof (prove)
goal (1 subgoal):
 1. \<And>x b. x = Inr b \<Longrightarrow> bisim_underlying sr r P (\<lambda>s. case x of Inl e \<Rightarrow> P' e s | Inr r \<Rightarrow> False) a (case x of Inl e \<Rightarrow> m e | Inr b \<Rightarrow> return b) proof (prove)
goal (1 subgoal):
 1. \<And>x b. x = Inr b \<Longrightarrow> bisim_underlying sr r P (\<lambda>s. False) a (return b) proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma bisim_validE_R:
  assumes ac: "bisim_underlying (=) (dc \<oplus> (=)) 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 (dc \<oplus> (=)) 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'). (dc \<oplus> (=)) r r' \<and> t = t') \<and> (\<forall>(r', t')\<in>fst (a' s'). \<exists>(r, t)\<in>fst (a s). (dc \<oplus> (=)) 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')