theory TcbQueue_C

lemma distinct_remove1_take_drop:
  "\<lbrakk> distinct ls; n < length ls \<rbrakk> \<Longrightarrow> remove1 (ls ! n) ls = (take n ls) @ drop (Suc n) ls" proof (induct ls arbitrary: n) case Nil thus ?case by simp next case (Cons x xs n) show ?case proof (cases n) case 0 thus ?thesis by simp next case (Suc m) hence "((x # xs) ! n) \<noteq> x" using Cons.prems by clarsimp thus ?thesis using Suc Cons.prems by (clarsimp simp add: Cons.hyps) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct ls; n < length ls\<rbrakk> \<Longrightarrow> remove1 (ls ! n) ls = take n ls @ drop (Suc n) ls proof (state)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>distinct []; n < length []\<rbrakk> \<Longrightarrow> remove1 ([] ! n) [] = take n [] @ drop (Suc n) []
 2. \<And>x1 ls n. \<lbrakk>\<And>n. \<lbrakk>distinct ls; n < length ls\<rbrakk> \<Longrightarrow> remove1 (ls ! n) ls = take n ls @ drop (Suc n) ls; distinct (x1 # ls); n < length (x1 # ls)\<rbrakk> \<Longrightarrow> remove1 ((x1 # ls) ! n) (x1 # ls) = take n (x1 # ls) @ drop (Suc n) (x1 # ls) proof (state)
this:
distinct []
n < length []

goal (2 subgoals):
 1. \<And>n. \<lbrakk>distinct []; n < length []\<rbrakk> \<Longrightarrow> remove1 ([] ! n) [] = take n [] @ drop (Suc n) []
 2. \<And>x1 ls n. \<lbrakk>\<And>n. \<lbrakk>distinct ls; n < length ls\<rbrakk> \<Longrightarrow> remove1 (ls ! n) ls = take n ls @ drop (Suc n) ls; distinct (x1 # ls); n < length (x1 # ls)\<rbrakk> \<Longrightarrow> remove1 ((x1 # ls) ! n) (x1 # ls) = take n (x1 # ls) @ drop (Suc n) (x1 # ls) proof (prove)
using this:
distinct []
n < length []

goal (1 subgoal):
 1. remove1 ([] ! n) [] = take n [] @ drop (Suc n) [] proof (state)
this:
remove1 ([] ! n) [] = take n [] @ drop (Suc n) []

goal (1 subgoal):
 1. \<And>x1 ls n. \<lbrakk>\<And>n. \<lbrakk>distinct ls; n < length ls\<rbrakk> \<Longrightarrow> remove1 (ls ! n) ls = take n ls @ drop (Suc n) ls; distinct (x1 # ls); n < length (x1 # ls)\<rbrakk> \<Longrightarrow> remove1 ((x1 # ls) ! n) (x1 # ls) = take n (x1 # ls) @ drop (Suc n) (x1 # ls) proof (state)
goal (1 subgoal):
 1. \<And>x1 ls n. \<lbrakk>\<And>n. \<lbrakk>distinct ls; n < length ls\<rbrakk> \<Longrightarrow> remove1 (ls ! n) ls = take n ls @ drop (Suc n) ls; distinct (x1 # ls); n < length (x1 # ls)\<rbrakk> \<Longrightarrow> remove1 ((x1 # ls) ! n) (x1 # ls) = take n (x1 # ls) @ drop (Suc n) (x1 # ls) proof (state)
this:
\<lbrakk>distinct xs; ?n < length xs\<rbrakk> \<Longrightarrow> remove1 (xs ! ?n) xs = take ?n xs @ drop (Suc ?n) xs
distinct (x # xs)
n < length (x # xs)

goal (1 subgoal):
 1. \<And>x1 ls n. \<lbrakk>\<And>n. \<lbrakk>distinct ls; n < length ls\<rbrakk> \<Longrightarrow> remove1 (ls ! n) ls = take n ls @ drop (Suc n) ls; distinct (x1 # ls); n < length (x1 # ls)\<rbrakk> \<Longrightarrow> remove1 ((x1 # ls) ! n) (x1 # ls) = take n (x1 # ls) @ drop (Suc n) (x1 # ls) proof (prove)
goal (1 subgoal):
 1. remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs) proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs) proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs) proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs) proof (state)
this:
remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs) proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs) proof (state)
this:
n = Suc m

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs) proof (prove)
using this:
n = Suc m

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

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs) proof (prove)
using this:
(x # xs) ! n \<noteq> x

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

goal (1 subgoal):
 1. remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs) proof (state)
this:
remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs)

goal:
No subgoals! proof (state)
this:
remove1 ((x # xs) ! n) (x # xs) = take n (x # xs) @ drop (Suc n) (x # xs)

goal:
No subgoals!