File OpenHowe.ML

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";


Goal" env |- s <howe> t ==>  env |--  s & env |-- t ";
be howe.induct 1;
by (ALLGOALS (fast_tac (claset() addDs [opensim_iwff] addIs iwff.intrs )));
qed "howe_iwff";


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


Goal" [] |- s <howe> t ==>  cloexp  s & cloexp t ";
bd howe_wff 1;
by(asm_full_simp_tac (simpset() addsimps [wff_Nil_cloexp]) 1);
qed "howe_Nil_cloexp";


Goal  " env |-- s ==> env |- s <howe> s ";
be iwff.induct 1;
by(ALLGOALS(fast_tac (HOL_cs addIs iwff.intrs@howe.intrs@[opensim_refl_i])));
qed "howe_refl";

val cand_refl = howe_refl;


Goal "(env |- s <howe> t)  ==> (  env |- t <opensim> u)  -->   (env |- s <howe> u)";
be howe.induct 1;
by(ALLGOALS(best_tac (HOL_cs addIs howe.intrs addDs [opensim_trans])));
qed_spec_mp "howe_trans";

val cand_right = howe_trans;


Goal  "env |- s <opensim> t ==> env |- s <howe> t";
by(blast_tac(HOL_cs addDs [opensim_iwff] addIs [cand_right,cand_refl]) 1);
qed "opensim_howe";


(* precongruence of howe *)

Goal "[| env |- M <howe> M';env |- N <howe> N' |] ==> env |- (M $ N)<howe> (M' $ N')";
by(blast_tac(HOL_cs addDs [howe_iwff]addIs [opensim_refl_i]@howe.intrs@iwff.intrs) 1);
qed "howe_cong_App";

Goal " [|abstr M;abstr N; ALL x.  x # env |- M (VAR x) <howe> N (VAR x)|] ==> env |- (bLam M) <howe> (bLam N)";
by(blast_tac(HOL_cs addDs [howe_iwff] addIs [opensim_refl_i]@howe.intrs@iwff.intrs) 1);
qed "howe_cong_bLam";


(* howe subst: to be completed *)

Goal " env |- s <howe> t \
   \ ==>! n env1.  ((env = n # env1) &  (  env1 |- a <howe> b)) --> env1 |-  subst s n a <howe> subst t n b";

be howe.induct 1;
by(strip_tac 1);
by(Simp_tac 1);
by(Step_tac 1);

(* n = x *)
by(subgoal_tac "env1 |-- b" 1);
by(forward_tac [open_ss] 1);
by(Asm_full_simp_tac 1);
by(blast_tac (HOL_cs addIs[cand_right] ) 1);
by(blast_tac(HOL_cs addDs[howe_iwff] ) 1);

(* n~= x *)

by(subgoal_tac "env1 |-- b" 1);
by(forward_tac [open_ss] 1);
by(Asm_full_simp_tac 1);
by(blast_tac(HOL_cs addDs[howe_iwff] addIs [opensim_howe]) 1);
by(blast_tac(HOL_cs addDs[howe_iwff] ) 1);
by(defer_tac 1);

(* app *)

Addsimps [subst_App];

by(subgoal_tac "env1 |-- b" 1);
bd open_ss 1; 
by(fast_tac(HOL_cs addDs [howe_iwff]) 2);

by(subgoal_tac "isexp M1 & isexp M2 & isexp M1' & isexp M2' " 1);
by(fast_tac(HOL_cs addDs [howe_wff] addss(simpset() addsimps [wff_def])) 2);

by(rotate_tac ~1 1);
by(Asm_full_simp_tac 1);
by(fast_tac(claset() addIs howe.intrs) 1);

Delsimps [subst_App];

(* lam *)
Addsimps [subst_lam];
by(subgoal_tac "env1 |-- b" 1);
auto();
bd open_ss 1;


by(fast_tac(HOL_cs addDs [howe_iwff]) 2);

by(Asm_full_simp_tac 1);
brs howe.intrs 1;

by(defer_tac 1);
br biAbstr_proper_abstr1 1;br abstr_biAbstr_biSubst 1;ba 1;
by(fast_tac(HOL_cs addDs [howe_wff,isexp_proper] addss(simpset() addsimps [wff_def])) 1); 
br biAbstr_proper_abstr1 1;br abstr_biAbstr_biSubst 1;ba 1;
by(fast_tac(HOL_cs addDs [howe_wff,isexp_proper] addss(simpset() addsimps [wff_def])) 1); 

