Expr.thy

(*
      File: Expr.thy
    Author: Simon Ambler (sja4@mcs.le.ac.uk)
 Copyright: Leicester University, 1998.
Time-stamp: <99/08/24 18:43:21 sja4>

	HOL theory of lambda expressions
	using deBruijn notation.

Proofs adapted from those given by Tobias Nipkow in HOL/Lambda/Lambda.ML
in the Isabelle98 distribution. See the paper

	Tobias Nipkow. More Church-Rosser Proofs (in Isabelle/HOL).
	In Automated Deduction - CADE-13, LNCS 1104, 1996, 733-747.
	http://www4.informatik.tu-muenchen.de/~nipkow/pubs/cade96.html

*)

Expr = Arith +

datatype name = tt   | ff   | cond  |
		zero | succ | ncase |
		pair | pfst | psnd  |
		nil  | cons | scase |
		rec

datatype expr =   Con name
		| Var nat
		| App expr expr		("(_) /@@ (_)" [60,61] 60)
		| Lam expr  

consts

  lift  :: "[expr,nat] => expr"
  subst :: "[expr,expr,nat] => expr"	("(_) [(_) '/ (_)]" [70,0,0] 70)

primrec lift expr

  lift_Con "lift (Con k)  j = Con k"
  lift_Var "lift (Var i)  j = (if i < j then Var i else Var(Suc i))"
  lift_App "lift (s @@ t) j = (lift s j) @@ (lift t j)"
  lift_Lam "lift (Lam s)  j = Lam (lift s (Suc j))"

primrec subst expr

  subst_Con "(Con k)[s/j]  = Con k"
  subst_Var "(Var i)[s/j]  = (if j < i then Var(pred i)
				else if i = j then s else Var i)"
  subst_App "(t @@ u)[s/j] = t[s/j] @@ u[s/j]"
  subst_Lam "(Lam t)[s/j]  = Lam (t[lift s 0 / Suc j])"

constdefs

  undef :: expr
  "undef == Con rec @@ Lam (Var 0)"

end

Theorems proved in Expr.ML:

Var k [u / k] = u

i < j ==> Var j [u / i] = Var (j - 1)

j < i ==> Var j [u / i] = Var j

i < Suc k ==> lift (lift t i) (Suc k) = lift (lift t k) i

j < Suc i ==> lift (t [s / j]) i = lift t (Suc i) [lift s i / j]

i < Suc j ==> lift (t [s / j]) i = lift t i [lift s i / Suc j]

lift t k [s / k] = t

i < Suc j ==> t [lift v i / Suc j] [u [v / j] / i] = t [u / i] [v / j]