File OpenSim.ML

(*
      File: OpenSim.ML
    Author: Simon Ambler (sja4@mcs.le.ac.uk)
 Copyright: Leicester University, 1998.
Time-stamp: <2002-04-16 15:09:29 am133>

	Extension of simulation to open terms.
*)




(* opensim hygiene *)
Goal" env |- s <opensim> t ==>  env |-  s";
be opensim.induct 1;
by(asm_full_simp_tac(simpset() addsimps [cloexp_def,wff_def]) 1);
bw  wff_def;
auto();
by(eres_inst_tac [("x"," (lam x. x)")] allE 1);
bd mp 1;
br cloexp_udflt 1;
by(Clarify_tac 1);
be allE 1;auto();
by (asm_full_simp_tac (simpset() addsimps [newFor_subst]) 1);
auto();
qed "opensim_wff1";


Goal " env |- s <opensim> t ==>  env |-  t";
be opensim.induct 1;
by(asm_full_simp_tac(simpset() addsimps [cloexp_def,wff_def]) 1);
bw  wff_def;
auto();
by(eres_inst_tac [("x"," (lam x. x)")] allE 1);
bd mp 1;
br cloexp_udflt 1;
by(Clarify_tac 1);
be allE 1;auto();
by (asm_full_simp_tac (simpset() addsimps [newFor_subst]) 1);
auto();
qed "opensim_wff2";


Goal " env |- s <opensim> t ==>  env |- s & env |-  t";
by(fast_tac(HOL_cs addIs [opensim_wff1,opensim_wff2]) 1);
qed "opensim_wff";


Goal " env |- s <opensim> t ==>  env |-- s & env |--  t";
bd opensim_wff 1;
by(asm_full_simp_tac (simpset() addsimps [wff_iwff]) 1);
qed "opensim_iwff";


Goal "[] |- s <opensim> t  ==> s <sim> t ";
by(fast_tac(claset() addEs opensim.elims) 1);
qed "opensim_sim";


Goal "s <sim> t  --> env |- s <opensim> t ";				
by (induct_tac "env" 1);
by (fast_tac (claset() addDs [sim_cloexp] addIs opensim.intrs) 1);
by (strip_tac 1);
brs opensim.intrs 1;
 by(fast_tac(HOL_cs  addDs[cloexp_isexp, sim_cloexp]) 1);
 by(fast_tac(HOL_cs  addDs[cloexp_isexp, sim_cloexp]) 1);
by(strip_tac 1);
by(forward_tac [sim_cloexp] 1);
auto();
by (asm_full_simp_tac (simpset() addsimps [cloexp_subst_id]) 1);
qed_spec_mp "sim_opensim";


Goal  "! s.  env |- s --> env |- s <opensim> s ";
br list.induct 1;
auto();
br sim_opensim 1;
br sim_refl 1;
by(asm_full_simp_tac (simpset() addsimps [wff_Nil_cloexp]) 1);
brs opensim.intrs 1;
by (asm_full_simp_tac (simpset() addsimps [wff_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [wff_def]) 1);
by(fast_tac (HOL_cs addDs [wff_closed_subst]) 1);
qed_spec_mp "opensim_refl";


Goal " env |-- s ==> env |- s <opensim> s ";
br opensim_refl 1;
by(asm_full_simp_tac (simpset() addsimps [wff_iwff]) 1);
qed "opensim_refl_i";


(*
by (fast_tac (claset() addIs ([sim_opensim,sim_refl])) 1);
br opensim.intrs 1 ;
force 1;
 by(fast_tac(HOL_cs addIs [ proper_abstr_const] addDs[isexp_proper,osim_isexp]) 1);
 by(fast_tac(HOL_cs addIs [ proper_abstr_const] addDs[isexp_proper,osim_isexp]) 1);
qed_spec_mp "opensim_refl";

*)

val opensim_Cons_E  = opensim.mk_cases "n#env |- r <opensim> s";
val opensim_Nil_E  = opensim.mk_cases "[] |- r <opensim> s";
val opensim_App_Nil_E  = opensim.mk_cases "[] |- (M1' $ M2') <opensim> s";

val opensimEs = [opensim_Nil_E,opensim_Cons_E];


Goal "! s t u. (env |- s <opensim> t ) \
		\  --> (env |- t <opensim> u ) \
		\  --> (env |- s <opensim> u )";
br list.induct 1;
by (ALLGOALS(blast_tac (HOL_cs addIs (opensim.intrs@[sim_trans])
			addEs opensimEs)));
qed_spec_mp "opensim_trans";






(*
val prems = goal thy "env |- s <opensim> t  \
	\ ==> ! j b. j <= length env \
		\ --> splice j env b |- lift s j <opensim> lift t j ";
by (cut_facts_tac prems 1);
be opensim.induct 1;
by (Simp_tac 1);
br allI 1;
by (resolve_tac opensim.intrs 1);
bw opensimrel_def;
by (full_simp_tac (simpset() addsimps [subst_lift]) 1);
by (fast_tac (claset() addIs (opensim.intrs@[weakening_0 RS typing_lift_0])
			addEs [sim_typing1, sim_typing2]) 1);
by (Full_simp_tac 1);
by (safe_tac HOL_cs);

by (case_tac "j=0" 1);
by (hyp_subst_tac 1);
by (Full_simp_tac 1);
by (resolve_tac opensim.intrs 1);
bw opensimrel_def;
by (full_simp_tac (simpset() addsimps [subst_lift]) 1);
by (safe_tac HOL_cs);

br typing_lift_0 1;
ba 1;
br typing_lift_0 1;
ba 1;

by (resolve_tac opensim.intrs 1);
bw opensimrel_def;
by (Fast_tac 1);

(* Level 24 --- case j~=0 *)

be (not0_implies_Suc RS exE) 1;
by (hyp_subst_tac 1);


by (Full_simp_tac 1);
by (resolve_tac opensim.intrs 1);
bw opensimrel_def;
by (Full_simp_tac 1);
by (safe_tac HOL_cs);

by (dres_inst_tac [("j","Suc x"),("s","s")] typing_lift 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addss simpset()) 1);

by (dres_inst_tac [("j","Suc x"),("s","t")] typing_lift 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addss simpset()) 1);

