Efficient_Nat streamlined and improved
authorhaftmann
Mon Jan 21 08:45:36 2008 +0100 (2008-01-21)
changeset 259382c1c0e989615
parent 25937 6e5b0f176dac
child 25939 ddea202704b4
Efficient_Nat streamlined and improved
src/HOL/Complex/ex/linreif.ML
src/HOL/ex/coopereif.ML
     1.1 --- a/src/HOL/Complex/ex/linreif.ML	Mon Jan 21 08:43:37 2008 +0100
     1.2 +++ b/src/HOL/Complex/ex/linreif.ML	Mon Jan 21 08:45:36 2008 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4        | Const("RealDef.real",_)$ @{term "1::int"} => C 1
     1.5        | @{term "0::real"} => C 0
     1.6        | @{term "0::real"} => C 1
     1.7 -      | Term.Bound i => Bound (nat i)
     1.8 +      | Term.Bound i => Bound i
     1.9        | Const (@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
    1.10        | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
    1.11        | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
    1.12 @@ -60,9 +60,9 @@
    1.13  
    1.14  
    1.15  fun start_vs t =
    1.16 -    let val fs = term_frees t
    1.17 -    in fs ~~ map nat (0 upto  (length fs - 1))
    1.18 -    end ;
    1.19 +  let
    1.20 +    val fs = term_frees t
    1.21 +  in fs ~~ (0 upto (length fs - 1)) end;
    1.22  
    1.23  (* transform num and fm back to terms *)
    1.24  
    1.25 @@ -111,9 +111,8 @@
    1.26  (* The oracle *)
    1.27  
    1.28  fun linrqe_oracle thy t = 
    1.29 -    let 
    1.30 -	val vs = start_vs t
    1.31 -    in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (linrqe (fm_of_term vs t))))
    1.32 -    end;
    1.33 +  let 
    1.34 +    val vs = start_vs t
    1.35 +  in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (linrqe (fm_of_term vs t)))) end;
    1.36  
    1.37  end;
     2.1 --- a/src/HOL/ex/coopereif.ML	Mon Jan 21 08:43:37 2008 +0100
     2.2 +++ b/src/HOL/ex/coopereif.ML	Mon Jan 21 08:45:36 2008 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4      | SOME n => Bound n)
     2.5      | @{term "0::int"} => C 0
     2.6      | @{term "1::int"} => C 1
     2.7 -    | Term.Bound i => Bound (nat i)
     2.8 +    | Term.Bound i => Bound 0
     2.9      | Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t')
    2.10      | Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
    2.11      | Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
    2.12 @@ -42,12 +42,12 @@
    2.13        | Const("Not",_)$t' => Not(qf_of_term ps vs t')
    2.14        | Const("Ex",_)$Abs(xn,xT,p) => 
    2.15           let val (xn',p') = variant_abs (xn,xT,p)
    2.16 -             val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
    2.17 +             val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1 + n)) vs)
    2.18           in E (qf_of_term ps vs' p')
    2.19           end
    2.20        | Const("All",_)$Abs(xn,xT,p) => 
    2.21           let val (xn',p') = variant_abs (xn,xT,p)
    2.22 -             val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
    2.23 +             val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1 + n)) vs)
    2.24           in A (qf_of_term ps vs' p')
    2.25           end
    2.26        | _ =>(case AList.lookup (op aconv) ps t of 
    2.27 @@ -77,8 +77,7 @@
    2.28      val fs = term_frees t
    2.29      val ps = term_bools [] t
    2.30    in
    2.31 -    (fs ~~ (map nat (0 upto  (length fs - 1))),
    2.32 -      ps ~~ (map nat (0 upto  (length ps - 1))))
    2.33 +    (fs ~~ (0 upto (length fs - 1)), ps ~~ (0 upto (length ps - 1)))
    2.34    end;
    2.35  
    2.36  fun term_of_i vs t = case t