[STATEMENT]
lemma carrier_vec_induct [consumes 1, case_names 0 Suc, induct set:carrier_vec]:
  assumes v: "v \<in> carrier_vec n"
    and 1: "P 0 vNil" and 2: "\<And>n a v. v \<in> carrier_vec n \<Longrightarrow> P n v \<Longrightarrow> P (Suc n) (vCons a v)"
  shows "P n v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P n v
[PROOF STEP]
proof (insert v, induct n arbitrary: v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. v \<in> carrier_vec 0 \<Longrightarrow> P 0 v
 2. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec 0

goal (2 subgoals):
 1. \<And>v. v \<in> carrier_vec 0 \<Longrightarrow> P 0 v
 2. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec 0
[PROOF STEP]
have "v = vec 0 ((!) [])"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec 0

goal (1 subgoal):
 1. v = vNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = vNil

goal (2 subgoals):
 1. \<And>v. v \<in> carrier_vec 0 \<Longrightarrow> P 0 v
 2. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
P 0 vNil
v = vNil
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P 0 vNil
v = vNil

goal (1 subgoal):
 1. P 0 v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P 0 v

goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
?v \<in> carrier_vec n \<Longrightarrow> P n ?v
v \<in> carrier_vec (Suc n)

goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?v \<in> carrier_vec n \<Longrightarrow> P n ?v
v \<in> carrier_vec (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?v \<in> carrier_vec n \<Longrightarrow> P n ?v
v \<in> carrier_vec (Suc n)

goal (1 subgoal):
 1. P (Suc n) v
[PROOF STEP]
by (cases v, auto dest!: carrier_vecD intro:2)
[PROOF STATE]
proof (state)
this:
P (Suc n) v

goal:
No subgoals!
[PROOF STEP]
qed