equal
deleted
inserted
replaced
27 by (force_tac (claset() addEs [reachable.induct] |
27 by (force_tac (claset() addEs [reachable.induct] |
28 addIs reachable.intrs, simpset()) 1); |
28 addIs reachable.intrs, simpset()) 1); |
29 qed "reachable_SKIP"; |
29 qed "reachable_SKIP"; |
30 |
30 |
31 Addsimps [reachable_SKIP]; |
31 Addsimps [reachable_SKIP]; |
|
32 |
|
33 (** SKIP and safety properties **) |
|
34 |
|
35 Goalw [constrains_def] "(SKIP : A co B) = (A<=B)"; |
|
36 by Auto_tac; |
|
37 qed "SKIP_in_constrains_iff"; |
|
38 AddIffs [SKIP_in_constrains_iff]; |
|
39 |
|
40 Goalw [Constrains_def] "(SKIP : A Co B) = (A<=B)"; |
|
41 by Auto_tac; |
|
42 qed "SKIP_in_Constrains_iff"; |
|
43 AddIffs [SKIP_in_Constrains_iff]; |
|
44 |
|
45 Goalw [stable_def] "SKIP : stable A"; |
|
46 by Auto_tac; |
|
47 qed "SKIP_in_stable"; |
|
48 AddIffs [SKIP_in_stable, SKIP_in_stable RS stable_imp_Stable]; |
32 |
49 |
33 |
50 |
34 (** Join **) |
51 (** Join **) |
35 |
52 |
36 Goal "Init (F Join G) = Init F Int Init G"; |
53 Goal "Init (F Join G) = Init F Int Init G"; |
118 Goal "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))"; |
135 Goal "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))"; |
119 by (auto_tac (claset() addSIs [program_equalityI], |
136 by (auto_tac (claset() addSIs [program_equalityI], |
120 simpset() addsimps [Acts_JN, Acts_Join])); |
137 simpset() addsimps [Acts_JN, Acts_Join])); |
121 qed "JN_Un"; |
138 qed "JN_Un"; |
122 |
139 |
123 Goal "i: I ==> (JN i:I. c) = c"; |
140 Goal "(JN i:I. c) = (if I={} then SKIP else c)"; |
124 by (auto_tac (claset() addSIs [program_equalityI], |
141 by (auto_tac (claset() addSIs [program_equalityI], |
125 simpset() addsimps [Acts_JN])); |
142 simpset() addsimps [Acts_JN])); |
126 qed "JN_constant"; |
143 qed "JN_constant"; |
127 |
144 |
128 Goal "(JN i:I. F i Join G i) = (JN i:I. F i) Join (JN i:I. G i)"; |
145 Goal "(JN i:I. F i Join G i) = (JN i:I. F i) Join (JN i:I. G i)"; |
130 simpset() addsimps [Acts_JN, Acts_Join])); |
147 simpset() addsimps [Acts_JN, Acts_Join])); |
131 qed "JN_Join_distrib"; |
148 qed "JN_Join_distrib"; |
132 |
149 |
133 Goal "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)"; |
150 Goal "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)"; |
134 by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1); |
151 by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1); |
|
152 by Auto_tac; |
135 qed "JN_Join_miniscope"; |
153 qed "JN_Join_miniscope"; |
136 |
154 |
137 |
155 |
138 (*** Safety: co, stable, FP ***) |
156 (*** Safety: co, stable, FP ***) |
139 |
157 |