File RawConfluence.ML

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

- Confluence of (alpha U beta), the raw characterisation of real beta

*)

Goal "beta <= par_beta";
by(rtac subsetI 1);
by(split_all_tac 1);
by(etac beta.induct 1);
by(Auto_tac);
qed "beta_subset_par_beta";


Goal "alpha Un beta <= relation2";
by(rtac subsetI 1);
by(split_all_tac 1);
by(etac UnE 1);
by(ALLGOALS (rtac relation2.cons));
by(etac r_into_rtrancl 1);
by(rtac par_beta_refl 1);
by(rtac rtrancl_refl 1);
by(cut_facts_tac [beta_subset_par_beta] 1);
by(datac subsetD 2 1);
qed "alphabeta_subset_relation2";


Goal "s ->>B t ==> Abs x s ->>B Abs x t";
by(etac rtrancl_induct 1);
by(Fast_tac 1);
by(dres_inst_tac [("x","x")] beta.babs 1);
by(eatac rtrancl_into_rtrancl 1 1);
qed "rtrancl_beta_abs";


Goal "s ->>B t ==> s $ u ->>B t $ u";
by(etac rtrancl_induct 1);
by(Fast_tac 1);
by(dres_inst_tac [("u","u")] beta.bappL 1);
by(eatac rtrancl_into_rtrancl 1 1);
qed "rtrancl_beta_appL";


Goal "s ->>B t ==> u $ s ->>B u $ t";
by(etac rtrancl_induct 1);
by(Fast_tac 1);
by(dres_inst_tac [("u","u")] beta.bappR 1);
by(eatac rtrancl_into_rtrancl 1 1);
qed "rtrancl_beta_appR";


Goal "par_beta <= beta^*";
by(rtac subsetI 1);
by(split_all_tac 1);
by(etac par_beta.induct 1);
by(Blast_tac 1);
by(etac rtrancl_beta_abs 1);
by(dres_inst_tac [("u","t")] rtrancl_beta_appL 1);
by(dres_inst_tac [("u","s'")] rtrancl_beta_appR 1);
by(eatac rtrancl_trans 1 1);
by(dres_inst_tac [("x","x")] rtrancl_beta_abs 1);
by(rotate_tac ~1 1);
by(dres_inst_tac [("u","t")] rtrancl_beta_appL 1);
by(dres_inst_tac [("u","Abs x s'")] rtrancl_beta_appR 1);
by(rotate_tac 3 1);
by(datac rtrancl_trans 1 1);
by(etac rtrancl_into_rtrancl 1);
by(etac beta.beta 1);
qed "par_beta_subset_rtrancl_beta";


Goal "(s,t):R^* ==> (s,t):(R Un T)^*";
by(etac rtrancl_induct 1);
by(rtac rtrancl_refl 1);
by(rotate_tac 1 1);
by(dres_inst_tac [("B","T")] UnI1 1);
by(eatac rtrancl_into_rtrancl 1 1);
qed "rtrancl_left_inclusion";


Goal "(s,t):R^* ==> (s,t):(T Un R)^*";
by(etac rtrancl_induct 1);
by(rtac rtrancl_refl 1);
by(rotate_tac 1 1);
by(dres_inst_tac [("A","T")] UnI2 1);
by(eatac rtrancl_into_rtrancl 1 1);
qed "rtrancl_right_inclusion";


Goal "relation2 <= (alpha Un beta)^*";
by(rtac subsetI 1);
by(split_all_tac 1);
by(etac relation2_E 1);
by(cut_facts_tac [par_beta_subset_rtrancl_beta] 1);
by(datac subsetD 1 1);
by(dres_inst_tac [("T","beta")] rtrancl_left_inclusion 1);
by(etac rtrancl_trans 1);
by(dres_inst_tac [("T","alpha")] rtrancl_right_inclusion 1);
by(atac 1);
qed "relation2_subset_alphabeta";


(* Confluence *)
Goal "confluent(alpha Un beta)";
by(cut_facts_tac [diamond_relation2,alphabeta_subset_relation2,relation2_subset_alphabeta] 1);
by(eatac diamond_to_confluence 2 1);
qed "raw_confluence";