theory Invariants_H

lemma ex_cte_cap_to'_pres:
  "\<lbrakk> \<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>;
     \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace>ex_cte_cap_wp_to' P p\<rbrace> f \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p\<rbrace>" apply (simp add: ex_cte_cap_wp_to'_def) apply (rule hoare_pre) apply (erule hoare_use_eq_irq_node') apply (rule hoare_vcg_ex_lift) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>ex_cte_cap_wp_to' P p\<rbrace> f \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace>
 2. \<And>s. \<lbrakk>\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>; \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>fa. (\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>) \<Longrightarrow> \<lbrace>?P3 fa\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) fa) cref s\<rbrace>
 2. \<And>s. \<lbrakk>\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>; \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrakk> \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (2 subgoals):
 1. \<And>fa cref. (\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>) \<Longrightarrow> \<lbrace>?P5 fa cref\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) fa) cref\<rbrace>
 2. \<And>s. \<lbrakk>\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>; \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrakk> \<Longrightarrow> \<exists>x. ?P5 (irq_node' s) x s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>; \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrakk> \<Longrightarrow> \<exists>x. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) x s proof (prove)
goal:
No subgoals!