beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction
authorhuffman
Mon Dec 20 09:41:55 2010 -0800 (2010-12-20)
changeset 4132243a5b9a0ee8a
parent 41321 4e72b6fc9dd4
child 41323 ae1c227534f5
beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction
src/HOL/HOLCF/Cfun.thy
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Mon Dec 20 08:26:47 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Mon Dec 20 09:41:55 2010 -0800
     1.3 @@ -142,16 +142,19 @@
     1.4    using @{text beta_cfun} as a simp rule.  The advantage of the
     1.5    simproc is that it can avoid deeply-nested calls to the simplifier
     1.6    that would otherwise be caused by large continuity side conditions.
     1.7 +
     1.8 +  Update: The simproc now uses rule @{text Abs_cfun_inverse2} instead
     1.9 +  of @{text beta_cfun}, to avoid problems with eta-contraction.
    1.10  *}
    1.11  
    1.12 -simproc_setup beta_cfun_proc ("Abs_cfun f\<cdot>x") = {*
    1.13 +simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = {*
    1.14    fn phi => fn ss => fn ct =>
    1.15      let
    1.16        val dest = Thm.dest_comb;
    1.17 -      val (f, x) = (apfst (snd o dest o snd o dest) o dest) ct;
    1.18 +      val f = (snd o dest o snd o dest) ct;
    1.19        val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
    1.20 -      val tr = instantiate' [SOME T, SOME U] [SOME f, SOME x]
    1.21 -          (mk_meta_eq @{thm beta_cfun});
    1.22 +      val tr = instantiate' [SOME T, SOME U] [SOME f]
    1.23 +          (mk_meta_eq @{thm Abs_cfun_inverse2});
    1.24        val rules = Cont2ContData.get (Simplifier.the_context ss);
    1.25        val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
    1.26      in SOME (perhaps (SINGLE (tac 1)) tr) end
    1.27 @@ -251,10 +254,7 @@
    1.28  lemma lub_LAM:
    1.29    "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
    1.30      \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
    1.31 -apply (simp add: lub_cfun)
    1.32 -apply (simp add: Abs_cfun_inverse2)
    1.33 -apply (simp add: lub_fun ch2ch_lambda)
    1.34 -done
    1.35 +by (simp add: lub_cfun lub_fun ch2ch_lambda)
    1.36  
    1.37  lemmas lub_distribs = lub_APP lub_LAM
    1.38