theory Deterministic_AI

lemma after_in_list_not_self_helper:
  "\<lbrakk>distinct list;
        after_in_list list c = Some c;
        (list, c) = (x # y # xs, a)\<rbrakk>
       \<Longrightarrow> False" apply (induct list arbitrary: x y xs a,simp) apply atomize apply (case_tac xs) apply (case_tac "aa =x") apply (case_tac "x = y",simp,simp) apply (simp split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; after_in_list list c = Some c; (list, c) = (x # y # xs, a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a list x y xs aa. \<lbrakk>\<And>x y xs a. \<lbrakk>distinct list; after_in_list list c = Some c; (list, c) = (x # y # xs, a)\<rbrakk> \<Longrightarrow> False; distinct (a # list); after_in_list (a # list) c = Some c; (a # list, c) = (x # y # xs, aa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a list x y xs aa. \<lbrakk>\<forall>x y xs a. distinct list \<longrightarrow> after_in_list list c = Some c \<longrightarrow> (list, c) = (x # y # xs, a) \<longrightarrow> False; distinct (a # list); after_in_list (a # list) c = Some c; (a # list, c) = (x # y # xs, aa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a list x y xs aa. \<lbrakk>\<forall>x y xs a. distinct list \<longrightarrow> after_in_list list c = Some c \<longrightarrow> (list, c) = (x # y # xs, a) \<longrightarrow> False; distinct (a # list); after_in_list (a # list) c = Some c; (a # list, c) = (x # y # xs, aa); xs = []\<rbrakk> \<Longrightarrow> False
 2. \<And>a list x y xs aa ab lista. \<lbrakk>\<forall>x y xs a. distinct list \<longrightarrow> after_in_list list c = Some c \<longrightarrow> (list, c) = (x # y # xs, a) \<longrightarrow> False; distinct (a # list); after_in_list (a # list) c = Some c; (a # list, c) = (x # y # xs, aa); xs = ab # lista\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a list x y xs aa. \<lbrakk>\<forall>x y xs a. distinct list \<longrightarrow> after_in_list list c = Some c \<longrightarrow> (list, c) = (x # y # xs, a) \<longrightarrow> False; distinct (a # list); after_in_list (a # list) c = Some c; (a # list, c) = (x # y # xs, aa); xs = []; aa = x\<rbrakk> \<Longrightarrow> False
 2. \<And>a list x y xs aa. \<lbrakk>\<forall>x y xs a. distinct list \<longrightarrow> after_in_list list c = Some c \<longrightarrow> (list, c) = (x # y # xs, a) \<longrightarrow> False; distinct (a # list); after_in_list (a # list) c = Some c; (a # list, c) = (x # y # xs, aa); xs = []; aa \<noteq> x\<rbrakk> \<Longrightarrow> False
 3. \<And>a list x y xs aa ab lista. \<lbrakk>\<forall>x y xs a. distinct list \<longrightarrow> after_in_list list c = Some c \<longrightarrow> (list, c) = (x # y # xs, a) \<longrightarrow> False; distinct (a # list); after_in_list (a # list) c = Some c; (a # list, c) = (x # y # xs, aa); xs = ab # lista\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a list x y xs aa. \<lbrakk>\<forall>x y xs a. distinct list \<longrightarrow> after_in_list list c = Some c \<longrightarrow> (list, c) = (x # y # xs, a) \<longrightarrow> False; distinct (a # list); after_in_list (a # list) c = Some c; (a # list, c) = (x # y # xs, aa); xs = []; aa \<noteq> x\<rbrakk> \<Longrightarrow> False
 2. \<And>a list x y xs aa ab lista. \<lbrakk>\<forall>x y xs a. distinct list \<longrightarrow> after_in_list list c = Some c \<longrightarrow> (list, c) = (x # y # xs, a) \<longrightarrow> False; distinct (a # list); after_in_list (a # list) c = Some c; (a # list, c) = (x # y # xs, aa); xs = ab # lista\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!