Up to index of Isabelle/HOL/sHowe

(* 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