File Abstr.ML

(*
      File: Abstr.ML
    Author: Simon Ambler (sja4@mcs.le.ac.uk)
 Copyright: Leicester University, 2001.
Time-stamp: <2002-04-10 15:04:40 am133>

	Abstract syntax for the Lambda Calculus
*)


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


Goal "abst 0 e ==> abst i e";
br abst_le_abst 1;
ba 1;
br le0 1;
qed "abst_0_abst";


Goalw [abstr_def] "abstr (% x. (CON n))";
brs abstSet.intrs 1;
qed "abstr_CON";


Goalw [abstr_def] "abstr (% x. x)";
brs abstSet.intrs 1;
qed "abstr_id";


Goalw [abstr_def] "abstr (% x. (VAR n))";
brs abstSet.intrs 1;
qed "abstr_VAR";


Goalw [abstr_def] "[| abstr e; abstr f |] ==> abstr (% x. e x $$ f x)";
brs abstSet.intrs 1;
ba 1;
ba 1;
qed "abstr_APP";


Goal "level i s ==> abst i (% x. s)";
be levelSet.induct 1;
by (ALLGOALS (fast_tac (claset() addIs abstSet.intrs)));
qed "level_abst_const";


Goalw [proper_def, abstr_def] "proper s ==> abstr (% x. s)";
br level_abst_const 1;
ba 1;
qed "proper_abstr_const";


Goal "((% i. e i) = (% j. f j)) = (! k. e k = f k)";
br iffI 1;
be subst 1;
br allI 1;
br refl 1;
br ext 1;
be allE 1;
ba 1;
qed "ext_simp";


val ext_expr_inject = 
  let
	fun prv form = prove_goal thy form
		(fn prs => [fast_tac (claset()
			addss (simpset() addsimps [ext_simp])) 1]);
  in
	map prv [
		"((% x. CON a) = (% x. CON b)) = (a = b)",
		"((% x. VAR j) = (% x. VAR k)) = (j = k)",
		"((% x. BND j) = (% x. BND k)) = (j = k)",
		"((% x. e x $$ g x) = (% y. f y $$ h y)) = (e = f & g = h)",
		"((% x. ABS (e x)) = (% y. ABS (f y))) = (e = f)"
		]
  end;


Goal "(% x :: 'a expr. x) ~= (% x. s)";
by (simp_tac (simpset() addsimps [ext_simp]) 1);
by (res_inst_tac [("x","if VAR 0 = s then VAR 1 else VAR 0")] exI 1);
by (fast_tac (claset()
	addss (simpset() addsplits [split_if_asm])) 1);
qed "id_neq_const";


Goal "(% x :: 'a expr. x) ~= (% x. f x $$ g x)";
by (asm_full_simp_tac (simpset() addsimps [ext_simp]) 1);
auto();
qed "id_neq_APP";


Goal "(% x :: 'a expr. x) ~= (% x. ABS (e x))";
by (asm_full_simp_tac (simpset() addsimps [ext_simp]) 1);
auto();
qed "id_neq_ABS";

Goal " (%x. x) = (%x. VAR n) ==> False";
by (asm_full_simp_tac (simpset() addsimps [ext_simp]) 1);
auto();
qed "id_neq_VAR";

val ext_expr_distinct =
  let
	fun prv form = prove_goal thy form
		(fn prs => [simp_tac (simpset() addsimps [ext_simp]) 1]);

	val expr_distinct = [id_neq_const, id_neq_APP, id_neq_ABS]
		@
		map prv [
		"(% x. CON a) ~= (% x. VAR n)",
		"(% x. CON a) ~= (% x. BND j)",
		"(% x. CON a) ~= (% x. f x $$ g x)",
		"(% x. CON a) ~= (% x. ABS (e x))",
		"(% x. VAR n) ~= (% x. BND j)",
		"(% x. VAR n) ~= (% x. f x $$ g x)",
		"(% x. VAR n) ~= (% x. ABS (e x))",
		"(% x. BND j) ~= (% x. f x $$ g x)",
		"(% x. BND j) ~= (% x. ABS (e x))",
		"(% x. f x $$ g x) ~= (% x. ABS (e x))"
		]
 
  in
	expr_distinct @ (expr_distinct RL [not_sym])

  end;


val ext_simps = ext_expr_inject @ ext_expr_distinct;


