File AbstractRewrites.ML

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

- Reflection / preservation of diamond property of rewrite relations across
  structural collapse.

*)


Goalw [onto_def] "[|onto F A B; RelB <= B<*>B; (x,y):RelB|] ==> EX a. F(a)=x";
by(Blast_tac 1);
qed "onto_lemma_1";

Goalw [onto_def] "[|onto F A B; RelB <= B<*>B; (x,u):RelB|] ==> EX c. F(c)=u & c:A";
by(Blast_tac 1);
qed "onto_lemma_2";


(* Proof of the diamond preservation theorem using a stronger premise *)

Goalw [struct_coll_def,homo_def,square_def,commute_def,diamond_def] "[|struct_coll F A B RelA RelB & (ALL x x' y'. (x',y'):RelB --> F(x)=x' --> (EX y. F(y)=y' & (x,y):RelA))|] ==> diamond(RelA) --> diamond(RelB)";
by(strip_tac 1);
by(REPEAT_DETERM (etac conjE 1));
by(rotate_tac ~2 1);
(* Use F onto *)
by(datac onto_lemma_1 2 1);
by(etac exE 1);
(* Use case premise x 2 *)
by(rotate_tac ~3 1 THEN etac all_dupE 1);
by(rotate_tac ~2 1 THEN etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(REPEAT_DETERM (mp_tac 1));
by(thin_tac "(x,y):RelB" 1);
by(etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(REPEAT_DETERM (mp_tac 1));
by(REPEAT_DETERM (etac exE 1));
by(REPEAT_DETERM (etac conjE 1));
(* Use confluence of ->A *)
by(rotate_tac 4 1);
by(etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(mp_tac 1);
by(thin_tac "(a,ya):RelA" 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(mp_tac 1);
by(thin_tac "(a,yb):RelA" 1);
by(etac exE 1 THEN etac conjE 1);
(* Use F homomorphism x 2 *)
by(res_inst_tac [("x","F u")] exI 1);
by(etac all_dupE 1);
by(Auto_tac);
qed "diamond_preservation";


(* Reflection of diamond property across structural collapse *)

Goalw [struct_coll_def,homo_def,square_def,commute_def,diamond_def] "[|struct_coll F A B RelA RelB & (ALL x y x' y'. (x',y'):RelB & F(x)=x' & F(y)=y' --> (x,y):RelA)|] ==> diamond(RelB) --> diamond(RelA)";
by(strip_tac 1);
by(REPEAT_DETERM (etac conjE 1));
by(rotate_tac ~1 1);
(* Use F total homomorphism x2 *)
by(etac all_dupE 1);
by(rotate_tac ~2 1 THEN etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(mp_tac 1);
by(cut_inst_tac [("t","F(x)")] refl 1);
by(cut_inst_tac [("t","F(y)")] refl 1);
by(mp_tac 1);
by(mp_tac 1);
by(etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(rotate_tac 2 1 THEN mp_tac 1);
by(mp_tac 1);
by(cut_inst_tac [("t","F(z)")] refl 1);
by(mp_tac 1);
by(thin_tac "F x = F x" 1);
by(thin_tac "F y = F y" 1);
by(thin_tac "F z = F z" 1);
(* Use confluence of ->B *)
by(rotate_tac ~3 1);
by(etac allE 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(mp_tac 1);
by(thin_tac "(F x, F z):RelB" 1);
by(rotate_tac ~1 1 THEN etac allE 1);
by(mp_tac 1);
by(etac exE 1);
(* Use onto-ness of F *)
by(etac conjE 1);
by(rotate_tac ~1 1);
by(datac onto_lemma_2 2 1);
by(etac exE 1);
by(etac conjE 1);
(* Use case premise x2 *)
by(Auto_tac);
qed "diamond_reflection";


Goalw [struct_coll_def, homo_def] "[|struct_coll F A B RelA RelB & (ALL x y x' y'. (x',y'):RelB & F(x)=x' & F(y)=y' --> (x,y):RelA) |] ==> ALL x x' y'. (x',y'):RelB --> F(x)=x' --> (EX y. F(y)=y' & (x,y):RelA)";
by(strip_tac 1);
by(REPEAT_DETERM (etac conjE 1));
by(thin_tac "RelA <= A<*>A" 1);
by(thin_tac "ALL x x' y y'. (x,y):RelA --> F(x)=x' --> F(y)=y' -->(x',y'):RelB" 1);
by(datac onto_lemma_2 2 1);
by(etac exE 1 THEN etac conjE 1);
by(Auto_tac);
qed "lift_case3_premise_to_case4";


(* EQUIVALENCE OF DIAMOND PROPERTY ACROSS STRUCTURAL COLLAPSE *)

Goal "[|struct_coll F A B RelA RelB & (ALL x y x' y'. (x',y'):RelB & F(x)=x' & F(y)=y' --> (x,y):RelA)|] ==> diamond(RelB) = diamond(RelA)";
by(rtac iffI 1);
by(datac (diamond_reflection RS mp) 2 1);
by(ftac lift_case3_premise_to_case4 1);
by(rtac (diamond_preservation RS mp) 1);
by(Auto_tac);
qed "diamond_equivalence";