[STATEMENT]
lemma foldl_rule_aux:
  fixes I :: "'\<sigma> \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes initial: "I \<sigma>0 l0"
  assumes step: "!!l1 l2 x \<sigma>. \<lbrakk> l0=l1@x#l2; I \<sigma> (x#l2) \<rbrakk> \<Longrightarrow> I (f \<sigma> x) l2"
  shows "I (foldl f \<sigma>0 l0) []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I (foldl f \<sigma>0 l0) []
[PROOF STEP]
using initial step
[PROOF STATE]
proof (prove)
using this:
I \<sigma>0 l0
\<lbrakk>l0 = ?l1.0 @ ?x # ?l2.0; I ?\<sigma> (?x # ?l2.0)\<rbrakk> \<Longrightarrow> I (f ?\<sigma> ?x) ?l2.0

goal (1 subgoal):
 1. I (foldl f \<sigma>0 l0) []
[PROOF STEP]
apply (induct l0 arbitrary: \<sigma>0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>0. \<lbrakk>I \<sigma>0 []; \<And>l1 x l2 \<sigma>. \<lbrakk>[] = l1 @ x # l2; I \<sigma> (x # l2)\<rbrakk> \<Longrightarrow> I (f \<sigma> x) l2\<rbrakk> \<Longrightarrow> I (foldl f \<sigma>0 []) []
 2. \<And>a l0 \<sigma>0. \<lbrakk>\<And>\<sigma>0. \<lbrakk>I \<sigma>0 l0; \<And>l1 x l2 \<sigma>. \<lbrakk>l0 = l1 @ x # l2; I \<sigma> (x # l2)\<rbrakk> \<Longrightarrow> I (f \<sigma> x) l2\<rbrakk> \<Longrightarrow> I (foldl f \<sigma>0 l0) []; I \<sigma>0 (a # l0); \<And>l1 x l2 \<sigma>. \<lbrakk>a # l0 = l1 @ x # l2; I \<sigma> (x # l2)\<rbrakk> \<Longrightarrow> I (f \<sigma> x) l2\<rbrakk> \<Longrightarrow> I (foldl f \<sigma>0 (a # l0)) []
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done