author  paulson 
Wed, 19 May 1999 11:21:34 +0200  
changeset 6672  8542c6dda828 
parent 6575  70d758762c50 
child 6704  5febcf428342 
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 

6536  46 
overload_1st_set "Constrains.op Co"; 
5340  47 

6536  48 
(*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

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

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

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

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

53 

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

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

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

58 
addIs [constrains_weaken]) 1); 

59 
qed "Constrains_eq_constrains"; 

60 

6536  61 
Goalw [Constrains_def] "F : A co A' ==> F : A Co A'"; 
6575  62 
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

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

64 

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

68 

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

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

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

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

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

75 

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

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

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

79 

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

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

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

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

84 

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

85 
Goalw [Constrains_def] 
6536  86 
"[ 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

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

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

89 

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

90 
Goalw [Constrains_def] 
6536  91 
"[ 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

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

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

94 

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

95 
Goalw [Constrains_def] 
6536  96 
"[ 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

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

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

99 

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

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

101 

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

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

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

105 
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

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

107 

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

5648  110 
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

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

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

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

114 

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

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

116 

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

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

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

120 
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

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

122 

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

5648  125 
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

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

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

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

130 

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

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

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

135 

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

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

138 
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

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

140 

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

143 
constrains_def]) 1); 

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

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

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

146 

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

147 

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

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

149 

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

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

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

154 

6536  155 
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

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

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

158 

6536  159 
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

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

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

162 

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

163 
Goalw [Stable_def] 
5648  164 
"[ 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

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

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

167 

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

168 
Goalw [Stable_def] 
5648  169 
"[ 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

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

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

172 

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

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

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

176 
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

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

178 

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

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

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

182 
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

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

184 

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

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

186 
"(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

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

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

189 

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

190 
Goalw [Stable_def] 
5648  191 
"(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

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

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

194 

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

196 
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

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

198 

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 

5784  201 
(*** Increasing ***) 
202 

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

204 
"Increasing f <= Increasing (length o f)"; 

205 
by Auto_tac; 

206 
by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1); 

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

207 
qed "Increasing_size"; 
5784  208 

209 
Goalw [Increasing_def] 

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

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

212 
by (Blast_tac 1); 

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

213 
qed "Increasing_Stable_less"; 
5784  214 

215 
Goalw [increasing_def, Increasing_def] 

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

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

218 
qed "increasing_imp_Increasing"; 

219 

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 

6575  300 
Goal "[ F : Always INV; F : (INV Int A) Co A' ] ==> F : A Co A'"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

301 
by (asm_full_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); 
6570  304 
qed "Always_ConstrainsI"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

305 

6570  306 
(* [ F : Always INV; F : (INV Int A) Co A ] 
5648  307 
==> F : Stable A *) 
6570  308 
bind_thm ("Always_StableI", Always_ConstrainsI RS StableI); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

309 

6570  310 
Goal "[ F : Always INV; F : A Co A' ] \ 
6536  311 
\ ==> F : A Co (INV Int A')"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

312 
by (asm_full_simp_tac 
6570  313 
(simpset() addsimps [Always_includes_reachable RS Int_absorb2, 
6575  314 
Constrains_eq_constrains, Int_assoc RS sym]) 1); 
6570  315 
qed "Always_ConstrainsD"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

316 

6570  317 
bind_thm ("Always_StableD", StableD RSN (2,Always_ConstrainsD)); 
5313
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 

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

320 

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

322 

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

325 
qed "Always_Int"; 

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

326 

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

327 
(*Delete the nearest invariance assumption (which will be the second one 
6570  328 
used by Always_Int) *) 
329 
val Always_thin = 

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

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

332 

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

333 
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*) 
6570  334 
val Always_Int_tac = dtac Always_Int THEN' assume_tac THEN' etac Always_thin; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

335 

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

336 
(*Combines a list of invariance THEOREMS into one.*) 
6570  337 
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

338 

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

339 

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

342 

6536  343 
(*proves "co" properties when the program is specified*) 
5648  344 
fun constrains_tac i = 
5422  345 
SELECT_GOAL 
5648  346 
(EVERY [simp_tac (simpset() addsimps !program_defs_ref) 1, 
347 
REPEAT (resolve_tac [StableI, stableI, 

5422  348 
constrains_imp_Constrains] 1), 
349 
rtac constrainsI 1, 

5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5422
diff
changeset

350 
Full_simp_tac 1, 
5620  351 
REPEAT (FIRSTGOAL (etac disjE)), 
5422  352 
ALLGOALS Clarify_tac, 
5648  353 
ALLGOALS Asm_full_simp_tac]) i; 
5422  354 

355 