theory FinalCaps

lemma intra_label_cap_pres:
  assumes cte: "\<And>P. \<lbrace>\<lambda> s. \<not> cte_wp_at P slot s\<rbrace> f \<lbrace>\<lambda> _ s. \<not> cte_wp_at P slot s\<rbrace>"
  shows "\<lbrace>intra_label_cap aag slot\<rbrace> f \<lbrace>\<lambda>_. intra_label_cap aag slot\<rbrace>" apply (clarsimp simp: valid_def intra_label_cap_def) apply (drule_tac x=cap in spec) apply (case_tac "cte_wp_at ((=) cap) slot s") apply blast apply (drule_tac use_valid[OF _ cte]) apply assumption apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>intra_label_cap aag slot\<rbrace> f \<lbrace>\<lambda>_. intra_label_cap aag slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); (a, b) \<in> fst (f s); cte_wp_at ((=) cap) slot b\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) \<in> fst (f s); cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>(a, b) \<in> fst (f s); cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
 2. \<And>s a b cap. \<lbrakk>(a, b) \<in> fst (f s); cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); \<not> cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) \<in> fst (f s); cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); \<not> cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); \<not> cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> \<not> cte_wp_at (?P20 s a b cap) slot s
 2. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); \<not> cte_wp_at ((=) cap) slot s; \<not> cte_wp_at (?P20 s a b cap) slot b\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); \<not> cte_wp_at ((=) cap) slot s; \<not> cte_wp_at ((=) cap) slot b\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal:
No subgoals!