theory Deterministic_AI

lemma empty_slot_valid_list[wp]:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrace>valid_list\<rbrace>
     empty_slot sl irqopt
   \<lbrace>\<lambda>rv. valid_list\<rbrace>" apply (simp add: empty_slot_def) apply (simp add: set_cdt_def update_cdt_list_def set_cdt_list_def
                   empty_slot_ext_def bind_assoc cong: if_cong) apply (wp get_cap_wp hoare_weak_lift_imp | wpc | wp (once) hoare_vcg_all_lift)+ apply (clarsimp simp del: fun_upd_apply) apply (frule mdb_empty_abs_simple.intro) apply(case_tac "cdt s sl") apply (frule(1) mdb_empty_abs_simple.valid_list_post_no_parent) apply simp apply (case_tac "a = sl") apply (frule(2) mdb_empty_abs_simple.valid_list_post_self_parent) apply simp apply (frule(2) mdb_empty_abs_simple.valid_list_post) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> empty_slot sl irqopt \<lbrace>\<lambda>rv. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do cap <- get_cap sl;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s sl);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some sl then cdt sl else cdt p)(sl := None));
y <- empty_slot_ext sl slot_p;
y <- set_original sl False;
y <- set_cap NullCap sl;
post_cap_deletion irqopt
od
od \<lbrace>\<lambda>rv. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do cap <- get_cap sl;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s sl);
cdt <- gets cdt;
x <- get;
y <- put (x\<lparr>cdt := (\<lambda>p. if cdt p = Some sl then cdt sl else cdt p)(sl := None)\<rparr>);
x <- gets cdt_list;
xa <- get;
y <- put (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> x(sl := []) | Some p \<Rightarrow> if p = sl then x(sl := list_remove (x sl) sl) else x(p := list_replace_list (x p) sl (x sl), sl := [])) xa);
y <- set_original sl False;
y <- set_cap NullCap sl;
post_cap_deletion irqopt
od
od \<lbrace>\<lambda>rv. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_list s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) sl s \<longrightarrow> (cap = NullCap \<longrightarrow> valid_list s) \<and> (cap \<noteq> NullCap \<longrightarrow> valid_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None), cdt_list := case cdt s sl of None \<Rightarrow> (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>))(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>))(sl := list_remove (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>) sl) sl) else (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>))(p := list_replace_list (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>) p) sl (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>) sl), sl := []), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. case cdt s sl of None \<Rightarrow> (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>))(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>))(sl := list_remove (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>) sl) sl) else (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>))(p := list_replace_list (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>) p) sl (cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>) sl), sl := [])) (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)\<rparr>)))(sl := False)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s)\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = None\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None))
 2. \<And>s cap a. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = Some a\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = None; valid_list_2 ((cdt_list s)(sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None))\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None))
 2. \<And>s cap a. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = Some a\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap a. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = Some a\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap a. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = Some a; a = sl\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None))
 2. \<And>s cap a. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = Some a; a \<noteq> sl\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap a. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = Some a; a = sl; valid_list_2 ((cdt_list s)(a := list_remove (cdt_list s a) sl)) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None))\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None))
 2. \<And>s cap a. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = Some a; a \<noteq> sl\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap a. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = Some a; a \<noteq> sl\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap a. \<lbrakk>valid_list s; cte_wp_at ((=) cap) sl s; cap \<noteq> NullCap; mdb_empty_abs_simple (cdt s) (cdt_list s); cdt s sl = Some a; a \<noteq> sl; valid_list_2 ((cdt_list s)(a := list_replace_list (cdt_list s a) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None))\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s sl of None \<Rightarrow> (cdt_list s)(sl := []) | Some p \<Rightarrow> if p = sl then (cdt_list s)(sl := list_remove (cdt_list s sl) sl) else (cdt_list s)(p := list_replace_list (cdt_list s p) sl (cdt_list s sl), sl := [])) ((\<lambda>p. if cdt s p = Some sl then cdt s sl else cdt s p)(sl := None)) proof (prove)
goal:
No subgoals!