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)
 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