theory Deterministic_AI

lemma wf_next_slot:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_mdb s; valid_list s\<rbrakk>
    \<Longrightarrow> wf {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}" apply(rule finite_acyclic_wf) apply(insert cte_wp_at_set_finite)[1] apply(rule_tac B="{p. cte_wp_at \<top> p s} \<times> {p. cte_wp_at \<top> p s}" in finite_subset) apply(fastforce dest: cte_at_next_slot cte_at_next_slot' simp: finite_depth) apply(fastforce intro: finite_cartesian_product) apply(rule acyclicI) apply(frule finite_depth) apply(rule allI) apply(drule next_slot_no_loop, simp add: valid_mdb_def, simp add: finite_depth) apply(fastforce simp: next_slot_set_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> wf {(next, p). next_slot p (cdt_list s) (cdt s) = Some next} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> finite {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}
 2. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> acyclicP (\<lambda>next p. next_slot p (cdt_list s) (cdt s) = Some next) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb s; valid_list s; \<And>P s. finite {p. cte_wp_at (P p) p s}\<rbrakk> \<Longrightarrow> finite {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}
 2. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> acyclicP (\<lambda>next p. next_slot p (cdt_list s) (cdt s) = Some next) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_mdb s; valid_list s; \<And>P s. finite {p. cte_wp_at (P p) p s}\<rbrakk> \<Longrightarrow> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next} \<subseteq> {p. cte_wp_at (\<lambda>_. True) p s} \<times> {p. cte_wp_at (\<lambda>_. True) p s}
 2. \<lbrakk>valid_mdb s; valid_list s; \<And>P s. finite {p. cte_wp_at (P p) p s}\<rbrakk> \<Longrightarrow> finite ({p. cte_wp_at (\<lambda>_. True) p s} \<times> {p. cte_wp_at (\<lambda>_. True) p s})
 3. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> acyclicP (\<lambda>next p. next_slot p (cdt_list s) (cdt s) = Some next) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb s; valid_list s; \<And>P s. finite {p. cte_wp_at (P p) p s}\<rbrakk> \<Longrightarrow> finite ({p. cte_wp_at (\<lambda>_. True) p s} \<times> {p. cte_wp_at (\<lambda>_. True) p s})
 2. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> acyclicP (\<lambda>next p. next_slot p (cdt_list s) (cdt s) = Some next) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> acyclicP (\<lambda>next p. next_slot p (cdt_list s) (cdt s) = Some next) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> \<forall>x. (x, x) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_list s; finite_depth (cdt s)\<rbrakk> \<Longrightarrow> \<forall>x. (x, x) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_mdb s; valid_list s; finite_depth (cdt s)\<rbrakk> \<Longrightarrow> (x, x) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_mdb s; finite_depth (cdt s); ?x33 x \<notin> next_slot_set (?x33 x) (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> (x, x) \<notin> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ proof (prove)
goal:
No subgoals!