File RawToReal.ML

(*  Title:      RawToReal.ML
    Author:     James Brotherston / Rene Vestergaard
    Revised:    17th January, 2001

- Proof of equivalence of confluence of beta on the raw and real lambda
  calculus, and hence a proof of beta-confluence on the real calculus

*)

val beta_mod_alpha_E = beta_mod_alpha.mk_cases "e -ABA-> e'";
val real_beta_E = real_beta.mk_cases "e =>B e'";


Goal "e -ABA->> e' | e =A= e' ==> Abs_acls(alphaclass(e)) =>>B Abs_acls(alphaclass(e'))";
by(etac disjE 1);
by(dtac alphaclass_lemma_1 2);
by(Asm_simp_tac 2);
by(etac rtrancl_induct 1);
by(rtac rtrancl_refl 1);
by(etac beta_mod_alpha_E 1);
by(REPEAT_DETERM (dtac alphaclass_lemma_1 1));
by(rotate_tac ~1 1 THEN dtac sym 1);
by(etac rtrancl_trans 1);
by(Asm_simp_tac 1);
by(rtac r_into_rtrancl 1);
by(etac real_beta.lift 1);
qed "raw_to_real_beta";


Goalw[mem_ac_def] "e in Abs_acls(alphaclass(e))";
by(rtac Abs_acls_inverse 1);
by(rewrite_goals_tac [acls_def]);
by(Fast_tac 1);
qed "alphaclass_self_inclusion_2";


Goalw[mem_ac_def] "e in Abs_acls(alphaclass(t)) ==> e:alphaclass(t)";
by(cut_inst_tac [("y","alphaclass(t)")] Abs_acls_inverse 1);
by(rewrite_goals_tac [acls_def]);
by(Fast_tac 1);
by(dtac sym 1);
by(Asm_full_simp_tac 1);
by(rotate_tac 1 1 THEN dtac sym 1);
by(Asm_simp_tac 1);
by(rtac alphaclass_self_inclusion 1);
qed "alphaclass_mem_elim";


Goal "ac1 =>>B ac2 ==> ALL e e'. (e in ac1 --> e' in ac2 --> (e -ABA->> e' | e =A= e'))";
by(etac rtrancl_induct 1);
by(ALLGOALS strip_tac);
by(rtac disjI2 1);
by(rtac disjI1 2);
(* Reflexive case *)
by(SELECT_GOAL (rewrite_goals_tac [mem_ac_def] ) 1);
by(cut_inst_tac [("e","e")] alphaclass_self_inclusion 1);
by(cut_inst_tac [("e","e'")] alphaclass_self_inclusion 1);
by(Asm_full_simp_tac 1);
by(SELECT_GOAL (rewrite_goals_tac [alphaclass]) 1); 
by(Full_simp_tac 1);
(* Transitive case *)
by(etac real_beta_E 1);
by(Asm_full_simp_tac 1);
by(etac allE 1);
by(mp_tac 1);
by(cut_inst_tac [("e","s")] alphaclass_self_inclusion_2 1);
by(etac allE 1);
by(mp_tac 1);
by(etac disjE 1);
by(etac rtrancl_into_rtrancl 1);
by(rtac beta_mod_alpha.cons 1);
by(Fast_tac 1);
by(atac 1);
by(dtac alphaclass_mem_elim 1);
by(rtac alphaeq_sym 1);
by(etac alphaclass_lemma_3 1);
by(rtac r_into_rtrancl 1);
by(eatac beta_mod_alpha.cons 1 1);
by(dtac alphaclass_mem_elim 1);
by(etac (alphaclass_lemma_3 RS alphaeq_sym) 1);
qed "real_to_raw_beta_aux";


Goal "Abs_acls(alphaclass(e)) =>>B Abs_acls(alphaclass(e')) = (e -ABA->> e' | e =A= e')";
by(rtac iffI 1);
by(etac raw_to_real_beta 2);
by(dtac real_to_raw_beta_aux 1);
by(cut_inst_tac [("e","e")] alphaclass_self_inclusion_2 1);
by(cut_inst_tac [("e","e'")] alphaclass_self_inclusion_2 1);
by(Asm_full_simp_tac 1);
qed "RawToReal_Lemma8";