by (fast_tac (claset() addss
	(simpset() addsimps [zero_less_Suc RS lift_subst,
				lift_id_lemma])) 1);

qed_spec_mp "opensim_lift";


val prems = goal thy "env |- s <opensim> t  \
	\ ==>  b # env |- lift s 0 <opensim> lift t 0 ";
by (cut_facts_tac prems 1);
bd (le0 RSN (2,opensim_lift)) 1;
by (Full_simp_tac 1);
qed "opensim_lift_0";


val prems = goal thy "! s t a p b j. j <= length env --> [] |- p ::: b \
		\ --> (splice j env b |- s <opensim> t ) \
		\ --> (env |- s[p/j] <opensim> t[p/j] )";
by (induct_tac "env" 1);
by (fast_tac (claset() addIs opensimIs addEs opensimEs addss simpset()) 1);
by (safe_tac HOL_cs); 
by (resolve_tac opensimIs 1);

br typing_subst 1;
ba 1;
bd opensim_typing1 1;
ba 1;
br weakening_0 1;
ba 1;
br typing_subst 1;
ba 1;
bd opensim_typing2 1;
ba 1;
br weakening_0 1;
ba 1;

by (case_tac "j=0" 1);
by (hyp_subst_tac 1);
by (Full_simp_tac 1);
by (fast_tac (claset() addEs opensimEs) 1);

be (not0_implies_Suc RS exE) 1;
by (hyp_subst_tac 1);
by (Full_simp_tac 1);

by (eresolve_tac opensimEs 1);
by (subgoal_tac "list |- s[pa/0][p/x] <opensim> t[pa/0][p/x] a" 1);
by (Fast_tac 2);


by (asm_full_simp_tac (simpset()
	addsimps [zero_less_Suc RS subst_subst RS sym,
	lift_id_lemma, subst_id_lemma]) 1);

qed_spec_mp "opensim_subst_gnd";



val prems = goal thy "! s t a p b. (b # env |- s <opensim> t ) \
		\ --> env |- p ::: b \
		\ --> (env |- s[p/0] <opensim> t[p/0] )";
by (induct_tac "env" 1);
by (fast_tac (claset() addIs opensimIs addEs opensimEs
		addss simpset()) 1);
by (safe_tac HOL_cs);
by (resolve_tac opensimIs 1);

br typing_subst 1;
br le0 1;
by (Asm_simp_tac 1);
br opensim_typing1 1;
ba 1;
ba 1;

br typing_subst 1;
br le0 1;
by (Asm_simp_tac 1);
br opensim_typing2 1;
ba 1;
ba 1;

by (stac (zero_less_Suc RS subst_subst RS sym) 1);
by (stac (zero_less_Suc RS subst_subst RS sym) 1);

by (asm_simp_tac (simpset() addsimps [lift_id_lemma]) 1);

