equal
deleted
inserted
replaced
402 |
402 |
403 AddIs [fst_imageI, snd_imageI, prod_fun_imageI]; |
403 AddIs [fst_imageI, snd_imageI, prod_fun_imageI]; |
404 AddSEs [fst_imageE, snd_imageE, prod_fun_imageE]; |
404 AddSEs [fst_imageE, snd_imageE, prod_fun_imageE]; |
405 |
405 |
406 |
406 |
407 (*simplification procedure for unit_eq; cannot use this rule directly -- loops!*) |
407 (*simplification procedure for unit_eq. |
|
408 Cannot use this rule directly -- it loops!*) |
408 local |
409 local |
409 val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT)); |
410 val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT)); |
410 val unit_meta_eq = standard (mk_meta_eq unit_eq); |
411 val unit_meta_eq = standard (mk_meta_eq unit_eq); |
411 fun proc _ _ t = |
412 fun proc _ _ t = |
412 if HOLogic.is_unit t then None |
413 if HOLogic.is_unit t then None |
414 in |
415 in |
415 val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc; |
416 val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc; |
416 end; |
417 end; |
417 |
418 |
418 Addsimprocs [unit_eq_proc]; |
419 Addsimprocs [unit_eq_proc]; |
|
420 |
|
421 |
|
422 (*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u), |
|
423 replacing it by f rather than by %u.f(). *) |
|
424 Goal "(%u::unit. f()) = f"; |
|
425 by (rtac ext 1); |
|
426 by (Simp_tac 1); |
|
427 qed "unit_abs_eta_conv"; |
|
428 Addsimps [unit_abs_eta_conv]; |
419 |
429 |
420 |
430 |
421 structure Prod_Syntax = (* FIXME eliminate (use HOLogic instead!) *) |
431 structure Prod_Syntax = (* FIXME eliminate (use HOLogic instead!) *) |
422 struct |
432 struct |
423 |
433 |