Goal "(beta_mod_alpha)^* Un (alpha Un rev_alpha)^* = (alpha Un beta)^*";
by(rtac equalityI 1);
by(ALLGOALS (rtac subsetI));
by(ALLGOALS (Full_simp_tac));
by(etac disjE 1);
by(auto_tac (claset() delrules[disjCI], simpset()));
(* e =A= e' --> e ->>AB e' *)
by(dtac alphaeq_sym 2);
by(dtac Lemma_D 2);
by(dres_inst_tac [("T","beta")] rtrancl_left_inclusion 2);
by(atac 2);
(* e -ABA->> e' --> e ->>AB e' *)
by(etac rtrancl_induct 1);
by(rtac rtrancl_refl 1);
by(etac rtrancl_trans 1);
by(etac beta_mod_alpha_E 1);
by(dtac alphaeq_sym 1);
by(dtac alphaeq_sym 1);
by(dtac Lemma_D 1);
by(dtac Lemma_D 1);
by(thin_tac "a -ABA->> y" 1);
by(dres_inst_tac [("T","beta")] rtrancl_left_inclusion 1);
by(dres_inst_tac [("T","beta")] rtrancl_left_inclusion 1);
by(etac rtrancl_trans 1);
by(dtac r_into_rtrancl 1);
by(rotate_tac 1 1);
by(dres_inst_tac [("T","alpha")] rtrancl_right_inclusion 1);
by(eatac rtrancl_trans 1 1);
(* e ->>AB e' --> e -ABA->> e' v e =A= e' *)
by(etac rtrancl_induct 1);
by(rtac disjI2 1);
by(rtac rtrancl_refl 1);
by(etac disjE 1);
by(Full_simp_tac 2);
by(etac disjE 2);
by(rtac disjI2 2);
by(rotate_tac ~1 2);
by(dtac r_into_rtrancl 2);
by(rotate_tac ~1 2);
by(dres_inst_tac [("T","rev_alpha")] rtrancl_left_inclusion 2);
by(eatac rtrancl_trans 1 2);
by(rtac disjI1 2);
by(rtac r_into_rtrancl 2);
by(eatac beta_mod_alpha.cons 1 2);
by(rtac rtrancl_refl 2);
by(Full_simp_tac 1);
by(etac disjE 1);
by(rtac disjI1 2);
by(etac rtrancl_into_rtrancl 2);
by(rtac beta_mod_alpha.cons 2);
by(rtac rtrancl_refl 2);
by(atac 2);
by(rtac rtrancl_refl 2);
by(rotate_tac ~1 1);
by(dtac r_into_rtrancl 1);
by(rotate_tac ~1 1);
by(dres_inst_tac [("T","rev_alpha")] rtrancl_left_inclusion 1);
by(thin_tac "a ->>AB y" 1);
by(rotate_tac 1 1);
by(rtac mp 1);
by(atac 2);
by(thin_tac "y =A= z" 1);
by(etac rtrancl_induct 1);
by(ALLGOALS strip_tac);
by(etac disjI2 1);
by(rtac disjI1 1);
by(etac rtrancl_into_rtrancl 1);
by(etac beta_mod_alpha_E 1);
by(eatac beta_mod_alpha.cons 1 1);
by(eatac alphaeq_trans 1 1);
qed "RawToReal_Prop9";


Goal "e ->>AB e' ==> Abs_acls(alphaclass(e)) =>>B Abs_acls(alphaclass(e'))";
by(cut_facts_tac [RawToReal_Prop9 RS sym] 1);
by(asm_full_simp_tac (simpset() addsimps[RawToReal_Lemma8]) 1);
qed "RawToReal_Lemma7";


Goal "Abs_acls(alphaclass(e)) =>>B Abs_acls(alphaclass(e')) ==> e ->>AB e'";
by(cut_facts_tac [RawToReal_Prop9 RS sym] 1);
by(asm_full_simp_tac (simpset() addsimps[RawToReal_Lemma8]) 1);
qed "RawToReal_Lemma10";


Goalw[acls_def] "y:acls ==> EX x. alphaclass x = y";
by(Auto_tac);
qed "acls_type_lemma_1";


Goalw[struct_coll_def,onto_def,homo_def] "struct_coll (Abs_acls o alphaclass) (UNIV::lterm set) (UNIV::acls set) ((alpha Un beta)^*) (real_beta^*)";
by(Auto_tac);
by(etac RawToReal_Lemma7 2);
by(cut_inst_tac [("y","Rep_acls y")] acls_type_lemma_1 1);
by(rtac Rep_acls 1);
by(etac exE 1);
by(res_inst_tac [("x","x")] exI 1);
by(Auto_tac);
by(rtac Rep_acls_inverse 1);
qed "alphaclass_struct_coll";


Goal "ALL x y x' y'. (x',y'):(real_beta^*) & (Abs_acls o alphaclass)(x)=x' & (Abs_acls o alphaclass)(y)=y' --> (x,y):((alpha Un beta)^*)";
by(strip_tac 1);
by(REPEAT_DETERM (etac conjE 1));
by(dtac sym 1);
by(dtac sym 1);
by(Asm_full_simp_tac 1);
by(etac RawToReal_Lemma10 1);
qed "alphaclass_satisfies_preservation_premise";


Goal "confluent(real_beta)";
by(cut_facts_tac [alphaclass_struct_coll] 1);
by(stac diamond_equivalence 1);
by(etac conjI 1);
by(rtac raw_confluence 2);
by(rtac alphaclass_satisfies_preservation_premise 1);
qed "real_confluence";