theory Schedule_AI

lemma postfix_tails:
  "\<lbrakk> suffix (xs # ys) (tails zs) \<rbrakk>
     \<Longrightarrow> suffix xs zs \<and> (xs # ys) = tails xs" apply (induct zs arbitrary: xs ys) apply (clarsimp elim!: suffixE) apply (case_tac zs, simp_all)[1] apply (clarsimp elim!: suffixE) apply (case_tac zsa, simp_all) apply clarsimp apply clarsimp apply (erule meta_allE, erule meta_allE, drule meta_mp,
         rule suffix_appendI[OF suffix_order.refl]) apply clarsimp apply (erule suffix_ConsI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. suffix (xs # ys) (tails zs) \<Longrightarrow> suffix xs zs \<and> xs # ys = tails xs proof (prove)
goal (2 subgoals):
 1. \<And>xs ys. suffix (xs # ys) (tails []) \<Longrightarrow> suffix xs [] \<and> xs # ys = tails xs
 2. \<And>a zs xs ys. \<lbrakk>\<And>xs ys. suffix (xs # ys) (tails zs) \<Longrightarrow> suffix xs zs \<and> xs # ys = tails xs; suffix (xs # ys) (tails (a # zs))\<rbrakk> \<Longrightarrow> suffix xs (a # zs) \<and> xs # ys = tails xs proof (prove)
goal (2 subgoals):
 1. \<And>xs ys zs. [[]] = zs @ xs # ys \<Longrightarrow> xs = [] \<and> xs # ys = tails xs
 2. \<And>a zs xs ys. \<lbrakk>\<And>xs ys. suffix (xs # ys) (tails zs) \<Longrightarrow> suffix xs zs \<and> xs # ys = tails xs; suffix (xs # ys) (tails (a # zs))\<rbrakk> \<Longrightarrow> suffix xs (a # zs) \<and> xs # ys = tails xs proof (prove)
goal (1 subgoal):
 1. \<And>a zs xs ys. \<lbrakk>\<And>xs ys. suffix (xs # ys) (tails zs) \<Longrightarrow> suffix xs zs \<and> xs # ys = tails xs; suffix (xs # ys) (tails (a # zs))\<rbrakk> \<Longrightarrow> suffix xs (a # zs) \<and> xs # ys = tails xs proof (prove)
goal (1 subgoal):
 1. \<And>a zs xs ys zsa. \<lbrakk>\<And>xs ys. suffix (xs # ys) (tails zs) \<Longrightarrow> suffix xs zs \<and> xs # ys = tails xs; (a # zs) # tails zs = zsa @ xs # ys\<rbrakk> \<Longrightarrow> suffix xs (a # zs) \<and> xs # ys = tails xs proof (prove)
goal (2 subgoals):
 1. \<And>a zs xs zsa. \<lbrakk>\<And>xs ys. suffix (xs # ys) (tails zs) \<Longrightarrow> suffix xs zs \<and> xs # ys = tails xs; a # zs = xs; zsa = []\<rbrakk> \<Longrightarrow> xs # tails zs = tails xs
 2. \<And>a zs xs ys zsa list. \<lbrakk>\<And>xsa ysa. suffix (xsa # ysa) (list @ xs # ys) \<Longrightarrow> suffix xsa zs \<and> xsa # ysa = tails xsa; tails zs = list @ xs # ys; zsa = (a # zs) # list\<rbrakk> \<Longrightarrow> suffix xs (a # zs) \<and> xs # ys = tails xs proof (prove)
goal (1 subgoal):
 1. \<And>a zs xs ys zsa list. \<lbrakk>\<And>xsa ysa. suffix (xsa # ysa) (list @ xs # ys) \<Longrightarrow> suffix xsa zs \<and> xsa # ysa = tails xsa; tails zs = list @ xs # ys; zsa = (a # zs) # list\<rbrakk> \<Longrightarrow> suffix xs (a # zs) \<and> xs # ys = tails xs proof (prove)
goal (1 subgoal):
 1. \<And>a zs xs ys list. \<lbrakk>\<And>xsa ysa. suffix (xsa # ysa) (list @ xs # ys) \<Longrightarrow> suffix xsa zs \<and> xsa # ysa = tails xsa; tails zs = list @ xs # ys\<rbrakk> \<Longrightarrow> suffix xs (a # zs) \<and> xs # ys = tails xs proof (prove)
goal (1 subgoal):
 1. \<And>a zs xs ys list. \<lbrakk>tails zs = list @ xs # ys; suffix xs zs \<and> xs # ys = tails xs\<rbrakk> \<Longrightarrow> suffix xs (a # zs) \<and> xs # ys = tails xs proof (prove)
goal (1 subgoal):
 1. \<And>a zs xs ys list. \<lbrakk>tails zs = list @ tails xs; suffix xs zs; xs # ys = tails xs\<rbrakk> \<Longrightarrow> suffix xs (a # zs) proof (prove)
goal:
No subgoals!