author | haftmann |
Tue, 20 Jul 2010 06:35:29 +0200 | |
changeset 37891 | c26f9d06e82c |
parent 35416 | d8d7d1b785af |
child 37936 | 1e4c5015a72e |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26826
diff
changeset
|
1 |
(* Title: HOL/UNITY/Reachability.thy |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Tanja Vos, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 2000 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26826
diff
changeset
|
5 |
Reachability in Graphs. |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26826
diff
changeset
|
7 |
From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26826
diff
changeset
|
8 |
and 11.3. |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
|
26826 | 11 |
theory Reachability imports "../Detects" Reach begin |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
types edge = "(vertex*vertex)" |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
record state = |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
16 |
reach :: "vertex => bool" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
17 |
nmsg :: "edge => nat" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
|
23767 | 19 |
consts root :: "vertex" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
20 |
E :: "edge set" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
21 |
V :: "vertex set" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
|
23767 | 23 |
inductive_set REACHABLE :: "edge set" |
24 |
where |
|
25 |
base: "v \<in> V ==> ((v,v) \<in> REACHABLE)" |
|
26 |
| step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)" |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
28 |
definition reachable :: "vertex => state set" where |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
"reachable p == {s. reach s p}" |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
31 |
definition nmsg_eq :: "nat => edge => state set" where |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
"nmsg_eq k == %e. {s. nmsg s e = k}" |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
34 |
definition nmsg_gt :: "nat => edge => state set" where |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
"nmsg_gt k == %e. {s. k < nmsg s e}" |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
37 |
definition nmsg_gte :: "nat => edge => state set" where |
13806 | 38 |
"nmsg_gte k == %e. {s. k \<le> nmsg s e}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
40 |
definition nmsg_lte :: "nat => edge => state set" where |
13806 | 41 |
"nmsg_lte k == %e. {s. nmsg s e \<le> k}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
42 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
43 |
definition final :: "state set" where |
13806 | 44 |
"final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter> |
45 |
(INTER E (nmsg_eq 0))" |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
46 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
47 |
axioms |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
48 |
|
13806 | 49 |
Graph1: "root \<in> V" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
50 |
|
13806 | 51 |
Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
52 |
|
13806 | 53 |
MA1: "F \<in> Always (reachable root)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
54 |
|
13806 | 55 |
MA2: "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
56 |
|
13806 | 57 |
MA3: "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
58 |
|
13806 | 59 |
MA4: "(v,w) \<in> E ==> |
60 |
F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
61 |
|
13806 | 62 |
MA5: "[|v \<in> V; w \<in> V|] |
63 |
==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
64 |
|
13806 | 65 |
MA6: "[|v \<in> V|] ==> F \<in> Stable (reachable v)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
66 |
|
13806 | 67 |
MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
68 |
|
13806 | 69 |
MA7: "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
70 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
71 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
72 |
lemmas E_imp_in_V_L = Graph2 [THEN conjunct1, standard] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
73 |
lemmas E_imp_in_V_R = Graph2 [THEN conjunct2, standard] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
74 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
75 |
lemma lemma2: |
13806 | 76 |
"(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
77 |
apply (rule MA7 [THEN PSP_Stable, THEN LeadsTo_weaken_L]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
78 |
apply (rule_tac [3] MA6) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
79 |
apply (auto simp add: E_imp_in_V_L E_imp_in_V_R) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
80 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
81 |
|
13806 | 82 |
lemma Induction_base: "(v,w) \<in> E ==> F \<in> reachable v LeadsTo reachable w" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
83 |
apply (rule MA4 [THEN Always_LeadsTo_weaken]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
84 |
apply (rule_tac [2] lemma2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
85 |
apply (auto simp add: nmsg_eq_def nmsg_gt_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
86 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
87 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
88 |
lemma REACHABLE_LeadsTo_reachable: |
13806 | 89 |
"(v,w) \<in> REACHABLE ==> F \<in> reachable v LeadsTo reachable w" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
90 |
apply (erule REACHABLE.induct) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
91 |
apply (rule subset_imp_LeadsTo, blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
92 |
apply (blast intro: LeadsTo_Trans Induction_base) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
93 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
94 |
|
13806 | 95 |
lemma Detects_part1: "F \<in> {s. (root,v) \<in> REACHABLE} LeadsTo reachable v" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
96 |
apply (rule single_LeadsTo_I) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
97 |
apply (simp split add: split_if_asm) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
98 |
apply (rule MA1 [THEN Always_LeadsToI]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
99 |
apply (erule REACHABLE_LeadsTo_reachable [THEN LeadsTo_weaken_L], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
100 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
101 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
102 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
103 |
lemma Reachability_Detected: |
13806 | 104 |
"v \<in> V ==> F \<in> (reachable v) Detects {s. (root,v) \<in> REACHABLE}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
105 |
apply (unfold Detects_def, auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
106 |
prefer 2 apply (blast intro: MA2 [THEN Always_weaken]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
107 |
apply (rule Detects_part1 [THEN LeadsTo_weaken_L], blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
108 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
109 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
110 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
111 |
lemma LeadsTo_Reachability: |
13806 | 112 |
"v \<in> V ==> F \<in> UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE})" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
113 |
by (erule Reachability_Detected [THEN Detects_Imp_LeadstoEQ]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
114 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
115 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
116 |
(* ------------------------------------ *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
117 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
118 |
(* Some lemmas about <==> *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
119 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
120 |
lemma Eq_lemma1: |
13806 | 121 |
"(reachable v <==> {s. (root,v) \<in> REACHABLE}) = |
122 |
{s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}" |
|
123 |
by (unfold Equality_def, blast) |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
124 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
125 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
126 |
lemma Eq_lemma2: |
13806 | 127 |
"(reachable v <==> (if (root,v) \<in> REACHABLE then UNIV else {})) = |
128 |
{s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}" |
|
129 |
by (unfold Equality_def, auto) |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
130 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
131 |
(* ------------------------------------ *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
132 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
133 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
134 |
(* Some lemmas about final (I don't need all of them!) *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
135 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
136 |
lemma final_lemma1: |
13806 | 137 |
"(\<Inter>v \<in> V. \<Inter>w \<in> V. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE)) & |
138 |
s \<in> nmsg_eq 0 (v,w)}) |
|
139 |
\<subseteq> final" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
140 |
apply (unfold final_def Equality_def, auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
141 |
apply (frule E_imp_in_V_R) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
142 |
apply (frule E_imp_in_V_L, blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
143 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
144 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
145 |
lemma final_lemma2: |
13806 | 146 |
"E\<noteq>{} |
147 |
==> (\<Inter>v \<in> V. \<Inter>e \<in> E. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))} |
|
148 |
\<inter> nmsg_eq 0 e) \<subseteq> final" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
149 |
apply (unfold final_def Equality_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
150 |
apply (auto split add: split_if_asm) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
151 |
apply (frule E_imp_in_V_L, blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
152 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
153 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
154 |
lemma final_lemma3: |
13806 | 155 |
"E\<noteq>{} |
156 |
==> (\<Inter>v \<in> V. \<Inter>e \<in> E. |
|
157 |
(reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e) |
|
158 |
\<subseteq> final" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
159 |
apply (frule final_lemma2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
160 |
apply (simp (no_asm_use) add: Eq_lemma2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
161 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
162 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
163 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
164 |
lemma final_lemma4: |
13806 | 165 |
"E\<noteq>{} |
166 |
==> (\<Inter>v \<in> V. \<Inter>e \<in> E. |
|
167 |
{s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))} \<inter> nmsg_eq 0 e) |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
168 |
= final" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
169 |
apply (rule subset_antisym) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
170 |
apply (erule final_lemma2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
171 |
apply (unfold final_def Equality_def, blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
172 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
173 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
174 |
lemma final_lemma5: |
13806 | 175 |
"E\<noteq>{} |
176 |
==> (\<Inter>v \<in> V. \<Inter>e \<in> E. |
|
177 |
((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e) |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
178 |
= final" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
179 |
apply (frule final_lemma4) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
180 |
apply (simp (no_asm_use) add: Eq_lemma2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
181 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
182 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
183 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
184 |
lemma final_lemma6: |
13806 | 185 |
"(\<Inter>v \<in> V. \<Inter>w \<in> V. |
186 |
(reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 (v,w)) |
|
187 |
\<subseteq> final" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
188 |
apply (simp (no_asm) add: Eq_lemma2 Int_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
189 |
apply (rule final_lemma1) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
190 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
191 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
192 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
193 |
lemma final_lemma7: |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
194 |
"final = |
13806 | 195 |
(\<Inter>v \<in> V. \<Inter>w \<in> V. |
196 |
((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> |
|
197 |
(-{s. (v,w) \<in> E} \<union> (nmsg_eq 0 (v,w))))" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
198 |
apply (unfold final_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
199 |
apply (rule subset_antisym, blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
200 |
apply (auto split add: split_if_asm) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
201 |
apply (blast dest: E_imp_in_V_L E_imp_in_V_R)+ |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
202 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
203 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
204 |
(* ------------------------------------ *) |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
205 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
206 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
207 |
(* ------------------------------------ *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
208 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
209 |
(* Stability theorems *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
210 |
lemma not_REACHABLE_imp_Stable_not_reachable: |
13806 | 211 |
"[| v \<in> V; (root,v) \<notin> REACHABLE |] ==> F \<in> Stable (- reachable v)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
212 |
apply (drule MA2 [THEN AlwaysD], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
213 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
214 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
215 |
lemma Stable_reachable_EQ_R: |
13806 | 216 |
"v \<in> V ==> F \<in> Stable (reachable v <==> {s. (root,v) \<in> REACHABLE})" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
217 |
apply (simp (no_asm) add: Equality_def Eq_lemma2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
218 |
apply (blast intro: MA6 not_REACHABLE_imp_Stable_not_reachable) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
219 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
220 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
221 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
222 |
lemma lemma4: |
13806 | 223 |
"((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter> |
224 |
(- nmsg_gt 0 (v,w) \<union> A)) |
|
225 |
\<subseteq> A \<union> nmsg_eq 0 (v,w)" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
226 |
apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
227 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
228 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
229 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
230 |
lemma lemma5: |
13806 | 231 |
"reachable v \<inter> nmsg_eq 0 (v,w) = |
232 |
((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter> |
|
233 |
(reachable v \<inter> nmsg_lte 0 (v,w)))" |
|
234 |
by (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto) |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
235 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
236 |
lemma lemma6: |
13806 | 237 |
"- nmsg_gt 0 (v,w) \<union> reachable v \<subseteq> nmsg_eq 0 (v,w) \<union> reachable v" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
238 |
apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
239 |
done |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
240 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
241 |
lemma Always_reachable_OR_nmsg_0: |
13806 | 242 |
"[|v \<in> V; w \<in> V|] ==> F \<in> Always (reachable v \<union> nmsg_eq 0 (v,w))" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
243 |
apply (rule Always_Int_I [OF MA5 MA3, THEN Always_weaken]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
244 |
apply (rule_tac [5] lemma4, auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
245 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
246 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
247 |
lemma Stable_reachable_AND_nmsg_0: |
13806 | 248 |
"[|v \<in> V; w \<in> V|] ==> F \<in> Stable (reachable v \<inter> nmsg_eq 0 (v,w))" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
249 |
apply (subst lemma5) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
250 |
apply (blast intro: MA5 Always_imp_Stable [THEN Stable_Int] MA6b) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
251 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
252 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
253 |
lemma Stable_nmsg_0_OR_reachable: |
13806 | 254 |
"[|v \<in> V; w \<in> V|] ==> F \<in> Stable (nmsg_eq 0 (v,w) \<union> reachable v)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
255 |
by (blast intro!: Always_weaken [THEN Always_imp_Stable] lemma6 MA3) |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
256 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
257 |
lemma not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0: |
13806 | 258 |
"[| v \<in> V; w \<in> V; (root,v) \<notin> REACHABLE |] |
259 |
==> F \<in> Stable (- reachable v \<inter> nmsg_eq 0 (v,w))" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
260 |
apply (rule Stable_Int [OF MA2 [THEN Always_imp_Stable] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
261 |
Stable_nmsg_0_OR_reachable, |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
262 |
THEN Stable_eq]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
263 |
prefer 4 apply blast |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
264 |
apply auto |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
265 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
266 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
267 |
lemma Stable_reachable_EQ_R_AND_nmsg_0: |
13806 | 268 |
"[| v \<in> V; w \<in> V |] |
269 |
==> F \<in> Stable ((reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
270 |
nmsg_eq 0 (v,w))" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
271 |
by (simp add: Equality_def Eq_lemma2 Stable_reachable_AND_nmsg_0 |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
272 |
not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
273 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
274 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
275 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
276 |
(* ------------------------------------ *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
277 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
278 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
279 |
(* LeadsTo final predicate (Exercise 11.2 page 274) *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
280 |
|
13806 | 281 |
lemma UNIV_lemma: "UNIV \<subseteq> (\<Inter>v \<in> V. UNIV)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
282 |
by blast |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
283 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
284 |
lemmas UNIV_LeadsTo_completion = |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
285 |
LeadsTo_weaken_L [OF Finite_stable_completion UNIV_lemma] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
286 |
|
13806 | 287 |
lemma LeadsTo_final_E_empty: "E={} ==> F \<in> UNIV LeadsTo final" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
288 |
apply (unfold final_def, simp) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
289 |
apply (rule UNIV_LeadsTo_completion) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
290 |
apply safe |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
291 |
apply (erule LeadsTo_Reachability [simplified]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
292 |
apply (drule Stable_reachable_EQ_R, simp) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
293 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
294 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
295 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
296 |
lemma Leadsto_reachability_AND_nmsg_0: |
13806 | 297 |
"[| v \<in> V; w \<in> V |] |
298 |
==> F \<in> UNIV LeadsTo |
|
299 |
((reachable v <==> {s. (root,v): REACHABLE}) \<inter> nmsg_eq 0 (v,w))" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
300 |
apply (rule LeadsTo_Reachability [THEN LeadsTo_Trans], blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
301 |
apply (subgoal_tac |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26826
diff
changeset
|
302 |
"F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> |
13806 | 303 |
UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
304 |
nmsg_eq 0 (v,w) ") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
305 |
apply simp |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
306 |
apply (rule PSP_Stable2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
307 |
apply (rule MA7) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
308 |
apply (rule_tac [3] Stable_reachable_EQ_R, auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
309 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
310 |
|
13806 | 311 |
lemma LeadsTo_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> UNIV LeadsTo final" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
312 |
apply (rule LeadsTo_weaken_L [OF LeadsTo_weaken_R UNIV_lemma]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
313 |
apply (rule_tac [2] final_lemma6) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
314 |
apply (rule Finite_stable_completion) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
315 |
apply blast |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
316 |
apply (rule UNIV_LeadsTo_completion) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
317 |
apply (blast intro: Stable_INT Stable_reachable_EQ_R_AND_nmsg_0 |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
318 |
Leadsto_reachability_AND_nmsg_0)+ |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
319 |
done |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
320 |
|
13806 | 321 |
lemma LeadsTo_final: "F \<in> UNIV LeadsTo final" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
322 |
apply (case_tac "E={}") |
13806 | 323 |
apply (rule_tac [2] LeadsTo_final_E_NOT_empty) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
324 |
apply (rule LeadsTo_final_E_empty, auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
325 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
326 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
327 |
(* ------------------------------------ *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
328 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
329 |
(* Stability of final (Exercise 11.2 page 274) *) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
330 |
|
13806 | 331 |
lemma Stable_final_E_empty: "E={} ==> F \<in> Stable final" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
332 |
apply (unfold final_def, simp) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
333 |
apply (rule Stable_INT) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
334 |
apply (drule Stable_reachable_EQ_R, simp) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
335 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
336 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
337 |
|
13806 | 338 |
lemma Stable_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> Stable final" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
339 |
apply (subst final_lemma7) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
340 |
apply (rule Stable_INT) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
341 |
apply (rule Stable_INT) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
342 |
apply (simp (no_asm) add: Eq_lemma2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
343 |
apply safe |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
344 |
apply (rule Stable_eq) |
13806 | 345 |
apply (subgoal_tac [2] |
346 |
"({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) = |
|
347 |
({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))") |
|
26826 | 348 |
prefer 2 apply simp |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
349 |
prefer 2 apply blast |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
350 |
apply (rule Stable_reachable_EQ_R_AND_nmsg_0 |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
351 |
[simplified Eq_lemma2 Collect_const]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
352 |
apply (blast, blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
353 |
apply (rule Stable_eq) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
354 |
apply (rule Stable_reachable_EQ_R [simplified Eq_lemma2 Collect_const]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
355 |
apply simp |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
356 |
apply (subgoal_tac |
13806 | 357 |
"({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) }) = |
358 |
({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } Int |
|
359 |
(- {} \<union> nmsg_eq 0 (v,w)))") |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
360 |
apply blast+ |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
361 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
362 |
|
13806 | 363 |
lemma Stable_final: "F \<in> Stable final" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
364 |
apply (case_tac "E={}") |
13806 | 365 |
prefer 2 apply (blast intro: Stable_final_E_NOT_empty) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
366 |
apply (blast intro: Stable_final_E_empty) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11701
diff
changeset
|
367 |
done |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
368 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
369 |
end |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
370 |