theory IsolatedThreadAction

lemma getCTE_assert_opt:
  "getCTE p = gets (\<lambda>s. ctes_of s p) >>= assert_opt" apply (intro ext) apply (simp add: exec_gets assert_opt_def prod_eq_iff
                   fail_def return_def
            split: option.split) apply (rule conjI) apply clarsimp apply (rule context_conjI) apply (rule ccontr, clarsimp elim!: nonemptyE) apply (frule use_valid[OF _ getCTE_sp], rule TrueI) apply (frule in_inv_by_hoareD[OF getCTE_inv]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (simp add: empty_failD[OF empty_fail_getCTE]) apply clarsimp apply (simp add: no_failD[OF no_fail_getCTE, OF ctes_of_cte_at]) apply (subgoal_tac "cte_wp_at' ((=) x2) p x") apply (clarsimp simp: cte_wp_at'_def getCTE_def) apply (simp add: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. getCTE p = gets (\<lambda>s. ctes_of s p) >>= assert_opt proof (prove)
goal (1 subgoal):
 1. \<And>x. getCTE p x = (gets (\<lambda>s. ctes_of s p) >>= assert_opt) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (ctes_of x p = None \<longrightarrow> fst (getCTE p x) = {} \<and> snd (getCTE p x)) \<and> (\<forall>x2. ctes_of x p = Some x2 \<longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. ctes_of x p = None \<longrightarrow> fst (getCTE p x) = {} \<and> snd (getCTE p x)
 2. \<And>x. \<forall>x2. ctes_of x p = Some x2 \<longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x) proof (prove)
goal (2 subgoals):
 1. \<And>x. ctes_of x p = None \<Longrightarrow> fst (getCTE p x) = {} \<and> snd (getCTE p x)
 2. \<And>x. \<forall>x2. ctes_of x p = Some x2 \<longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x) proof (prove)
goal (3 subgoals):
 1. \<And>x. ctes_of x p = None \<Longrightarrow> fst (getCTE p x) = {}
 2. \<And>x. \<lbrakk>ctes_of x p = None; fst (getCTE p x) = {}\<rbrakk> \<Longrightarrow> snd (getCTE p x)
 3. \<And>x. \<forall>x2. ctes_of x p = Some x2 \<longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x) proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>ctes_of x p = None; (a, b) \<in> fst (getCTE p x)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>ctes_of x p = None; fst (getCTE p x) = {}\<rbrakk> \<Longrightarrow> snd (getCTE p x)
 3. \<And>x. \<forall>x2. ctes_of x p = Some x2 \<longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x) proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>ctes_of x p = None; (a, b) \<in> fst (getCTE p x); (cte_wp_at' (\<lambda>c. c = a) p and (\<lambda>a. True)) b\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>ctes_of x p = None; fst (getCTE p x) = {}\<rbrakk> \<Longrightarrow> snd (getCTE p x)
 3. \<And>x. \<forall>x2. ctes_of x p = Some x2 \<longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x) proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>ctes_of x p = None; (a, b) \<in> fst (getCTE p x); (cte_wp_at' (\<lambda>c. c = a) p and (\<lambda>a. True)) b; b = x\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>ctes_of x p = None; fst (getCTE p x) = {}\<rbrakk> \<Longrightarrow> snd (getCTE p x)
 3. \<And>x. \<forall>x2. ctes_of x p = Some x2 \<longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ctes_of x p = None; fst (getCTE p x) = {}\<rbrakk> \<Longrightarrow> snd (getCTE p x)
 2. \<And>x. \<forall>x2. ctes_of x p = Some x2 \<longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x2. ctes_of x p = Some x2 \<longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x) proof (prove)
goal (1 subgoal):
 1. \<And>x x2. ctes_of x p = Some x2 \<Longrightarrow> fst (getCTE p x) = {(x2, x)} \<and> \<not> snd (getCTE p x) proof (prove)
goal (1 subgoal):
 1. \<And>x x2. ctes_of x p = Some x2 \<Longrightarrow> fst (getCTE p x) = {(x2, x)} proof (prove)
goal (2 subgoals):
 1. \<And>x x2. \<lbrakk>ctes_of x p = Some x2; cte_wp_at' ((=) x2) p x\<rbrakk> \<Longrightarrow> fst (getCTE p x) = {(x2, x)}
 2. \<And>x x2. ctes_of x p = Some x2 \<Longrightarrow> cte_wp_at' ((=) x2) p x proof (prove)
goal (1 subgoal):
 1. \<And>x x2. ctes_of x p = Some x2 \<Longrightarrow> cte_wp_at' ((=) x2) p x proof (prove)
goal:
No subgoals!