theory ListLibLemmas

lemma list_eq_after_in_list':
  "\<lbrakk> distinct xs; p = xs ! i; i < length xs \<rbrakk>
    \<Longrightarrow> \<exists>list. xs = list @ p # after_in_list_list xs p" apply (induct xs arbitrary: i) apply (simp) apply (atomize) apply (case_tac i) apply (simp) apply (drule_tac x = nat in spec, simp) apply (erule exE, rule impI, rule_tac x = "a # list" in exI) apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; p = xs ! i; i < length xs\<rbrakk> \<Longrightarrow> \<exists>list. xs = list @ p # after_in_list_list xs p proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>distinct []; p = [] ! i; i < length []\<rbrakk> \<Longrightarrow> \<exists>list. [] = list @ p # after_in_list_list [] p
 2. \<And>a xs i. \<lbrakk>\<And>i. \<lbrakk>distinct xs; p = xs ! i; i < length xs\<rbrakk> \<Longrightarrow> \<exists>list. xs = list @ p # after_in_list_list xs p; distinct (a # xs); p = (a # xs) ! i; i < length (a # xs)\<rbrakk> \<Longrightarrow> \<exists>list. a # xs = list @ p # after_in_list_list (a # xs) p proof (prove)
goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>\<And>i. \<lbrakk>distinct xs; p = xs ! i; i < length xs\<rbrakk> \<Longrightarrow> \<exists>list. xs = list @ p # after_in_list_list xs p; distinct (a # xs); p = (a # xs) ! i; i < length (a # xs)\<rbrakk> \<Longrightarrow> \<exists>list. a # xs = list @ p # after_in_list_list (a # xs) p proof (prove)
goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>\<forall>i. distinct xs \<longrightarrow> p = xs ! i \<longrightarrow> i < length xs \<longrightarrow> (\<exists>list. xs = list @ p # after_in_list_list xs p); distinct (a # xs); p = (a # xs) ! i; i < length (a # xs)\<rbrakk> \<Longrightarrow> \<exists>list. a # xs = list @ p # after_in_list_list (a # xs) p proof (prove)
goal (2 subgoals):
 1. \<And>a xs i. \<lbrakk>\<forall>i. distinct xs \<longrightarrow> p = xs ! i \<longrightarrow> i < length xs \<longrightarrow> (\<exists>list. xs = list @ p # after_in_list_list xs p); distinct (a # xs); p = (a # xs) ! i; i < length (a # xs); i = 0\<rbrakk> \<Longrightarrow> \<exists>list. a # xs = list @ p # after_in_list_list (a # xs) p
 2. \<And>a xs i nat. \<lbrakk>\<forall>i. distinct xs \<longrightarrow> p = xs ! i \<longrightarrow> i < length xs \<longrightarrow> (\<exists>list. xs = list @ p # after_in_list_list xs p); distinct (a # xs); p = (a # xs) ! i; i < length (a # xs); i = Suc nat\<rbrakk> \<Longrightarrow> \<exists>list. a # xs = list @ p # after_in_list_list (a # xs) p proof (prove)
goal (1 subgoal):
 1. \<And>a xs i nat. \<lbrakk>\<forall>i. distinct xs \<longrightarrow> p = xs ! i \<longrightarrow> i < length xs \<longrightarrow> (\<exists>list. xs = list @ p # after_in_list_list xs p); distinct (a # xs); p = (a # xs) ! i; i < length (a # xs); i = Suc nat\<rbrakk> \<Longrightarrow> \<exists>list. a # xs = list @ p # after_in_list_list (a # xs) p proof (prove)
goal (1 subgoal):
 1. \<And>a xs i nat. \<lbrakk>a \<notin> set xs \<and> distinct xs; p = xs ! nat; nat < length xs; i = Suc nat; \<exists>list. xs = list @ xs ! nat # after_in_list_list xs (xs ! nat)\<rbrakk> \<Longrightarrow> xs ! nat \<noteq> a \<longrightarrow> (\<exists>list. a # xs = list @ xs ! nat # after_in_list_list xs (xs ! nat)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs i nat list. \<lbrakk>a \<notin> set xs \<and> distinct xs; p = xs ! nat; nat < length xs; i = Suc nat; xs = list @ xs ! nat # after_in_list_list xs (xs ! nat); xs ! nat \<noteq> a\<rbrakk> \<Longrightarrow> a # xs = (a # list) @ xs ! nat # after_in_list_list xs (xs ! nat) proof (prove)
goal:
No subgoals!