374 (Conv.params_conv ~1 (fn ctxt => |
374 (Conv.params_conv ~1 (fn ctxt => |
375 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
375 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
376 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
376 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
377 *} |
377 *} |
378 |
378 |
|
379 (* |
379 ML {* |
380 ML {* |
380 lambda_prs_conv @{context} quot |
381 lambda_prs_conv @{context} quot |
381 @{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x\<Colon>'a list \<Rightarrow> bool. id ((f ((REP_fset ---> id) x) ((REP_fset ---> id) x))))"} |
382 @{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x\<Colon>'a list \<Rightarrow> bool. id ((f ((REP_fset ---> id) x) ((REP_fset ---> id) x))))"} |
382 *} |
383 *} |
383 |
384 |
393 (ABS_fset ---> id) ((REP_fset ---> id) P) |
394 (ABS_fset ---> id) ((REP_fset ---> id) P) |
394 (REP_fset (ABS_fset (a # REP_fset (ABS_fset list))))))) \<longrightarrow> |
395 (REP_fset (ABS_fset (a # REP_fset (ABS_fset list))))))) \<longrightarrow> |
395 (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)))))"} |
396 (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)))))"} |
396 |
397 |
397 *} |
398 *} |
398 |
399 *) |
399 |
400 |
400 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
401 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
401 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) |
402 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) |
402 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
403 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
403 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
404 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
404 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
405 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
405 |
406 oops |
406 |
407 |
|
408 (* |
407 thm LAMBDA_PRS |
409 thm LAMBDA_PRS |
408 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *}) |
410 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *}) |
409 |
411 |
410 apply(tactic {* (lambda_prs_tac @{context} quot) 1 *}) |
412 apply(tactic {* (lambda_prs_tac @{context} quot) 1 *}) |
411 |
413 |
412 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) |
414 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) |
413 |
415 |
414 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
416 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
415 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
417 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
416 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
418 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
417 ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *} |
419 ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}*) |
418 |
420 |
419 |
421 |
420 |
422 lemma "\<forall>f x xa. fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
421 |
|
422 thm map_append |
|
423 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
|
424 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) |
423 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) |
425 apply(tactic {* prepare_tac 1 *}) |
424 oops |
426 thm map_append |
425 |
427 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
426 |
428 done |
427 lemma "fmap f (FUNION (x::'b fset) (y::'b fset)) = FUNION (fmap f x) (fmap f y)" |
429 |
428 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) |
|
429 oops |
430 |
430 |
431 |
431 |
432 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
432 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
433 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
433 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
434 done |
434 done |