theory Deterministic_AI

lemma next_slot_no_parent:
  "valid_list_2 t m \<Longrightarrow> m src = None
    \<Longrightarrow> next_slot p (t(src := [], dest := t src)) m'
      = (if p = src then None
         else if p = dest then next_slot src t m
         else if next_slot p t m = Some src then Some dest
         else next_slot p t m)" apply (simp only: next_slot_def split: if_split) apply (intro impI conjI) apply (subst next_child_no_parent| subst next_not_child_no_parent | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_slot p (t(src := [], dest := t src)) m' = (if p = src then None else if p = dest then next_slot src t m else if next_slot p t m = Some src then Some dest else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> (t src \<noteq> [] \<longrightarrow> ((t(src := [], dest := t src)) p \<noteq> [] \<longrightarrow> (t p \<noteq> [] \<longrightarrow> (next_child p t = Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_child src t)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = Some dest))) \<and> (next_child p t \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_child src t)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_child p t)))) \<and> (\<not> t p \<noteq> [] \<longrightarrow> (next_not_child p t m = Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_child src t)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = Some dest))) \<and> (next_not_child p t m \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_child src t)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_not_child p t m))))) \<and> (\<not> (t(src := [], dest := t src)) p \<noteq> [] \<longrightarrow> (t p \<noteq> [] \<longrightarrow> (next_child p t = Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_child src t)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = Some dest))) \<and> (next_child p t \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_child src t)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_child p t)))) \<and> (\<not> t p \<noteq> [] \<longrightarrow> (next_not_child p t m = Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_child src t)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = Some dest))) \<and> (next_not_child p t m \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_child src t)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_not_child p t m)))))) \<and> (\<not> t src \<noteq> [] \<longrightarrow> ((t(src := [], dest := t src)) p \<noteq> [] \<longrightarrow> (t p \<noteq> [] \<longrightarrow> (next_child p t = Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_not_child src t m)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = Some dest))) \<and> (next_child p t \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_not_child src t m)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_child p t)))) \<and> (\<not> t p \<noteq> [] \<longrightarrow> (next_not_child p t m = Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_not_child src t m)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = Some dest))) \<and> (next_not_child p t m \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_not_child src t m)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child p (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_not_child p t m))))) \<and> (\<not> (t(src := [], dest := t src)) p \<noteq> [] \<longrightarrow> (t p \<noteq> [] \<longrightarrow> (next_child p t = Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_not_child src t m)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = Some dest))) \<and> (next_child p t \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_not_child src t m)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_child p t)))) \<and> (\<not> t p \<noteq> [] \<longrightarrow> (next_not_child p t m = Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_not_child src t m)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = Some dest))) \<and> (next_not_child p t m \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_not_child src t m)) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = None) \<and> (p \<noteq> src \<longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = next_not_child p t m)))))) proof (prove)
goal (64 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; t p \<noteq> []; next_child p t = Some src; p = dest; p = src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = None
 2. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; t p \<noteq> []; next_child p t = Some src; p = dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = next_child src t
 3. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; t p \<noteq> []; next_child p t = Some src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = None
 4. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; t p \<noteq> []; next_child p t = Some src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = Some dest
 5. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; t p \<noteq> []; next_child p t \<noteq> Some src; p = dest; p = src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = None
 6. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; t p \<noteq> []; next_child p t \<noteq> Some src; p = dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = next_child src t
 7. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; t p \<noteq> []; next_child p t \<noteq> Some src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = None
 8. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; t p \<noteq> []; next_child p t \<noteq> Some src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = next_child p t
 9. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; \<not> t p \<noteq> []; next_not_child p t m = Some src; p = dest; p = src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = None
 10. \<lbrakk>valid_list_2 t m; m src = None; t src \<noteq> []; (t(src := [], dest := t src)) p \<noteq> []; \<not> t p \<noteq> []; next_not_child p t m = Some src; p = dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = next_child src t
A total of 64 subgoals... proof (prove)
goal:
No subgoals!