File Closed.ML

Addsimps [closed_def];

 val clopen_defs = [cloAbstr_def,open_def];
 val clo_defs = [cloexp_def,cloAbstr_def];

fun closed_tac defs prems =
 (asm_full_simp_tac (simpset() addsimps clo_defs) )
 THEN'
	(best_tac (HOL_cs addIs isexpSet.intrs @ prems
	addss	(simpset() addsimps ([newFor_LAM]@defs))));



fun clolam_tac defs  = EVERY'[
        (simp_tac (simpset()
		addsimps [open_def,cloexp_def])),
	(rtac conjI), 
 	(fast_tac(HOL_cs addIs isexpSet.intrs addss (simpset() addSolver abstr_solver defs) )),
		(simp_tac (simpset()
		addsimps defs @ [abstr_def, lambda_def,newFor_LAM] @ lbind_simps))];


Goalw[cloexp_def] "cloexp t ==> isexp t";
auto();
qed "cloexp_isexp";

Goal "[|cloexp s;cloexp t|] ==> cloexp (s $ t)";
 by(closed_tac unlam_defs [] 1);
qed "cloexp_App";


Goal "[| cloAbstr E; cloexp p |] ==> cloexp (E p)" ;
bws clo_defs;
auto();
be isexp_Abs_E 1;
br isexp_sub 1;
back();
bd abstr_LAM_simp 3;
auto();
by(fast_tac(HOL_cs addIs [isexp_proper,abstr_newFor_apply] addss (simpset() addsimps [newFor_LAM]@unlam_defs))1);
qed "clo_sub";

Goal "cloexp (lam x. x)";
by(clolam_tac unlam_defs 1);
qed "cloexp_udflt";

Goal "l |- e ==> l |-- e";
by(asm_full_simp_tac(simpset() addsimps [wff_iwff]) 1);
qed "wff_to_iwff";

Goal "l |-- e ==> l |- e";
by(asm_full_simp_tac(simpset() addsimps [wff_iwff]) 1);
qed "iwff_to_wff";

Goalw [wff_def,cloexp_def] "( [] |- s ) = cloexp s";
auto();
qed "wff_Nil_cloexp";


Goalw [wff_def,cloexp_def] "( [] |- s ) ==> cloexp s";
auto();
qed "wff_Nil_cloexp1";



Goalw [wff_def,cloexp_def]"  cloexp s ==> ( [] |- s )";auto();
qed "wff_Nil_cloexp2";

Goal "  cloexp s ==> ( [] |-- s )";
bd wff_Nil_cloexp2 1;
by(asm_full_simp_tac(simpset() addsimps [wff_iwff]) 1);
qed "iwff_Nil_cloexp2";




Goal "( [] |-- s ) ==> cloexp s";
br wff_Nil_cloexp1 1;
by(asm_full_simp_tac(simpset() addsimps [wff_iwff]) 1);
qed "iwff_Nil_cloexp1";

Goal "env |- s ==> isexp s";
bw wff_def;
auto();
qed "wff_isexp";


Goal "list |- s --> (!a. a # list |- s )";
br list.induct 1;
bw wff_def;
auto();
(* qed "wff_weak";*)
qed_spec_mp "wff_weak";


Goal "[| a # list |- s; cloexp p|] ==> list |-   subst s a p";
bws[cloexp_def,wff_def] ;
auto();
br isexp_sub2 1;auto();
by(asm_full_simp_tac(simpset() addsimps [newFor_subst]) 1);
be allE 1;auto();
br (make_elim not_sym ) 1;
auto();
qed "wff_closed_subst";

(*
brs closed.intrs 1;


Goal "closed (lam x y. x $ y)";
brs closed.intrs 1;
by(abstr_tac unlam_defs [] 1);
brs closed.intrs 1;
brs closed.intrs 2;
brs closed.intrs 2;
brs closed.intrs 2;
by(abstr_tac ([udflt_def]@unlam_defs) [] 1);
*)

val udefs = ([udflt_def]@unlam_defs);
(*
fun  closed_mk_cases  head =  let
         val rbt = rule_by_tactic (ALLGOALS (hysimp udefs) THEN (fold_tac udefs))
  in
 (rbt o closed.mk_cases) head end;


bind_thm ("closed_Abs_E", closed_mk_cases "closed (bLam  E   ) ");
bind_thm ("closed_App_E", closed_mk_cases "closed (e $ e1) ");
bind_thm ("closed_VAR_E", closed_mk_cases "closed (VAR (n)) ");
bind_thm ("closed_Df_E", closed_mk_cases "closed (udflt) ");

val closed_E = [closed_Abs_E,closed_App_E,closed_VAR_E,closed_Df_E];

*)

Goal "open ((VAR n))";
bws clopen_defs;auto();
brs isexpSet.intrs 1;




Goal "[| isexp s; isexp t |] \
	\ ==> subst (s $ t) n = (% x. subst s n x $ subst t n x)";
br abstr_subst 1;
by (asm_simp_tac (simpset() addsimps [subst_VAR_id]) 1);
by(hysimp unlam_defs 1);
br abstr_APP 1;
br abstr_APP 1;
by(abstr_tac unlam_defs [] 1);
by(fast_tac(HOL_cs addIs [isexp_proper,proper_abstr_subst]) 1);;
by(fast_tac(HOL_cs addIs [isexp_proper,proper_abstr_subst]) 1);;
by(hysimp unlam_defs 1);
by (asm_simp_tac (simpset() addsimps [newFor_subst]) 1);
qed "subst_App";



Goal "[| isexp s; isexp t |] \
	\ ==>  subst (s $ t) n p = ( subst s n p) $ (subst t n p)";
by(asm_simp_tac(simpset() addsimps [subst_App]) 1);
 qed "subst_App1";

Goal "abstr e ==> subst (lam y. e y) n = (% x. lam y. biSubst e n x y)";
br abstr_subst 1;
by(hysimp unlam_defs 1);
by (asm_simp_tac (simpset()
	addsimps [abstr_LAM_simp, abstr_biSubst_id,
		abstr_biAbstr_biSubst RS biAbstr_abstr_LAM1]) 1);
by(hysimp unlam_defs 1);
br abstr_APP 1;
by(abstr_tac unlam_defs [] 1);

br (abstr_biAbstr_biSubst RS biAbstr_abstr_LAM1) 1;
ba 1;
by(hysimp unlam_defs 1);


by (asm_simp_tac (simpset()
	addsimps [newFor_LAM, abstr_newFor_biSubst,
		abstr_biAbstr_biSubst RS biAbstr_proper_abstr1,
		proper_dflt]) 1);

qed "subst_lam";

Goalw[cloexp_def] "cloexp s ==> subst s n p = s";
auto();
by (asm_full_simp_tac (simpset() addsimps [newFor_subst_id]) 1);
qed "cloexp_subst_id";