--- a/src/HOL/UNITY/Simple/Reachability.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy Wed Feb 05 13:35:32 2003 +0100
@@ -23,8 +23,8 @@
inductive "REACHABLE"
intros
- base: "v : V ==> ((v,v) : REACHABLE)"
- step: "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"
+ base: "v \<in> V ==> ((v,v) \<in> REACHABLE)"
+ step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)"
constdefs
reachable :: "vertex => state set"
@@ -37,65 +37,64 @@
"nmsg_gt k == %e. {s. k < nmsg s e}"
nmsg_gte :: "nat => edge => state set"
- "nmsg_gte k == %e. {s. k <= nmsg s e}"
+ "nmsg_gte k == %e. {s. k \<le> nmsg s e}"
nmsg_lte :: "nat => edge => state set"
- "nmsg_lte k == %e. {s. nmsg s e <= k}"
-
-
+ "nmsg_lte k == %e. {s. nmsg s e \<le> k}"
final :: "state set"
- "final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))"
+ "final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter>
+ (INTER E (nmsg_eq 0))"
axioms
- Graph1: "root : V"
+ Graph1: "root \<in> V"
- Graph2: "(v,w) : E ==> (v : V) & (w : V)"
+ Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)"
- MA1: "F : Always (reachable root)"
+ MA1: "F \<in> Always (reachable root)"
- MA2: "v: V ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"
+ MA2: "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})"
- MA3: "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"
+ MA3: "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))"
- MA4: "(v,w) : E ==>
- F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
+ MA4: "(v,w) \<in> E ==>
+ F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))"
- MA5: "[|v:V; w:V|]
- ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w))"
+ MA5: "[|v \<in> V; w \<in> V|]
+ ==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))"
- MA6: "[|v:V|] ==> F : Stable (reachable v)"
+ MA6: "[|v \<in> V|] ==> F \<in> Stable (reachable v)"
- MA6b: "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"
+ MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))"
- MA7: "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"
+ MA7: "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)"
lemmas E_imp_in_V_L = Graph2 [THEN conjunct1, standard]
lemmas E_imp_in_V_R = Graph2 [THEN conjunct2, standard]
lemma lemma2:
- "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v"
+ "(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v"
apply (rule MA7 [THEN PSP_Stable, THEN LeadsTo_weaken_L])
apply (rule_tac [3] MA6)
apply (auto simp add: E_imp_in_V_L E_imp_in_V_R)
done
-lemma Induction_base: "(v,w) : E ==> F : reachable v LeadsTo reachable w"
+lemma Induction_base: "(v,w) \<in> E ==> F \<in> reachable v LeadsTo reachable w"
apply (rule MA4 [THEN Always_LeadsTo_weaken])
apply (rule_tac [2] lemma2)
apply (auto simp add: nmsg_eq_def nmsg_gt_def)
done
lemma REACHABLE_LeadsTo_reachable:
- "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w"
+ "(v,w) \<in> REACHABLE ==> F \<in> reachable v LeadsTo reachable w"
apply (erule REACHABLE.induct)
apply (rule subset_imp_LeadsTo, blast)
apply (blast intro: LeadsTo_Trans Induction_base)
done
-lemma Detects_part1: "F : {s. (root,v) : REACHABLE} LeadsTo reachable v"
+lemma Detects_part1: "F \<in> {s. (root,v) \<in> REACHABLE} LeadsTo reachable v"
apply (rule single_LeadsTo_I)
apply (simp split add: split_if_asm)
apply (rule MA1 [THEN Always_LeadsToI])
@@ -104,7 +103,7 @@
lemma Reachability_Detected:
- "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}"
+ "v \<in> V ==> F \<in> (reachable v) Detects {s. (root,v) \<in> REACHABLE}"
apply (unfold Detects_def, auto)
prefer 2 apply (blast intro: MA2 [THEN Always_weaken])
apply (rule Detects_part1 [THEN LeadsTo_weaken_L], blast)
@@ -112,7 +111,7 @@
lemma LeadsTo_Reachability:
- "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})"
+ "v \<in> V ==> F \<in> UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE})"
by (erule Reachability_Detected [THEN Detects_Imp_LeadstoEQ])
@@ -121,17 +120,15 @@
(* Some lemmas about <==> *)
lemma Eq_lemma1:
- "(reachable v <==> {s. (root,v) : REACHABLE}) =
- {s. ((s : reachable v) = ((root,v) : REACHABLE))}"
-apply (unfold Equality_def, blast)
-done
+ "(reachable v <==> {s. (root,v) \<in> REACHABLE}) =
+ {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
+by (unfold Equality_def, blast)
lemma Eq_lemma2:
- "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) =
- {s. ((s : reachable v) = ((root,v) : REACHABLE))}"
-apply (unfold Equality_def, auto)
-done
+ "(reachable v <==> (if (root,v) \<in> REACHABLE then UNIV else {})) =
+ {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
+by (unfold Equality_def, auto)
(* ------------------------------------ *)
@@ -139,37 +136,37 @@
(* Some lemmas about final (I don't need all of them!) *)
lemma final_lemma1:
- "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) &
- s : nmsg_eq 0 (v,w)})
- <= final"
+ "(\<Inter>v \<in> V. \<Inter>w \<in> V. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE)) &
+ s \<in> nmsg_eq 0 (v,w)})
+ \<subseteq> final"
apply (unfold final_def Equality_def, auto)
apply (frule E_imp_in_V_R)
apply (frule E_imp_in_V_L, blast)
done
lemma final_lemma2:
- "E~={}
- ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))}
- Int nmsg_eq 0 e) <= final"
+ "E\<noteq>{}
+ ==> (\<Inter>v \<in> V. \<Inter>e \<in> E. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}
+ \<inter> nmsg_eq 0 e) \<subseteq> final"
apply (unfold final_def Equality_def)
apply (auto split add: split_if_asm)
apply (frule E_imp_in_V_L, blast)
done
lemma final_lemma3:
- "E~={}
- ==> (INT v: V. INT e: E.
- (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e)
- <= final"
+ "E\<noteq>{}
+ ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.
+ (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)
+ \<subseteq> final"
apply (frule final_lemma2)
apply (simp (no_asm_use) add: Eq_lemma2)
done
lemma final_lemma4:
- "E~={}
- ==> (INT v: V. INT e: E.
- {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e)
+ "E\<noteq>{}
+ ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.
+ {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))} \<inter> nmsg_eq 0 e)
= final"
apply (rule subset_antisym)
apply (erule final_lemma2)
@@ -177,9 +174,9 @@
done
lemma final_lemma5:
- "E~={}
- ==> (INT v: V. INT e: E.
- ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e)
+ "E\<noteq>{}
+ ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.
+ ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)
= final"
apply (frule final_lemma4)
apply (simp (no_asm_use) add: Eq_lemma2)
@@ -187,9 +184,9 @@
lemma final_lemma6:
- "(INT v: V. INT w: V.
- (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w))
- <= final"
+ "(\<Inter>v \<in> V. \<Inter>w \<in> V.
+ (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 (v,w))
+ \<subseteq> final"
apply (simp (no_asm) add: Eq_lemma2 Int_def)
apply (rule final_lemma1)
done
@@ -197,9 +194,9 @@
lemma final_lemma7:
"final =
- (INT v: V. INT w: V.
- ((reachable v) <==> {s. (root,v) : REACHABLE}) Int
- (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))"
+ (\<Inter>v \<in> V. \<Inter>w \<in> V.
+ ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter>
+ (-{s. (v,w) \<in> E} \<union> (nmsg_eq 0 (v,w))))"
apply (unfold final_def)
apply (rule subset_antisym, blast)
apply (auto split add: split_if_asm)
@@ -213,56 +210,55 @@
(* Stability theorems *)
lemma not_REACHABLE_imp_Stable_not_reachable:
- "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)"
+ "[| v \<in> V; (root,v) \<notin> REACHABLE |] ==> F \<in> Stable (- reachable v)"
apply (drule MA2 [THEN AlwaysD], auto)
done
lemma Stable_reachable_EQ_R:
- "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})"
+ "v \<in> V ==> F \<in> Stable (reachable v <==> {s. (root,v) \<in> REACHABLE})"
apply (simp (no_asm) add: Equality_def Eq_lemma2)
apply (blast intro: MA6 not_REACHABLE_imp_Stable_not_reachable)
done
lemma lemma4:
- "((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int
- (- nmsg_gt 0 (v,w) Un A))
- <= A Un nmsg_eq 0 (v,w)"
+ "((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter>
+ (- nmsg_gt 0 (v,w) \<union> A))
+ \<subseteq> A \<union> nmsg_eq 0 (v,w)"
apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
done
lemma lemma5:
- "reachable v Int nmsg_eq 0 (v,w) =
- ((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int
- (reachable v Int nmsg_lte 0 (v,w)))"
-apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
-done
+ "reachable v \<inter> nmsg_eq 0 (v,w) =
+ ((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter>
+ (reachable v \<inter> nmsg_lte 0 (v,w)))"
+by (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
lemma lemma6:
- "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v"
+ "- nmsg_gt 0 (v,w) \<union> reachable v \<subseteq> nmsg_eq 0 (v,w) \<union> reachable v"
apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
done
lemma Always_reachable_OR_nmsg_0:
- "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))"
+ "[|v \<in> V; w \<in> V|] ==> F \<in> Always (reachable v \<union> nmsg_eq 0 (v,w))"
apply (rule Always_Int_I [OF MA5 MA3, THEN Always_weaken])
apply (rule_tac [5] lemma4, auto)
done
lemma Stable_reachable_AND_nmsg_0:
- "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))"
+ "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (reachable v \<inter> nmsg_eq 0 (v,w))"
apply (subst lemma5)
apply (blast intro: MA5 Always_imp_Stable [THEN Stable_Int] MA6b)
done
lemma Stable_nmsg_0_OR_reachable:
- "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)"
+ "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (nmsg_eq 0 (v,w) \<union> reachable v)"
by (blast intro!: Always_weaken [THEN Always_imp_Stable] lemma6 MA3)
lemma not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0:
- "[| v : V; w:V; (root,v) ~: REACHABLE |]
- ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))"
+ "[| v \<in> V; w \<in> V; (root,v) \<notin> REACHABLE |]
+ ==> F \<in> Stable (- reachable v \<inter> nmsg_eq 0 (v,w))"
apply (rule Stable_Int [OF MA2 [THEN Always_imp_Stable]
Stable_nmsg_0_OR_reachable,
THEN Stable_eq])
@@ -271,8 +267,8 @@
done
lemma Stable_reachable_EQ_R_AND_nmsg_0:
- "[| v : V; w:V |]
- ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int
+ "[| v \<in> V; w \<in> V |]
+ ==> F \<in> Stable ((reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter>
nmsg_eq 0 (v,w))"
by (simp add: Equality_def Eq_lemma2 Stable_reachable_AND_nmsg_0
not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0)
@@ -284,13 +280,13 @@
(* LeadsTo final predicate (Exercise 11.2 page 274) *)
-lemma UNIV_lemma: "UNIV <= (INT v: V. UNIV)"
+lemma UNIV_lemma: "UNIV \<subseteq> (\<Inter>v \<in> V. UNIV)"
by blast
lemmas UNIV_LeadsTo_completion =
LeadsTo_weaken_L [OF Finite_stable_completion UNIV_lemma]
-lemma LeadsTo_final_E_empty: "E={} ==> F : UNIV LeadsTo final"
+lemma LeadsTo_final_E_empty: "E={} ==> F \<in> UNIV LeadsTo final"
apply (unfold final_def, simp)
apply (rule UNIV_LeadsTo_completion)
apply safe
@@ -300,13 +296,13 @@
lemma Leadsto_reachability_AND_nmsg_0:
- "[| v : V; w:V |]
- ==> F : UNIV LeadsTo
- ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))"
+ "[| v \<in> V; w \<in> V |]
+ ==> F \<in> UNIV LeadsTo
+ ((reachable v <==> {s. (root,v): REACHABLE}) \<inter> nmsg_eq 0 (v,w))"
apply (rule LeadsTo_Reachability [THEN LeadsTo_Trans], blast)
apply (subgoal_tac
- "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int
- UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int
+ "F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter>
+ UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter>
nmsg_eq 0 (v,w) ")
apply simp
apply (rule PSP_Stable2)
@@ -314,7 +310,7 @@
apply (rule_tac [3] Stable_reachable_EQ_R, auto)
done
-lemma LeadsTo_final_E_NOT_empty: "E~={} ==> F : UNIV LeadsTo final"
+lemma LeadsTo_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> UNIV LeadsTo final"
apply (rule LeadsTo_weaken_L [OF LeadsTo_weaken_R UNIV_lemma])
apply (rule_tac [2] final_lemma6)
apply (rule Finite_stable_completion)
@@ -324,9 +320,9 @@
Leadsto_reachability_AND_nmsg_0)+
done
-lemma LeadsTo_final: "F : UNIV LeadsTo final"
+lemma LeadsTo_final: "F \<in> UNIV LeadsTo final"
apply (case_tac "E={}")
-apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
+ apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
apply (rule LeadsTo_final_E_empty, auto)
done
@@ -334,21 +330,23 @@
(* Stability of final (Exercise 11.2 page 274) *)
-lemma Stable_final_E_empty: "E={} ==> F : Stable final"
+lemma Stable_final_E_empty: "E={} ==> F \<in> Stable final"
apply (unfold final_def, simp)
apply (rule Stable_INT)
apply (drule Stable_reachable_EQ_R, simp)
done
-lemma Stable_final_E_NOT_empty: "E~={} ==> F : Stable final"
+lemma Stable_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> Stable final"
apply (subst final_lemma7)
apply (rule Stable_INT)
apply (rule Stable_INT)
apply (simp (no_asm) add: Eq_lemma2)
apply safe
apply (rule Stable_eq)
-apply (subgoal_tac [2] "({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))) ")
+apply (subgoal_tac [2]
+ "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) =
+ ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))")
prefer 2 apply blast
prefer 2 apply blast
apply (rule Stable_reachable_EQ_R_AND_nmsg_0
@@ -358,15 +356,15 @@
apply (rule Stable_reachable_EQ_R [simplified Eq_lemma2 Collect_const])
apply simp
apply (subgoal_tac
- "({s. (s : reachable v) = ((root,v) : REACHABLE) }) =
- ({s. (s : reachable v) = ( (root,v) : REACHABLE) } Int
- (- {} Un nmsg_eq 0 (v,w)))")
+ "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) }) =
+ ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } Int
+ (- {} \<union> nmsg_eq 0 (v,w)))")
apply blast+
done
-lemma Stable_final: "F : Stable final"
+lemma Stable_final: "F \<in> Stable final"
apply (case_tac "E={}")
-prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
+ prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
apply (blast intro: Stable_final_E_empty)
done