File Dyn.ML

section "Big Step Evaluation ";

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


bind_thm ("eval_Abs_E", eval_mk_cases "(bLam  E   ) >> v");
bind_thm ("eval_App_E", eval_mk_cases "( e $ e1) >> v");


val eval_E = [eval_Abs_E,eval_App_E];
 val clo_defs = [cloexp_def,cloAbstr_def]; 
(* val clo_defs = [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))));

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

Goal " [| cloAbstr e |] ==> closed (bLam e)";
by(closed_tac unlam_defs [] 1);
qed "closed_bLam";

val closed_intrs = [closed_App,closed_bLam];

Goal "e >> v ==> closed e ";
be eval.induct 1;
by(ALLGOALS(closed_tac unlam_defs []));
qed "eval_closed1";

Goal "e >> v ==> closed v ";
be eval.induct 1;
by(closed_tac unlam_defs [] 1);
ba 1;
qed "eval_closed2";
*)

Goal "e >> v ==> cloexp e & cloexp v ";
be eval.induct 1;
bw cloAbstr_def;
by(ALLGOALS(fast_tac (HOL_cs addIs [cloexp_App])));
qed "eval_cloexp";

(* Uniqueness of evaluation *)

Goal "(e >> v) ==> !v1.  (e >> v1) --> (v =  v1)";

be eval.induct 1;
by(fast_tac(HOL_cs  addEs [ eval_Abs_E] addss (hsimpset  unlam_defs)) 1); 

(* scrpt cannot be shortened *)
by(strip_tac 1);
be eval_App_E 1;
be conjE 1;
by(hyp_subst_tac 1);
be allE 1; bd mp  1;ba 1;back();
by(hysimp (unlam_defs@clo_defs) 1);
qed "eval_determ";


section "Convergence";

val prems = goalw thy  [converges_def]	"[| converges p; !! v. p >> v ==> Q |] ==> Q";
by (cut_facts_tac prems 1);
 by(fast_tac (HOL_cs addIs prems) 1);
qed "convergesE";

Goalw [converges_def] "converges (f $  p) ==> converges f";
by(fast_tac(HOL_cs addDs [App_inject]   addEs [ eval_App_E] addss ( hsimpset  unlam_defs)) 1); 
qed "converges_App";



section "Values";

(* Value Soundness *)

Goal "e >> v ==> value v";
be eval.induct 1;
by (ALLGOALS(fast_tac (HOL_cs addIs value.intrs ) ));
qed "value_sound";

(* Values evaluates to themselves  *)

Goal "value v ==>  v >>  v ";
be value.induct 1;
by(ALLGOALS(fast_tac(HOL_cs  addIs eval.intrs )));
qed "val_to_eval";

(* Value hygiene *)

Goal "value v ==> cloexp v";
by(fast_tac(HOL_cs addDs [val_to_eval,eval_cloexp] ) 1);
qed "value_cloexp";


Goal "p >> v ==> v >> v";
be eval.induct 1;
by (ALLGOALS (fast_tac (HOL_cs addIs eval.intrs)));
qed "eval_value";