(*
by(strip_tac 1);
by(eres_inst_tac [("x"," y")] allE 1);
by(Clarify_tac 1);
 by(thin_tac " env1 |- a <howe> b" 1);
by(forward_tac [howe_wff] 1);
by(Clarify_tac 1);
by(rotate_tac ~2 1);
Delsimps  [subst_lam] ;
 by(asm_full_simp_tac(simpset() addsimps [sub_biSub]) 1);


qed "howe_subst1";
qed_spec_mp "howe_subst";
*)

Goal "[| n # env |- s <opensim> t ;  env |-- p|] ==> env |- subst s n p <opensim> subst t n p";
bd open_ss 1;
auto();
qed "open_ss_mp";


(* used in cand_eval_bLAM *)

Goal "[|!n . n # env |-  N (VAR n) <howe> N' (VAR n); abstr N; abstr N';env |--  q|] ==> env |- (N q) <howe> (N' q)";
by(blast_tac(HOL_cs addIs [howe_subst,howe_refl]) 1);
qed "howe_lift";


(* start Lemma 5.3 or A.6 *)

fun  howe_mk_cases  head =  let
         val rbt = rule_by_tactic (ALLGOALS (hysimp ([bLam_inject]@unlam_defs)) THEN (fold_tac unlam_defs))
  in
 (rbt o howe.mk_cases) head end;

bind_thm ("howeApp_E",howe_mk_cases " env |- (p1 $ p2) <howe> N ");
bind_thm ("howebLam_E",howe_mk_cases " env |- (bLam E) <howe> N ");


Goal"[| abstr M;[] |- (bLam M) <howe> P|]   ==> ? N. P >> (bLam N) & abstr N &  (! Q . cloexp Q   --> [] |- ( M Q)  <howe> (N  Q))"; 
be howebLam_E 1; 
be opensim_Nil_E 1;
bes simEs 1;
by(eres_inst_tac [("x"," N'")] allE 1);
bd mp 1;
br  eval.eval_abs 1;
by(fast_tac (HOL_cs addss (simpset() addsimps [cloAbstr_def])) 1);
bd mp 1;
by(fast_tac (HOL_cs addss (simpset() addsimps [cloAbstr_def])) 1);

be exE 1;by(Clarify_tac 1);
br exI 1; br conjI 1;
auto();
by(fast_tac (HOL_cs addss (simpset() addsimps [cloAbstr_def])) 1);

br cand_right 1;
(* keep the following here *)
by(blast_tac(HOL_cs addDs [sim_cloexp] addIs opensim.intrs ) 2);

by(hysimp_and_sub [] 1);
by(blast_tac(HOL_cs addIs [howe_lift,iwff_Nil_cloexp2] addss (simpset() addsimps [cloexp_def])) 1);

qed "cand_eval_bLam";


 (* downward closure *)

Goal "P >> v ==> ! Q  .( [] |- P <howe> Q)  --> ([] |-  v <howe> Q) ";

be eval.induct 1;
by(Fast_tac 1);
by(strip_tac 1);
be howeApp_E 1;
be conjE 1;
by(hyp_subst_tac 1);
be allE 1 ;bd mp 1; ba 1;
be howebLam_E 1;
by(hysimp_and_sub [cloAbstr_def] 1);

be opensim_Nil_E 1 ;back();
bes simEs 1;

by(eres_inst_tac [("x"," N'")] allE 1);
bd mp 1;brs eval.intrs 1;
by(fast_tac(HOL_cs addss (simpset() addsimps [cloAbstr_def])) 1);
bd mp 1;
by(fast_tac(HOL_cs addss (simpset() addsimps [cloAbstr_def])) 1);


by(Clarify_tac 1);
bd howe_subst  1;
ba 1;ba 1;ba 1;back();
by(eres_inst_tac [("x"," M2'")] allE 1);back();
bd mp 1;

by(fast_tac(claset() addDs[howe_Nil_cloexp]) 1);

by(forward_tac [cand_right]  1);
back();back();
brs opensim.intrs 1;

by(fast_tac(claset() addDs[howe_Nil_cloexp]) 1);ba 2;
by(fast_tac(claset() addDs[howe_Nil_cloexp,clo_sub]) 1);

be allE 1; bd mp 1;ba 1;back();

(* case analysys *)

by(forward_tac [value_sound] 1);back();
be value.elim 1;
by(hyp_subst_tac 1);

be howebLam_E 1;by(hysimp_and_sub [cloAbstr_def] 1);
be opensim_Nil_E 1 ;back();

bes simEs 1;back();
by(eres_inst_tac [("x"," N'a")] allE 1);
bd mp 1;brs eval.intrs 1;

