338 

   338 

   339 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"

   339 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"

   340 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})

   340 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})

   341 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})

   341 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})

   342 apply(tactic {* regularize_tac @{context} 1 *})

   342 apply(tactic {* regularize_tac @{context} 1 *})

   344 apply(tactic {* clean_tac @{context} 1 *})

   344 apply(tactic {* clean_tac @{context} 1 *})

   346 done

   345 done

   347 

   346 

   348 lemma list_induct_part:

   347 lemma list_induct_part:

   349   assumes a: "P (x :: 'a list) ([] :: 'c list)"

   348   assumes a: "P (x :: 'a list) ([] :: 'c list)"

   350   assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"

   349   assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"