theory CSpace_AI

lemma no_True_set_nth:
  "(True \<notin> set xs) = (\<forall>n < length xs. xs ! n = False)" apply (induct xs) apply simp apply (case_tac a, simp_all) apply (rule_tac x=0 in exI) apply simp apply safe apply (case_tac n, simp_all)[1] apply (case_tac na, simp_all)[1] apply (erule_tac x="Suc n" in allE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (True \<notin> set xs) = (\<forall>n<length xs. xs ! n = False) proof (prove)
goal (2 subgoals):
 1. (True \<notin> set []) = (\<forall>n<length []. [] ! n = False)
 2. \<And>a xs. (True \<notin> set xs) = (\<forall>n<length xs. xs ! n = False) \<Longrightarrow> (True \<notin> set (a # xs)) = (\<forall>n<length (a # xs). (a # xs) ! n = False) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. (True \<notin> set xs) = (\<forall>n<length xs. xs ! n = False) \<Longrightarrow> (True \<notin> set (a # xs)) = (\<forall>n<length (a # xs). (a # xs) ! n = False) proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>(True \<notin> set xs) = (\<forall>n<length xs. \<not> xs ! n); a\<rbrakk> \<Longrightarrow> \<exists>n<Suc (length xs). (True # xs) ! n
 2. \<And>a xs. \<lbrakk>(True \<notin> set xs) = (\<forall>n<length xs. \<not> xs ! n); \<not> a\<rbrakk> \<Longrightarrow> (\<forall>n<length xs. \<not> xs ! n) = (\<forall>n<Suc (length xs). \<not> (False # xs) ! n) proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>(True \<notin> set xs) = (\<forall>n<length xs. \<not> xs ! n); a\<rbrakk> \<Longrightarrow> 0 < Suc (length xs) \<and> (True # xs) ! 0
 2. \<And>a xs. \<lbrakk>(True \<notin> set xs) = (\<forall>n<length xs. \<not> xs ! n); \<not> a\<rbrakk> \<Longrightarrow> (\<forall>n<length xs. \<not> xs ! n) = (\<forall>n<Suc (length xs). \<not> (False # xs) ! n) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(True \<notin> set xs) = (\<forall>n<length xs. \<not> xs ! n); \<not> a\<rbrakk> \<Longrightarrow> (\<forall>n<length xs. \<not> xs ! n) = (\<forall>n<Suc (length xs). \<not> (False # xs) ! n) proof (prove)
goal (3 subgoals):
 1. \<And>a xs n. \<lbrakk>\<not> a; True \<notin> set xs; \<forall>n<length xs. \<not> xs ! n; \<forall>n<length xs. \<not> xs ! n; n < Suc (length xs); (False # xs) ! n\<rbrakk> \<Longrightarrow> False
 2. \<And>a xs n na. \<lbrakk>\<not> a; n < length xs; True \<in> set xs; \<not> False; xs ! n; \<not> False; \<forall>n<length xs. \<not> xs ! n; na < Suc (length xs); (False # xs) ! na\<rbrakk> \<Longrightarrow> False
 3. \<And>a xs n na. \<lbrakk>\<not> a; n < length xs; True \<in> set xs; \<not> False; xs ! n; \<not> False; \<forall>n<Suc (length xs). \<not> (False # xs) ! n; na < length xs; xs ! na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a xs n na. \<lbrakk>\<not> a; n < length xs; True \<in> set xs; \<not> False; xs ! n; \<not> False; \<forall>n<length xs. \<not> xs ! n; na < Suc (length xs); (False # xs) ! na\<rbrakk> \<Longrightarrow> False
 2. \<And>a xs n na. \<lbrakk>\<not> a; n < length xs; True \<in> set xs; \<not> False; xs ! n; \<not> False; \<forall>n<Suc (length xs). \<not> (False # xs) ! n; na < length xs; xs ! na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a xs n na. \<lbrakk>\<not> a; n < length xs; True \<in> set xs; \<not> False; xs ! n; \<not> False; \<forall>n<Suc (length xs). \<not> (False # xs) ! n; na < length xs; xs ! na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a xs n na. \<lbrakk>\<not> a; n < length xs; True \<in> set xs; \<not> False; xs ! n; \<not> False; na < length xs; xs ! na; Suc n < Suc (length xs) \<longrightarrow> \<not> (False # xs) ! Suc n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!