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)),
```