Theory UnLam

Up to index of Isabelle/HOL/sHowe

(*
      File: UnLam.thy
    Author: AM
 Copyright: Leicester University, 2001.
Time-stamp: <2002-04-10 18:41:51 am133>

  Hybrid syntax representation of the
  Untyped Lambda Calculus

*)


UnLam = BiAbstr +

datatype con
        = cApp
        | cLam

types

  uexp = con expr

consts

  isexpSet :: uexp set

syntax

  isexp :: "uexp => bool"

translations

  "isexp p" == "p : isexpSet"

constdefs

  App :: "[uexp,uexp] => uexp"          ("(_) /$ (_)" [200,201] 200)
  "p $ q  == CON cApp $$ p $$ q"

  bLam :: "[ uexp => uexp] => uexp"      (binder "lam " 190)
  "bLam e ==  CON cLam  $$ lambda e"

rules

(* isexp_sub "[| abstr E; isexp p; isexp (bLam E) |] ==> isexp (E p)" *)
isexp_sub "[| abstr E; isexp p; !n . isexp  (E (VAR n)) |] ==> isexp (E p)" 
isexp_sub2 "[|isexp s ;isexp p|] ==> isexp (subst s a p)"

isexp_induct  "[| isexp u; \
        \ !! n. P (VAR n); \
        \ !! s t. [| isexp s; P s; isexp t; P t |] ==> P (s $ t); \
        \ !! e. [| abstr e; ! t. isexp t --> P t --> P (e t) |] \
                        \ ==> P (lam x. e x) |] \
                \ ==> P u"
abstr_induct
        "[| abstr e; \
        \     !! j. P (% x. VAR j); \
        \           P (% x. x); \
        \   !! f g. [| abstr f; P f; abstr g; P g |] ==> P (% x. f x $ g x); \
        \     !! f. [| biAbstr f; ! n. P (% x. f x (VAR n)); \
                                \ ! n. P (% x. f (VAR n) x) |] \
                        \ ==> P (% x. lam y. f x y) \
        \ |] ==> P e"

inductive isexpSet
intrs

isexp_VAR       "isexp (VAR n)"
isexp_or        "[| isexp p; isexp q |] ==> isexp (p $ q)"
isexp_all       "[|abstr p ; !y . isexp (p (VAR y))|] ==> isexp (lam x .  p x)"


end

theorem abstr_LAM_inject:

  [| abstr e; abstr f; LAM x. e x = LAM y. f y |] ==> e = f

theorem id_neq_VAR:

  (%x. x) = (%x. VAR n) ==> False

theorem abstr_LAM_simp2:

  [| abstr e; abstr f; LAM x. e x = lambda f |] ==> e = f

theorem App_inject1:

  f $ p = e1 $ e2 ==> f = e1 & p = e2

theorem App_cong:

  f = e1 & p = e2 ==> f $ p = e1 $ e2

theorem App_inject:

  (f $ p = e1 $ e2) = (f = e1 & p = e2)

theorem clash_App_Lam:

  e1 $ e2 = lam x. Ea x ==> P

theorem bLam_inject:

  [| abstr E; abstr Ea |] ==> (bLam E = bLam Ea) = (E = Ea)

theorem bLam_inject1:

  [| abstr E; abstr Ea; bLam E = bLam Ea |] ==> E = Ea

theorem isexp_proper:

  isexp e ==> proper e

theorem isexp_abstr_const:

  isexp s ==> abstr (%x. s)

theorem isexp_Abs_E:

  [| isexp (bLam E);
     !!p. [| lambda E = lambda p; abstr p; ALL y. isexp (p (VAR y)) |] ==> P |]
  ==> P