src/HOL/Proofs/Lambda/WeakNorm.thy
changeset 51143 0a2371e7ced3
parent 50336 1d9a31b58053
child 56073 29e308b56d23
     1.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Weak normalization for simply-typed lambda calculus *}
     1.5  
     1.6  theory WeakNorm
     1.7 -imports LambdaType NormalForm "~~/src/HOL/Library/Code_Integer"
     1.8 +imports LambdaType NormalForm "~~/src/HOL/Library/Code_Target_Int"
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -387,14 +387,16 @@
    1.13  *}
    1.14  
    1.15  ML {*
    1.16 +val nat_of_integer = @{code nat} o @{code int_of_integer};
    1.17 +
    1.18  fun dBtype_of_typ (Type ("fun", [T, U])) =
    1.19        @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
    1.20    | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
    1.21 -        ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
    1.22 +        ["'", a] => @{code Atom} (nat_of_integer (ord a - 97))
    1.23        | _ => error "dBtype_of_typ: variable name")
    1.24    | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
    1.25  
    1.26 -fun dB_of_term (Bound i) = @{code dB.Var} (@{code nat} i)
    1.27 +fun dB_of_term (Bound i) = @{code dB.Var} (nat_of_integer i)
    1.28    | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
    1.29    | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
    1.30    | dB_of_term _ = error "dB_of_term: bad term";
    1.31 @@ -402,23 +404,23 @@
    1.32  fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
    1.33        Abs ("x", T, term_of_dB (T :: Ts) U dBt)
    1.34    | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
    1.35 -and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code int_of_nat} n)
    1.36 +and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code integer_of_nat} n)
    1.37    | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
    1.38        let val t = term_of_dB' Ts dBt
    1.39        in case fastype_of1 (Ts, t) of
    1.40 -          Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
    1.41 +          Type ("fun", [T, _]) => t $ term_of_dB Ts T dBu
    1.42          | _ => error "term_of_dB: function type expected"
    1.43        end
    1.44    | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
    1.45  
    1.46  fun typing_of_term Ts e (Bound i) =
    1.47 -      @{code Var} (e, @{code nat} i, dBtype_of_typ (nth Ts i))
    1.48 +      @{code Var} (e, nat_of_integer i, dBtype_of_typ (nth Ts i))
    1.49    | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
    1.50          Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
    1.51            dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
    1.52            typing_of_term Ts e t, typing_of_term Ts e u)
    1.53        | _ => error "typing_of_term: function type expected")
    1.54 -  | typing_of_term Ts e (Abs (s, T, t)) =
    1.55 +  | typing_of_term Ts e (Abs (_, T, t)) =
    1.56        let val dBT = dBtype_of_typ T
    1.57        in @{code Abs} (e, dBT, dB_of_term t,
    1.58          dBtype_of_typ (fastype_of1 (T :: Ts, t)),