src/HOL/UNITY/PriorityAux.ML

new examples by Sidi Ehmety

(*  Title:      HOL/UNITY/PriorityAux
    ID:         $Id$
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    Copyright   2001  University of Cambridge

Auxiliary definitions needed in Priority.thy
*)

Addsimps [derive_def, derive1_def, symcl_def, A_def, R_def,  
          above_def, reach_def, reverse_def, neighbors_def];

(*All vertex sets are finite \\<dots>*)
AddIffs [[subset_UNIV, finite_vertex_univ] MRS finite_subset];

(* and relatons over vertex are finite too *)
AddIffs [[subset_UNIV, [finite_vertex_univ, finite_vertex_univ] 
           MRS finite_Prod_UNIV] MRS finite_subset];


(* The equalities (above i r = {}) = (A i r = {}) 
   and (reach i r = {}) = (R i r) rely on the following theorem  *)

Goal "((r^+)^^{i} = {}) = (r^^{i} = {})";
by Auto_tac;
by (etac trancl_induct 1);
by Auto_tac;
qed "image0_trancl_iff_image0_r";

(* Another form usefull in some situation *)
Goal "(r^^{i}={}) = (ALL x. ((i,x):r^+) = False)";
by Auto_tac;
by (dtac (image0_trancl_iff_image0_r RS ssubst) 1);
by Auto_tac;
qed "image0_r_iff_image0_trancl";


(* In finite universe acyclic coincides with wf *)
Goal 
"!!r::(vertex*vertex)set. acyclic r = wf r";
by (auto_tac (claset(), simpset() addsimps [wf_iff_acyclic_if_finite]));
qed "acyclic_eq_wf";

(* derive and derive1 are equivalent *)
Goal "derive i r q = derive1 i r q";
by Auto_tac;
qed "derive_derive1_eq";

(* Lemma 1 *)
Goalw [reach_def]
"[| x:reach i q; derive1 k r q |] ==> x~=k --> x:reach i r";
by (etac ImageE 1);
by (etac trancl_induct 1);
by (case_tac "i=k" 1);
by (auto_tac (claset() addIs [r_into_trancl], simpset()));
by (dres_inst_tac [("x", "y")] spec 1);
by (rotate_tac ~1 1);
by (dres_inst_tac [("x", "z")] spec 1);
by (auto_tac (claset() addDs [r_into_trancl] addIs [trancl_trans], simpset()));
qed "lemma1_a";

Goal "ALL k r q. derive k r q -->(reach i q <= (reach i r Un {k}))";
by (REPEAT(rtac allI 1));
by (rtac impI 1);
by (rtac subsetI 1 THEN dtac lemma1_a 1);
by (auto_tac (claset(), simpset() addsimps [derive_derive1_eq]
                    delsimps [reach_def, derive_def, derive1_def]));
qed "reach_lemma";

(* An other possible formulation of the above theorem based on
   the equivalence x:reach y r = y:above x r                  *)
Goal 
"(ALL i. reach i q <= (reach i r Un {k})) =\
\ (ALL x. x~=k --> (ALL i. i~:above x r --> i~:above x q))";
by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
qed "reach_above_lemma";

(* Lemma 2 *)
Goal 
"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)^^{z}={})";
by Auto_tac;
by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1);
by Auto_tac;
qed "maximal_converse_image0";

Goal
 "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})";
by (full_simp_tac (simpset() 
            addsimps [acyclic_eq_wf, wf_eq_minimal]) 1);
by (dres_inst_tac [("x", "((r^-1)^+)^^{i}")] spec 1);
by Auto_tac;
by (rotate_tac ~1 1);
by (asm_full_simp_tac (simpset() 
        addsimps [maximal_converse_image0, trancl_converse]) 1);
qed "above_lemma_a";


Goal
 "acyclic r ==> above i r~={}-->(EX j:above i r. above j r = {})";
by (dtac above_lemma_a 1);
by (auto_tac (claset(), simpset() 
        addsimps [image0_trancl_iff_image0_r]));
qed "above_lemma_b";