theory Deterministic_AI

lemma distinct_list_replace_list:
 "\<lbrakk>distinct list; distinct list'; set list \<inter> set list' = {}; slot \<in> set list\<rbrakk>
    \<Longrightarrow> distinct (list_replace_list list slot list')" apply(induct list) apply(simp) apply(simp) apply(intro conjI impI) apply(fastforce) apply(subst set_list_replace_list) apply(simp) apply(simp) apply(fastforce) apply(simp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; distinct list'; set list \<inter> set list' = {}; slot \<in> set list\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct []; distinct list'; set [] \<inter> set list' = {}; slot \<in> set []\<rbrakk> \<Longrightarrow> distinct (list_replace_list [] slot list')
 2. \<And>a list. \<lbrakk>\<lbrakk>distinct list; distinct list'; set list \<inter> set list' = {}; slot \<in> set list\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list'); distinct (a # list); distinct list'; set (a # list) \<inter> set list' = {}; slot \<in> set (a # list)\<rbrakk> \<Longrightarrow> distinct (list_replace_list (a # list) slot list') proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<lbrakk>distinct list; distinct list'; set list \<inter> set list' = {}; slot \<in> set list\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list'); distinct (a # list); distinct list'; set (a # list) \<inter> set list' = {}; slot \<in> set (a # list)\<rbrakk> \<Longrightarrow> distinct (list_replace_list (a # list) slot list') proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list\<rbrakk> \<Longrightarrow> (a = slot \<longrightarrow> set list' \<inter> set list = {}) \<and> (a \<noteq> slot \<longrightarrow> a \<notin> set (list_replace_list list slot list') \<and> distinct (list_replace_list list slot list')) proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a = slot\<rbrakk> \<Longrightarrow> set list' \<inter> set list = {}
 2. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> a \<notin> set (list_replace_list list slot list')
 3. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list') proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> a \<notin> set (list_replace_list list slot list')
 2. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list') proof (prove)
goal (5 subgoals):
 1. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> distinct list
 2. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> slot \<in> set list
 3. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> slot \<notin> set list'
 4. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> a \<notin> set list \<union> set list' - {slot}
 5. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list') proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> slot \<in> set list
 2. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> slot \<notin> set list'
 3. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> a \<notin> set list \<union> set list' - {slot}
 4. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list') proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> slot \<notin> set list'
 2. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> a \<notin> set list \<union> set list' - {slot}
 3. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list') proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> a \<notin> set list \<union> set list' - {slot}
 2. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list') proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>slot \<in> set list \<Longrightarrow> distinct (list_replace_list list slot list'); a \<notin> set list \<and> distinct list; distinct list'; a \<notin> set list' \<and> set list \<inter> set list' = {}; slot = a \<or> slot \<in> set list; a \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list list slot list') proof (prove)
goal:
No subgoals!