File Expr.ML

(*
      File: Expr.thy
    Author: Simon Ambler (sja4@mcs.le.ac.uk)
 Copyright: Leicester University, 2001.
Time-stamp: <2002-04-08 15:46:38 sja4>

  A de Bruijn representation of expressions
      in the untyped lambda-calculus.

*)


val levelEs = map levelSet.mk_cases [
	"level i (BND j)",
	"level i (s $$ t)",
	"level i (ABS s)"];


Goal "level i s ==> ! j. i <= j --> level j s";
be levelSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs levelSet.intrs
	addss simpset())));
qed_spec_mp "level_le_level";


Goal "level 0 s ==> level i s";
br level_le_level 1;
ba 1;
br le0 1;
qed "level_0_level";


Goal "gV s <= j --> newFor j s";
by (induct_tac "s" 1);
by Auto_tac;
qed_spec_mp "gV_newFor";


bind_thm("newFor_gV", order_refl RS gV_newFor);


Goal "level i s ==> ! j. i <= j --> inst j u s = s";
be levelSet.induct 1;
by Auto_tac;
qed_spec_mp "level_inst_id";


Goalw [proper_def]
  "proper s ==> inst j u s = s";
br level_inst_id 1;
by Auto_tac;
qed "proper_inst";


Goalw [proper_def] "proper (CON a)";
brs levelSet.intrs 1;
qed "proper_CON";


Goalw [proper_def] "proper (VAR n)";
brs levelSet.intrs 1;
qed "proper_VAR";


Goalw [proper_def] "[| proper s; proper t |] ==> proper (s $$ t)";
brs levelSet.intrs 1;
ba 1;
ba 1;
qed "proper_APP";


val prems = Goalw [proper_def]
  "[| proper (s $$ t); [| proper s; proper t |] ==> P |] ==> P";
by (cut_facts_tac prems 1);
bes levelEs 1;
brs prems 1;
ba 1;
ba 1;
qed "proper_APP_E";


Goalw [proper_def] "proper (s $$ t) ==> proper s";
bes levelEs 1;
ba 1;
qed "proper_APPD1";


Goalw [proper_def] "proper (s $$ t) ==> proper t";
bes levelEs 1;
ba 1;
qed "proper_APPD2";


Goalw [proper_def] "proper (BND j) ==> P";
bes levelEs 1;
be less_zeroE 1;
qed "proper_BND_E";


Goal "~ proper (BND j)";
br notI 1;
be proper_BND_E 1;
qed "not_proper_BND";


Goal "[| level 0 s; level 0 t |] \
	\ ==> ! i j. i~=j --> inst i s (inst j t u) = inst j t (inst i s u)";
by (induct_tac "u" 1);
by (ALLGOALS (asm_simp_tac (simpset()
	addsimps [le0 RSN (2,level_inst_id)])));
qed_spec_mp "inst_swap";


Goal "newFor n (subst s m t) \
	\ = ((newFor n s | n=m) & (newFor n t | newFor m s))";
by (induct_tac "s" 1);
by Auto_tac;
qed "newFor_subst";


Goal "subst s n (VAR n) = s";
by (induct_tac "s" 1);
by Auto_tac;
qed "subst_VAR_id";


Goal "newFor n s --> subst s n u = s";
by (induct_tac "s" 1);
by Auto_tac;
qed_spec_mp "newFor_subst_id";