Theory Expr

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