theory Deterministic_AI

lemma next_slot_no_loop:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk>
    \<Longrightarrow> x \<notin> next_slot_set x t m" apply(rule notI) apply(case_tac "m x") apply(drule(2) next_slot_setD, simp) apply(simp add: next_sib_set_not_self) apply(erule disjE) apply(simp add: no_mloop_def descendants_of_def) apply(elim exE conjE) apply(erule disjE) apply(fastforce simp: descendants_of_def cdt_parent_defs dest: tranclD2) apply(fastforce simp: next_sib_set_def next_sib_def split: option.splits dest: tranclD2) apply(drule next_slot_set_after_in_list) apply(assumption)+ apply(simp add: next_sib_set_not_self) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> x \<notin> next_slot_set x t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = None\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = None; x \<in> descendants_of x m \<or> x \<in> next_sib_set x t m \<or> (\<exists>p q. (x \<in> descendants_of p m \<or> p = x) \<and> q \<in> next_sib_set p t m \<and> x \<in> descendants_of q m \<union> {q})\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = None; x \<in> descendants_of x m \<or> (\<exists>p. (x \<in> descendants_of p m \<or> p = x) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (x = q \<or> x \<in> descendants_of q m)))\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = None; x \<in> descendants_of x m\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = None; \<exists>p. (x \<in> descendants_of p m \<or> p = x) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (x = q \<or> x \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = None; \<exists>p. (x \<in> descendants_of p m \<or> p = x) \<and> (\<exists>q. q \<in> next_sib_set p t m \<and> (x = q \<or> x \<in> descendants_of q m))\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = None; x \<in> descendants_of p m \<or> p = x; q \<in> next_sib_set p t m; x = q \<or> x \<in> descendants_of q m\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = None; q \<in> next_sib_set p t m; x = q \<or> x \<in> descendants_of q m; x \<in> descendants_of p m\<rbrakk> \<Longrightarrow> False
 2. \<And>p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = None; q \<in> next_sib_set p t m; x = q \<or> x \<in> descendants_of q m; p = x\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p q. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = None; q \<in> next_sib_set p t m; x = q \<or> x \<in> descendants_of q m; p = x\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; x \<in> next_slot_set x t m; m x = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = Some a\<rbrakk> \<Longrightarrow> m x = Some (?p77 a)
 2. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = Some a\<rbrakk> \<Longrightarrow> m x = Some (?p77 a)
 3. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = Some a\<rbrakk> \<Longrightarrow> valid_list_2 t m
 4. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = Some a\<rbrakk> \<Longrightarrow> no_mloop m
 5. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = Some a\<rbrakk> \<Longrightarrow> finite_depth m
 6. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = Some a; x \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; no_mloop m; finite_depth m; m x = Some a; x \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!