src/HOL/UNITY/Reachability.ML

exhaust_tac -> cases_tac

(*  Title:      HOL/UNITY/Reachability
    ID:         $Id$
    Author:     Tanja Vos, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge

Reachability in Graphs

From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
*)

bind_thm("E_imp_in_V_L", Graph2 RS conjunct1);
bind_thm("E_imp_in_V_R", Graph2 RS conjunct2);

Goal "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v";
by (rtac (MA7 RS PSP_Stable RS LeadsTo_weaken_L) 1);
by (rtac MA6 3);
by (auto_tac (claset(), simpset() addsimps [E_imp_in_V_L, E_imp_in_V_R]));
qed "lemma2";

Goal "(v,w) : E ==> F : reachable v LeadsTo reachable w";
by (rtac (MA4 RS Always_LeadsTo_weaken) 1);
by (rtac lemma2 2);
by (auto_tac (claset(), simpset() addsimps [nmsg_eq_def, nmsg_gt_def]));
qed "Induction_base";

Goal "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w";
by (etac REACHABLE.induct 1);
by (rtac subset_imp_LeadsTo 1);
by (Blast_tac 1);
by (blast_tac (claset() addIs [LeadsTo_Trans, Induction_base]) 1);
qed "REACHABLE_LeadsTo_reachable";

Goal "F : {s. (root,v) : REACHABLE} LeadsTo reachable v";
by (rtac single_LeadsTo_I 1);
by (full_simp_tac (simpset() addsplits [split_if_asm]) 1);
by (rtac (MA1 RS Always_LeadsToI) 1);
by (etac (REACHABLE_LeadsTo_reachable RS LeadsTo_weaken_L) 1);
by Auto_tac;
qed "Detects_part1";


Goalw [Detects_def]
     "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}";
by Auto_tac;
by (blast_tac (claset() addIs [MA2 RS Always_weaken]) 2);
by (rtac (Detects_part1 RS LeadsTo_weaken_L) 1);
by (Blast_tac 1);
qed "Reachability_Detected";


Goal "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})";
by (etac (Reachability_Detected RS Detects_Imp_LeadstoEQ) 1);
qed "LeadsTo_Reachability";

(* ------------------------------------ *)

(* Some lemmas about <==> *)

Goalw [Equality_def]
     "(reachable v <==> {s. (root,v) : REACHABLE}) = \
\     {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
by (Blast_tac 1);
qed "Eq_lemma1";


Goalw [Equality_def]
     "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) = \
\     {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
by Auto_tac;
qed "Eq_lemma2";

(* ------------------------------------ *)


