theory Ipc_C

lemma takeWhile_eq:
  "\<lbrakk> \<And>m. \<lbrakk> m < length ys \<rbrakk> \<Longrightarrow> P (xs ! m);
       length ys < length xs \<Longrightarrow> \<not> P (xs ! length ys);
       length ys \<le> length xs;
     \<And>m. m < length ys \<Longrightarrow> xs ! m = ys ! m \<rbrakk>
    \<Longrightarrow> takeWhile P xs = ys" proof (induct xs arbitrary: n ys) case Nil thus ?case by simp next case (Cons x xs' ys') have P: "\<And>v m. \<lbrakk> (x # xs') ! m = v; m < length ys' \<rbrakk>
                     \<Longrightarrow> P v" using Cons.prems by clarsimp show ?case using Cons.prems(2-3) apply simp apply (cases ys') apply simp apply (subst P[where m1=0]) apply simp+ apply (rule conjI) apply (cut_tac m1=0 in Cons.prems(4), simp+) apply (rule Cons.hyps) apply (rule_tac m1="Suc m" in P, simp+) apply (cut_tac m1="Suc m" in Cons.prems(4), simp+) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>m. m < length ys \<Longrightarrow> P (xs ! m); length ys < length xs \<Longrightarrow> \<not> P (xs ! length ys); length ys \<le> length xs; \<And>m. m < length ys \<Longrightarrow> xs ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P xs = ys proof (state)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>\<And>m. m < length ys \<Longrightarrow> P ([] ! m); length ys < length [] \<Longrightarrow> \<not> P ([] ! length ys); length ys \<le> length []; \<And>m. m < length ys \<Longrightarrow> [] ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P [] = ys
 2. \<And>x1 xs ys. \<lbrakk>\<And>ys. \<lbrakk>\<And>m. m < length ys \<Longrightarrow> P (xs ! m); length ys < length xs \<Longrightarrow> \<not> P (xs ! length ys); length ys \<le> length xs; \<And>m. m < length ys \<Longrightarrow> xs ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P xs = ys; \<And>m. m < length ys \<Longrightarrow> P ((x1 # xs) ! m); length ys < length (x1 # xs) \<Longrightarrow> \<not> P ((x1 # xs) ! length ys); length ys \<le> length (x1 # xs); \<And>m. m < length ys \<Longrightarrow> (x1 # xs) ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P (x1 # xs) = ys proof (state)
this:
?m1 < length ys \<Longrightarrow> P ([] ! ?m1)
length ys < length [] \<Longrightarrow> \<not> P ([] ! length ys)
length ys \<le> length []
?m1 < length ys \<Longrightarrow> [] ! ?m1 = ys ! ?m1

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>\<And>m. m < length ys \<Longrightarrow> P ([] ! m); length ys < length [] \<Longrightarrow> \<not> P ([] ! length ys); length ys \<le> length []; \<And>m. m < length ys \<Longrightarrow> [] ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P [] = ys
 2. \<And>x1 xs ys. \<lbrakk>\<And>ys. \<lbrakk>\<And>m. m < length ys \<Longrightarrow> P (xs ! m); length ys < length xs \<Longrightarrow> \<not> P (xs ! length ys); length ys \<le> length xs; \<And>m. m < length ys \<Longrightarrow> xs ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P xs = ys; \<And>m. m < length ys \<Longrightarrow> P ((x1 # xs) ! m); length ys < length (x1 # xs) \<Longrightarrow> \<not> P ((x1 # xs) ! length ys); length ys \<le> length (x1 # xs); \<And>m. m < length ys \<Longrightarrow> (x1 # xs) ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P (x1 # xs) = ys proof (prove)
using this:
?m1 < length ys \<Longrightarrow> P ([] ! ?m1)
length ys < length [] \<Longrightarrow> \<not> P ([] ! length ys)
length ys \<le> length []
?m1 < length ys \<Longrightarrow> [] ! ?m1 = ys ! ?m1

goal (1 subgoal):
 1. takeWhile P [] = ys proof (state)
this:
takeWhile P [] = ys

goal (1 subgoal):
 1. \<And>x1 xs ys. \<lbrakk>\<And>ys. \<lbrakk>\<And>m. m < length ys \<Longrightarrow> P (xs ! m); length ys < length xs \<Longrightarrow> \<not> P (xs ! length ys); length ys \<le> length xs; \<And>m. m < length ys \<Longrightarrow> xs ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P xs = ys; \<And>m. m < length ys \<Longrightarrow> P ((x1 # xs) ! m); length ys < length (x1 # xs) \<Longrightarrow> \<not> P ((x1 # xs) ! length ys); length ys \<le> length (x1 # xs); \<And>m. m < length ys \<Longrightarrow> (x1 # xs) ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P (x1 # xs) = ys proof (state)
goal (1 subgoal):
 1. \<And>x1 xs ys. \<lbrakk>\<And>ys. \<lbrakk>\<And>m. m < length ys \<Longrightarrow> P (xs ! m); length ys < length xs \<Longrightarrow> \<not> P (xs ! length ys); length ys \<le> length xs; \<And>m. m < length ys \<Longrightarrow> xs ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P xs = ys; \<And>m. m < length ys \<Longrightarrow> P ((x1 # xs) ! m); length ys < length (x1 # xs) \<Longrightarrow> \<not> P ((x1 # xs) ! length ys); length ys \<le> length (x1 # xs); \<And>m. m < length ys \<Longrightarrow> (x1 # xs) ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P (x1 # xs) = ys proof (state)
this:
\<lbrakk>\<And>m. m < length ?ys1 \<Longrightarrow> P (xs' ! m); length ?ys1 < length xs' \<Longrightarrow> \<not> P (xs' ! length ?ys1); length ?ys1 \<le> length xs'; \<And>m. m < length ?ys1 \<Longrightarrow> xs' ! m = ?ys1 ! m\<rbrakk> \<Longrightarrow> takeWhile P xs' = ?ys1
?m1 < length ys' \<Longrightarrow> P ((x # xs') ! ?m1)
length ys' < length (x # xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys')
length ys' \<le> length (x # xs')
?m1 < length ys' \<Longrightarrow> (x # xs') ! ?m1 = ys' ! ?m1

goal (1 subgoal):
 1. \<And>x1 xs ys. \<lbrakk>\<And>ys. \<lbrakk>\<And>m. m < length ys \<Longrightarrow> P (xs ! m); length ys < length xs \<Longrightarrow> \<not> P (xs ! length ys); length ys \<le> length xs; \<And>m. m < length ys \<Longrightarrow> xs ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P xs = ys; \<And>m. m < length ys \<Longrightarrow> P ((x1 # xs) ! m); length ys < length (x1 # xs) \<Longrightarrow> \<not> P ((x1 # xs) ! length ys); length ys \<le> length (x1 # xs); \<And>m. m < length ys \<Longrightarrow> (x1 # xs) ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P (x1 # xs) = ys proof (prove)
goal (1 subgoal):
 1. \<And>v m. \<lbrakk>(x # xs') ! m = v; m < length ys'\<rbrakk> \<Longrightarrow> P v proof (prove)
using this:
?m1 < length ys' \<Longrightarrow> P ((x # xs') ! ?m1)
length ys' < length (x # xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys')
length ys' \<le> length (x # xs')
?m1 < length ys' \<Longrightarrow> (x # xs') ! ?m1 = ys' ! ?m1

goal (1 subgoal):
 1. \<And>v m. \<lbrakk>(x # xs') ! m = v; m < length ys'\<rbrakk> \<Longrightarrow> P v proof (state)
this:
\<lbrakk>(x # xs') ! ?m1 = ?v1; ?m1 < length ys'\<rbrakk> \<Longrightarrow> P ?v1

goal (1 subgoal):
 1. \<And>x1 xs ys. \<lbrakk>\<And>ys. \<lbrakk>\<And>m. m < length ys \<Longrightarrow> P (xs ! m); length ys < length xs \<Longrightarrow> \<not> P (xs ! length ys); length ys \<le> length xs; \<And>m. m < length ys \<Longrightarrow> xs ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P xs = ys; \<And>m. m < length ys \<Longrightarrow> P ((x1 # xs) ! m); length ys < length (x1 # xs) \<Longrightarrow> \<not> P ((x1 # xs) ! length ys); length ys \<le> length (x1 # xs); \<And>m. m < length ys \<Longrightarrow> (x1 # xs) ! m = ys ! m\<rbrakk> \<Longrightarrow> takeWhile P (x1 # xs) = ys proof (prove)
goal (1 subgoal):
 1. takeWhile P (x # xs') = ys' proof (prove)
using this:
length ys' < length (x # xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys')
length ys' \<le> length (x # xs')

goal (1 subgoal):
 1. takeWhile P (x # xs') = ys' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ys' < Suc (length xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys'); length ys' \<le> Suc (length xs')\<rbrakk> \<Longrightarrow> (if P x then x # takeWhile P xs' else []) = ys' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length ys' < Suc (length xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys'); length ys' \<le> Suc (length xs'); ys' = []\<rbrakk> \<Longrightarrow> (if P x then x # takeWhile P xs' else []) = ys'
 2. \<And>a list. \<lbrakk>length ys' < Suc (length xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys'); length ys' \<le> Suc (length xs'); ys' = a # list\<rbrakk> \<Longrightarrow> (if P x then x # takeWhile P xs' else []) = ys' proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>length ys' < Suc (length xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys'); length ys' \<le> Suc (length xs'); ys' = a # list\<rbrakk> \<Longrightarrow> (if P x then x # takeWhile P xs' else []) = ys' proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>length ys' < Suc (length xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys'); length ys' \<le> Suc (length xs'); ys' = a # list\<rbrakk> \<Longrightarrow> (x # xs') ! 0 = x
 2. \<And>a list. \<lbrakk>length ys' < Suc (length xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys'); length ys' \<le> Suc (length xs'); ys' = a # list\<rbrakk> \<Longrightarrow> 0 < length ys'
 3. \<And>a list. \<lbrakk>length ys' < Suc (length xs') \<Longrightarrow> \<not> P ((x # xs') ! length ys'); length ys' \<le> Suc (length xs'); ys' = a # list\<rbrakk> \<Longrightarrow> (if True then x # takeWhile P xs' else []) = ys' proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>length list < length xs' \<Longrightarrow> \<not> P (xs' ! length list); length list \<le> length xs'; ys' = a # list\<rbrakk> \<Longrightarrow> x = a \<and> takeWhile P xs' = list proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>length list < length xs' \<Longrightarrow> \<not> P (xs' ! length list); length list \<le> length xs'; ys' = a # list\<rbrakk> \<Longrightarrow> x = a
 2. \<And>a list. \<lbrakk>length list < length xs' \<Longrightarrow> \<not> P (xs' ! length list); length list \<le> length xs'; ys' = a # list\<rbrakk> \<Longrightarrow> takeWhile P xs' = list proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>length list < length xs' \<Longrightarrow> \<not> P (xs' ! length list); length list \<le> length xs'; ys' = a # list\<rbrakk> \<Longrightarrow> takeWhile P xs' = list proof (prove)
goal (4 subgoals):
 1. \<And>a list m. \<lbrakk>length list < length xs' \<Longrightarrow> \<not> P (xs' ! length list); length list \<le> length xs'; ys' = a # list; m < length list\<rbrakk> \<Longrightarrow> P (xs' ! m)
 2. \<And>a list. \<lbrakk>length list < length xs' \<Longrightarrow> \<not> P (xs' ! length list); length list \<le> length xs'; ys' = a # list; length list < length xs'\<rbrakk> \<Longrightarrow> \<not> P (xs' ! length list)
 3. \<And>a list. \<lbrakk>length list < length xs' \<Longrightarrow> \<not> P (xs' ! length list); length list \<le> length xs'; ys' = a # list\<rbrakk> \<Longrightarrow> length list \<le> length xs'
 4. \<And>a list m. \<lbrakk>length list < length xs' \<Longrightarrow> \<not> P (xs' ! length list); length list \<le> length xs'; ys' = a # list; m < length list\<rbrakk> \<Longrightarrow> xs' ! m = list ! m proof (prove)
goal (1 subgoal):
 1. \<And>a list m. \<lbrakk>length list < length xs' \<Longrightarrow> \<not> P (xs' ! length list); length list \<le> length xs'; ys' = a # list; m < length list\<rbrakk> \<Longrightarrow> xs' ! m = list ! m proof (prove)
goal:
No subgoals! proof (state)
this:
takeWhile P (x # xs') = ys'

goal:
No subgoals!