by(asm_full_simp_tac(simpset() addsimps [cloAbstr_def]) 1);

bd mp 1;by(asm_full_simp_tac(simpset() addsimps [cloAbstr_def]) 1);

by(Clarify_tac 1);
bd eval.eval_app 1;back();back();
by(asm_full_simp_tac(simpset() addsimps [cloAbstr_def]) 1);
ba 2;

by(fast_tac(claset() addDs[howe_Nil_cloexp]) 1);

be opensim_App_Nil_E 1;
be sim_app_E 1;
by(eres_inst_tac [("x"," ua")] allE 1);
by(Clarify_tac 1);

by(subgoal_tac "bLam N'a <sim> Q" 1);

br howe.hbLam 1;by(Best_tac 1); ba 1;ba 1;

by(fast_tac(HOL_cs addIs opensim.intrs ) 1);

brs sim.intrs 1;ba 1;ba 1;

by(strip_tac 1);
br exI 1;
br conjI 1;ba 1 ; br conjI 1;ba 1;
by(strip_tac 1);
by(eres_inst_tac [("x"," p")] allE 1);
by(eres_inst_tac [("x"," p")] allE 1);
by(Clarify_tac 1);
be  eval_Abs_E 1;
by(hysimp_and_sub [cloAbstr_def] 1);

by(subgoal_tac "t = Ea" 1);
by(hyp_subst_tac 1);
by(blast_tac(HOL_cs addIs [sim_trans] ) 1);

by(fast_tac(HOL_cs addIs[bLam_inject1] ) 1);

qed_spec_mp "down_howe_closure";


(* main lemma: howe_sim *)


Goal "  [] |- M <howe> N  ==> M <sim> N  ";
Addsimps[cloAbstr_def];
br sim.coinduct 1;
by (res_inst_tac [("P","% (u,v). [] |- u <howe> v")] CollectI 1);
auto();
by(fast_tac(HOL_cs addIs[wff_Nil_cloexp1] addDs [howe_wff]) 1);
by(fast_tac(HOL_cs addIs[wff_Nil_cloexp1] addDs [howe_wff]) 1);
bd down_howe_closure 1;
ba 1;
bd cand_eval_bLam 1;
ba 1;
by(best_tac(HOL_cs addDs[eval_cloexp ]) 1);
Delsimps[cloAbstr_def];
qed "howe_sim";



Goal"! s t. (env |- s <howe> t)  --> (env |- s <opensim>  t)";
by (induct_tac "env" 1);
by(fast_tac(HOL_cs addIs[wff_Nil_cloexp1,howe_sim]@opensim.intrs addDs [howe_wff]) 1);
by(strip_tac 1);
brs opensim.intrs 1;
by(fast_tac(HOL_cs addDs[howe_wff] addss(simpset() addsimps [wff_def])) 1);
by(fast_tac(HOL_cs addDs[howe_wff] addss(simpset() addsimps [wff_def])) 1);
by(strip_tac 1);
bd howe_sub 1;
auto();
br howe_refl 1;
br wff_to_iwff 1;
by(asm_full_simp_tac(simpset() addsimps[cloexp_def,wff_def]) 1);
qed_spec_mp "howe_opensim";


Goal "(env |- M <opensim> N ) =  (env |- M <howe> N )";
br iffI 1;
br opensim_howe 1;
br howe_opensim 2;
auto();
qed "howe_is_sim";

(* precongruence of sim *)

Goal "[|M <sim> M';N <sim> N' |] ==> (M $ N)<sim> (M' $ N')";
by(best_tac(HOL_cs addIs [howe_sim,howe_cong_App,opensim_howe]
@ opensim.intrs  addDs [sim_cloexp]) 1);
qed "sim_cong_App";

Goal "[|env |- M <opensim> M'; env |- N <opensim> N' |] ==> env |- (M $ N)<opensim> (M' $ N')";
by(blast_tac (HOL_cs addIs [ howe_opensim, howe_cong_App , opensim_howe ]) 1);
qed "opensim_cong_App";

Goal " [|abstr M;abstr N; ALL x. x#env |-  M (VAR x) <opensim> N (VAR x)|] ==> env |- (bLam M) <opensim> (bLam N)";
by(blast_tac (HOL_cs addIs [ howe_opensim, howe_cong_bLam , opensim_howe ]) 1);
qed "opensim_cong_bLam";





(* start junk *)