val ordinaryIs =
  let
	fun prv form = prove_goalw thy [ordinary_def] form
		(fn prs => [
			simp_tac (simpset() addsimps ext_simps) 1
		])
  in
	map prv [
	"ordinary (% x. CON a)",
	"ordinary (% x. x)",
	"ordinary (% x. VAR n)",
	"ordinary (% x. BND j)",
	"ordinary (% x. f x $$ g x)",
	"ordinary (% x. ABS (e x))"
	]

  end;


Addsimps (ext_simps);


val lbndSet_Es =
  let
	val rbt = rule_by_tactic (ALLGOALS (full_simp_tac
		(simpset() addsimps ordinaryIs)))
  in
	map (rbt o lbndSet.mk_cases) [
		"lbnd i (% x. CON a) s",
		"lbnd i (% x. x) s",
		"lbnd i (% x. VAR n) s",
		"lbnd i (% x. BND j) s",
		"lbnd i (% x. f x $$ g x) s",
		"lbnd i (% x. ABS (e x)) s"
	 ]
  end;


Delsimps (ext_simps);


Goal "lbnd i e s ==> ! t. lbnd i e t --> s = t";
be lbndSet.induct 1;
by (fast_tac (claset()
	addEs [lbndSet.elim]
	addss (simpset() addsimps ordinaryIs)) 7);
by (ALLGOALS (blast_tac (claset() addEs lbndSet_Es)));
qed_spec_mp "lbnd_unique";


Goalw [lbind_def] "lbnd i e s ==> lbind i e = s";
br some_equality 1;
ba 1;
br lbnd_unique 1;
ba 1;
ba 1;
qed "lbnd_lbind";


Goalw [rank_def] "rank f < rank (% x. f x $$ g x)";
by (Simp_tac 1);
qed "rank_APP1";

Goalw [rank_def] "rank g < rank (% x. f x $$ g x)";
by (Simp_tac 1);
qed "rank_APP2";

Goalw [rank_def] "rank e < rank (% x. ABS (e x))";
by (Simp_tac 1);
qed "rank_ABS";


val expr_ranks = [rank_APP1, rank_APP2, rank_ABS];


val prems = Goal "[| !! 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";
by (res_inst_tac [("P","P"), ("f", "rank")]
	measure_induct 1);
by (case_tac "ordinary x" 1);
brs prems 2;
ba 2;
bw ordinary_def;
by Safe_tac;
by (ALLGOALS (blast_tac (claset()
	addIs prems @ expr_ranks
	addss simpset())));
qed "abstraction_induct";


Goalw [lbind_def] "! i. lbnd i e (lbind i e)";
by (res_inst_tac [("P","% e. ! i. lbnd i e (@ s. lbnd i e s)")]
	abstraction_induct 1);
by (ALLGOALS (rtac allI THEN'
	rtac someI THEN' resolve_tac lbndSet.intrs));
by Auto_tac;
qed_spec_mp "lbnd_existence";


Goal "lbind i (% x. CON a) = CON a";
br lbnd_lbind 1;
brs lbndSet.intrs 1;
qed "lbind_CON";


Goal "lbind i (% x. x) = BND i";
br lbnd_lbind 1;
brs lbndSet.intrs 1;
qed "lbind_id";


Goal "lbind i (% x. VAR n) = VAR n";
br lbnd_lbind 1;
brs lbndSet.intrs 1;
qed "lbind_VAR";


Goal "lbind i (% x. BND j) = BND j";
br lbnd_lbind 1;
brs lbndSet.intrs 1;
qed "lbind_BND";


Goal "lbind i (% x. f x $$ g x) = lbind i f $$ lbind i g";
br lbnd_lbind 1;
brs lbndSet.intrs 1;
br lbnd_existence 1;
br lbnd_existence 1;
qed "lbind_APP";


Goal "lbind i (% x. ABS (e x)) = ABS (lbind (Suc i) e)";
br lbnd_lbind 1;
brs lbndSet.intrs 1;
br lbnd_existence 1;
qed "lbind_ABS";


Goal "~ordinary e ==> lbind i e = BND 0";
br lbnd_lbind 1;
brs lbndSet.intrs 1;
ba 1;
qed "lbind_not_ordinary";


Goal "! i. lbind i (% x. s) = s";
by (induct_tac "s" 1);
by (ALLGOALS (asm_simp_tac (simpset()
	addsimps [lbind_CON, lbind_id, lbind_VAR, lbind_BND,
		lbind_APP, lbind_ABS])));
qed_spec_mp "lbind_const";


val lbind_simps = [lbind_id, lbind_const, lbind_APP, lbind_ABS];


Goal "abst i e ==> ! f. abst i f --> (lbind i e = lbind i f) = (e = f)";
be abstSet.induct 1;
by (ALLGOALS strip_tac);
by (ALLGOALS (
	eres_inst_tac [("aa","(i,fa)")] abstSet.elim
	ORELSE'
	eres_inst_tac [("aa","(i,f)")] abstSet.elim));
by (ALLGOALS (fast_tac (claset()
	addss (simpset() addsimps lbind_simps))));
qed_spec_mp "abst_lbind_simp";


Goalw [abstr_def, lambda_def]
	"[| abstr e; abstr f |] ==> (LAM x. e x = LAM y. f y) = (e = f)";
by (Simp_tac 1);
br abst_lbind_simp 1;
ba 1;
ba 1;
qed "abstr_LAM_simp";


Goal "abst i e ==> level (Suc i) (lbind i e)";
be abstSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs levelSet.intrs
	addss (simpset() addsimps lbind_simps))));
