File ResidualBeta.ML

(*  Title:      ResidualBeta.ML
    Author:     James Brotherston / Rene Vestergaard
    Revised:    3rd April, 2001

- Lemma: any BCF term has a residual beta-completion. 
- Lemma: for all terms which have a residual beta-completion, any residual 
         beta-divergence can be resolved to this residual beta-completion.
- Theorem: the residual beta-completion of any BCF term can never be blocked by
           any sequence of residual beta-steps.

*)

AddSIs comp_res_beta.intrs;

(* Decomposition properties of BCF terms *)
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) ==> BCF(e1) & BCF(e2)";
by(Auto_tac);
qed "BCF_redex";

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

(* Monotonicity results about FV and BV under ->|RB *)
Goal "s ->|RB t ==> BV(t) <= BV(s)";
by(etac comp_res_beta.induct 1);
by(Auto_tac);
by(dtac BV_subst_lemma_1 1);
by(Fast_tac 1);
qed "comp_res_beta_BV_lemma";


Goal "s ->|RB t ==> FV(t) <= FV(s)";
by(etac comp_res_beta.induct 1);
by(Auto_tac);
by(dtac FV_subst_lemma_1 1);
by(Fast_tac 1);
by(cut_inst_tac [("x","x"),("e'","t'"),("e","s'")] renaming_sanity_3 1);
by(ALLGOALS Fast_tac);
qed "comp_res_beta_FV_lemma";


(* Lemma: any BCF term has a residual beta-completion *)
Goal "BCF(s) --> (EX t. s ->|RB t)"; 
by(induct_tac "s" 1);
by(ALLGOALS strip_tac);
(* Variable case - trivial by Var rule *)
by(Fast_tac 1);
(* Application case - apply IH by BCF decomposition, then use App *)
by(dtac BCF_app 1);
by(Fast_tac 1);
(* Abstraction case - apply IH by BCF decomposition, then use Abs *)
by(dtac BCF_abs 1);
by(Fast_tac 1);
(* Redex case - first apply IH by BCF decomposition *)
by(ftac BCF_redex 1);
by(Asm_full_simp_tac 1);
by(REPEAT_DETERM (etac exE 1));
(* Then resolve with residual-beta contraction rule *)
by(res_inst_tac [("x","t[var:=ta]")] exI 1);
by(case_tac "var:FV(t)" 1);
by(Asm_simp_tac 2);
by(eatac comp_res_beta.crbeta2 1 2);
by(rtac comp_res_beta.crbeta1 1 THEN atac 1 THEN atac 1 THEN atac 2);
(* Proof burden is now to satisfy the side condition on the contraction rule *)
by(dtac BCF_consq_1 1);
by(cut_inst_tac [("x","var"),("e","t")] Capt_in_BV 1);
by(dtac comp_res_beta_BV_lemma 1);
by(dtac comp_res_beta_FV_lemma 1);
by(Fast_tac 1);
(* Lazy case *)
qed_spec_mp "BCF_residual_completion";


(* Lemmas for proving substitutivity *)

Goal "[|(Capt y e) Int FV(e1) = {}; (Capt y (e[x:=e1])) Int FV(e2) = {}|] ==> (Capt y e) Int FV(e1[x:=e2]) = {}";
by(case_tac "x:FV(e1)" 1);
by(Asm_simp_tac 2);
by(rotate_tac ~1 1);
by(case_tac "y=x" 1);
by(dtac disjI2 1);
by(dtac Capt_in_capt_subst_1 1);
by(etac Int_subst_lemma_1 1);
by(Fast_tac 1);
by(rotate_tac ~1 1);
by(ftac disjI1 1);
by(dtac Capt_in_capt_subst_1 1);
by(etac Int_subst_lemma_1 1);
by(Fast_tac 1);
qed "case1_lemma_1";


Goal "[|(Capt x (e[y:=e'])) Int A = {}; (Capt y e) Int FV(e') = {}; y:FV(e)|] ==> (Capt x e') Int A = {}";
by(rotate_tac 1 1);
by(datac Capt_in_capt_subst_2 1 1);
by(Fast_tac 1);
qed "key_induction_2";


