theory TcbQueue_C

lemma distinct_nth_cons:
  assumes dist: "distinct xs"
  and     xxs: "x \<notin> set xs"
  and     ln: "n < length xs"
  and     lm: "m < length xs"
  shows   "((x # xs) ! n = xs ! m) = (n = Suc m)" proof (cases "n = Suc m") case True thus ?thesis by simp next case False have ln': "n < length (x # xs)" using ln by simp have lm': "Suc m < length (x # xs)" using lm by simp have "distinct (x # xs)" using dist xxs by simp thus ?thesis using False unfolding distinct_conv_nth apply - apply (drule spec, drule mp [OF _ ln']) apply (drule spec, drule mp [OF _ lm']) apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x # xs) ! n = xs ! m) = (n = Suc m) proof (state)
goal (2 subgoals):
 1. n = Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m)
 2. n \<noteq> Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (state)
this:
n = Suc m

goal (2 subgoals):
 1. n = Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m)
 2. n \<noteq> Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
using this:
n = Suc m

goal (1 subgoal):
 1. ((x # xs) ! n = xs ! m) = (n = Suc m) proof (state)
this:
((x # xs) ! n = xs ! m) = (n = Suc m)

goal (1 subgoal):
 1. n \<noteq> Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (state)
goal (1 subgoal):
 1. n \<noteq> Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (state)
this:
n \<noteq> Suc m

goal (1 subgoal):
 1. n \<noteq> Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
goal (1 subgoal):
 1. n < length (x # xs) proof (prove)
using this:
n < length xs

goal (1 subgoal):
 1. n < length (x # xs) proof (state)
this:
n < length (x # xs)

goal (1 subgoal):
 1. n \<noteq> Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
goal (1 subgoal):
 1. Suc m < length (x # xs) proof (prove)
using this:
m < length xs

goal (1 subgoal):
 1. Suc m < length (x # xs) proof (state)
this:
Suc m < length (x # xs)

goal (1 subgoal):
 1. n \<noteq> Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
goal (1 subgoal):
 1. distinct (x # xs) proof (prove)
using this:
distinct xs
x \<notin> set xs

goal (1 subgoal):
 1. distinct (x # xs) proof (state)
this:
distinct (x # xs)

goal (1 subgoal):
 1. n \<noteq> Suc m \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
using this:
distinct (x # xs)

goal (1 subgoal):
 1. ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
using this:
distinct (x # xs)
n \<noteq> Suc m

goal (1 subgoal):
 1. ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
using this:
\<forall>i<length (x # xs). \<forall>j<length (x # xs). i \<noteq> j \<longrightarrow> (x # xs) ! i \<noteq> (x # xs) ! j
n \<noteq> Suc m

goal (1 subgoal):
 1. ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i<length (x # xs). \<forall>j<length (x # xs). i \<noteq> j \<longrightarrow> (x # xs) ! i \<noteq> (x # xs) ! j; n \<noteq> Suc m\<rbrakk> \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> Suc m; \<forall>j<length (x # xs). n \<noteq> j \<longrightarrow> (x # xs) ! n \<noteq> (x # xs) ! j\<rbrakk> \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> Suc m; n \<noteq> Suc m \<longrightarrow> (x # xs) ! n \<noteq> (x # xs) ! Suc m\<rbrakk> \<Longrightarrow> ((x # xs) ! n = xs ! m) = (n = Suc m) proof (prove)
goal:
No subgoals! proof (state)
this:
((x # xs) ! n = xs ! m) = (n = Suc m)

goal:
No subgoals!