qed "abst_level_lbind";


Goalw [proper_def] "proper s ==> level i s";
br level_0_level 1;
ba 1;
qed "proper_level";


Goalw [abstr_def] "abstr e ==> level i (ABS (lbind i e))";
brs levelSet.intrs 1;
br (abst_0_abst RS abst_level_lbind) 1;
ba 1;
qed "abstr_level";


(* Proper solver --- for goals of the form "proper s" *)


local

  (* Will only resolve against goals of the right form *)
  val proper_filter_thm =
	prove_goal thy "proper s ==> proper s"
		(fn prems => [resolve_tac prems 1]);
in

  fun proper_tac defs prems =
	rtac proper_filter_thm
	THEN'
	simp_tac (simpset()
		addsimps defs @ [proper_def, lambda_def] @ lbind_simps)
	THEN'
	fast_tac (claset()
		addIs levelSet.intrs @ prems
		addEs [proper_level, abstr_level])
end;


fun proper_solver defs = mk_solver "proper"
		(fn prems => proper_tac defs prems);



Goalw [abstr_def] "abstr e ==> abst i e";
br abst_0_abst 1;
ba 1;
qed "abstr_abst";


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


Goalw [proper_def] "proper s ==> abst i (% x. s)";
br level_abst_const 1;
br level_0_level 1;
ba 1;
br le_refl 1;
qed "proper_abst";


(* Abstraction solver --- for goals of the form "abstr (% x. e x)" *)


local

  (* Will only resolve against goals of the right form *)
  val abstr_filter_thm =
	prove_goal thy "abstr (% x. e x) ==> abstr (% x. e x)"
		(fn prems => [resolve_tac prems 1]);
in

  fun abstr_tac defs prems =
	rtac abstr_filter_thm
	THEN'
	simp_tac (simpset()
		addsimps defs @ [abstr_def, lambda_def] @ lbind_simps)
	THEN'
	fast_tac (claset()
		addIs abstSet.intrs @ prems
		addEs [abstr_abst, proper_abst])
end;


fun abstr_solver defs = mk_solver "abstr"
		(fn prems => abstr_tac defs prems);


val LAM_distinct =
  let
	fun prv form = prove_goal thy form
		(fn prs => [simp_tac (simpset() addsimps [lambda_def]) 1]);

	val distinct = map prv [
		"LAM x. e x ~= VAR n",
		"LAM x. e x ~= BND j",
		"LAM x. e x ~= s $$ t"
		]
  in
	distinct @ (distinct RL [not_sym])

  end;


Addsimps LAM_distinct;


val ext_LAM_distinct =
  let
	fun prv form = prove_goal thy form
		(fn prs => [simp_tac (simpset()
				addsimps ext_simps @ [lambda_def]) 1]);

	val distinct = map prv [
		"(% x. LAM y. f y x) ~= (% x. VAR n)",
		"(% x. LAM y. f y x) ~= (% x. x)",
		"(% x. LAM y. f y x) ~= (% x. BND j)",
		"(% x. LAM y. f y x) ~= (% x. g x $$ h x)"
		]
  in
	distinct @ (distinct RL [not_sym])

  end;



(* The following two results for `inst' are made obsolete by
   the results for `insts' following. Need multiple instantiation. *)

Goal "! i. s = lbind i (% x. inst i x s)";
by (induct_tac "s" 1);
br allI 3;
by (case_tac "nat=i" 3);
by (ALLGOALS (asm_simp_tac (simpset() addsimps lbind_simps)));
qed_spec_mp "lbind_inst";


Goalw [lambda_def] "ABS s = LAM x. inst 0 x s";
by (simp_tac (simpset() addsimps [lbind_inst]) 1);
qed "ABS_LAM";


Goal "abst i e ==> e = (% x. inst i x (lbind i e))";
br ext 1;
be abstSet.induct 1;
by (ALLGOALS (asm_simp_tac (simpset() addsimps lbind_simps)));
qed "abst_inst_lbind";


Goal "! i. insts (Suc i) xs s = lbind i (% x. insts i (x#xs) s)";
by (induct_tac "s" 1);
by (asm_simp_tac (simpset() addsimps lbind_simps) 1);
by (asm_simp_tac (simpset() addsimps lbind_simps) 1);
br allI 1;
by (case_tac "Suc i <= nat" 1);
by (case_tac "nat" 1);
by (Asm_full_simp_tac 1);
by (asm_simp_tac (simpset() addsimps [Suc_diff_le] @ lbind_simps) 1);
by (case_tac "nat - i < Suc (length xs)" 1);
bd not_leE 1;
by (eres_inst_tac [("m","nat")] less_SucE 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps lbind_simps)));
qed_spec_mp "insts_lbind";


Goalw [lambda_def, lconv_def] "lconv xs (ABS s) = LAM x. lconv (x # xs) s";
by (simp_tac (simpset() addsimps [insts_lbind]) 1);
qed "lconv_ABS";


val lconv_simps = 
  let
	fun prv form = prove_goalw thy [lconv_def] form
		(fn prs => [simp_tac (simpset() addsimps []) 1]);
  in
	map prv [
		"lconv xs (CON a) = CON a",
		"lconv xs (VAR n) = VAR n",
  		"lconv xs (BND j) = (if j < length xs then xs ! j else BND j)",
		"lconv xs (s $$ t) = lconv xs s $$ lconv xs t"
		]
	@ [lconv_ABS]
  end;


Goal "! i. insts i [] s = s";
by (induct_tac "s" 1);
by Auto_tac;
qed_spec_mp "insts_empty";


Goalw [lconv_def] "lconv [] s = s";
by (simp_tac (simpset() addsimps [insts_empty]) 1);
qed "lconv_id";


(*

To convert HOAS into de Bruijn form:

by (simp_tac (simpset() addsimps [lambda_def] @ lbind_simps) 1);

To convert de Bruijn back into HOAS:

by (res_inst_tac [("P","?P"), ("t","?t")] (lconv_id RS subst) 1);
by (simp_tac (simpset() addsimps lconv_simps) 1);

It helps to choose a suitable instantiation for "P" or "t"
so as to indicate which term is being rewritten.

*)


Goal "abst i e ==> level i (e (VAR n))";
be abstSet.induct 1;
by (ALLGOALS (fast_tac (claset() addIs levelSet.intrs)));
qed "abst_level";


Goalw [dflt_def] "proper dflt";
by (proper_tac [] [] 1);
qed "proper_dflt";


Goalw [dflt_def, lambda_def] "newFor n dflt";
by (simp_tac (simpset() addsimps lbind_simps) 1);
qed "newFor_dflt";


Goalw [dflt_def, lambda_def] "gV dflt = 0";
by (simp_tac (simpset() addsimps lbind_simps) 1);
qed "gV_dflt";

Addsimps [newFor_dflt, gV_dflt];


Goalw [abstr_def]
  "abstr e ==> ! f n. abstr f --> newFor n (e dflt) --> newFor n (f dflt) \
	\ --> e (VAR n) = f (VAR n) --> e = f";
be abstSet.induct 1;
by (ALLGOALS strip_tac);
by (ALLGOALS (
	eres_inst_tac [("aa","(i,fa)")] abstSet.elim
	ORELSE'
	eres_inst_tac [("aa","(i,f)")] abstSet.elim));
by (ALLGOALS (fast_tac (claset()
	addss (simpset() addsimps ext_simps))));
qed_spec_mp "abstr_extensionality";


Goal "[| abstr e; abstr f; ! n. e (VAR n) = f (VAR n) |] ==> e = f";
br abstr_extensionality 1;
ba 1;
ba 1;
by (res_inst_tac [("j","gV (e dflt) + gV (f dflt)")] gV_newFor 1);
by (res_inst_tac [("j","gV (e dflt) + gV (f dflt)")] gV_newFor 2);
by Auto_tac;
qed "abstr_all_extensionality";


Goal "abst i e ==> level 0 t --> level i (e t)";
be abstSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs levelSet.intrs
	addEs [level_0_level])));
qed_spec_mp "abst_level_0_level";


Goalw [proper_def, abstr_def]
  "[| abstr e; proper t |] ==> proper (e t)";
by (rtac abst_level_0_level 1 THEN atac 1 THEN atac 1);
qed "abstr_proper_proper";


Goal "level i s ==> abst i (subst s n)";
be levelSet.induct 1;
by (case_tac "n=na" 2);
by (ALLGOALS (fast_tac (claset()
	addIs abstSet.intrs
	addss simpset())));
qed "level_abst_subst";


Goalw [proper_def, abstr_def] "proper s ==> abstr (subst s n)";
br level_abst_subst 1;
ba 1;
qed "proper_abstr_subst";


Goal "[| e (VAR n) = s; abstr e; newFor n (e dflt) |] ==> subst s n = e";
br abstr_extensionality 1;
by (ALLGOALS (fast_tac (claset()
	addIs [proper_abstr_subst, proper_VAR,
		abstr_proper_proper, subst_VAR_id]
	addss (simpset() addsimps [newFor_subst]))));
qed_spec_mp "abstr_subst";


(* Old version, when subst was defined via epsilon

Goalw [subst_def]
  "[| e (VAR n) = s; abstr e; newFor n (e dflt) |] ==> subst s n = e";
br some_equality 1;
by (Fast_tac 1);
by (REPEAT (etac conjE 1));
br abstr_extensionality 1;
by Auto_tac;
qed_spec_mp "abstr_subst";

*)


(* abstr_subst allows us to calculate the effect of substituting for a
   free variable (VAR n) directly via higher order unification, e.g.

Goal "subst (LAM x y z. x $$ VAR 0 $$ z) 0 = ?e";
br abstr_subst 1;
br refl 1;
by (abstr_tac [] [] 1);
by (asm_simp_tac (simpset() addsimps [newFor_LAM]
	addSolver (abstr_solver [dflt_def])) 1);

*)

(*

Goalw [proper_def, abstr_def]
  "proper s ==> ? e. abstr e & newFor n (e dflt) & e (VAR n) = s";
be levelSet.induct 1;
by (res_inst_tac [("x","% x. CON a")] exI 1);

by (case_tac "n=na" 2);
by (res_inst_tac [("x","% x. x")] exI 2);
by (res_inst_tac [("x","% x. VAR na")] exI 3);
by (res_inst_tac [("x","% x. BND j")] exI 4);
by (REPEAT (eresolve_tac [exE, conjE] 5));
by (res_inst_tac [("x","% x. e x $$ ea x")] exI 5);
by (REPEAT (eresolve_tac [exE, conjE] 6));
by (res_inst_tac [("x","% x. ABS (e x)")] exI 6);

by (ALLGOALS (fast_tac (claset()
	addIs abstSet.intrs
	addss simpset())));
qed "proper_subst_lemma";


Goalw [subst_def] "proper s ==> abstr (subst s n)";
br (proper_subst_lemma RS someI_ex RS conjunct1) 1;
ba 1;
qed "proper_abstr_subst";


Goalw [subst_def] "proper s ==> subst s n (VAR n) = s";
br (proper_subst_lemma RS someI_ex RS conjunct2 RS conjunct2) 1;
ba 1;
qed "proper_subst_id";


Goalw [subst_def] "proper s ==> newFor n (subst s n dflt)";
br (proper_subst_lemma RS someI_ex RS conjunct2 RS conjunct1) 1;
ba 1;
qed "proper_newFor_subst";

*)


Goal "abst i e ==> newFor n (lbind i e) = newFor n (e dflt)";
be abstSet.induct 1;
by (ALLGOALS (asm_simp_tac (simpset() addsimps lbind_simps)));
qed "abst_newFor_lbind";


Goalw [lambda_def, abstr_def]
  "abstr e ==> newFor n (LAM x. e x) = newFor n (e dflt)";
by (asm_simp_tac (simpset() addsimps [abst_newFor_lbind]) 1);
qed "newFor_LAM";


Goalw [abstr_def] "abstr e ==> ! t. proper t \
	\ --> newFor n t --> newFor n (e dflt) --> newFor n (e t)";
be abstSet.induct 1;
by (ALLGOALS (fast_tac (claset() addss simpset())));
qed_spec_mp "abstr_newFor_apply";


Goal "abst i e ==> gV (lbind i e) = gV (e dflt)";
be abstSet.induct 1;
by (ALLGOALS (asm_simp_tac (simpset() addsimps lbind_simps)));
qed "abst_gV_lbind";


Goalw [lambda_def, abstr_def]
  "abstr e ==> gV (LAM x. e x) = gV (e dflt)";
by (asm_simp_tac (simpset() addsimps [abst_gV_lbind]) 1);
qed "gV_LAM";


Goal "level i s ==> ! j. i = Suc j --> abst j (% x. inst j x s)";
be levelSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs abstSet.intrs
	addEs [less_SucE] addss simpset())));
val lemma = result();


Goal "level (Suc j) s ==> abst j (% x. inst j x s)";
bd lemma 1;
by Auto_tac;
qed "level_abst_inst";


Goalw [proper_def, abstr_def]
  "proper (ABS s) ==> abstr (% x. inst 0 x s)";
br level_abst_inst 1;
bes levelEs 1;
ba 1;
qed "proper_abstr_inst";


Goalw [proper_def, abstr_def]
  "abstr (% x. inst 0 x s) ==> proper (ABS s)";
bd abst_level_lbind 1;
by (full_simp_tac (simpset() addsimps [lbind_inst RS sym]) 1);
brs levelSet.intrs 1;
ba 1;
qed "abstr_inst_proper";


Goal "level i s ==> ! j. i = Suc j --> level 0 t --> level j (inst j t s)";
be levelSet.induct 1;
by (strip_tac 3);
bd level_0_level 3;
by (ALLGOALS (fast_tac (claset()
	addIs levelSet.intrs
	addEs [less_SucE]
	addss simpset())));
val lemma = result();


Goal "[| level (Suc j) s; level 0 t |] ==> level j (inst j t s)";
bd lemma 1;
by Auto_tac;
qed "level_inst";


Goal "level (Suc j) s ==> level j (inst j (VAR n) s)";
br level_inst 1;
ba 1;
brs levelSet.intrs 1;
qed "level_inst_VAR";


Goal "! i. size (inst i (VAR n) s) = size s";
by (induct_tac "s" 1);
by Auto_tac;
qed_spec_mp "size_inst_VAR";


val prems = Goalw [proper_def]
      "[| 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; ! n. P (e (VAR n)) |] ==> P (LAM x. e x) |] \
		\ ==> P u";
by (res_inst_tac [("P","level 0 u"), ("Q", "P u")] mp  1);
brs prems 2;
by (res_inst_tac [("P","% s. level 0 s --> P s"), ("f", "size")]
	measure_induct 1);
by (case_tac "x" 1);
by (ALLGOALS hyp_subst_tac);
by (strip_tac 5);
br (ABS_LAM RS ssubst) 5;
brs prems 5;
br allI 6;
by (eres_inst_tac [("x", "inst 0 (VAR n) expr")] allE 6);
by (ALLGOALS (fast_tac (claset()
	addIs prems @ [level_abst_inst, level_inst_VAR]
	addEs levelEs
	addss (simpset() addsimps [abstr_def, size_inst_VAR]))));
qed "proper_VAR_induct";


Goalw [proper_def, abstr_def, lambda_def]
  "abstr e ==> proper (LAM x. e x)";
brs levelSet.intrs 1;
br abst_level_lbind 1;
ba 1;
qed "abstr_proper_LAM";


val properIs = [proper_CON, proper_VAR, proper_APP, abstr_proper_LAM];


val prems = Goal "[| 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";
by (cut_facts_tac prems 1);
by (subgoal_tac "s = s --> P" 1);
be impE 1;
br refl 1;
ba 1;
by (eres_inst_tac [("P","% x. (s=x --> P)")] proper_VAR_induct 1);
by (ALLGOALS (strip_tac THEN' eresolve_tac prems));
by (ALLGOALS atac);
qed "properE";