(* Some lemmas about final (I don't need all of them!)  *)

Goalw [final_def, Equality_def]
     "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) & \
\                             s : nmsg_eq 0 (v,w)}) \
\     <= final";
by Auto_tac;
by (ftac E_imp_in_V_R 1);
by (ftac E_imp_in_V_L 1);
by (Blast_tac 1);
qed "final_lemma1";

Goalw [final_def, Equality_def] 
 "E~={} \
\ ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))} \
\                          Int nmsg_eq 0 e)    <=  final";
by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
by (ftac E_imp_in_V_L 1);
by (Blast_tac 1);
qed "final_lemma2";

Goal "E~={} \
\     ==> (INT v: V. INT e: E. \
\          (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
\         <= final";
by (ftac final_lemma2 1);
by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
qed "final_lemma3";


Goal "E~={} \
\     ==> (INT v: V. INT e: E. \
\          {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e) \
\         = final";
by (rtac subset_antisym 1);
by (etac final_lemma2 1);
by (rewrite_goals_tac [final_def,Equality_def]);
by (Blast_tac 1); 
qed "final_lemma4";

Goal "E~={} \
\     ==> (INT v: V. INT e: E. \
\          ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
\         = final";
by (ftac final_lemma4 1);
by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
qed "final_lemma5";


Goal "(INT v: V. INT w: V. \
\      (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)) \
\     <= final";
by (simp_tac (simpset() addsimps [Eq_lemma2, Int_def]) 1);
by (rtac final_lemma1 1);
qed "final_lemma6";


Goalw [final_def] 
     "final = \
\     (INT v: V. INT w: V. \
\      ((reachable v) <==> {s. (root,v) : REACHABLE}) Int \
\      (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))";
by (rtac subset_antisym 1);
by (Blast_tac 1);
by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
by (ftac E_imp_in_V_R 1);
by (ftac E_imp_in_V_L 1);
by (Blast_tac 1);
qed "final_lemma7"; 

(* ------------------------------------ *)


(* ------------------------------------ *)

(* Stability theorems *)


Goal "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)";
by (dtac (MA2 RS AlwaysD) 1);
by Auto_tac;
qed "not_REACHABLE_imp_Stable_not_reachable";

Goal "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})";
by (simp_tac (simpset() addsimps [Equality_def, Eq_lemma2]) 1);
by (blast_tac (claset() addIs [MA6,not_REACHABLE_imp_Stable_not_reachable]) 1);
qed "Stable_reachable_EQ_R";


Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
     "((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
\     <= A Un nmsg_eq 0 (v,w)";
by Auto_tac;
qed "lemma4";


Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
     "reachable v Int nmsg_eq 0 (v,w) = \
\     ((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int \
\      (reachable v Int nmsg_lte 0 (v,w)))";
by Auto_tac;
qed "lemma5";

Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
     "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v";
by Auto_tac;
qed "lemma6";

Goal "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))";
by (rtac ([MA5, MA3] MRS Always_Int_I RS Always_weaken) 1);
by (rtac lemma4 5); 
by Auto_tac;
qed "Always_reachable_OR_nmsg_0";

Goal "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))";
by (stac lemma5 1);
by (blast_tac (claset() addIs [MA5, Always_imp_Stable RS Stable_Int, MA6b]) 1);
qed "Stable_reachable_AND_nmsg_0";

Goal "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)";
by (blast_tac (claset() addSIs [Always_weaken RS Always_imp_Stable,
			       lemma6, MA3]) 1);
qed "Stable_nmsg_0_OR_reachable";

Goal "[| v : V; w:V; (root,v) ~: REACHABLE |] \
\     ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))";
by (rtac ([MA2 RS Always_imp_Stable, Stable_nmsg_0_OR_reachable] MRS 
	  Stable_Int RS Stable_eq) 1);
by (Blast_tac 4);
by Auto_tac;
qed "not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0";

Goal "[| v : V; w:V |] \
\     ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int \
\                     nmsg_eq 0 (v,w))";
by (asm_simp_tac
    (simpset() addsimps [Equality_def, Eq_lemma2,
			 not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0,
			 Stable_reachable_AND_nmsg_0]) 1);
qed "Stable_reachable_EQ_R_AND_nmsg_0";


(* ------------------------------------ *)


(* LeadsTo final predicate (Exercise 11.2 page 274) *)

Goal "UNIV <= (INT v: V. UNIV)";
by (Blast_tac 1);
val UNIV_lemma = result();

val UNIV_LeadsTo_completion = 
    [Finite_stable_completion, UNIV_lemma] MRS LeadsTo_weaken_L;

Goalw [final_def] "E={} ==> F : UNIV LeadsTo final";
by (Asm_full_simp_tac 1);
by (rtac UNIV_LeadsTo_completion 1);
by Safe_tac;
by (etac (simplify (simpset()) LeadsTo_Reachability) 1);
by (dtac Stable_reachable_EQ_R 1);
by (Asm_full_simp_tac 1);
qed "LeadsTo_final_E_empty";


Goal "[| v : V; w:V |] \
\  ==> F : UNIV LeadsTo \
\          ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))";
by (rtac (LeadsTo_Reachability RS LeadsTo_Trans) 1);
by (Blast_tac 1);
by (subgoal_tac "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)" 1);
by (Asm_full_simp_tac 1);
by (rtac PSP_Stable2 1);
by (rtac MA7 1); 
by (rtac Stable_reachable_EQ_R 3);
by Auto_tac;
qed "Leadsto_reachability_AND_nmsg_0";


Goal "E~={} ==> F : UNIV LeadsTo final";
by (rtac ([LeadsTo_weaken_R, UNIV_lemma] MRS LeadsTo_weaken_L) 1);
by (rtac final_lemma6 2);
by (rtac Finite_stable_completion 1);
by (Blast_tac 1); 
by (rtac UNIV_LeadsTo_completion 1);
by (REPEAT
    (blast_tac (claset() addIs [Stable_INT,
				Stable_reachable_EQ_R_AND_nmsg_0,
				Leadsto_reachability_AND_nmsg_0]) 1));
qed "LeadsTo_final_E_NOT_empty";


Goal "F : UNIV LeadsTo final";
by (case_tac "E={}" 1);
by (rtac LeadsTo_final_E_NOT_empty 2);
by (rtac LeadsTo_final_E_empty 1);
by Auto_tac;
qed "LeadsTo_final";

(* ------------------------------------ *)

(* Stability of final (Exercise 11.2 page 274) *)

Goalw [final_def] "E={} ==> F : Stable final";
by (Asm_full_simp_tac 1);
by (rtac Stable_INT 1); 
by (dtac Stable_reachable_EQ_R 1);
by (Asm_full_simp_tac 1);
qed "Stable_final_E_empty";


Goal "E~={} ==> F : Stable final";
by (stac final_lemma7 1); 
by (rtac Stable_INT 1); 
by (rtac Stable_INT 1); 
by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
by Safe_tac;
by (rtac Stable_eq 1);
by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)} Int nmsg_eq 0 (v,w)) = \
\                ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- UNIV Un nmsg_eq 0 (v,w)))" 2);
by (Blast_tac 2); by (Blast_tac 2);
by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R_AND_nmsg_0) 1);
by (Blast_tac 1);by (Blast_tac 1);
by (rtac Stable_eq 1);
by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)}) = ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- {} Un nmsg_eq 0 (v,w)))" 2);
by (Blast_tac 2); by (Blast_tac 2);
by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R) 1);
by Auto_tac;
qed "Stable_final_E_NOT_empty";

Goal "F : Stable final";
by (case_tac "E={}" 1);
by (blast_tac (claset() addIs [Stable_final_E_NOT_empty]) 2);
by (blast_tac (claset() addIs [Stable_final_E_empty]) 1);
qed "Stable_final";