theory Ipc_AI

lemma list_all2_zip_same:
  assumes rl: "\<And>a a' x y. P (x, a) (y, a) \<Longrightarrow> P (x, a') (y, a')"
  shows "list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as)" apply (induct xs arbitrary: as ys a) apply simp apply (case_tac as) apply simp apply simp apply (case_tac ys) apply simp apply clarsimp apply (erule rl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as) proof (prove)
goal (2 subgoals):
 1. \<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) [] ys \<Longrightarrow> list_all2 P (zip [] as) (zip ys as)
 2. \<And>a xs as ys aa. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) (a # xs) ys\<rbrakk> \<Longrightarrow> list_all2 P (zip (a # xs) as) (zip ys as) proof (prove)
goal (1 subgoal):
 1. \<And>a xs as ys aa. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) (a # xs) ys\<rbrakk> \<Longrightarrow> list_all2 P (zip (a # xs) as) (zip ys as) proof (prove)
goal (2 subgoals):
 1. \<And>a xs as ys aa. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) (a # xs) ys; as = []\<rbrakk> \<Longrightarrow> list_all2 P (zip (a # xs) as) (zip ys as)
 2. \<And>a xs as ys aa ab list. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) (a # xs) ys; as = ab # list\<rbrakk> \<Longrightarrow> list_all2 P (zip (a # xs) as) (zip ys as) proof (prove)
goal (1 subgoal):
 1. \<And>a xs as ys aa ab list. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) (a # xs) ys; as = ab # list\<rbrakk> \<Longrightarrow> list_all2 P (zip (a # xs) as) (zip ys as) proof (prove)
goal (1 subgoal):
 1. \<And>a xs as ys aa ab list. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) (a # xs) ys; as = ab # list\<rbrakk> \<Longrightarrow> list_all2 P ((a, ab) # zip xs list) (zip ys (ab # list)) proof (prove)
goal (2 subgoals):
 1. \<And>a xs as ys aa ab list. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) (a # xs) ys; as = ab # list; ys = []\<rbrakk> \<Longrightarrow> list_all2 P ((a, ab) # zip xs list) (zip ys (ab # list))
 2. \<And>a xs as ys aa ab list ac lista. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) (a # xs) ys; as = ab # list; ys = ac # lista\<rbrakk> \<Longrightarrow> list_all2 P ((a, ab) # zip xs list) (zip ys (ab # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs as ys aa ab list ac lista. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) (a # xs) ys; as = ab # list; ys = ac # lista\<rbrakk> \<Longrightarrow> list_all2 P ((a, ab) # zip xs list) (zip ys (ab # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa ab ac lista. \<lbrakk>\<And>as ys a. list_all2 (\<lambda>x y. P (x, a) (y, a)) xs ys \<Longrightarrow> list_all2 P (zip xs as) (zip ys as); P (a, aa) (ac, aa); list_all2 (\<lambda>x y. P (x, aa) (y, aa)) xs lista\<rbrakk> \<Longrightarrow> P (a, ab) (ac, ab) proof (prove)
goal:
No subgoals!