# Theory Expr

Up to index of Isabelle/HOL/sHowe

theory Expr = Main
files [Expr.ML]:
```(*
File: Expr.thy
Author: Simon Ambler (sja4@mcs.le.ac.uk)
Copyright: Leicester University, 2001.
Time-stamp: <2002-04-08 16:27:18 sja4>

A de Bruijn representation of expressions
in the untyped lambda-calculus.

*)

Expr = Main +

types

var = nat         (* an enumerable set of free variable names *)

bnd = nat         (* indices for bound variables *)

datatype 'a expr
= CON 'a
| VAR var
| BND bnd
| APP ('a expr) ('a expr)               ("(_) /\$\$ (_)" [200,201] 200)
| ABS ('a expr)

consts

(* level predicate determines expressions which are well-formed
at each de Bruijn level.

`level i s' holds if and only if the addition of i enclosing
ABS constructors results in an expression which is well-formed
and has no dangling references.

*)

levelSet :: "(bnd * 'a expr) set"

(* instantiation of a bound variable by an expression *)

inst  :: "[bnd, 'a expr, 'a expr] => 'a expr"

(* simultaneous instantiation of consecutive bound variables *)

insts :: "[bnd, ('a expr) list, 'a expr] => 'a expr"

(* variable name does not occur in expression *)

newFor  :: "[var, 'a expr] => bool"

(* function to generate fresh variable names *)

gV :: "'a expr => var"

(* substitution for a free variable *)

subst :: "['a expr, var, 'a expr] => 'a expr"

syntax

level :: "[bnd, 'a expr] => bool"

translations

"level i s" == "(i,s) : levelSet"

constdefs

free  :: "[var, 'a expr] => bool"
"free == % n s. ~newFor n s"

closed :: "'a expr => bool"
"closed == % s. (! n. newFor n s)"

proper :: 'a expr => bool
"proper == % s. level 0 s"

inductive levelSet
intrs

level_CON "level i (CON a)"
level_VAR "level i (VAR n)"
level_BND "j<i ==> level i (BND j)"
level_APP "[| level i s; level i t |] ==> level i (s \$\$ t)"
level_ABS "level (Suc i) s ==> level i (ABS s)"

primrec

"inst k u (CON a) = CON a"
"inst k u (VAR i) = VAR i"
"inst k u (BND i) = (if i=k then u else BND i)"
"inst k u (s \$\$ t) = inst k u s \$\$ inst k u t"
"inst k u (ABS s) = ABS (inst (Suc k) u s)"

primrec

(* simultaneous instantiation of consecutive bound variables,
starting from level i, by expressions in the list xs *)

"insts i xs (CON a) = CON a"
"insts i xs (VAR n) = VAR n"
"insts i xs (BND j) = (if i<=j & j-i < length xs then xs!(j-i) else BND j)"
"insts i xs (s \$\$ t) = insts i xs s \$\$ insts i xs t"
"insts i xs (ABS s) = ABS (insts (Suc i) xs s)"

primrec

"newFor j (CON a) = True"
"newFor j (VAR i) = (j~=i)"
"newFor j (BND i) = True"
"newFor j (s \$\$ t) = (newFor j s & newFor j t)"
"newFor j (ABS s) = (newFor j s)"

primrec

"gV (CON a) = 0"
"gV (VAR i) = Suc i"
"gV (BND i) = 0"
"gV (s \$\$ t) = max (gV s) (gV t)"
"gV (ABS s) = (gV s)"

primrec

"subst (CON a) n u = CON a"
"subst (VAR m) n u = (if n=m then u else VAR m)"
"subst (BND i) n u = BND i"
"subst (s \$\$ t) n u = subst s n u \$\$ subst t n u"
"subst (ABS s) n u = ABS (subst s n u)"

end

```

theorem level_le_level:

`  [| level i s; i <= j |] ==> level j s`

theorem level_0_level:

`  level 0 s ==> level i s`

theorem gV_newFor:

`  gV s <= j ==> newFor j s`

theorem newFor_gV:

`  newFor (gV s) s`

theorem level_inst_id:

`  [| level i s; i <= j |] ==> inst j u s = s`

theorem proper_inst:

`  proper s ==> inst j u s = s`

theorem proper_CON:

`  proper (CON a)`

theorem proper_VAR:

`  proper (VAR n)`

theorem proper_APP:

`  [| proper s; proper t |] ==> proper (s \$\$ t)`

theorem proper_APP_E:

`  [| proper (s \$\$ t); [| proper s; proper t |] ==> P |] ==> P`

theorem proper_APPD1:

`  proper (s \$\$ t) ==> proper s`

theorem proper_APPD2:

`  proper (s \$\$ t) ==> proper t`

theorem proper_BND_E:

`  proper (BND j) ==> P`

theorem not_proper_BND:

`  ¬ proper (BND j)`

theorem inst_swap:

```  [| level 0 s; level 0 t; i ~= j |]
==> inst i s (inst j t u) = inst j t (inst i s u)```

theorem newFor_subst:

`  newFor n (subst s m t) = ((newFor n s | n = m) & (newFor n t | newFor m s))`

theorem subst_VAR_id:

`  subst s n (VAR n) = s`

theorem newFor_subst_id:

`  newFor n s ==> subst s n u = s`