335 lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) = |
335 lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) = |
336 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" |
336 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" |
337 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
337 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
338 done |
338 done |
339 |
339 |
340 (* |
340 ML {* |
341 ML {* |
341 |
342 fun lambda_prs_conv ctxt ctrm = |
342 fun lambda_prs_conv ctxt quot ctrm = |
343 case (Thm.term_of ctrm) of |
343 case (Thm.term_of ctrm) of |
344 (@{term "op --->"} $ x $ y) $ (Abs (_, T, x)) => |
344 (Const (@{const_name "fun_map"}, _) $ y $ z) $ (Abs (_, T, x)) => |
345 let |
345 let |
|
346 val _ = tracing "AAA"; |
346 val lty = T; |
347 val lty = T; |
347 val rty = fastype_of x; |
348 val rty = fastype_of x; |
348 val thy = ProofContext.theory_of ctxt; |
349 val thy = ProofContext.theory_of ctxt; |
349 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
350 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
350 val inst = [SOME lcty, NONE, SOME rcty]; |
351 val inst = [SOME lcty, NONE, SOME rcty]; |
351 val lpi = Drule.instantiate' inst [] thm; |
352 val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS}; |
352 |
353 val tac = |
353 (Conv.all_conv ctrm) |
354 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
354 | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt) ctrm |
355 (quotient_tac quot); |
355 | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt) ctxt ctrm |
356 val gc = Drule.strip_imp_concl (cprop_of lpi); |
|
357 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
|
358 val _ = tracing (Syntax.string_of_term @{context} (prop_of t)) |
|
359 in |
|
360 Conv.rewr_conv (eq_reflection OF [t]) ctrm |
|
361 end |
|
362 | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm |
|
363 | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm |
356 | _ => Conv.all_conv ctrm |
364 | _ => Conv.all_conv ctrm |
357 *} |
365 *} |
358 |
366 |
359 |
367 ML {* |
360 ML {* |
368 lambda_prs_conv @{context} quot |
361 fun lambda_prs_tac ctxt = CSUBGOAL (fn (goal, i) => |
369 *} |
|
370 |
|
371 ML {* |
|
372 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => |
362 CONVERSION |
373 CONVERSION |
363 (Conv.params_conv ~1 (fn ctxt => |
374 (Conv.params_conv ~1 (fn ctxt => |
364 (Conv.prems_conv ~1 (lambda_prs_conv ctxt) then_conv |
375 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
365 Conv.concl_conv ~1 (lambda_prs_conv ctxt))) ctxt) i) |
376 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
366 *} |
377 *} |
367 *) |
378 |
|
379 ML {* |
|
380 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 *} |
|
383 |
|
384 ML {* |
|
385 @{cterm "((ABS_fset ---> id) ---> id) |
|
386 (\<lambda>P. |
|
387 All ((REP_fset ---> id) |
|
388 (\<lambda>list. |
|
389 (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \<longrightarrow> |
|
390 (\<forall>a. All ((REP_fset ---> id) |
|
391 (\<lambda>list. |
|
392 (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)) \<longrightarrow> |
|
393 (ABS_fset ---> id) ((REP_fset ---> id) P) |
|
394 (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 |
|
397 *} |
|
398 |
|
399 |
|
400 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 {* 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 (allex_prs_tac @{context} quot) 1 *}) |
|
405 |
|
406 |
|
407 thm LAMBDA_PRS |
|
408 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *}) |
|
409 |
|
410 apply(tactic {* (lambda_prs_tac @{context} quot) 1 *}) |
|
411 |
|
412 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) |
|
413 |
|
414 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
|
415 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
|
416 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"} *} |
|
418 |
|
419 |
|
420 |
368 |
421 |
369 thm map_append |
422 thm map_append |
370 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
423 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
371 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) |
424 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) |
372 apply(tactic {* prepare_tac 1 *}) |
425 apply(tactic {* prepare_tac 1 *}) |
373 thm map_append |
426 thm map_append |
374 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
427 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
375 done |
428 done |
376 |
429 |
377 |
430 |
378 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
|
379 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) |
|
380 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
|
381 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
|
382 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
|
383 thm LAMBDA_PRS |
|
384 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *}) |
|
385 |
|
386 apply(tactic {* (lambda_prs_tac @{context} quot) 1 *}) |
|
387 |
|
388 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) |
|
389 |
|
390 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
|
391 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
|
392 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
|
393 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"} *} |
|
394 |
431 |
395 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
432 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
396 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
433 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
397 done |
434 done |
398 |
435 |