theory Deterministic_AI

lemma cte_at_next_slot:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s)\<rbrakk>
    \<Longrightarrow> next_slot p (cdt_list s) (cdt s) = Some n \<Longrightarrow> cte_at p s" apply(simp add: next_slot_def) apply(simp split: if_split_asm) apply(drule next_childD, simp) apply(rule_tac p=n in descendants_of_cte_at2) apply(simp add: child_descendant) apply(simp) apply(subgoal_tac "next_not_child_dom (p, cdt_list s, cdt s)") prefer 2 apply(simp add: next_not_child_termination valid_mdb_def valid_list_2_def) apply(simp split: if_split_asm) apply(case_tac "cdt s p") apply(simp) apply(rule descendants_of_cte_at) apply(simp add: descendants_of_def cdt_parent_defs) apply(rule r_into_trancl, simp) apply(simp) apply(drule next_sibD) apply(elim exE conjE) apply(drule after_in_list_in_list) apply(rule descendants_of_cte_at) apply(simp add: descendants_of_def cdt_parent_defs) apply(rule r_into_trancl, simp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); next_slot p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); (if cdt_list s p \<noteq> [] then next_child p (cdt_list s) else next_not_child p (cdt_list s) (cdt s)) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p \<noteq> []; next_child p (cdt_list s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p \<noteq> []; (\<exists>xs. cdt_list s p = n # xs) \<and> cdt s n = Some p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p \<noteq> []; (\<exists>xs. cdt_list s p = n # xs) \<and> cdt s n = Some p\<rbrakk> \<Longrightarrow> n \<in> descendants_of p (cdt s)
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p \<noteq> []; (\<exists>xs. cdt_list s p = n # xs) \<and> cdt s n = Some p\<rbrakk> \<Longrightarrow> valid_mdb s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p \<noteq> []; (\<exists>xs. cdt_list s p = n # xs) \<and> cdt s n = Some p\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; next_not_child_dom (p, cdt_list s, cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> next_not_child_dom (p, cdt_list s, cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> next_not_child_dom (p, cdt_list s, cdt s)
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; next_not_child_dom (p, cdt_list s, cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; next_not_child_dom (p, cdt_list s, cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s)) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s)) = Some n; cdt s p = None\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<And>a. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 3. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> p \<in> descendants_of (?x109 a) (cdt s)
 2. \<And>a. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> valid_mdb s
 3. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; next_not_child a (cdt_list s) (cdt s) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> (?x109 a, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<And>a. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> valid_mdb s
 3. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; \<exists>pa. cdt s p = Some pa \<and> after_in_list (cdt_list s pa) p = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; cdt s p = Some pa; after_in_list (cdt_list s pa) p = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; cdt s p = Some pa; n \<in> set (cdt_list s pa)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; cdt s p = Some pa; n \<in> set (cdt_list s pa)\<rbrakk> \<Longrightarrow> p \<in> descendants_of (?x123 pa) (cdt s)
 2. \<And>pa. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; cdt s p = Some pa; n \<in> set (cdt_list s pa)\<rbrakk> \<Longrightarrow> valid_mdb s proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; cdt s p = Some pa; n \<in> set (cdt_list s pa)\<rbrakk> \<Longrightarrow> (?x123 pa, p) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<And>pa. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; cdt s p = Some pa; n \<in> set (cdt_list s pa)\<rbrakk> \<Longrightarrow> valid_mdb s proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>next_not_child_dom (p, cdt_list s, cdt s); valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; cdt s p = Some pa; n \<in> set (cdt_list s pa)\<rbrakk> \<Longrightarrow> valid_mdb s proof (prove)
goal:
No subgoals!