Up to index of Isabelle/HOL/sHowe
theory Abstr = Expr(*
File: Abstr.thy
Author: Simon Ambler (sja4@mcs.le.ac.uk)
Copyright: Leicester University, 2001.
Time-stamp: <2002-04-08 15:25:41 sja4>
Abstract syntax for the Lambda Calculus
*)
Abstr = Expr +
consts
abstSet :: "(bnd * ('a expr => 'a expr)) set"
lbndSet :: "(bnd * ('a expr => 'a expr) * 'a expr) set"
syntax
abst :: "[bnd, 'a expr => 'a expr] => bool"
lbnd :: "[bnd, 'a expr => 'a expr, 'a expr] => bool"
translations
"abst i e" == "(i, e) : abstSet"
"lbnd i e s" == "(i, e, s) : lbndSet"
constdefs
abstr :: "('a expr => 'a expr) => bool"
"abstr == % e. abst 0 e"
lambda :: "('a expr => 'a expr) => 'a expr" (binder "LAM " 190)
"lambda == % e. ABS (lbind 0 e)"
lbind :: "[bnd, 'a expr => 'a expr] => 'a expr"
"lbind == % i e. @ s. (i, e, s) : lbndSet"
ordinary :: "('a expr => 'a expr) => bool"
"ordinary == % e. (? a. e = (% x. CON a)) \
\ | ( e = (% x. x)) \
\ | (? n. e = (% x. VAR n)) \
\ | (? j. e = (% x. BND j)) \
\ | (? f g. e = (% x. f x $$ g x)) \
\ | (? f. e = (% x. ABS (f x)))"
rank :: "('a expr => 'a expr) => nat"
"rank == % e. size (e (VAR 0))"
lconv :: "['a expr list, 'a expr] => 'a expr"
"lconv == insts 0"
dflt :: 'a expr
"dflt == LAM x. x"
(* defined as primitive on the underlying representation
subst :: "['a expr, var, 'a expr] => 'a expr"
"subst == % s n. @ e. abstr e & newFor n (e dflt) & e (VAR n) = s"
*)
inductive abstSet
intrs
abst_CON "abst i (% x. CON a)"
abst_id "abst i (% x. x)"
abst_VAR "abst i (% x. VAR n)"
abst_BND "j < i ==> abst i (% x. BND j)"
abst_APP "[| abst i f; abst i g |] ==> abst i (% x. f x $$ g x)"
abst_ABS "abst (Suc i) f ==> abst i (% x. ABS (f x))"
inductive lbndSet
intrs
lbnd_CON "lbnd i (% x. CON a) (CON a)"
lbnd_id "lbnd i (% x. x) (BND i)"
lbnd_VAR "lbnd i (% x. VAR n) (VAR n)"
lbnd_BND "lbnd i (% x. BND j) (BND j)"
lbnd_APP "[| lbnd i f s; lbnd i g t |] \
\ ==> lbnd i (% x. f x $$ g x) (s $$ t)"
lbnd_ABS "lbnd (Suc i) f s ==> lbnd i (% x. ABS (f x)) (ABS s)"
lbnd_Err "~ordinary e ==> lbnd i e (BND 0)"
end
theorem abst_le_abst:
[| abst i s; i <= j |] ==> abst j s
theorem abst_0_abst:
abst 0 e ==> abst i e
theorem abstr_CON:
abstr (%x. CON n)
theorem abstr_id:
abstr (%x. x)
theorem abstr_VAR:
abstr (%x. VAR n)
theorem abstr_APP:
[| abstr e; abstr f |] ==> abstr (%x. e x $$ f x)
theorem level_abst_const:
level i s ==> abst i (%x. s)
theorem proper_abstr_const:
proper s ==> abstr (%x. s)
theorem ext_simp:
(e = f) = (ALL k. e k = f k)
theorem id_neq_const:
(%x. x) ~= (%x. s)
theorem id_neq_APP:
(%x. x) ~= (%x. f x $$ g x)
theorem id_neq_ABS:
(%x. x) ~= (%x. ABS (e x))
theorem id_neq_VAR:
(%x. x) = (%x. VAR n) ==> False
theorem lbnd_unique:
[| lbnd i e s; lbnd i e t |] ==> s = t
theorem lbnd_lbind:
lbnd i e s ==> lbind i e = s
theorem rank_APP1:
rank f < rank (%x. f x $$ g x)
theorem rank_APP2:
rank g < rank (%x. f x $$ g x)
theorem rank_ABS:
rank e < rank (%x. ABS (e x))
theorem abstraction_induct:
[| !!j. P (%x. VAR j); !!a. P (%x. CON a); P (%x. x); !!j. P (%x. BND j);
!!f g. [| P f; P g |] ==> P (%x. f x $$ g x); !!f. P f ==> P (%x. ABS (f x));
!!f. ¬ ordinary f ==> P f |]
==> P e
theorem lbnd_existence:
lbnd i e (lbind i e)
theorem lbind_CON:
lbind i (%x. CON a) = CON a
theorem lbind_id:
lbind i (%x. x) = BND i
theorem lbind_VAR:
lbind i (%x. VAR n) = VAR n
theorem lbind_BND:
lbind i (%x. BND j) = BND j
theorem lbind_APP:
lbind i (%x. f x $$ g x) = lbind i f $$ lbind i g
theorem lbind_ABS:
lbind i (%x. ABS (e x)) = ABS (lbind (Suc i) e)
theorem lbind_not_ordinary:
¬ ordinary e ==> lbind i e = BND 0
theorem lbind_const:
lbind i (%x. s) = s
theorem abst_lbind_simp:
[| abst i e; abst i f |] ==> (lbind i e = lbind i f) = (e = f)
theorem abstr_LAM_simp:
[| abstr e; abstr f |] ==> (LAM x. e x = LAM y. f y) = (e = f)
theorem abst_level_lbind:
abst i e ==> level (Suc i) (lbind i e)
theorem proper_level:
proper s ==> level i s
theorem abstr_level:
abstr e ==> level i (ABS (lbind i e))
theorem abstr_abst:
abstr e ==> abst i e
theorem level_abst_const:
[| level i s; i <= j |] ==> abst j (%x. s)
theorem proper_abst:
proper s ==> abst i (%x. s)
theorem lbind_inst:
s = lbind i (%x. inst i x s)
theorem ABS_LAM:
ABS s = LAM x. inst 0 x s
theorem abst_inst_lbind:
abst i e ==> e = (%x. inst i x (lbind i e))
theorem insts_lbind:
insts (Suc i) xs s = lbind i (%x. insts i (x # xs) s)
theorem lconv_ABS:
lconv xs (ABS s) = LAM x. lconv (x # xs) s
theorem insts_empty:
insts i [] s = s
theorem lconv_id:
lconv [] s = s
theorem abst_level:
abst i e ==> level i (e (VAR n))
theorem proper_dflt:
proper dflt
theorem newFor_dflt:
newFor n dflt
theorem gV_dflt:
gV dflt = 0
theorem abstr_extensionality:
[| abstr e; abstr f; newFor n (e dflt); newFor n (f dflt);
e (VAR n) = f (VAR n) |]
==> e = f
theorem abstr_all_extensionality:
[| abstr e; abstr f; ALL n. e (VAR n) = f (VAR n) |] ==> e = f
theorem abst_level_0_level:
[| abst i e; level 0 t |] ==> level i (e t)
theorem abstr_proper_proper:
[| abstr e; proper t |] ==> proper (e t)
theorem level_abst_subst:
level i s ==> abst i (subst s n)
theorem proper_abstr_subst:
proper s ==> abstr (subst s n)
theorem abstr_subst:
[| e (VAR n) = s; abstr e; newFor n (e dflt) |] ==> subst s n = e
theorem abst_newFor_lbind:
abst i e ==> newFor n (lbind i e) = newFor n (e dflt)
theorem newFor_LAM:
abstr e ==> newFor n (LAM x. e x) = newFor n (e dflt)
theorem abstr_newFor_apply:
[| abstr e; proper t; newFor n t; newFor n (e dflt) |] ==> newFor n (e t)
theorem abst_gV_lbind:
abst i e ==> gV (lbind i e) = gV (e dflt)
theorem gV_LAM:
abstr e ==> gV (LAM x. e x) = gV (e dflt)
theorem level_abst_inst:
level (Suc j) s ==> abst j (%x. inst j x s)
theorem proper_abstr_inst:
proper (ABS s) ==> abstr (%x. inst 0 x s)
theorem abstr_inst_proper:
abstr (%x. inst 0 x s) ==> proper (ABS s)
theorem level_inst:
[| level (Suc j) s; level 0 t |] ==> level j (inst j t s)
theorem level_inst_VAR:
level (Suc j) s ==> level j (inst j (VAR n) s)
theorem size_inst_VAR:
size (inst i (VAR n) s) = size s
theorem proper_VAR_induct:
[| proper u; !!a. P (CON a); !!n. P (VAR n);
!!s t. [| proper s; P s; proper t; P t |] ==> P (s $$ t);
!!e. [| abstr e; ALL n. P (e (VAR n)) |] ==> P (LAM x. e x) |]
==> P u
theorem abstr_proper_LAM:
abstr e ==> proper (LAM x. e x)
theorem properE:
[| proper s; !!a. s = CON a ==> P; !!n. s = VAR n ==> P;
!!t u. [| s = t $$ u; proper t; proper u |] ==> P;
!!e. [| s = LAM x. e x; abstr e |] ==> P |]
==> P