File DiamondPB.ML

(*  Title:      DiamondPB.ML
    Author:     James Brotherston / Rene Vestergaard
    Revised:    30th August, 2000

- Proof of the diamond property of (raw) parallel-beta, via complete 
  developments a la Takahashi

*)


AddSIs comp_dev.intrs;
val comp_dev_E1 = comp_dev.mk_cases "Abs x e ->CD e'";


Goal "s ->CD t' ==> ALL t. s -|>B t --> t -|>B t'";
by(etac comp_dev.induct 1);
by(ALLGOALS strip_tac);
by(ALLGOALS (blast_tac (claset() addSIs[par_beta_subst])));
qed "par_beta_CD_triangle";


Goal "s ->CD t ==> s -|>B t";
by(etac comp_dev.induct 1);
by(ALLGOALS Fast_tac);
qed "CD_subset_par_beta";


Goalw[BCF] "BCF(Abs x e) ==> BCF(e)";
by(Auto_tac);
qed "BCF_abs";


Goalw[BCF] "BCF(e1 $ e2) ==> BCF(e1) & BCF(e2)";
by(Auto_tac);
qed "BCF_app";


Goalw[BCF] "BCF((Abs x e1) $ e2) ==> BV(e1) Int FV(e2) = {}";
by(Auto_tac);
qed "BCF_consq_1";


Goal "BCF(s) --> (EX t. s ->CD t)"; 
by(induct_tac "s" 1);
by(ALLGOALS strip_tac);
by(Fast_tac 1);
by(dtac BCF_abs 2);
by(Fast_tac 2);
by(ftac BCF_app 1);
by(etac conjE 1);
by(Asm_full_simp_tac 1);
by(case_tac "lterm1" 1);
by(Fast_tac 1);
by(Fast_tac 1);
by(etac exE 1);
by(etac exE 1);
by(Asm_full_simp_tac 1);
by(etac comp_dev_E1 1);
by(rotate_tac ~2 1);
by(ftac comp_dev.beta 1);
by(rotate_tac ~1 1);
by(atac 1);
by(rotate_tac ~1 1);
by(dtac CD_subset_par_beta 1);
by(dtac par_beta_FV_lemma 1);
by(dtac BCF_consq_1 1);
by(cut_inst_tac [("x","var"),("e","tb")] capt_in_bound_var 1);
by(dtac CD_subset_par_beta 1);
by(dtac par_beta_BV_lemma 1);
by(Blast_tac 1);
by(Blast_tac 1);
qed "BCF_implies_exists_CD";


(* DIAMOND PROPERTY OF PARALLEL-BETA *)

Goal "[|BCF(s); s -|>B t; s -|>B t'|] ==> EX s'. t -|>B s' & t' -|>B s'";
by(dtac (BCF_implies_exists_CD RS mp) 1);
by(etac exE 1);
by(dtac par_beta_CD_triangle 1);
by(Blast_tac 1);
qed "par_beta_diamond";