File Sim.ML

(*
      File: Sim.ML
    Author: Simon Ambler (sja4@mcs.le.ac.uk) modified by AM
 Copyright: Leicester University, 1998.


	Simulation for terms under normal order reduction.
*)

section "Simulation";

Goal  "s <sim> t ==> cloexp s & cloexp t";
be sim.elim 1;
auto();
qed "sim_cloexp";

Goal  " cloexp s ==> s <sim> s";
br sim.coinduct 1;
by (res_inst_tac [("P","% (u,v).  u = v & cloexp u & cloexp v ")] CollectI 1);
auto();
by(fast_tac (HOL_cs addDs [clo_sub]) 1);
qed "sim_refl";




val simEs = [sim.mk_cases "r <sim> s"];
val sim_app_E =  sim.mk_cases "m1 $ m2 <sim> s";


Goal  "[| s <sim> t  ; t <sim> u  |] \
			\ ==> s <sim> u ";
br sim.coinduct 1;
by (res_inst_tac [("P","% (p,r). ? q. p <sim> q  & q <sim> r ")]
	CollectI 1);
by (Fast_tac 1);
by (REPEAT (eresolve_tac [CollectE, splitE, conjE, exE] 1));
by (hyp_subst_tac 1);
by (ALLGOALS (simp_tac (simpset()
	addsimps [])));
by(Safe_tac);
by(fast_tac(HOL_cs addDs[sim_cloexp]) 1);
by(fast_tac(HOL_cs addDs[sim_cloexp]) 1);
bes simEs 1;back();back();
be allE 1; bd mp 1;ba 1;bd mp 1;ba 1;
be exE 1;by(Clarify_tac 1);
bes simEs 1;back();back();
by(Blast_tac 1);
qed "sim_trans";



(* non-coinductive, but using relexivity of <sim>  *)
  Goalw[kleene_def] "p <kleene> q  ==> p <sim> q ";
 by(fast_tac(claset() addIs [sim_refl,clo_sub]@sim.intrs) 1);
qed "kleene_sim";



bind_thm ("sim_beta_conv1", kleene_beta RS kleene_sim);

bind_thm ("sim_beta_conv2", kleene_beta RS kleene_sym RS kleene_sim);



val kleene_eval = eval_kleene;

bind_thm ("sim_eval1", kleene_eval RS kleene_sim);

bind_thm ("sim_eval2", kleene_eval RS kleene_sym RS kleene_sim);


(* note: not-coinductive but by intro rule *)
Goalw[converges_def] "[|cloexp p;cloexp q; ~converges p|] ==> p <sim> q ";
by(ALLGOALS(fast_tac(claset()  addIs sim.intrs)));
qed "not_converges_sim";


(* co-inductive proof *)
(*
Goal " ~converges p  ==> p <sim> q ";
br sim.coinduct 1;
by (res_inst_tac [("P","% (s,t). ~ converges s ")] CollectI 1);
by (Fast_tac 1);
by (REPEAT (eresolve_tac [CollectE,splitE,conjE] 1));
by (hyp_subst_tac 1);
by (ALLGOALS (fast_tac (HOL_cs addss (simpset() addsimps [converges_def]))));
qed "not_converges_sim'";
*)

Goal  "[|cloexp q;divrg p|]  ==> p <sim> q ";
 by(forward_tac [divrg_cloexp] 1);
bd divrg_imp_not_converges 1;
br not_converges_sim 1;
auto();
qed "divrg_sim";

Goalw [converges_def]
	"[| s <sim> t ; converges s |] ==> converges t";
bes simEs 1;
be exE 1;
by(forward_tac [value_sound] 1);
by(fast_tac (HOL_cs addEs[value.elim]) 1);
qed "sim_converges";

section "Bisimulation"; 

Goalw[bisim_def]  "cloexp s ==> s =~= s";
by(fast_tac(claset() addIs [sim_refl]) 1);
qed "bisim_refl";

Goalw[bisim_def]  " s =~= t ==> t =~= s";
auto();
qed "bisim_sym";


Goalw[bisim_def]  "[| s =~= t  ; t =~= u  |]  ==> s =~= u ";
 by(fast_tac(claset() addIs [sim_trans]) 1);
qed "bisim_trans";










(*
Goal "[| f <sim> g ; cloexp p|]  ==> f $ p <sim> g $ p";

bes  simEs 1;

by (case_tac "converges f" 1);
be convergesE 1;
by(blast_tac(claset() addDs [converges_App] addIs [ not_converges_sim,cloexp_App]) 2);
by (blast_tac (claset()
	addIs  [kleene_eval RS kleene_App RS kleene_sim RS sim_trans,
		kleene_eval RS kleene_App RS kleene_sym
					RS kleene_sim RSN (2,sim_trans)]) 1);

qed "sim_App";


*)