theory More_Sublist

lemma list_all2_induct_suffixeq [consumes 1, case_names Nil Cons]:
  assumes lall: "list_all2 Q as bs"
  and     nilr: "P [] []"
  and    consr: "\<And>x xs y ys.
  \<lbrakk>list_all2 Q xs ys; Q x y; P xs ys; suffix (x # xs) as; suffix (y # ys) bs\<rbrakk>
  \<Longrightarrow> P (x # xs) (y # ys)"
  shows  "P as bs" proof - define as' where "as' == as" define bs' where "bs' == bs" have "suffix as as' \<and> suffix bs bs'" unfolding as'_def bs'_def by simp then show ?thesis using lall proof (induct rule: list_induct2 [OF list_all2_lengthD [OF lall]]) case 1 show ?case by fact next case (2 x xs y ys) show ?case proof (rule consr) from "2.prems" show "list_all2 Q xs ys" and "Q x y" by simp_all then show "P xs ys" using "2.hyps" "2.prems" by (auto dest: suffix_ConsD) from "2.prems" show "suffix (x # xs) as" and "suffix (y # ys) bs" by (auto simp: as'_def bs'_def) qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P as bs proof (state)
goal (1 subgoal):
 1. P as bs proof (state)
this:
as' \<equiv> as

goal (1 subgoal):
 1. P as bs proof (state)
this:
bs' \<equiv> bs

goal (1 subgoal):
 1. P as bs proof (prove)
goal (1 subgoal):
 1. suffix as as' \<and> suffix bs bs' proof (prove)
goal (1 subgoal):
 1. suffix as as \<and> suffix bs bs proof (state)
this:
suffix as as' \<and> suffix bs bs'

goal (1 subgoal):
 1. P as bs proof (chain)
picking this:
suffix as as' \<and> suffix bs bs' proof (prove)
using this:
suffix as as' \<and> suffix bs bs'

goal (1 subgoal):
 1. P as bs proof (prove)
using this:
suffix as as' \<and> suffix bs bs'
list_all2 Q as bs

goal (1 subgoal):
 1. P as bs proof (state)
goal (2 subgoals):
 1. \<lbrakk>suffix [] as' \<and> suffix [] bs'; list_all2 Q [] []\<rbrakk> \<Longrightarrow> P [] []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>suffix xs as' \<and> suffix ys bs'; list_all2 Q xs ys\<rbrakk> \<Longrightarrow> P xs ys; suffix (x # xs) as' \<and> suffix (y # ys) bs'; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (state)
this:
suffix [] as' \<and> suffix [] bs'
list_all2 Q [] []

goal (2 subgoals):
 1. \<lbrakk>suffix [] as' \<and> suffix [] bs'; list_all2 Q [] []\<rbrakk> \<Longrightarrow> P [] []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>suffix xs as' \<and> suffix ys bs'; list_all2 Q xs ys\<rbrakk> \<Longrightarrow> P xs ys; suffix (x # xs) as' \<and> suffix (y # ys) bs'; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (prove)
goal (1 subgoal):
 1. P [] [] proof (state)
this:
P [] []

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>suffix xs as' \<and> suffix ys bs'; list_all2 Q xs ys\<rbrakk> \<Longrightarrow> P xs ys; suffix (x # xs) as' \<and> suffix (y # ys) bs'; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>suffix xs as' \<and> suffix ys bs'; list_all2 Q xs ys\<rbrakk> \<Longrightarrow> P xs ys; suffix (x # xs) as' \<and> suffix (y # ys) bs'; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (state)
this:
length xs = length ys
\<lbrakk>suffix xs as' \<and> suffix ys bs'; list_all2 Q xs ys\<rbrakk> \<Longrightarrow> P xs ys
suffix (x # xs) as' \<and> suffix (y # ys) bs'
list_all2 Q (x # xs) (y # ys)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>suffix xs as' \<and> suffix ys bs'; list_all2 Q xs ys\<rbrakk> \<Longrightarrow> P xs ys; suffix (x # xs) as' \<and> suffix (y # ys) bs'; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (prove)
goal (1 subgoal):
 1. P (x # xs) (y # ys) proof (state)
goal (5 subgoals):
 1. list_all2 Q xs ys
 2. Q x y
 3. P xs ys
 4. suffix (x # xs) as
 5. suffix (y # ys) bs proof (chain)
picking this:
suffix (x # xs) as' \<and> suffix (y # ys) bs'
list_all2 Q (x # xs) (y # ys) proof (prove)
using this:
suffix (x # xs) as' \<and> suffix (y # ys) bs'
list_all2 Q (x # xs) (y # ys)

goal (1 subgoal):
 1. list_all2 Q xs ys &&& Q x y proof (state)
this:
list_all2 Q xs ys
Q x y

goal (3 subgoals):
 1. P xs ys
 2. suffix (x # xs) as
 3. suffix (y # ys) bs proof (chain)
picking this:
list_all2 Q xs ys
Q x y proof (prove)
using this:
list_all2 Q xs ys
Q x y

goal (1 subgoal):
 1. P xs ys proof (prove)
using this:
list_all2 Q xs ys
Q x y
length xs = length ys
\<lbrakk>suffix xs as' \<and> suffix ys bs'; list_all2 Q xs ys\<rbrakk> \<Longrightarrow> P xs ys
suffix (x # xs) as' \<and> suffix (y # ys) bs'
list_all2 Q (x # xs) (y # ys)

goal (1 subgoal):
 1. P xs ys proof (state)
this:
P xs ys

goal (2 subgoals):
 1. suffix (x # xs) as
 2. suffix (y # ys) bs proof (chain)
picking this:
suffix (x # xs) as' \<and> suffix (y # ys) bs'
list_all2 Q (x # xs) (y # ys) proof (prove)
using this:
suffix (x # xs) as' \<and> suffix (y # ys) bs'
list_all2 Q (x # xs) (y # ys)

goal (1 subgoal):
 1. suffix (x # xs) as &&& suffix (y # ys) bs proof (state)
this:
suffix (x # xs) as
suffix (y # ys) bs

goal:
No subgoals! proof (state)
this:
P (x # xs) (y # ys)

goal:
No subgoals! proof (state)
this:
P as bs

goal:
No subgoals!