theory Enumeration

lemma the_index_last_distinct:
  "distinct xs \<and> xs \<noteq> [] \<Longrightarrow> the_index xs (last xs) = length xs - 1" apply safe apply (subgoal_tac "xs ! (length xs - 1) = last xs") apply (subgoal_tac "xs ! the_index xs (last xs) = last xs") apply (subst nth_eq_iff_index_eq[symmetric]) apply assumption apply (rule the_index_bounded) apply simp_all apply (rule nth_the_index) apply simp apply (induct xs, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct xs \<and> xs \<noteq> [] \<Longrightarrow> the_index xs (last xs) = length xs - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> the_index xs (last xs) = length xs - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs\<rbrakk> \<Longrightarrow> the_index xs (last xs) = length xs - 1
 2. \<lbrakk>distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs ! (length xs - 1) = last xs proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> the_index xs (last xs) = length xs - 1
 2. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs\<rbrakk> \<Longrightarrow> xs ! the_index xs (last xs) = last xs
 3. \<lbrakk>distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs ! (length xs - 1) = last xs proof (prove)
goal (6 subgoals):
 1. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> distinct ?xs4
 2. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> the_index xs (last xs) < length ?xs4
 3. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> length xs - 1 < length ?xs4
 4. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> ?xs4 ! the_index xs (last xs) = ?xs4 ! (length xs - 1)
 5. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs\<rbrakk> \<Longrightarrow> xs ! the_index xs (last xs) = last xs
 6. \<lbrakk>distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs ! (length xs - 1) = last xs proof (prove)
goal (5 subgoals):
 1. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> the_index xs (last xs) < length xs
 2. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> length xs - 1 < length xs
 3. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> xs ! the_index xs (last xs) = xs ! (length xs - 1)
 4. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs\<rbrakk> \<Longrightarrow> xs ! the_index xs (last xs) = last xs
 5. \<lbrakk>distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs ! (length xs - 1) = last xs proof (prove)
goal (5 subgoals):
 1. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> last xs \<in> set xs
 2. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> length xs - 1 < length xs
 3. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs; xs ! the_index xs (last xs) = last xs\<rbrakk> \<Longrightarrow> xs ! the_index xs (last xs) = xs ! (length xs - 1)
 4. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - 1) = last xs\<rbrakk> \<Longrightarrow> xs ! the_index xs (last xs) = last xs
 5. \<lbrakk>distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs ! (length xs - 1) = last xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - Suc 0) = last xs\<rbrakk> \<Longrightarrow> xs ! the_index xs (last xs) = last xs
 2. \<lbrakk>distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs ! (length xs - Suc 0) = last xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct xs; xs \<noteq> []; xs ! (length xs - Suc 0) = last xs\<rbrakk> \<Longrightarrow> last xs \<in> set xs
 2. \<lbrakk>distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs ! (length xs - Suc 0) = last xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs ! (length xs - Suc 0) = last xs proof (prove)
goal:
No subgoals!