(*
Goal "value U ==> U <howe> P  --> (? V. P >> V & U <howe> V)"; 

be value.elim 1;auto();
be howebLam_E 1; 
bes simEsc  1;
by(eres_inst_tac [("x","N' ")] allE 1);
br (make_elim eval.eval_abs) 1;
ba 1;
by(Fast_tac 1);
bd mp 1 ; brs eval.intrs 1;
ba 1;
by(hysimp [] 1); by(hyp_subst_tac 1);
by(fast_tac(claset() addDs [howe_isexp] ) 1);
bd mp 1; ba 1;
 
be exE 1; be conjE 1;
br exI 1; br conjI 1;
ba 1;

 by(hysimp [] 1);
brs howe.intrs 1;
by(Fast_tac 1);
ba 1;ba 1;


brs sim.intrs 1;
by(strip_tac 1);
br exI 1; br conjI 1;
 brs eval.intrs 1;by(Fast_tac 1);

 by(thin_tac "lam x. N x >> lam x. N x" 1);
bd eval_isexp 1;
be conjE 1;
be conjE 1;
be isexp_Abs_E 1;


by(subgoal_tac "p = u" 1);
by(Fast_tac 1);
 br abstr_LAM_inject 1;
auto();

 by(thin_tac "lam x. N x >> lam x. N x" 1);
 by(thin_tac "P  >> lam x. u x" 1);
 be eval_Abs_E 1;

by(subgoal_tac "t = E" 1);
 by(hysimp [] 1);


br bLam_inject1 1;
auto();

 qed_spec_mp "lemma_iv";


(* specilized form *)

Goal " [| abstr M; bLam M <howe> P |] ==> EX N. P >> (bLam N)  & bLam M <howe> (bLam N) ";
be howebLam_E 1; 
bes simEsc  1;
by(eres_inst_tac [("x","N' ")] allE 1);
br (make_elim eval.eval_abs) 1;
ba 1;
by(hysimp_and_sub [] 1);
by(fast_tac(claset() addDs[howe_isexp]) 1);

bd mp 1 ; brs eval.intrs 1;
ba 1;
by(hysimp [] 1); by(hyp_subst_tac 1);
by(fast_tac(claset() addDs [howe_isexp] ) 1);
bd mp 1; ba 1;
 
by(Safe_tac );
by(hysimp_and_sub [] 1);
br exI 1; br conjI 1;
ba 1;

brs howe.intrs 1;
by(Fast_tac 1);
ba 1;ba 1;




brs sim.intrs 1;
by(strip_tac 1);
br exI 1; br conjI 1;
 brs eval.intrs 1;by(Fast_tac 1);

 


Goal " [| abstr M; bLam M <howe> P |] ==> EX N. P >> N & bLam M <howe> N ";
 by(best_tac(HOL_cs addIs [lemma_iv]@value.intrs addDs[howe_isexp,abstr_LAM_inject] addEs [isexp_Abs_E]) 1);
qed_spec_mp "lemma_iv_bLam'";


 Goal " [| abstr M; bLam M <howe> P |] ==> EX N. P >> (bLam N) & abstr N & bLam M <howe> (bLam N) ";
 by(forward_tac [lemma_iv_bLam'] 1);
auto();
by(forward_tac [value_sound] 1);
 by(fast_tac(claset() addEs value.elims) 1);
qed_spec_mp "lemma_iv_bLam";


(*

bind_thm ("howebbLam_E",howe_mk_cases " env |- (bLam Q1) <howe> (bLam Q2) ");

Goal "M >> C ==> ! N  . M <howe> N  --> C <howe> N ";
be eval.induct 1;

(* trivial case *)

by(Fast_tac 1);
	(* app *)

by(strip_tac 1);
be howeApp_E 1;
be conjE 1;
by(hyp_subst_tac 1);

be allE 1 ;bd mp 1; ba 1;

by(forward_tac [lemma_iv_bLam]  1);

ba 1;by(Safe_tac);

be howebbLam_E 1;
by(hysimp_and_sub [] 1);
by(forward_tac [howe_subst]  1);
ba 1;ba 1;ba 1;back();

be allE 1; bd mp 1;ba 1;

(* case analysys *)
by(forward_tac [value_sound] 1);back();
be value.elim 1;
by(hyp_subst_tac 1);

be howebLam_E 1;back();by(hysimp_and_sub [] 1);

by(subgoal_tac "bLam N'a <sim> N" 1);
 by(defer_tac 1);

bes simEsc 1;back();back();
by(eres_inst_tac [("x"," N'a")] allE 1);
bd mp 1;brs eval.intrs 1; ba 1;by(fast_tac(claset() addDs[howe_cloexp]) 1);


bd mp 1;ba 1; 
by(Clarify_tac 1);
bd eval.eval_app 1;back();back();




*)
*)