author  paulson 
Mon, 20 Sep 1999 10:42:09 +0200  
changeset 7541  1a7a38d8f5bd 
parent 7403  c318acb88251 
child 7689  affe0c2fdfbf 
permissions  rwrr 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

1 
(* Title: HOL/UNITY/Constrains 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

2 
ID: $Id$ 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

4 
Copyright 1998 University of Cambridge 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

5 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

6 
Safety relations: restricted to the set of reachable states. 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

7 
*) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

8 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

9 

6535  10 
(*** traces and reachable ***) 
11 

12 
Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"; 

13 
by Safe_tac; 

14 
by (etac traces.induct 2); 

15 
by (etac reachable.induct 1); 

16 
by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs))); 

17 
qed "reachable_equiv_traces"; 

18 

19 
Goal "Init F <= reachable F"; 

20 
by (blast_tac (claset() addIs reachable.intrs) 1); 

21 
qed "Init_subset_reachable"; 

22 

23 
Goal "Acts G <= Acts F ==> G : stable (reachable F)"; 

24 
by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1); 

25 
qed "stable_reachable"; 

26 

27 

28 
(*The set of all reachable states is an invariant...*) 

29 
Goal "F : invariant (reachable F)"; 

30 
by (simp_tac (simpset() addsimps [invariant_def]) 1); 

31 
by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1); 

32 
qed "invariant_reachable"; 

33 

34 
(*...in fact the strongest invariant!*) 

35 
Goal "F : invariant A ==> reachable F <= A"; 

36 
by (full_simp_tac 

37 
(simpset() addsimps [stable_def, constrains_def, invariant_def]) 1); 

38 
by (rtac subsetI 1); 

39 
by (etac reachable.induct 1); 

40 
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); 

41 
qed "invariant_includes_reachable"; 

42 

43 

6536  44 
(*** Co ***) 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

45 

7403  46 
(*Needed because its operands are sets*) 
47 
overload_1st_set "Constrains.Constrains"; 

5340  48 

