src/HOLCF/domain/theorems.ML
changeset 16403 294a7864063e
parent 16394 495dbcd4f4c9
child 16462 8ebc8f530ab4
     1.1 --- a/src/HOLCF/domain/theorems.ML	Wed Jun 15 21:48:35 2005 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Jun 15 23:35:43 2005 +0200
     1.3 @@ -93,36 +93,6 @@
     1.4  (* ----- generating beta reduction rules from definitions-------------------- *)
     1.5  
     1.6  local
     1.7 -  fun k NONE = cont_const | k (SOME x) = x;
     1.8 -  
     1.9 -  fun ap NONE NONE = NONE
    1.10 -  |   ap x    y    = SOME (standard (cont2cont_Rep_CFun OF [k x, k y]));
    1.11 -
    1.12 -  fun var 0 = [SOME cont_id]
    1.13 -  |   var n = NONE :: var (n-1);
    1.14 -
    1.15 -  fun zip []      []      = []
    1.16 -  |   zip []      (y::ys) = (ap NONE y   ) :: zip [] ys
    1.17 -  |   zip (x::xs) []      = (ap x    NONE) :: zip xs []
    1.18 -  |   zip (x::xs) (y::ys) = (ap x    y   ) :: zip xs ys
    1.19 -
    1.20 -  fun lam [] = ([], cont_const)
    1.21 -  |   lam (x::ys) = let val x' = k x
    1.22 -                        val Lx = x' RS cont2cont_LAM
    1.23 -                    in  (map (fn y => SOME (k y RS Lx)) ys, x')
    1.24 -                    end;
    1.25 -
    1.26 -  fun term_conts (Bound n) = (var n, [])
    1.27 -  |   term_conts (Const _) = ([],[])
    1.28 -  |   term_conts (Const _ $ Abs (_,_,t)) = let
    1.29 -          val (cs,ls) = term_conts t
    1.30 -          val (cs',l) = lam cs
    1.31 -          in  (cs',l::ls)
    1.32 -          end
    1.33 -  |   term_conts (Const _ $ f $ t)
    1.34 -         = (zip (fst (term_conts f)) (fst (term_conts t)), [])
    1.35 -  |   term_conts t = let val dummy = prin t in ([],[]) end;
    1.36 -
    1.37    fun arglist (Const _ $ Abs (s,_,t)) = let
    1.38          val (vars,body) = arglist t
    1.39          in  (s :: vars, body) end
    1.40 @@ -131,12 +101,12 @@
    1.41    fun bound_vars 0 = [] | bound_vars i = (Bound (i-1) :: bound_vars (i-1));
    1.42  in
    1.43    fun appl_of_def def = let
    1.44 -        val (_ $ con $ lam) = concl_of def
    1.45 -        val (vars, rhs) = arglist lam
    1.46 -        val lhs = Library.foldl (op `) (con, bound_vars (length vars));
    1.47 -        val appl = bind_fun vars (lhs == rhs)
    1.48 -        val ([],cs) = term_conts lam
    1.49 -        val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs
    1.50 +        val (_ $ con $ lam) = concl_of def;
    1.51 +        val (vars, rhs) = arglist lam;
    1.52 +        val lhs = mk_cRep_CFun (con, bound_vars (length vars));
    1.53 +        val appl = bind_fun vars (lhs == rhs);
    1.54 +        val cs = ContProc.cont_thms lam;
    1.55 +        val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
    1.56          in pg (def::betas) appl [rtac reflexive_thm 1] end;
    1.57  end;
    1.58