File Kleene.ML

(*
      File: Kleene.ML
    Author: Simon Ambler, modiifed by AM
 Copyright: Leicester University, 2001.
Time-stamp: <2002-04-10 14:54:06 am133>

	Kleene equivalence of expressions.
*)

val evalEs = eval_E;

Goalw [kleene_def] "s <kleene> t ==> cloexp s";
by Auto_tac;
qed "kleene_cloexp1";


Goalw [kleene_def] "s <kleene> t ==> cloexp t";
by Auto_tac;
qed "kleene_cloexp2";

Goalw [kleene_def] "s <kleene> t ==> cloexp s & cloexp t ";
by Auto_tac;
qed "kleene_cloexp";

Goalw [kleene_def] "cloexp s ==> s <kleene> s";
by (Simp_tac 1);
qed "kleene_refl";


Goalw [kleene_def] "s <kleene> t ==> t <kleene> s";
by (Fast_tac 1);
qed "kleene_sym";


Goalw [kleene_def] "[| s <kleene> t; t <kleene> u |] ==> s <kleene> u";
by (Fast_tac 1);
qed "kleene_trans";



Goalw [kleene_def] "[| cloAbstr e; cloexp t |] ==> (lam x. e x) $ t <kleene> (e t)"; 
br conjI 1;
br cloexp_App 1;
auto();
bd clo_sub 2;
auto();
bw cloAbstr_def;
auto();
be eval_App_E 1;
auto();
be eval_Abs_E 1;
bw cloAbstr_def;
by(hysimp_and_sub [] 1);
by(fast_tac(HOL_cs addDs [bLam_inject1] ) 1);
by(fast_tac(HOL_cs addIs eval.intrs addss (simpset() addsimps [cloAbstr_def])) 1);
qed "kleene_beta";



Goalw [kleene_def] "[| s >> v; t >> v |] ==> s <kleene> t";
by (blast_tac (claset()
	addDs [eval_determ, eval_cloexp]) 1);
qed "eval_same_kleene";


Goalw [kleene_def] "s >> v  ==> s <kleene> v";
by (blast_tac (claset()
  addDs ([eval_determ, eval_value, eval_cloexp])) 1);
qed "eval_kleene";

Goal
	"[|  ? v. p >> v & q >> v |]  ==> p <kleene> q ";
auto();
br (kleene_sym RSN (2,kleene_trans)) 1;
by(ALLGOALS(fast_tac(claset() addIs [ eval_kleene])));
qed "kleene_eval2";



Goalw [kleene_def] "[| s <kleene> t; cloexp u |] ==> s $ u <kleene> t $ u";
auto();
by (ALLGOALS (fast_tac (claset() addEs evalEs addIs [cloexp_App]@eval.intrs)));
qed "kleene_App";