theory Ipc_IF

lemma ensure_no_children_rev:
  "reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag (fst slot)))
                        (ensure_no_children slot)" unfolding ensure_no_children_def fun_app_def equiv_valid_def2 apply (rule equiv_valid_rv_guard_imp) apply (rule_tac Q="\<lambda> rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s"
                in equiv_valid_rv_liftE_bindE[OF equiv_valid_rv_guard_imp[OF gets_cdt_revrv']]) apply (rule TrueI) apply (clarsimp simp: equiv_valid_2_def) apply (drule reads_equiv_cdt_has_children) apply assumption apply assumption apply (fastforce elim: reads_equivE) apply (fastforce simp: in_whenE in_throwError) apply (wp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag (fst slot))) (ensure_no_children slot) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv A aag (=) (pas_refined aag and K (is_subject aag (fst slot))) (doE cdt <- liftE (gets cdt);
whenE (\<exists>c. cdt c = Some slot) (throwError RevokeFirst)
odE) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv A aag (=) ?P (doE cdt <- liftE (gets cdt);
whenE (\<exists>c. cdt c = Some slot) (throwError RevokeFirst)
odE)
 2. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P s proof (prove)
goal (4 subgoals):
 1. \<And>s. ?P s \<Longrightarrow> True
 2. \<And>rv rv'. equiv_for (aag_can_read aag \<circ> fst) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) A A (=) (\<lambda>s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s) (\<lambda>s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv' = cdt s) (whenE (\<exists>c. rv c = Some slot) (throwError RevokeFirst)) (whenE (\<exists>c. rv' c = Some slot) (throwError RevokeFirst))
 3. \<lbrace>?P\<rbrace> gets cdt \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s\<rbrace>
 4. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P s proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. equiv_for (aag_can_read aag \<circ> fst) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) A A (=) (\<lambda>s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s) (\<lambda>s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv' = cdt s) (whenE (\<exists>c. rv c = Some slot) (throwError RevokeFirst)) (whenE (\<exists>c. rv' c = Some slot) (throwError RevokeFirst))
 2. \<lbrace>?P\<rbrace> gets cdt \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s\<rbrace>
 3. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P s proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag s; pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv aag b ba \<and> A b ba
 2. \<lbrace>?P\<rbrace> gets cdt \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s\<rbrace>
 3. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P s proof (prove)
goal (6 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t\<rbrakk> \<Longrightarrow> pas_refined aag (?s'30 s t a b aa ba)
 2. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t\<rbrakk> \<Longrightarrow> is_subject aag (fst (?slot30 s t a b aa ba))
 3. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag \<circ> fst) cdt s (?s'30 s t a b aa ba)
 4. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t; (\<exists>c. cdt s c = Some (?slot30 s t a b aa ba)) = (\<exists>c. cdt (?s'30 s t a b aa ba) c = Some (?slot30 s t a b aa ba))\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv aag b ba \<and> A b ba
 5. \<lbrace>?P\<rbrace> gets cdt \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s\<rbrace>
 6. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P s proof (prove)
goal (5 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t\<rbrakk> \<Longrightarrow> is_subject aag (fst (?slot30 s t a b aa ba))
 2. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag \<circ> fst) cdt s t
 3. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t; (\<exists>c. cdt s c = Some (?slot30 s t a b aa ba)) = (\<exists>c. cdt t c = Some (?slot30 s t a b aa ba))\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv aag b ba \<and> A b ba
 4. \<lbrace>?P\<rbrace> gets cdt \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s\<rbrace>
 5. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P s proof (prove)
goal (4 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag \<circ> fst) cdt s t
 2. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t; (\<exists>c. cdt s c = Some slot) = (\<exists>c. cdt t c = Some slot)\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv aag b ba \<and> A b ba
 3. \<lbrace>?P\<rbrace> gets cdt \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s\<rbrace>
 4. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P s proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t); (a, b) \<in> fst (whenE (\<exists>a b. cdt s (a, b) = Some slot) (throwError RevokeFirst) s); (aa, ba) \<in> fst (whenE (\<exists>a b. cdt t (a, b) = Some slot) (throwError RevokeFirst) t); pas_refined aag t; is_subject aag (fst slot); reads_equiv aag s t; A s t; (\<exists>c. cdt s c = Some slot) = (\<exists>c. cdt t c = Some slot)\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv aag b ba \<and> A b ba
 2. \<lbrace>?P\<rbrace> gets cdt \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s\<rbrace>
 3. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P\<rbrace> gets cdt \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s\<rbrace>
 2. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P s proof (prove)
goal:
No subgoals!