6536  49 
(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

50 
bind_thm ("constrains_reachable_Int", 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

51 
subset_refl RS 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

52 
rewrite_rule [stable_def] stable_reachable RS 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

53 
constrains_Int); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

54 

6575  55 
(*Resembles the previous definition of Constrains*) 
56 
Goalw [Constrains_def] 

57 
"A Co B = {F. F : (reachable F Int A) co (reachable F Int B)}"; 

58 
by (blast_tac (claset() addDs [constrains_reachable_Int] 

59 
addIs [constrains_weaken]) 1); 

60 
qed "Constrains_eq_constrains"; 

61 

6536  62 
Goalw [Constrains_def] "F : A co A' ==> F : A Co A'"; 
6575  63 
by (blast_tac (claset() addIs [constrains_weaken_L]) 1); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

64 
qed "constrains_imp_Constrains"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

65 

5648  66 
Goalw [stable_def, Stable_def] "F : stable A ==> F : Stable A"; 
5631  67 
by (etac constrains_imp_Constrains 1); 
68 
qed "stable_imp_Stable"; 

69 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

70 
val prems = Goal 
5620  71 
"(!!act s s'. [ act: Acts F; (s,s') : act; s: A ] ==> s': A') \ 
6536  72 
\ ==> F : A Co A'"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

73 
by (rtac constrains_imp_Constrains 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

74 
by (blast_tac (claset() addIs (constrainsI::prems)) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

75 
qed "ConstrainsI"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

76 

6536  77 
Goalw [Constrains_def, constrains_def] "F : {} Co B"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

78 
by (Blast_tac 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

79 
qed "Constrains_empty"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

80 

6536  81 
Goal "F : A Co UNIV"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

82 
by (blast_tac (claset() addIs [ConstrainsI]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

83 
qed "Constrains_UNIV"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

84 
AddIffs [Constrains_empty, Constrains_UNIV]; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

85 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

86 
Goalw [Constrains_def] 
6536  87 
"[ F : A Co A'; A'<=B' ] ==> F : A Co B'"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

88 
by (blast_tac (claset() addIs [constrains_weaken_R]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

89 
qed "Constrains_weaken_R"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

90 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

91 
Goalw [Constrains_def] 
6536  92 
"[ F : A Co A'; B<=A ] ==> F : B Co A'"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

93 
by (blast_tac (claset() addIs [constrains_weaken_L]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

94 
qed "Constrains_weaken_L"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

95 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

96 
Goalw [Constrains_def] 
6536  97 
"[ F : A Co A'; B<=A; A'<=B' ] ==> F : B Co B'"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

98 
by (blast_tac (claset() addIs [constrains_weaken]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

99 
qed "Constrains_weaken"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

100 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

101 
(** Union **) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

102 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

103 
Goalw [Constrains_def] 
6536  104 
"[ F : A Co A'; F : B Co B' ] \ 
105 
\ ==> F : (A Un B) Co (A' Un B')"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

106 
by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

107 
qed "Constrains_Un"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

108 

6536  109 
Goal "ALL i:I. F : (A i) Co (A' i) \ 
110 
\ ==> F : (UN i:I. A i) Co (UN i:I. A' i)"; 

5648  111 
by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

112 
by (dtac ball_constrains_UN 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

113 
by (blast_tac (claset() addIs [constrains_weaken]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

114 
qed "ball_Constrains_UN"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

115 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

116 
(** Intersection **) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

117 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

118 
Goalw [Constrains_def] 
6536  119 
"[ F : A Co A'; F : B Co B' ] \ 
120 
\ ==> F : (A Int B) Co (A' Int B')"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

121 
by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

122 
qed "Constrains_Int"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

123 

6536  124 
Goal "ALL i:I. F : (A i) Co (A' i) \ 
125 
\ ==> F : (INT i:I. A i) Co (INT i:I. A' i)"; 

5648  126 
by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

127 
by (dtac ball_constrains_INT 1); 
5340  128 
by (dtac constrains_reachable_Int 1); 
129 
by (blast_tac (claset() addIs [constrains_weaken]) 1); 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

130 
qed "ball_Constrains_INT"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

131 

6536  132 
Goal "F : A Co A' ==> reachable F Int A <= A'"; 
6575  133 
by (asm_full_simp_tac (simpset() addsimps [constrains_imp_subset, 
134 
Constrains_def]) 1); 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

135 
qed "Constrains_imp_subset"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

136 

6575  137 
Goal "[ F : A Co B; F : B Co C ] ==> F : A Co C"; 
138 
by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1); 

6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

139 
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

140 
qed "Constrains_trans"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

141 

6575  142 
Goal "[ F : A Co (A' Un B); F : B Co B' ] ==> F : A Co (A' Un B')"; 
143 
by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains, 

144 
constrains_def]) 1); 

6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

145 
by (Blast_tac 1); 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

146 
qed "Constrains_cancel"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

147 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

148 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

149 
(*** Stable ***) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

150 

5648  151 
Goal "(F : Stable A) = (F : stable (reachable F Int A))"; 
6575  152 
by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains, 
153 
stable_def]) 1); 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

154 
qed "Stable_eq_stable"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

155 

6536  156 
Goalw [Stable_def] "F : A Co A ==> F : Stable A"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

157 
by (assume_tac 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

158 
qed "StableI"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

159 

6536  160 
Goalw [Stable_def] "F : Stable A ==> F : A Co A"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

161 
by (assume_tac 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

162 
qed "StableD"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

163 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

164 
Goalw [Stable_def] 
5648  165 
"[ F : Stable A; F : Stable A' ] ==> F : Stable (A Un A')"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

166 
by (blast_tac (claset() addIs [Constrains_Un]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

167 
qed "Stable_Un"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

168 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

169 
Goalw [Stable_def] 
5648  170 
"[ F : Stable A; F : Stable A' ] ==> F : Stable (A Int A')"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

171 
by (blast_tac (claset() addIs [Constrains_Int]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

172 
qed "Stable_Int"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

173 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

174 
Goalw [Stable_def] 
6536  175 
"[ F : Stable C; F : A Co (C Un A') ] \ 
176 
\ ==> F : (C Un A) Co (C Un A')"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

177 
by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

178 
qed "Stable_Constrains_Un"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

179 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

180 
Goalw [Stable_def] 
6536  181 
"[ F : Stable C; F : (C Int A) Co A' ] \ 
182 
\ ==> F : (C Int A) Co (C Int A')"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

183 
by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

184 
qed "Stable_Constrains_Int"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

185 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

186 
Goalw [Stable_def] 
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

187 
"(ALL i:I. F : Stable (A i)) ==> F : Stable (UN i:I. A i)"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

188 
by (etac ball_Constrains_UN 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

189 
qed "ball_Stable_UN"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

190 

8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

191 
Goalw [Stable_def] 
5648  192 
"(ALL i:I. F : Stable (A i)) ==> F : Stable (INT i:I. A i)"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

193 
by (etac ball_Constrains_INT 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

194 
qed "ball_Stable_INT"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

195 

5648  196 
Goal "F : Stable (reachable F)"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

197 
by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

198 
qed "Stable_reachable"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

199 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

200 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

201 

5784  202 
(*** Increasing ***) 
203 

204 
Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def] 

6704  205 
"mono g ==> Increasing f <= Increasing (g o f)"; 
5784  206 
by Auto_tac; 
6704  207 
by (blast_tac (claset() addIs [monoD, order_trans]) 1); 
208 
qed "mono_Increasing_o"; 

5784  209 

210 
Goalw [Increasing_def] 

211 
"Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}"; 

212 
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); 

213 
by (Blast_tac 1); 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

214 
qed "Increasing_Stable_less"; 
5784  215 

216 
Goalw [increasing_def, Increasing_def] 

217 
"F : increasing f ==> F : Increasing f"; 

218 
by (blast_tac (claset() addIs [stable_imp_Stable]) 1); 

219 
qed "increasing_imp_Increasing"; 

220 

221 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

222 
(*** The Elimination Theorem. The "free" m has become universally quantified! 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

223 
Should the premise be !!m instead of ALL m ? Would make it harder to use 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

224 
in forward proof. ***) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

225 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

226 
Goalw [Constrains_def, constrains_def] 
6536  227 
"[ ALL m. F : {s. s x = m} Co (B m) ] \ 
228 
\ ==> F : {s. s x : M} Co (UN m:M. B m)"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

229 
by (Blast_tac 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

230 
qed "Elimination"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

231 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

232 
(*As above, but for the trivial case of a onevariable state, in which the 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

233 
state is identified with its one variable.*) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

234 
Goalw [Constrains_def, constrains_def] 
6536  235 
"(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

236 
by (Blast_tac 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

237 
qed "Elimination_sing"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

238 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

239 

6570  240 
(*** Specialized laws for handling Always ***) 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

241 

6570  242 
(** Natural deduction rules for "Always A" **) 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

243 

6570  244 
Goal "[ Init F<=A; F : Stable A ] ==> F : Always A"; 
245 
by (asm_simp_tac (simpset() addsimps [Always_def]) 1); 

246 
qed "AlwaysI"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

247 

6570  248 
Goal "F : Always A ==> Init F<=A & F : Stable A"; 
249 
by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1); 

250 
qed "AlwaysD"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

251 

6570  252 
bind_thm ("AlwaysE", AlwaysD RS conjE); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

253 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

254 

6570  255 
(*The set of all reachable states is Always*) 
256 
Goal "F : Always A ==> reachable F <= A"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

257 
by (full_simp_tac 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

258 
(simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
6570  259 
Always_def]) 1); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

260 
by (rtac subsetI 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

261 
by (etac reachable.induct 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

262 
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); 
6570  263 
qed "Always_includes_reachable"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

264 

6575  265 
Goalw [Always_def, invariant_def, Stable_def, stable_def] 
6570  266 
"F : invariant A ==> F : Always A"; 
6575  267 
by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1); 
6570  268 
qed "invariant_imp_Always"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

269 

6672  270 
bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always); 
271 

6575  272 
Goal "Always A = {F. F : invariant (reachable F Int A)}"; 
273 
by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def, 

274 
Constrains_eq_constrains, stable_def]) 1); 

5648  275 
by (blast_tac (claset() addIs reachable.intrs) 1); 
6570  276 
qed "Always_eq_invariant_reachable"; 
5648  277 

6570  278 
(*the RHS is the traditional definition of the "always" operator*) 
279 
Goal "Always A = {F. reachable F <= A}"; 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

280 
by (auto_tac (claset() addDs [invariant_includes_reachable], 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

281 
simpset() addsimps [Int_absorb2, invariant_reachable, 
6570  282 
Always_eq_invariant_reachable])); 
283 
qed "Always_eq_includes_reachable"; 

5648  284 

285 

6570  286 
Goal "Always A = (UN I: Pow A. invariant I)"; 
287 
by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1); 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

288 
by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

289 
stable_reachable, 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

290 
impOfSubs invariant_includes_reachable]) 1); 
6570  291 
qed "Always_eq_UN_invariant"; 
292 

293 
Goal "[ F : Always A; A <= B ] ==> F : Always B"; 

294 
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); 

295 
qed "Always_weaken"; 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

296 

8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

297 

6570  298 
(*** "Co" rules involving Always ***) 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

299 

6739
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

300 
Goal "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"; 
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

301 
by (asm_simp_tac 
6570  302 
(simpset() addsimps [Always_includes_reachable RS Int_absorb2, 
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5784
diff
changeset

303 
Constrains_def, Int_assoc RS sym]) 1); 
6739
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

304 
qed "Always_Constrains_pre"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

305 

6739
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

306 
Goal "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')"; 
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

307 
by (asm_simp_tac 
6570  308 
(simpset() addsimps [Always_includes_reachable RS Int_absorb2, 
6575  309 
Constrains_eq_constrains, Int_assoc RS sym]) 1); 
6739
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

310 
qed "Always_Constrains_post"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

311 

6739
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

312 
(* [ F : Always INV; F : (INV Int A) Co A' ] ==> F : A Co A' *) 
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

313 
bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1); 
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

314 

66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

315 
(* [ F : Always INV; F : A Co A' ] ==> F : A Co (INV Int A') *) 
66e4118eead9
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents:
6704
diff
changeset

316 
bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

317 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

318 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

319 

6570  320 
(** Conjoining Always properties **) 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

321 

7541
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

322 
Goal "Always (A Int B) = Always A Int Always B"; 
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

323 
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); 
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

324 
qed "Always_Int_distrib"; 
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

325 

1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

326 
Goal "Always (INTER I A) = (INT i:I. Always (A i))"; 
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

327 
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); 
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

328 
qed "Always_INT_distrib"; 
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

329 

6570  330 
Goal "[ F : Always A; F : Always B ] ==> F : Always (A Int B)"; 
331 
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); 

7541
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

332 
qed "Always_Int_I"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

333 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

334 
(*Delete the nearest invariance assumption (which will be the second one 
7541
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

335 
used by Always_Int_I) *) 
6570  336 
val Always_thin = 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

337 
read_instantiate_sg (sign_of thy) 
6570  338 
[("V", "?F : Always ?A")] thin_rl; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

339 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

340 
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*) 
7541
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

341 
val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

342 

5319
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5313
diff
changeset

343 
(*Combines a list of invariance THEOREMS into one.*) 
7541
1a7a38d8f5bd
new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents:
7403
diff
changeset

344 
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

345 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

346 

5648  347 
(*To allow expansion of the program's definition when appropriate*) 
348 
val program_defs_ref = ref ([] : thm list); 

349 

6536  350 
(*proves "co" properties when the program is specified*) 
5648  351 
fun constrains_tac i = 
5422  352 
SELECT_GOAL 
7403  353 
(EVERY [REPEAT (Always_Int_tac 1), 
354 
REPEAT (etac Always_ConstrainsI 1 

355 
ORELSE 

356 
resolve_tac [StableI, stableI, 

5422  357 
constrains_imp_Constrains] 1), 
358 
rtac constrainsI 1, 

7403  359 
full_simp_tac (simpset() addsimps !program_defs_ref) 1, 
5620  360 
REPEAT (FIRSTGOAL (etac disjE)), 
5422  361 
ALLGOALS Clarify_tac, 
5648  362 
ALLGOALS Asm_full_simp_tac]) i; 
7403  363 

364 

365 
(*For proving invariants*) 

366 
fun always_tac i = 

367 
rtac AlwaysI i THEN Force_tac i THEN constrains_tac i; 