File Divrg.ML

(*
      File: Diverges.ML
    Author: Simon Ambler & AM
 Copyright: Leicester University, 1998-2001.
Time-stamp: <2002-04-10 14:52:53 am133>

	Divergence predicate.
*)

Goal "divrg p ==> cloexp p";
by(ALLGOALS(fast_tac(claset() addEs divrg.elims addIs [cloexp_App] addDs [eval_cloexp])));
qed "divrg_cloexp";

Addsimps [cloAbstr_def];

(* some divergent terms *)


Goalw [omega_def] "divrg omega";
	br divrg.coinduct 1;
	by(Fast_tac 1);
	br disjI2 1;
auto();
by(REPEAT(Step_tac 1));
auto();
brs eval.intrs 1;
bw cloAbstr_def;
br conjI 1;
by(abstr_tac unlam_defs [] 1);
by(clolam_tac unlam_defs  1);
by(abstr_tac unlam_defs [] 1);
by(clolam_tac unlam_defs  1);
qed "omega_diverges";


(*
Goalw []"divrg ((lam x . x) $ omega)";
br divrg.coinduct 1;
by (res_inst_tac [("B","{omega}")]  insertI1 1); 
bws [omega_def] ;
br disjI2 1;
auto();
by(REPEAT(Step_tac 1));
auto();
brs eval.intrs 1;
bw cloAbstr_def;
by(ALLGOALS(fast_tac(HOL_cs addIs [cloexp_App] addss (simpset() addSolver abstr_solver unlam_defs) )));
qed "id_omega_diverges";
*)


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


bind_thm ("divrg_Abs_E", divrg_hmk_cases "divrg ( bLam E) ");

bind_thm ("divrg_App_E", divrg_hmk_cases "divrg ( e $ e1) ");





(* Not the case that a program converges and diverges *)

Goalw  [converges_def] "converges s ==> ~ divrg s";
be exE 1;
be eval.induct 1;
auto();
be divrg_Abs_E 1;
be divrg_App_E 1;
by(hysimp unlam_defs 1);
bd eval_determ 1;
by(auto_tac(claset(), (hsimpset unlam_defs)));
qed "converges_imp_not_divrg";

(* Contrapposed *)

Goal  "divrg s ==> ~ converges s";
by(blast_tac(claset() addDs [ converges_imp_not_divrg]) 1);
qed "divrg_imp_not_converges";

Delsimps [cloAbstr_def];