File AlphaBetaDiamond.ML

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

- Diamond property of (alpha U beta), following from combining the key lemmas:
  
     * weak commutativity of alpha and parallel-beta
     * diamond property of parallel-beta
     * fresh-naming alpha confluence
     * existence of BCFs via an alpha0-rewrite sequence

*)

val relation2_E = relation2.mk_cases "s ->2 t";

Goalw [diamond_def,commute_def,square_def] "diamond(relation2)";
by(strip_tac 1);
by(etac relation2_E 1);
by(etac relation2_E 1);
(* Apply fresh-naming alpha confluence *)
by(datac FreshAlphaConf 1 1);
by(etac exE 1);
by(etac conjE 1);
(* Apply BCF-existence lemma *)
by(cut_inst_tac [("e1.0","e3")] ExistsBCF 1);
by(etac exE 1);
by(etac conjE 1);
by(rotate_tac ~4 1);
by(datac rtrancl_trans 1 1);
by(datac rtrancl_trans 1 1);
(* Apply weak alpha/par-beta commutativity x 2 *)
by(rotate_tac ~2 1);
by(datac WeakABComm 1 1);
by(datac WeakABComm 1 1);
by(REPEAT_DETERM (etac exE 1));
by(REPEAT_DETERM (etac conjE 1));
(* Apply diamond property of parallel-beta *)
by(datac par_beta_diamond 1 1);
by(rotate_tac ~2 1);
by(atac 1);
by(etac exE 1);
by(etac conjE 1);
(* Use the target of the diamond as the witness for the proof and tidy up *)
by(res_inst_tac [("x","s'b")] exI 1);
by(rtac conjI 1);
by(ALLGOALS (eatac relation2.cons 1));
qed "diamond_relation2";