theory BCorres_AI

lemma get_cap_helper:
  "(fst (get_cap cref (trans_state e x)) =
    {(cap', trans_state e x)}) = (fst (get_cap cref x) = {(cap', x)})" apply (rule iffI) apply (cut_tac x=cref and e="\<lambda>_. exst x" in get_cap_bcorres_any) apply (simp add: bcorres_underlying_def) apply (drule_tac x="trans_state e x" in spec) apply (simp add: s_bcorres_underlying_def) apply (drule get_cap_det) apply (simp add: trans_state_update') apply (cut_tac x=cref and e="e" in get_cap_bcorres_any) apply (simp add: bcorres_underlying_def) apply (drule_tac x="x" in spec) apply (simp add: s_bcorres_underlying_def) apply (drule get_cap_det) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)}) = (fst (get_cap cref x) = {(cap', x)}) proof (prove)
goal (2 subgoals):
 1. fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} \<Longrightarrow> fst (get_cap cref x) = {(cap', x)}
 2. fst (get_cap cref x) = {(cap', x)} \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)}; bcorres_underlying (trans_state (\<lambda>_. exst x)) (get_cap cref) (get_cap cref)\<rbrakk> \<Longrightarrow> fst (get_cap cref x) = {(cap', x)}
 2. fst (get_cap cref x) = {(cap', x)} \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)}; \<forall>s. s_bcorres_underlying (trans_state (\<lambda>_. exst x)) (get_cap cref) (get_cap cref) s\<rbrakk> \<Longrightarrow> fst (get_cap cref x) = {(cap', x)}
 2. fst (get_cap cref x) = {(cap', x)} \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)}; s_bcorres_underlying (trans_state (\<lambda>_. exst x)) (get_cap cref) (get_cap cref) (trans_state e x)\<rbrakk> \<Longrightarrow> fst (get_cap cref x) = {(cap', x)}
 2. fst (get_cap cref x) = {(cap', x)} \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)}; (cap', trans_state (\<lambda>e. exst x) x) \<in> fst (get_cap cref (trans_state (\<lambda>e. exst x) x))\<rbrakk> \<Longrightarrow> fst (get_cap cref x) = {(cap', x)}
 2. fst (get_cap cref x) = {(cap', x)} \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)}; get_cap cref (trans_state (\<lambda>e. exst x) x) = ({(cap', trans_state (\<lambda>e. exst x) x)}, False)\<rbrakk> \<Longrightarrow> fst (get_cap cref x) = {(cap', x)}
 2. fst (get_cap cref x) = {(cap', x)} \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (1 subgoal):
 1. fst (get_cap cref x) = {(cap', x)} \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap cref x) = {(cap', x)}; bcorres_underlying (trans_state e) (get_cap cref) (get_cap cref)\<rbrakk> \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap cref x) = {(cap', x)}; \<forall>s. s_bcorres_underlying (trans_state e) (get_cap cref) (get_cap cref) s\<rbrakk> \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap cref x) = {(cap', x)}; s_bcorres_underlying (trans_state e) (get_cap cref) (get_cap cref) x\<rbrakk> \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap cref x) = {(cap', x)}; (cap', trans_state e x) \<in> fst (get_cap cref (trans_state e x))\<rbrakk> \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap cref x) = {(cap', x)}; get_cap cref (trans_state e x) = ({(cap', trans_state e x)}, False)\<rbrakk> \<Longrightarrow> fst (get_cap cref (trans_state e x)) = {(cap', trans_state e x)} proof (prove)
goal:
No subgoals!