Goal "[|y~:FV(e'); y~=x|] ==> Capt y e = Capt y(e[x:=e'])";
by(induct_tac "e" 1);
by(dtac FV_Capt_2 1);
by(Asm_full_simp_tac 1);
by(Asm_simp_tac 1);
by(Asm_simp_tac 1);
by(rtac conjI 1);
by(ALLGOALS strip_tac);
by(etac conjE 1);
by(dtac FV_subst_lemma_1 1);
by(Fast_tac 1);
by(dtac FV_subst_lemma_5 1);
by(Fast_tac 1);
by(Asm_full_simp_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(etac conjE 1 THEN dtac FV_subst_lemma_1 1);
by(Fast_tac 1);
by(dtac FV_subst_lemma_5 1);
by(Fast_tac 1);
qed "subcase2_lemma_1";



Goal "(A Un B) Int C = {} ==> A Int C = {} & B Int C = {}";
by(Blast_tac 1);
qed "disjoint_monotinicity";


Goal "[|x:FV(e'); x~=y|] ==> (Capt y e) Int FV(e') = {} --> y:FV(e) --> Capt x (e[y:=e']) = Capt x e Un Capt x e' Un Capt y e";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(Asm_full_simp_tac 1);
by(Asm_full_simp_tac 1);
by(dtac disjoint_monotinicity 1);
by(Asm_full_simp_tac 1);
by(etac disjE 1);
by(case_tac "y:FV(mlterm2)" 1);
by(Asm_full_simp_tac 1 THEN Fast_tac 1);
by(ftac FV_Capt_2 1);
by(Asm_full_simp_tac 1 THEN Fast_tac 1);
by(case_tac "y:FV(mlterm1)" 1);
by(Asm_full_simp_tac 1 THEN Fast_tac 1);
by(ftac FV_Capt_2 1);
by(Asm_full_simp_tac 1 THEN Fast_tac 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(etac conjE 1);
by(ftac not_sym 1 THEN fatac Capt_Int_FV_lemma_1 1 1);
by(fatac Capt_induct_2 1 1);
by(mp_tac 1);
by(rtac conjI 1 THEN rtac conjI 2 THEN ALLGOALS strip_tac);
by(contr_tac 2);
by(Fast_tac 2);
by(etac conjE 1);
by(Asm_simp_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(rtac conjI 2 THEN ALLGOALS strip_tac);
by(rotate_tac ~2 2 THEN dtac FV_Capt_2 2);
by(Asm_simp_tac 2);
by(thin_tac "x:FV(mlterm)" 1);
by(thin_tac "x~:FV(mlterm)" 2);
by(distinct_subgoals_tac);
by(case_tac "x=var" 1);
by(Asm_full_simp_tac 1);
by(etac conjI 1);
by(dres_inst_tac [("e","mlterm"),("y","y")] FV_subst_lemma_6 1);
by(REPEAT_DETERM (atac 1));
(* JB: redex case, could be quite hard *)
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 1);
by(dtac Capt_induct_3 1);
by(etac conjE 1);
by(case_tac "var=y" 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 1);
by(Asm_full_simp_tac 1);
by(strip_tac 1 THEN rtac conjI 1 THEN ALLGOALS strip_tac);
by(Fast_tac 1);
by(Fast_tac 1);
by(mp_tac 1 THEN etac conjE 1);
by(case_tac "x=var" 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 1);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1 THEN ftac not_sym 1);
by(rotate_tac ~4 1 THEN ftac not_sym 1);
by(case_tac "y:FV(mlterm1)" 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 1);
by(etac disjE 2);
by(Fast_tac 2);
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 2);
by(rtac conjI 2 THEN ALLGOALS strip_tac);
by(Asm_full_simp_tac 3 THEN Fast_tac 3);
by(Asm_full_simp_tac 2 THEN Fast_tac 2);
by(case_tac "y:FV(mlterm2)" 1);
by(mp_tac 1);
by(Asm_full_simp_tac 1); 
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(Fast_tac 1);
by(dtac FV_subst_lemma_5 1 THEN Fast_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(rotate_tac ~2 1 THEN dtac FV_Capt_2 1 THEN Fast_tac 1);
by(rotate_tac 6 1 THEN datac FV_subst_lemma_6 2 1 THEN contr_tac 1); 
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 1);
by(Asm_full_simp_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(rotate_tac ~4 1 THEN dtac FV_Capt_2 1 THEN Fast_tac 1);
by(dtac FV_subst_lemma_5 1 THEN Fast_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(REPEAT_DETERM (dtac FV_Capt_2 1));
by(Fast_tac 1);
by(rotate_tac 6 1 THEN dtac FV_subst_lemma_6 1);
by(rotate_tac 3 1 THEN atac 1 THEN atac 1);
by(contr_tac 1);
qed_spec_mp "Capt_subst_distribute";


Goal "[|(Capt y e) Int FV(e1) = {}; (Capt x (e[y:=e1])) Int FV(e2) = {}; x~=y; y:FV(e)|] ==> (Capt y e) Int FV(e1[x:=e2]) = {}";
by(case_tac "x:FV(e1)" 1);
by(Asm_simp_tac 2);
by(fatac Capt_subst_distribute 3 1);
by(etac Int_subst_lemma_1 1);
by(Auto_tac);
qed "subcase2_lemma_2";


Goal "(Capt x e) Int FV(e1) = {} --> Capt x e Int FV(e1[x:=e2]) = {} --> e[x:=e1][x:=e2] = e[x:=e1[x:=e2]]";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(Simp_tac 1);
by(REPEAT_DETERM (dtac Capt_induct_1 1));
by(Asm_full_simp_tac 1);
(* Abs case *)
by(case_tac "var=x" 1);
by(Asm_simp_tac 1);
by(case_tac "x:FV(mlterm)" 1);
by(Asm_simp_tac 2);
by(ftac not_sym 1);
by(stac Capt_subst_enabling 1 THEN atac 1 THEN atac 1);
by(rotate_tac 2 1);
by(stac Capt_subst_enabling 1 THEN atac 1 THEN atac 1);
by(fatac Capt_induct_2 1 1);
by(rotate_tac 2 1);
by(fatac Capt_induct_2 1 1);
by(REPEAT_DETERM (mp_tac 1));
by(dtac sym 1 THEN Asm_simp_tac 1);
by(strip_tac 1);
by(case_tac "x:FV(e1)" 1);
by(Asm_simp_tac 2);
by(case_tac "var:FV(e1)" 1);
by(SELECT_GOAL Auto_tac 1);
by(rotate_tac ~2 1 THEN dtac FV_subst_lemma_7 1);
by(rotate_tac ~1 1 THEN atac 1);
by(etac disjE 1);
by(Asm_simp_tac 2);
by(SELECT_GOAL Auto_tac 1);
(* Redex case *)
by(ftac Capt_induct_3 1 THEN etac conjE 1);
by(rotate_tac 3 1 THEN ftac Capt_induct_3 1 THEN etac conjE 1);
by(REPEAT_DETERM (mp_tac 1));
by(case_tac "var=x" 1);
by(Asm_simp_tac 1);
by(REPEAT_DETERM (mp_tac 1));
by(REPEAT_DETERM (etac conjE 1));
by(REPEAT_DETERM (mp_tac 1));
by(case_tac "x:FV(mlterm1)" 1);
by(Asm_simp_tac 2);
by(REPEAT_DETERM (mp_tac 1));
by(ftac not_sym 1);
by(stac Capt_subst_enabling_2 1 THEN atac 1 THEN atac 1);
by(stac Capt_subst_enabling_2 1 THEN atac 1 THEN atac 1);
by(Asm_simp_tac 1 THEN strip_tac 1);
by(case_tac "x:FV(e1)" 1);
by(Asm_simp_tac 2);
by(rotate_tac ~1 1 THEN dtac FV_subst_lemma_7 1);
by(rotate_tac ~1 1 THEN atac 1);
by(etac disjE 1);
by(Asm_simp_tac 2);
by(contr_tac 1);
qed_spec_mp "subcase1_lemma_2";


Goal "[|A<=B; B Int C = {}|] ==> A Int C = {}";
by(Blast_tac 1);
qed "subset_lemma_2";


(* Lemma: substitutivity of ->|RB *)
Goal "s1 ->|RB t1 ==> s2 ->|RB t2 --> Capt x s1 Int FV(s2) = {} --> Capt x t1 Int FV(t2) = {} --> s1[x:=s2] ->|RB t1[x:=t2]";
by(etac comp_res_beta.induct 1);
by(ALLGOALS strip_tac);
by(defer_tac 1);
by(defer_tac 1);
(* Var rule case; two subcases, both straightforward *)
by(case_tac "x=xa" 1);
by(Asm_full_simp_tac 1);
by(Asm_simp_tac 1);
by(Fast_tac 1);
(* App rule case; immediate by induction hypothesis *)
by(REPEAT_DETERM (dtac Capt_induct_1 1));
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
(* Abs rule case; splits into subcases, all straightforward by induction *)
by(case_tac "xa=x" 1);
by(Asm_simp_tac 1);
by(Fast_tac 1);
by(ftac comp_res_beta_FV_lemma 1);
by(case_tac "x:FV(s)" 1);
by(datac subset_lemma_1 1 2);
by(Asm_simp_tac 2);
by(Fast_tac 2);
by(fatac Capt_induct_2 1 1);
by(rotate_tac 4 1 THEN fatac Capt_induct_2 1 1);
by(REPEAT_DETERM (mp_tac 1));
by(Asm_simp_tac 1);
by(datac Capt_Int_FV_lemma_1 1 1);
by(datac Capt_Int_FV_lemma_1 1 1);
by(etac disjE 1);
by(Asm_simp_tac 1);
by(etac disjE 1);
by(Asm_simp_tac 1 THEN Fast_tac 1);
by(datac subset_lemma_1 1 1);
by(Asm_simp_tac 1 THEN Fast_tac 1);
by(etac disjE 1);
by(Asm_simp_tac 2);
by(Fast_tac 2);
by(rotate_tac 5 1 THEN dtac comp_res_beta_FV_lemma 1);
by(rotate_tac ~1 1 THEN datac subset_lemma_1 1 1);
by(rotate_tac 2 1 THEN Asm_full_simp_tac 1);
by(Fast_tac 1);
(* Only the two redex rule cases remain at this stage.*)
(* The second case is much easier and we solve it first: *)
by(defer_tac 1);
by(case_tac "xa=x" 1);
by(Asm_full_simp_tac 1);
by(eatac comp_res_beta.crbeta2 1 1);
by(dtac Capt_induct_3 1);
by(Asm_full_simp_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(etac comp_res_beta.crbeta2 1);
by(etac FV_subst_lemma_4 1);
by(rotate_tac 1 1 THEN dtac comp_res_beta_FV_lemma 1);
by(eatac subset_lemma_1 1 1);
by(ftac comp_res_beta_FV_lemma 1);
by(Clarify_tac 1);
by(datac subset_lemma_1 1 1);
by(Asm_simp_tac 1);
by(Fast_tac 1);
(* Now we tackle the remaining redex rule case, which is harder *)
by(case_tac "xa=x" 1);
(* First subcase: xa=x *)
by(Asm_full_simp_tac 1);
by(rotate_tac ~2 1 THEN fatac case1_lemma_1 1 1);
by(datac key_induction_2 2 1);
by(mp_tac 1);
by(dtac comp_res_beta.crbeta1 1);
by(rotate_tac ~1 1 THEN REPEAT_DETERM(atac 1));
by(stac subcase1_lemma_2 1);
by(REPEAT_DETERM (atac 1));
(* Subgoal complete by substitution lemma *)
by(ftac not_sym 1);
by(ftac Capt_induct_3 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
(* Subcase xa~=x & xa~:FV(t2) & xa:FV(s') *)
by(rotate_tac 1 1 THEN ftac comp_res_beta_FV_lemma 1);
by(fatac subset_lemma_1 1 1);
(* Subcase xa~=x & xa~:FV(t2) & xa:FV(s') *)
by(cut_inst_tac [("y","xa"),("e","s'"),("e'","t2")] subcase2_lemma_1 1);
by(atac 1 THEN atac 1);
by(fatac key_induction_2 2 1);
by(fatac subcase2_lemma_2 3 1);
by(cut_inst_tac [("x","x"),("y","xa"),("e","s'"),("e'","t'")] Capt_in_capt_subst_1 1);
by(etac disjI1 1);
by(rotate_tac ~1 1 THEN fatac subset_lemma_2 1 1);
by(REPEAT_DETERM (mp_tac 1));
by(stac (Substitution_Lemma_1 RS sym) 1);
by(REPEAT_DETERM (atac 1));
by(eatac comp_res_beta.crbeta1 1 1);
by(Asm_full_simp_tac 1);
by(eatac FV_subst_lemma_2 1 1);
(* Subcase xa~=x & xa:FV(s2); splits into xa:FV(t2) and xa~:FV(t2) *)
by(case_tac "x:FV(s)" 1);
by(Fast_tac 1);
by(rotate_tac ~1 1);
by(case_tac "xa:FV(t2)" 1);
by(defer_tac 1);
(* Subsubcase xa~:FV(t2) is exactly like the previous case *)
(* Subsubcase xa~=x & xa~:FV(t2) & xa:FV(s') *)
by(cut_inst_tac [("y","xa"),("e","s'"),("e'","t2")] subcase2_lemma_1 1);
by(atac 1 THEN atac 1);
by(fatac key_induction_2 2 1);
by(fatac subcase2_lemma_2 3 1);
by(cut_inst_tac [("x","x"),("y","xa"),("e","s'"),("e'","t'")] Capt_in_capt_subst_1 1);
by(etac disjI1 1);
by(rotate_tac ~1 1 THEN fatac subset_lemma_2 1 1);
by(REPEAT_DETERM (mp_tac 1));
by(stac (Substitution_Lemma_1 RS sym) 1);
by(REPEAT_DETERM (atac 1));
by(rtac comp_res_beta.crbeta1 1);
by(Asm_full_simp_tac 1);
by(atac 1);
by(Asm_full_simp_tac 1);
by(eatac FV_subst_lemma_2 1 1);
(* Subcase xa~=x & xa:FV(s2) & xa:FV(t2) *)
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 1);
by(ftac comp_res_beta_FV_lemma 1);
by(fatac subset_lemma_1 1 1);
by(fatac key_induction_2 2 1);
by(fatac subcase2_lemma_2 3 1);
by(stac (Substitution_Lemma_2 RS sym) 1);
by(REPEAT_DETERM (atac 1));
by(mp_tac 1);
by(eatac comp_res_beta.crbeta1 3 1);
qed_spec_mp "comp_res_beta_substitutivity";



val comp_res_beta_E1 = comp_res_beta.mk_cases "Var x ->|RB e'";
val comp_res_beta_E2 = comp_res_beta.mk_cases "e1 $ e2 ->|RB e'";
val comp_res_beta_E3 = comp_res_beta.mk_cases "Abs x e ->|RB e'";
val comp_res_beta_E4 = comp_res_beta.mk_cases "<Abs x e1>@e2 ->|RB e'";


(* Special substitutivity lemma *)

Goal "s ->|RB s' ==> x~:FV(s') --> Capt x s Int FV(t) = {} --> s[x:=t] ->|RB s'";
by(etac comp_res_beta.induct 1);
by(ALLGOALS strip_tac);
(* Non-marked cases, straightforward by induction *)
by(SELECT_GOAL Auto_tac 3);
by(dtac Capt_induct_1 3);
by(SELECT_GOAL Auto_tac 3);
by(case_tac "xa=x" 3);
by(SELECT_GOAL Auto_tac 3);
by(fatac Capt_induct_2 1 3);
by(SELECT_GOAL Auto_tac 3);
by(defer_tac 1);
(* Lazy redex rule case *)
by(ftac Capt_induct_3 1 THEN etac conjE 1);
by(SELECT_GOAL Auto_tac 1);
(* Non-lazy redex rule case *)
by(dtac Capt_induct_3 1 THEN etac conjE 1);
by(case_tac "xa=x" 1);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(t')" 1);
by(rotate_tac ~1 1 THEN datac FV_subst_lemma_3 1 1);
by(Fast_tac 1);
by(mp_tac 1);
by(eatac comp_res_beta.crbeta1 3 1);
(* Subcase xa~=x *)
by(ftac not_sym 1);
by(ftac FV_subst_lemma_5 1);
by(Asm_full_simp_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(t')" 1);
by(rotate_tac ~1 1 THEN dtac FV_subst_lemma_6 1);
by(rotate_tac ~5 1 THEN atac 1 THEN atac 1);
by(contr_tac 1);
by(mp_tac 1);
by(eatac comp_res_beta.crbeta1 3 1);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(t')" 1);
by(rotate_tac ~1 1 THEN dtac FV_subst_lemma_6 1);
by(rotate_tac ~5 1 THEN atac 1 THEN atac 1);
by(contr_tac 1);
by(mp_tac 1);
by(eatac comp_res_beta.crbeta1 3 1);
qed_spec_mp "comp_res_beta_lazy_substitutivity";


(* Invoke the following only once substitutivity has been proved *)

AddSIs res_beta.intrs;
val res_beta_E1 = res_beta.mk_cases "Var x ->RB e'";
val res_beta_E2 = res_beta.mk_cases "e1 $ e2 ->RB e'";
val res_beta_E3 = res_beta.mk_cases "Abs x e ->RB e'";
val res_beta_E4 = res_beta.mk_cases "<Abs x e1> @ e2' ->RB e'";

(* Lemma: residual-completion of ->RB *)
Goal "s ->|RB u ==> ALL t. s ->RB t --> t ->|RB u";
by(etac comp_res_beta.induct 1);
by(ALLGOALS strip_tac);
by(defer_tac 1);
by(defer_tac 1);
(* Var rule case *)
by(etac res_beta_E1 1);
(* App rule case *)
by(etac res_beta_E2 1);
by(Fast_tac 1);
by(Fast_tac 1);
(* Abs rule case *)
by(etac res_beta_E3 1);
by(Fast_tac 1);
(* Redex rule case; three subcases, two of which are immediate by induction *)
by(etac res_beta_E4 1);
by(ALLGOALS Asm_full_simp_tac);
by(eatac comp_res_beta_substitutivity 3 1);
by(etac allE 1 THEN mp_tac 1);
by(eatac comp_res_beta.crbeta1 3 1);
by(etac allE 1 THEN mp_tac 1);
by(eatac comp_res_beta.crbeta1 3 1);
(* Lazy redex rule case; again three subcases *)
by(etac res_beta_E4 1);
by(ALLGOALS Asm_full_simp_tac);
by(eatac comp_res_beta.crbeta2 1 3);
by(etac allE 2 THEN mp_tac 2);
by(Fast_tac 2);
by(eatac comp_res_beta_lazy_substitutivity 2 1);
qed "comp_res_beta_triangle";


(* Lemma: residual-completion of ->>RB *)

Goal "s ->>RB t ==> s ->|RB u --> t ->|RB u";
by(etac rtrancl_induct 1);
by(Fast_tac 1);
by(strip_tac 1);
by(mp_tac 1);
by(rotate_tac ~1 1 THEN dtac comp_res_beta_triangle 1);
by(Fast_tac 1);
qed "res_beta_completion_absorption";


(* Non-Blocked Beta-Residual Theory *)

Goal "[| BCF(s); s ->>RB t |] ==> EX u. t ->|RB u ";
by(dtac BCF_residual_completion 1);
by(etac exE 1);
by(dtac res_beta_completion_absorption 1);
by(Fast_tac 1);
qed "non_blocked_beta_residual_theory";