# Theory UnLam

Up to index of Isabelle/HOL/sHowe

theory UnLam = BiAbstr
files [UnLam.ML]:
(*
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