340 |
344 |
341 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
345 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
342 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
346 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
343 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
347 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
344 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
348 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
345 prefer 2 |
349 defer |
346 apply(tactic {* clean_tac @{context} 1 *}) |
350 apply(tactic {* clean_tac @{context} 1 *}) |
347 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
351 apply(tactic {* inj_repabs_tac_fset @{context} 1*})+ |
348 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
349 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
|
350 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
|
351 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
352 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
|
353 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
|
354 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
|
355 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
|
356 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
|
357 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
358 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
359 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
360 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *) |
|
361 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
|
362 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
|
363 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
|
364 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
|
365 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
|
366 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *) |
|
367 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
|
368 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
369 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
|
370 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
|
371 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
|
372 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
|
373 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
|
374 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
375 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
376 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
377 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
378 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
|
379 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
380 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
381 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
382 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
|
383 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
|
384 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *) |
|
385 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
|
386 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
387 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
388 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
|
389 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
390 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
391 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
392 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
393 done |
352 done |
394 |
353 |
395 lemma list_induct_part: |
354 lemma list_induct_part: |
396 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
355 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
397 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
356 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |