File UnLam.ML

val unlam_defs = [App_def, bLam_def];

fun hsimpset def = (simpset() addsimps [abstr_LAM_simp] @ def);
fun hysimp defs = (asm_full_simp_tac (hsimpset defs));
fun hysimp_f defs i = (asm_full_simp_tac (hsimpset defs) i) THEN (fold_tac defs);
fun hysimp_and_sub defs i = (asm_full_simp_tac (hsimpset defs) i) THEN (hyp_subst_tac i);


Goal "[| abstr e; abstr f;(LAM x. e x = LAM y. f y) |] ==>  (e = f)";
by(asm_full_simp_tac (simpset() addsimps [abstr_LAM_simp])  1);
(* qed "abstr_LAM_simp1";*)
qed "abstr_LAM_inject";


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

Goal "[| abstr e; abstr f;(LAM x. e x = lambda f ) |] ==>  (e = f)";
 by(hysimp [] 1);
qed "abstr_LAM_simp2";

 Goal " f $ p = e1 $ e2 ==> f = e1 & p = e2";
 by(hysimp unlam_defs 1);
 qed "App_inject1";

 Goal "  f = e1 & p = e2 ==> f $ p = e1 $ e2 ";
 auto();
 qed "App_cong";

Goal " f $ p = e1 $ e2 = (f = e1 & p = e2)";
 by(hysimp unlam_defs 1);
qed "App_inject";

Goalw unlam_defs   "e1 $ e2 = lam x. Ea x ==> P";
auto();
qed "clash_App_Lam";

 Goal "[|abstr E; abstr Ea |] ==> bLam E = bLam Ea = (E = Ea)";
 by(hysimp unlam_defs 1);
qed "bLam_inject";

 Goal "[|abstr E; abstr Ea ; bLam E = bLam Ea |] ==>  (E = Ea)";
by(hysimp unlam_defs 1);
qed "bLam_inject1";

Goal "isexp e ==> proper e";
be isexpSet.induct 1;
bws unlam_defs;
by(ALLGOALS(fast_tac(claset() addIs properIs) ));
qed "isexp_proper";

Goal "isexp s ==> abstr (%x . s)";
by(fast_tac(HOL_cs addIs [proper_abstr_const,isexp_proper]) 1);
qed "isexp_abstr_const";


fun  isexp_mk_cases  head =  let
         val rbt = rule_by_tactic (ALLGOALS (hysimp unlam_defs) THEN (fold_tac unlam_defs))
  in
 (rbt o isexpSet.mk_cases) head end;


bind_thm ("isexp_Abs_E", isexp_mk_cases "isexp (bLam  E)   ");