theory CSpace_AI

lemma drop_postfixD:
  "(drop (length xs - length ys) xs = ys) \<Longrightarrow> (\<exists>zs. xs = zs @ ys)" proof (induct xs arbitrary: ys) case Nil thus ?case by simp next case (Cons x xs) from Cons.prems have "length ys \<le> length (x # xs)" by (rule len_drop_lemma) simp moreover { assume "length ys = length (x # xs)" with Cons.prems have ?case by simp } moreover { assume "length ys < length (x # xs)" hence "length ys \<le> length xs" by simp hence "drop (length xs - length ys) xs =
           drop (length (x # xs) - length ys) (x # xs)" by (simp add: Suc_diff_le) with Cons.prems have ?case by (auto dest: Cons.hyps) } ultimately show ?case by (auto simp: order_le_less) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys proof (state)
goal (2 subgoals):
 1. \<And>ys. drop (length [] - length ys) [] = ys \<Longrightarrow> \<exists>zs. [] = zs @ ys
 2. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
drop (length [] - length ys) [] = ys

goal (2 subgoals):
 1. \<And>ys. drop (length [] - length ys) [] = ys \<Longrightarrow> \<exists>zs. [] = zs @ ys
 2. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (prove)
using this:
drop (length [] - length ys) [] = ys

goal (1 subgoal):
 1. \<exists>zs. [] = zs @ ys proof (state)
this:
\<exists>zs. [] = zs @ ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
drop (length xs - length ?ys) xs = ?ys \<Longrightarrow> \<exists>zs. xs = zs @ ?ys
drop (length (x # xs) - length ys) (x # xs) = ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (chain)
picking this:
drop (length (x # xs) - length ys) (x # xs) = ys proof (prove)
using this:
drop (length (x # xs) - length ys) (x # xs) = ys

goal (1 subgoal):
 1. length ys \<le> length (x # xs) proof (state)
this:
length ys \<le> length (x # xs)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
length ys \<le> length (x # xs)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
length ys \<le> length (x # xs)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
length ys = length (x # xs)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (chain)
picking this:
drop (length (x # xs) - length ys) (x # xs) = ys
length ys = length (x # xs) proof (prove)
using this:
drop (length (x # xs) - length ys) (x # xs) = ys
length ys = length (x # xs)

goal (1 subgoal):
 1. \<exists>zs. x # xs = zs @ ys proof (state)
this:
\<exists>zs. x # xs = zs @ ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
length ys = length (x # xs) \<Longrightarrow> \<exists>zs. x # xs = zs @ ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
length ys = length (x # xs) \<Longrightarrow> \<exists>zs. x # xs = zs @ ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
length ys = length (x # xs) \<Longrightarrow> \<exists>zs. x # xs = zs @ ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
length ys < length (x # xs)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (prove)
using this:
length ys < length (x # xs)

goal (1 subgoal):
 1. length ys \<le> length xs proof (state)
this:
length ys \<le> length xs

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (prove)
using this:
length ys \<le> length xs

goal (1 subgoal):
 1. drop (length xs - length ys) xs = drop (length (x # xs) - length ys) (x # xs) proof (state)
this:
drop (length xs - length ys) xs = drop (length (x # xs) - length ys) (x # xs)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (chain)
picking this:
drop (length (x # xs) - length ys) (x # xs) = ys
drop (length xs - length ys) xs = drop (length (x # xs) - length ys) (x # xs) proof (prove)
using this:
drop (length (x # xs) - length ys) (x # xs) = ys
drop (length xs - length ys) xs = drop (length (x # xs) - length ys) (x # xs)

goal (1 subgoal):
 1. \<exists>zs. x # xs = zs @ ys proof (state)
this:
\<exists>zs. x # xs = zs @ ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (state)
this:
length ys < length (x # xs) \<Longrightarrow> \<exists>zs. x # xs = zs @ ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. drop (length xs - length ys) xs = ys \<Longrightarrow> \<exists>zs. xs = zs @ ys; drop (length (a # xs) - length ys) (a # xs) = ys\<rbrakk> \<Longrightarrow> \<exists>zs. a # xs = zs @ ys proof (chain)
picking this:
length ys \<le> length (x # xs)
length ys = length (x # xs) \<Longrightarrow> \<exists>zs. x # xs = zs @ ys
length ys < length (x # xs) \<Longrightarrow> \<exists>zs. x # xs = zs @ ys proof (prove)
using this:
length ys \<le> length (x # xs)
length ys = length (x # xs) \<Longrightarrow> \<exists>zs. x # xs = zs @ ys
length ys < length (x # xs) \<Longrightarrow> \<exists>zs. x # xs = zs @ ys

goal (1 subgoal):
 1. \<exists>zs. x # xs = zs @ ys proof (state)
this:
\<exists>zs. x # xs = zs @ ys

goal:
No subgoals!