(* Level 19 *)

by (subgoal_tac "b # list |- s[pa/1] <opensim> t[pa/1] a" 1);

br opensim_subst_gnd 2;
by (Simp_tac 2);
ba 2;
by (Asm_simp_tac 2);

by (subgoal_tac "list |- p [pa / 0] ::: b" 1);
br typing_subst 2;
br le0 2;
by (Asm_simp_tac 2);
br weakening_0 2;
ba 2;
by (Fast_tac 1);
qed_spec_mp "opensim_subst_0";


val prems = goal thy "! s t a p b j. (splice j env b |- s <opensim> t ) \
		\ -->j <= length env --> env |- p ::: b \
		\ --> (env |- s[p/j] <opensim> t[p/j] )";
by (induct_tac "env" 1);
by (fast_tac (claset() addIs opensimIs addEs opensimEs addss simpset()) 1);
by (safe_tac HOL_cs); 
by (resolve_tac opensimIs 1);

br typing_subst 1;
ba 1;
bd opensim_typing1 1;
ba 1;
ba 1;
br typing_subst 1;
ba 1;
bd opensim_typing2 1;
ba 1;
ba 1;

(* Level 14 *)

by (case_tac "j=0" 1);
by (hyp_subst_tac 1);
by (Full_simp_tac 1);

be (make_elim opensim_subst_0) 1;
ba 1;
by (fast_tac (HOL_cs addEs opensimEs) 1);

be (not0_implies_Suc RS exE) 1;
by (hyp_subst_tac 1);
by (Full_simp_tac 1);

(* Level 23 *)

by (asm_simp_tac (simpset() addsimps [gnd_subst_lemma]) 1);
by (eresolve_tac opensimEs 1);
by (blast_tac (claset() addIs [typing_subst_0,weakening_0]) 1);

qed_spec_mp "opensim_subst";


(* odds and ends *)

(*

bind_thm ("opensim_beta_conv1", sim_beta_conv1 RS opensim.opensim_Nil);

bind_thm ("opensim_beta_conv2", sim_beta_conv2 RS opensim.opensim_Nil);

*)

bind_thm ("opensim_eval1", sim_eval1 RS opensim.opensim_Nil);

bind_thm ("opensim_eval2", sim_eval2 RS opensim.opensim_Nil);


val prems = goal thy
	"[| b # env |- t ; env |- q ::: b |] \
		\ ==> env |- Lam t @@ q <opensim> t [q / 0] ";

goal thy "! t q a b. (b # env |- t ) --> (env |- q ::: b) \
		\ --> (env |- Lam t @@ q <opensim> t [q / 0] )";
by (induct_tac "env" 1);
by (fast_tac (claset() addIs opensimIs@[sim_beta_conv1]) 1);
by (strip_tac 1);

brs opensimIs 1;
by (typing_tac 1);
br typing_subst_0 1;
ba 1;
ba 1;

br (zero_less_Suc RS subst_subst RS subst) 1;
by (asm_simp_tac (simpset() addsimps [lift_id_lemma_0]) 1);

by (subgoal_tac "b # list |- t [p / 1] a" 1);
by (subgoal_tac "list |- q [p / 0] ::: b" 1);

by (Fast_tac 1);

br typing_subst_0 1;
ba 1;
br weakening_0 1;
ba 1;

br typing_subst 1;
by (Simp_tac 1);
by (Simp_tac 1);
br weakening_0 1;
ba 1;

qed_spec_mp "opensim_beta_conv1";


goal thy "! t q a b. (b # env |- t ) --> (env |- q ::: b) \
		\ --> (env |- t [q / 0] <opensim> Lam t @@ q )";
by (induct_tac "env" 1);
by (fast_tac (claset() addIs opensimIs@[sim_beta_conv2]) 1);
by (strip_tac 1);

brs opensimIs 1;
br typing_subst_0 1;
ba 1;
ba 1;
by (typing_tac 1);

br (zero_less_Suc RS subst_subst RS subst) 1;
by (asm_simp_tac (simpset() addsimps [lift_id_lemma_0]) 1);

by (subgoal_tac "b # list |- t [p / 1]   a" 1);
by (subgoal_tac "list |- q [p / 0] ::: b" 1);

by (Fast_tac 1);

br typing_subst_0 1;
ba 1;
br weakening_0 1;
ba 1;

br typing_subst 1;
by (Simp_tac 1);
by (Simp_tac 1);
br weakening_0 1;
ba 1;

qed_spec_mp "opensim_beta_conv2";

*)