1.1 --- a/src/HOLCF/Cfun.thy	Sat May 22 13:27:36 2010 -0700
     1.2 +++ b/src/HOLCF/Cfun.thy	Sat May 22 13:40:15 2010 -0700
     1.3 @@ -139,9 +139,37 @@
     1.4  lemma Abs_CFun_inverse2: "cont f \<Longrightarrow> Rep_CFun (Abs_CFun f) = f"
     1.5  by (simp add: Abs_CFun_inverse CFun_def)
     1.6  
     1.7 -lemma beta_cfun [simp]: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
     1.8 +lemma beta_cfun: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
     1.9  by (simp add: Abs_CFun_inverse2)
    1.10  
    1.11 +text {* Beta-reduction simproc *}
    1.12 +
    1.13 +text {*
    1.14 +  Given the term @{term "(\<Lambda> x. f x)\<cdot>y"}, the procedure tries to
    1.15 +  construct the theorem @{term "(\<Lambda> x. f x)\<cdot>y == f y"}.  If this
    1.16 +  theorem cannot be completely solved by the cont2cont rules, then
    1.17 +  the procedure returns the ordinary conditional @{text beta_cfun}
    1.18 +  rule.
    1.19 +
    1.20 +  The simproc does not solve any more goals that would be solved by
    1.21 +  using @{text beta_cfun} as a simp rule.  The advantage of the
    1.22 +  simproc is that it can avoid deeply-nested calls to the simplifier
    1.23 +  that would otherwise be caused by large continuity side conditions.
    1.24 +*}
    1.25 +
    1.26 +simproc_setup beta_cfun_proc ("Abs_CFun f\<cdot>x") = {*
    1.27 +  fn phi => fn ss => fn ct =>
    1.28 +    let
    1.29 +      val dest = Thm.dest_comb;
    1.30 +      val (f, x) = (apfst (snd o dest o snd o dest) o dest) ct;
    1.31 +      val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
    1.32 +      val tr = instantiate' [SOME T, SOME U] [SOME f, SOME x]
    1.33 +          (mk_meta_eq @{thm beta_cfun});
    1.34 +      val rules = Cont2ContData.get (Simplifier.the_context ss);
    1.35 +      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
    1.36 +    in SOME (perhaps (SINGLE (tac 1)) tr) end
    1.37 +*}
    1.38 +
    1.39  text {* Eta-equality for continuous functions *}
    1.40  
    1.41  lemma eta_cfun: "(\<Lambda> x. f\<cdot>x) = f"