# Theory Abstr

Up to index of Isabelle/HOL/sHowe

theory Abstr = Expr
files [Abstr.ML]:
```(*
File: Abstr.thy
Author: Simon Ambler (sja4@mcs.le.ac.uk)
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```