theory Deterministic_AI

lemma create_cap_valid_list[wp]:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrace>valid_list \<rbrace>
      create_cap tp sz p dev x \<lbrace>\<lambda>rv. valid_list\<rbrace>" apply (case_tac x) apply (simp add: create_cap_def) apply(simp add: set_cdt_def update_cdt_list_def set_cdt_list_def create_cap_ext_def bind_assoc) apply (rule hoare_pre) apply (simp add: valid_list_2_def) apply (wp | simp cong: option.case_cong if_cong del: fun_upd_apply split del: if_split)+ apply(wp set_cap_caps_of_state3 get_cap_wp)+ apply(simp del: fun_upd_apply split: option.splits split del: if_split cong:if_weak_cong) apply (intro impI conjI allI) apply (simp add: valid_list_2_def | intro impI conjI allI | fastforce simp: list_remove_removed list_remove_distinct)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> create_cap tp sz p dev x \<lbrace>\<lambda>rv. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. x = (a, b) \<Longrightarrow> \<lbrace>valid_list\<rbrace> create_cap tp sz p dev x \<lbrace>\<lambda>rv. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. x = (a, b) \<Longrightarrow> \<lbrace>valid_list\<rbrace> do dest_p <- gets (\<lambda>s. cdt s a);
cdt <- gets cdt;
y <- set_cdt (cdt(a \<mapsto> p));
y <- create_cap_ext p a dest_p;
y <- set_original a True;
set_cap (default_cap tp b sz dev) a
od \<lbrace>\<lambda>rv. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. x = (a, b) \<Longrightarrow> \<lbrace>valid_list\<rbrace> do dest_p <- gets (\<lambda>s. cdt s a);
cdt <- gets cdt;
x <- get;
y <- put (x\<lparr>cdt := cdt(a \<mapsto> p)\<rparr>);
x <- gets cdt_list;
xa <- get;
x <- put (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> x | Some p \<Rightarrow> x(p := list_remove (x p) a)) xa);
x <- gets cdt_list;
xa <- get;
y <- put (cdt_list_update (\<lambda>_. x(p := a # x p)) xa);
y <- set_original a True;
set_cap (default_cap tp b sz dev) a
od \<lbrace>\<lambda>rv. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b. x = (a, b) \<Longrightarrow> \<lbrace>?Q1 a b\<rbrace> do dest_p <- gets (\<lambda>s. cdt s a);
cdt <- gets cdt;
x <- get;
y <- put (x\<lparr>cdt := cdt(a \<mapsto> p)\<rparr>);
x <- gets cdt_list;
xa <- get;
x <- put (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> x | Some p \<Rightarrow> x(p := list_remove (x p) a)) xa);
x <- gets cdt_list;
xa <- get;
y <- put (cdt_list_update (\<lambda>_. x(p := a # x p)) xa);
y <- set_original a True;
set_cap (default_cap tp b sz dev) a
od \<lbrace>\<lambda>rv. valid_list\<rbrace>
 2. \<And>a b s. \<lbrakk>x = (a, b); valid_list s\<rbrakk> \<Longrightarrow> ?Q1 a b s proof (prove)
goal (2 subgoals):
 1. \<And>a b. x = (a, b) \<Longrightarrow> \<lbrace>?Q1 a b\<rbrace> do dest_p <- gets (\<lambda>s. cdt s a);
cdt <- gets cdt;
x <- get;
y <- put (x\<lparr>cdt := cdt(a \<mapsto> p)\<rparr>);
x <- gets cdt_list;
xa <- get;
x <- put (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> x | Some p \<Rightarrow> x(p := list_remove (x p) a)) xa);
x <- gets cdt_list;
xa <- get;
y <- put (cdt_list_update (\<lambda>_. x(p := a # x p)) xa);
y <- set_original a True;
set_cap (default_cap tp b sz dev) a
od \<lbrace>\<lambda>rv s. (\<forall>p. set (cdt_list s p) = {c. cdt s c = Some p}) \<and> (\<forall>p. distinct (cdt_list s p))\<rbrace>
 2. \<And>a b s. \<lbrakk>x = (a, b); valid_list s\<rbrakk> \<Longrightarrow> ?Q1 a b s proof (prove)
goal (13 subgoals):
 1. \<And>a b dest_p cdta xa xaa xb xd xe. x = (a, b) \<Longrightarrow> \<lbrace>?B15 a b dest_p cdta xa () xaa xb () xd xe () ()\<rbrace> set_cap (default_cap tp b sz dev) a \<lbrace>\<lambda>rv s. (\<forall>p. set (cdt_list s p) = {c. cdt s c = Some p}) \<and> (\<forall>p. distinct (cdt_list s p))\<rbrace>
 2. \<And>a b dest_p cdt xa y xaa xb xc xd xe ya. x = (a, b) \<Longrightarrow> \<lbrace>?B14 a b dest_p cdt xa y xaa xb xc xd xe ya\<rbrace> set_original a True \<lbrace>?B15 a b dest_p cdt xa y xaa xb xc xd xe ya\<rbrace>
 3. \<And>a b dest_p cdt xa y xaa xb xc xd xe. x = (a, b) \<Longrightarrow> \<lbrace>?B13 a b dest_p cdt xa y xaa xb xc xd xe\<rbrace> put (cdt_list_update (\<lambda>_. xd(p := a # xd p)) xe) \<lbrace>?B14 a b dest_p cdt xa y xaa xb xc xd xe\<rbrace>
 4. \<And>a b dest_p cdt xa y xaa xb xc xd. x = (a, b) \<Longrightarrow> \<lbrace>?B12 a b dest_p cdt xa y xaa xb xc xd\<rbrace> get \<lbrace>?B13 a b dest_p cdt xa y xaa xb xc xd\<rbrace>
 5. \<And>a b dest_p cdt xa y xaa xb xc. x = (a, b) \<Longrightarrow> \<lbrace>?B11 a b dest_p cdt xa y xaa xb xc\<rbrace> gets cdt_list \<lbrace>?B12 a b dest_p cdt xa y xaa xb xc\<rbrace>
 6. \<And>a b dest_p cdt xa y xaa xb. x = (a, b) \<Longrightarrow> \<lbrace>?B10 a b dest_p cdt xa y xaa xb\<rbrace> put (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> xaa | Some p \<Rightarrow> xaa(p := list_remove (xaa p) a)) xb) \<lbrace>?B11 a b dest_p cdt xa y xaa xb\<rbrace>
 7. \<And>a b dest_p cdt xa y xaa. x = (a, b) \<Longrightarrow> \<lbrace>?B9 a b dest_p cdt xa y xaa\<rbrace> get \<lbrace>?B10 a b dest_p cdt xa y xaa\<rbrace>
 8. \<And>a b dest_p cdt xa y. x = (a, b) \<Longrightarrow> \<lbrace>?B8 a b dest_p cdt xa y\<rbrace> gets cdt_list \<lbrace>?B9 a b dest_p cdt xa y\<rbrace>
 9. \<And>a b dest_p cdt xa. x = (a, b) \<Longrightarrow> \<lbrace>?B7 a b dest_p cdt xa\<rbrace> put (xa\<lparr>cdt := cdt(a \<mapsto> p)\<rparr>) \<lbrace>?B8 a b dest_p cdt xa\<rbrace>
 10. \<And>a b dest_p cdt. x = (a, b) \<Longrightarrow> \<lbrace>?B6 a b dest_p cdt\<rbrace> get \<lbrace>?B7 a b dest_p cdt\<rbrace>
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>x = (a, b); valid_list s\<rbrakk> \<Longrightarrow> (\<forall>pa. set (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p), cdt_list := case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a), cdt_list := (cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)))(p := a # cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)) p), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. (cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)))(p := a # cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)) p)) (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))))(a := True)\<rparr>) pa) = {c. cdt (s\<lparr>cdt := (cdt s)(a \<mapsto> p), cdt_list := case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a), cdt_list := (cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)))(p := a # cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)) p), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. (cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)))(p := a # cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)) p)) (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))))(a := True)\<rparr>) c = Some pa}) \<and> (\<forall>pa. distinct (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p), cdt_list := case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a), cdt_list := (cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)))(p := a # cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)) p), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. (cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)))(p := a # cdt_list (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>)) p)) (cdt_list_update (\<lambda>_. case cdt s a of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) | Some pa \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))(pa := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>) pa) a)) (s\<lparr>cdt := (cdt s)(a \<mapsto> p)\<rparr>))))(a := True)\<rparr>) pa)) proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>x = (a, b); valid_list s\<rbrakk> \<Longrightarrow> (cdt s a = None \<longrightarrow> (\<forall>pa. set (((cdt_list s)(p := a # cdt_list s p)) pa) = {c. ((cdt s)(a \<mapsto> p)) c = Some pa}) \<and> (\<forall>pa. distinct (((cdt_list s)(p := a # cdt_list s p)) pa))) \<and> (\<forall>x2. cdt s a = Some x2 \<longrightarrow> (\<forall>pa. set (((cdt_list s)(x2 := list_remove (cdt_list s x2) a, p := a # ((cdt_list s)(x2 := list_remove (cdt_list s x2) a)) p)) pa) = {c. ((cdt s)(a \<mapsto> p)) c = Some pa}) \<and> (\<forall>pa. distinct (((cdt_list s)(x2 := list_remove (cdt_list s x2) a, p := a # ((cdt_list s)(x2 := list_remove (cdt_list s x2) a)) p)) pa))) proof (prove)
goal (4 subgoals):
 1. \<And>a b s pa. \<lbrakk>x = (a, b); valid_list s; cdt s a = None\<rbrakk> \<Longrightarrow> set (((cdt_list s)(p := a # cdt_list s p)) pa) = {c. ((cdt s)(a \<mapsto> p)) c = Some pa}
 2. \<And>a b s pa. \<lbrakk>x = (a, b); valid_list s; cdt s a = None\<rbrakk> \<Longrightarrow> distinct (((cdt_list s)(p := a # cdt_list s p)) pa)
 3. \<And>a b s x2 pa. \<lbrakk>x = (a, b); valid_list s; cdt s a = Some x2\<rbrakk> \<Longrightarrow> set (((cdt_list s)(x2 := list_remove (cdt_list s x2) a, p := a # ((cdt_list s)(x2 := list_remove (cdt_list s x2) a)) p)) pa) = {c. ((cdt s)(a \<mapsto> p)) c = Some pa}
 4. \<And>a b s x2 pa. \<lbrakk>x = (a, b); valid_list s; cdt s a = Some x2\<rbrakk> \<Longrightarrow> distinct (((cdt_list s)(x2 := list_remove (cdt_list s x2) a, p := a # ((cdt_list s)(x2 := list_remove (cdt_list s x2) a)) p)) pa) proof (prove)
goal:
No subgoals!