author  wenzelm 
Sun, 07 Oct 2007 21:19:31 +0200  
changeset 24893  b8ef7afe3a6b 
parent 24892  c663e675e177 
child 32960  69916a850301 
permissions  rwrr 
14052  1 
(* Title: ZF/UNITY/Follows 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

2 
ID: $Id \<in> Follows.thy,v 1.1 2003/05/28 16:13:42 paulson Exp $ 
14052  3 
Author: Sidi O Ehmety, Cambridge University Computer Laboratory 
4 
Copyright 2002 University of Cambridge 

5 

6 
Theory ported from HOL. 

7 
*) 

8 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

9 
header{*The "Follows" relation of Charpentier and Sivilotte*} 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

10 

16417  11 
theory Follows imports SubstAx Increasing begin 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

12 

24893  13 
definition 
14 
Follows :: "[i, i, i=>i, i=>i] => i" where 

24892  15 
"Follows(A, r, f, g) == 
14052  16 
Increasing(A, r, g) Int 
17 
Increasing(A, r,f) Int 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

18 
Always({s \<in> state. <f(s), g(s)>:r}) Int 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

19 
(\<Inter>k \<in> A. {s \<in> state. <k, g(s)>:r} LeadsTo {s \<in> state. <k,f(s)>:r})" 
24892  20 

21 
abbreviation 

22 
Incr :: "[i=>i]=>i" where 

23 
"Incr(f) == Increasing(list(nat), prefix(nat), f)" 

14052  24 

24892  25 
abbreviation 
26 
n_Incr :: "[i=>i]=>i" where 

27 
"n_Incr(f) == Increasing(nat, Le, f)" 

28 

29 
abbreviation 

30 
s_Incr :: "[i=>i]=>i" where 

31 
"s_Incr(f) == Increasing(Pow(nat), SetLe(nat), f)" 

14052  32 

24892  33 
abbreviation 
34 
m_Incr :: "[i=>i]=>i" where 

35 
"m_Incr(f) == Increasing(Mult(nat), MultLe(nat, Le), f)" 

14052  36 

24892  37 
abbreviation 
38 
n_Fols :: "[i=>i, i=>i]=>i" (infixl "n'_Fols" 65) where 

39 
"f n_Fols g == Follows(nat, Le, f, g)" 

40 

41 
abbreviation 

42 
Follows' :: "[i=>i, i=>i, i, i] => i" 

43 
("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60) where 

44 
"f Fols g Wrt r/A == Follows(A,r,f,g)" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

45 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

46 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

47 
(*Does this hold for "invariant"?*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

48 

24892  49 
lemma Follows_cong: 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

50 
"[A=A'; r=r'; !!x. x \<in> state ==> f(x)=f'(x); !!x. x \<in> state ==> g(x)=g'(x)] ==> Follows(A, r, f, g) = Follows(A', r', f', g')" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

51 
by (simp add: Increasing_def Follows_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

52 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

53 

24892  54 
lemma subset_Always_comp: 
55 
"[ mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A ] ==> 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

56 
Always({x \<in> state. <f(x), g(x)> \<in> r})<=Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

57 
apply (unfold mono1_def metacomp_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

58 
apply (auto simp add: Always_eq_includes_reachable) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

59 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

60 

24892  61 
lemma imp_Always_comp: 
62 
"[ F \<in> Always({x \<in> state. <f(x), g(x)> \<in> r}); 

63 
mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A ] ==> 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

64 
F \<in> Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

65 
by (blast intro: subset_Always_comp [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

66 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

67 

24892  68 
lemma imp_Always_comp2: 
69 
"[ F \<in> Always({x \<in> state. <f1(x), f(x)> \<in> r}); 

70 
F \<in> Always({x \<in> state. <g1(x), g(x)> \<in> s}); 

71 
mono2(A, r, B, s, C, t, h); 

72 
\<forall>x \<in> state. f1(x):A & f(x):A & g1(x):B & g(x):B ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

73 
==> F \<in> Always({x \<in> state. <h(f1(x), g1(x)), h(f(x), g(x))> \<in> t})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

74 
apply (auto simp add: Always_eq_includes_reachable mono2_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

75 
apply (auto dest!: subsetD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

76 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

77 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

78 
(* comp LeadsTo *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

79 

24892  80 
lemma subset_LeadsTo_comp: 
81 
"[ mono1(A, r, B, s, h); refl(A,r); trans[B](s); 

82 
\<forall>x \<in> state. f(x):A & g(x):A ] ==> 

83 
(\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r}) <= 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

84 
(\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} LeadsTo {x \<in> state. <k, (h comp f)(x)> \<in> s})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

85 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

86 
apply (unfold mono1_def metacomp_def, clarify) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

87 
apply (simp_all (no_asm_use) add: INT_iff) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

88 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

89 
apply (rule single_LeadsTo_I) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

90 
prefer 2 apply (blast dest: LeadsTo_type [THEN subsetD], auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

91 
apply (rotate_tac 5) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

92 
apply (drule_tac x = "g (sa) " in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

93 
apply (erule_tac [2] LeadsTo_weaken) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

94 
apply (auto simp add: part_order_def refl_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

95 
apply (rule_tac b = "h (g (sa))" in trans_onD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

96 
apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

97 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

98 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

99 

24892  100 
lemma imp_LeadsTo_comp: 
101 
"[ F:(\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r}); 

102 
mono1(A, r, B, s, h); refl(A,r); trans[B](s); 

103 
\<forall>x \<in> state. f(x):A & g(x):A ] ==> 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

104 
F:(\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} LeadsTo {x \<in> state. <k, (h comp f)(x)> \<in> s})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

105 
apply (rule subset_LeadsTo_comp [THEN subsetD], auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

106 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

107 

24892  108 
lemma imp_LeadsTo_comp_right: 
109 
"[ F \<in> Increasing(B, s, g); 

110 
\<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r}; 

111 
mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t); 

112 
\<forall>x \<in> state. f1(x):A & f(x):A & g(x):B; k \<in> C ] ==> 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

113 
F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g(x))> \<in> t}" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

114 
apply (unfold mono2_def Increasing_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

115 
apply (rule single_LeadsTo_I, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

116 
apply (drule_tac x = "g (sa) " and A = B in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

117 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

118 
apply (drule_tac x = "f (sa) " and P = "%j. F \<in> ?X (j) \<longmapsto>w ?Y (j) " in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

119 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

120 
apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

121 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

122 
apply (force simp add: part_order_def refl_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

123 
apply (force simp add: part_order_def refl_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

124 
apply (drule_tac x = "f1 (x) " and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. ?P (x,y,u) " in bspec [THEN bspec]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

125 
apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) > ?d (x,y) \<in> t" in bspec [THEN bspec]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

126 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

127 
apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

128 
apply (auto simp add: part_order_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

129 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

130 

24892  131 
lemma imp_LeadsTo_comp_left: 
132 
"[ F \<in> Increasing(A, r, f); 

133 
\<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s}; 

134 
mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); 

135 
\<forall>x \<in> state. f(x):A & g1(x):B & g(x):B; k \<in> C ] ==> 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

136 
F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f(x), g1(x))> \<in> t}" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

137 
apply (unfold mono2_def Increasing_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

138 
apply (rule single_LeadsTo_I, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

139 
apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (?X (k))" in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

140 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

141 
apply (drule_tac x = "g (sa) " in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

142 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

143 
apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

144 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

145 
apply (force simp add: part_order_def refl_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

146 
apply (force simp add: part_order_def refl_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

147 
apply (drule_tac x = "f (x) " and x1 = "f (sa) " in bspec [THEN bspec]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

148 
apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) > ?d (x,y) \<in> t" in bspec [THEN bspec]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

149 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

150 
apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

151 
apply (auto simp add: part_order_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

152 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

153 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

154 
(** This general result is used to prove Follows Un, munion, etc. **) 
24892  155 
lemma imp_LeadsTo_comp2: 
156 
"[ F \<in> Increasing(A, r, f1) Int Increasing(B, s, g); 

157 
\<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r}; 

158 
\<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s}; 

159 
mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); 

160 
\<forall>x \<in> state. f(x):A & g1(x):B & f1(x):A &g(x):B; k \<in> C ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

161 
==> F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g1(x))> \<in> t}" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

162 
apply (rule_tac B = "{x \<in> state. <k, h (f1 (x), g (x))> \<in> t}" in LeadsTo_Trans) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

163 
apply (blast intro: imp_LeadsTo_comp_right) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

164 
apply (blast intro: imp_LeadsTo_comp_left) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

165 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

166 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

167 
(* Follows type *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

168 
lemma Follows_type: "Follows(A, r, f, g)<=program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

169 
apply (unfold Follows_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

170 
apply (blast dest: Increasing_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

171 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

172 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

173 
lemma Follows_into_program [TC]: "F \<in> Follows(A, r, f, g) ==> F \<in> program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

174 
by (blast dest: Follows_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

175 

24892  176 
lemma FollowsD: 
177 
"F \<in> Follows(A, r, f, g)==> 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

178 
F \<in> program & (\<exists>a. a \<in> A) & (\<forall>x \<in> state. f(x):A & g(x):A)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

179 
apply (unfold Follows_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

180 
apply (blast dest: IncreasingD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

181 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

182 

24892  183 
lemma Follows_constantI: 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

184 
"[ F \<in> program; c \<in> A; refl(A, r) ] ==> F \<in> Follows(A, r, %x. c, %x. c)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

185 
apply (unfold Follows_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

186 
apply (auto simp add: refl_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

187 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

188 

24892  189 
lemma subset_Follows_comp: 
190 
"[ mono1(A, r, B, s, h); refl(A, r); trans[B](s) ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

191 
==> Follows(A, r, f, g) <= Follows(B, s, h comp f, h comp g)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

192 
apply (unfold Follows_def, clarify) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

193 
apply (frule_tac f = g in IncreasingD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

194 
apply (frule_tac f = f in IncreasingD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

195 
apply (rule IntI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

196 
apply (rule_tac [2] h = h in imp_LeadsTo_comp) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

197 
prefer 5 apply assumption 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

198 
apply (auto intro: imp_Increasing_comp imp_Always_comp simp del: INT_simps) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

199 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

200 

24892  201 
lemma imp_Follows_comp: 
202 
"[ F \<in> Follows(A, r, f, g); mono1(A, r, B, s, h); refl(A, r); trans[B](s) ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

203 
==> F \<in> Follows(B, s, h comp f, h comp g)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

204 
apply (blast intro: subset_Follows_comp [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

205 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

206 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

207 
(* 2place monotone operation \<in> this general result is used to prove Follows_Un, Follows_munion *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

208 

24892  209 
(* 2place monotone operation \<in> this general result is 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

210 
used to prove Follows_Un, Follows_munion *) 
24892  211 
lemma imp_Follows_comp2: 
212 
"[ F \<in> Follows(A, r, f1, f); F \<in> Follows(B, s, g1, g); 

213 
mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

214 
==> F \<in> Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

215 
apply (unfold Follows_def, clarify) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

216 
apply (frule_tac f = g in IncreasingD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

217 
apply (frule_tac f = f in IncreasingD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

218 
apply (rule IntI, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

219 
apply (rule_tac [3] h = h in imp_Always_comp2) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

220 
prefer 5 apply assumption 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

221 
apply (rule_tac [2] h = h in imp_Increasing_comp2) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

222 
prefer 4 apply assumption 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

223 
apply (rule_tac h = h in imp_Increasing_comp2) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

224 
prefer 3 apply assumption 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

225 
apply simp_all 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

226 
apply (blast dest!: IncreasingD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

227 
apply (rule_tac h = h in imp_LeadsTo_comp2) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

228 
prefer 4 apply assumption 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

229 
apply auto 
24892  230 
prefer 3 apply (simp add: mono2_def) 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

231 
apply (blast dest: IncreasingD)+ 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

232 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

233 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

234 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

235 
lemma Follows_trans: 
24892  236 
"[ F \<in> Follows(A, r, f, g); F \<in> Follows(A,r, g, h); 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

237 
trans[A](r) ] ==> F \<in> Follows(A, r, f, h)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

238 
apply (frule_tac f = f in FollowsD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

239 
apply (frule_tac f = g in FollowsD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

240 
apply (simp add: Follows_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

241 
apply (simp add: Always_eq_includes_reachable INT_iff, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

242 
apply (rule_tac [2] B = "{s \<in> state. <k, g (s) > \<in> r}" in LeadsTo_Trans) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

243 
apply (rule_tac b = "g (x) " in trans_onD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

244 
apply blast+ 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

245 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

246 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

247 
(** Destruction rules for Follows **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

248 

24892  249 
lemma Follows_imp_Increasing_left: 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

250 
"F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, f)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

251 
by (unfold Follows_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

252 

24892  253 
lemma Follows_imp_Increasing_right: 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

254 
"F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, g)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

255 
by (unfold Follows_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

256 

24892  257 
lemma Follows_imp_Always: 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

258 
"F :Follows(A, r, f, g) ==> F \<in> Always({s \<in> state. <f(s),g(s)> \<in> r})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

259 
by (unfold Follows_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

260 

24892  261 
lemma Follows_imp_LeadsTo: 
262 
"[ F \<in> Follows(A, r, f, g); k \<in> A ] ==> 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

263 
F: {s \<in> state. <k,g(s)> \<in> r } LeadsTo {s \<in> state. <k,f(s)> \<in> r}" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

264 
by (unfold Follows_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

265 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

266 
lemma Follows_LeadsTo_pfixLe: 
24892  267 
"[ F \<in> Follows(list(nat), gen_prefix(nat, Le), f, g); k \<in> list(nat) ] 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

268 
==> F \<in> {s \<in> state. k pfixLe g(s)} LeadsTo {s \<in> state. k pfixLe f(s)}" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

269 
by (blast intro: Follows_imp_LeadsTo) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

270 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

271 
lemma Follows_LeadsTo_pfixGe: 
24892  272 
"[ F \<in> Follows(list(nat), gen_prefix(nat, Ge), f, g); k \<in> list(nat) ] 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

273 
==> F \<in> {s \<in> state. k pfixGe g(s)} LeadsTo {s \<in> state. k pfixGe f(s)}" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

274 
by (blast intro: Follows_imp_LeadsTo) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

275 

24892  276 
lemma Always_Follows1: 
277 
"[ F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h); 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

278 
\<forall>x \<in> state. g(x):A ] ==> F \<in> Follows(A, r, g, h)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

279 
apply (unfold Follows_def Increasing_def Stable_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

280 
apply (simp add: INT_iff, auto) 
24892  281 
apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}" 
282 
and A = "{s \<in> state. <k, h (s)> \<in> r}" 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14093
diff
changeset

283 
and A' = "{s \<in> state. <k, f(s)> \<in> r}" in Always_LeadsTo_weaken) 
24892  284 
apply (erule_tac A = "{s \<in> state. <k,f(s) > \<in> r}" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14093
diff
changeset

285 
and A' = "{s \<in> state. <k,f(s) > \<in> r}" in Always_Constrains_weaken) 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

286 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

287 
apply (drule Always_Int_I, assumption) 
24892  288 
apply (erule_tac A = "{s \<in> state. f(s)=g(s)} \<inter> {s \<in> state. <f(s), h(s)> \<in> r}" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14093
diff
changeset

289 
in Always_weaken) 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

290 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

291 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

292 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14093
diff
changeset

293 

24892  294 
lemma Always_Follows2: 
295 
"[ F \<in> Always({s \<in> state. g(s) = h(s)}); 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

296 
F \<in> Follows(A, r, f, g); \<forall>x \<in> state. h(x):A ] ==> F \<in> Follows(A, r, f, h)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

297 
apply (unfold Follows_def Increasing_def Stable_def) 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14093
diff
changeset

298 
apply (simp add: INT_iff, auto) 
24892  299 
apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }" 
300 
and A = "{s \<in> state. <k, g (s) > \<in> r}" 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14093
diff
changeset

301 
and A' = "{s \<in> state. <k, f (s) > \<in> r}" in Always_LeadsTo_weaken) 
24892  302 
apply (erule_tac A = "{s \<in> state. <k, g(s)> \<in> r}" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14093
diff
changeset

303 
and A' = "{s \<in> state. <k, g(s)> \<in> r}" in Always_Constrains_weaken) 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

304 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

305 
apply (drule Always_Int_I, assumption) 
24892  306 
apply (erule_tac A = "{s \<in> state. g(s)=h(s)} \<inter> {s \<in> state. <f(s), g(s)> \<in> r}" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14093
diff
changeset

307 
in Always_weaken) 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

308 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

309 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

310 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

311 
(** Union properties (with the subset ordering) **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

312 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

313 
lemma refl_SetLe [simp]: "refl(Pow(A), SetLe(A))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

314 
by (unfold refl_def SetLe_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

315 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

316 
lemma trans_on_SetLe [simp]: "trans[Pow(A)](SetLe(A))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

317 
by (unfold trans_on_def SetLe_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

318 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

319 
lemma antisym_SetLe [simp]: "antisym(SetLe(A))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

320 
by (unfold antisym_def SetLe_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

321 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

322 
lemma part_order_SetLe [simp]: "part_order(Pow(A), SetLe(A))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

323 
by (unfold part_order_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

324 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

325 
lemma increasing_Un: 
24892  326 
"[ F \<in> Increasing.increasing(Pow(A), SetLe(A), f); 
327 
F \<in> Increasing.increasing(Pow(A), SetLe(A), g) ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

328 
==> F \<in> Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

329 
by (rule_tac h = "op Un" in imp_increasing_comp2, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

330 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

331 
lemma Increasing_Un: 
24892  332 
"[ F \<in> Increasing(Pow(A), SetLe(A), f); 
333 
F \<in> Increasing(Pow(A), SetLe(A), g) ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

334 
==> F \<in> Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

335 
by (rule_tac h = "op Un" in imp_Increasing_comp2, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

336 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

337 
lemma Always_Un: 
24892  338 
"[ F \<in> Always({s \<in> state. f1(s) <= f(s)}); 
339 
F \<in> Always({s \<in> state. g1(s) <= g(s)}) ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

340 
==> F \<in> Always({s \<in> state. f1(s) Un g1(s) <= f(s) Un g(s)})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

341 
by (simp add: Always_eq_includes_reachable, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

342 

24892  343 
lemma Follows_Un: 
344 
"[ F \<in> Follows(Pow(A), SetLe(A), f1, f); 

345 
F \<in> Follows(Pow(A), SetLe(A), g1, g) ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

346 
==> F \<in> Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

347 
by (rule_tac h = "op Un" in imp_Follows_comp2, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

348 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

349 
(** Multiset union properties (with the MultLe ordering) **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

350 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

351 
lemma refl_MultLe [simp]: "refl(Mult(A), MultLe(A,r))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

352 
by (unfold MultLe_def refl_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

353 

24892  354 
lemma MultLe_refl1 [simp]: 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

355 
"[ multiset(M); mset_of(M)<=A ] ==> <M, M> \<in> MultLe(A, r)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

356 
apply (unfold MultLe_def id_def lam_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

357 
apply (auto simp add: Mult_iff_multiset) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

358 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

359 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

360 
lemma MultLe_refl2 [simp]: "M \<in> Mult(A) ==> <M, M> \<in> MultLe(A, r)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

361 
by (unfold MultLe_def id_def lam_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

362 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

363 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

364 
lemma trans_on_MultLe [simp]: "trans[Mult(A)](MultLe(A,r))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

365 
apply (unfold MultLe_def trans_on_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

366 
apply (auto intro: trancl_trans simp add: multirel_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

367 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

368 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

369 
lemma MultLe_type: "MultLe(A, r)<= (Mult(A) * Mult(A))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

370 
apply (unfold MultLe_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

371 
apply (drule multirel_type [THEN subsetD], auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

372 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

373 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

374 
lemma MultLe_trans: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

375 
"[ <M,K> \<in> MultLe(A,r); <K,N> \<in> MultLe(A,r) ] ==> <M,N> \<in> MultLe(A,r)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

376 
apply (cut_tac A=A in trans_on_MultLe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

377 
apply (drule trans_onD, assumption) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

378 
apply (auto dest: MultLe_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

379 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

380 

24892  381 
lemma part_order_imp_part_ord: 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

382 
"part_order(A, r) ==> part_ord(A, rid(A))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

383 
apply (unfold part_order_def part_ord_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

384 
apply (simp add: refl_def id_def lam_def irrefl_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

385 
apply (simp (no_asm) add: trans_on_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

386 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

387 
apply (blast dest: trans_onD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

388 
apply (simp (no_asm_use) add: antisym_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

389 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

390 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

391 

24892  392 
lemma antisym_MultLe [simp]: 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

393 
"part_order(A, r) ==> antisym(MultLe(A,r))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

394 
apply (unfold MultLe_def antisym_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

395 
apply (drule part_order_imp_part_ord, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

396 
apply (drule irrefl_on_multirel) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

397 
apply (frule multirel_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

398 
apply (drule multirel_trans) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

399 
apply (auto simp add: irrefl_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

400 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

401 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

402 
lemma part_order_MultLe [simp]: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

403 
"part_order(A, r) ==> part_order(Mult(A), MultLe(A, r))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

404 
apply (frule antisym_MultLe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

405 
apply (auto simp add: part_order_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

406 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

407 

24892  408 
lemma empty_le_MultLe [simp]: 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

409 
"[ multiset(M); mset_of(M)<= A] ==> <0, M> \<in> MultLe(A, r)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

410 
apply (unfold MultLe_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

411 
apply (case_tac "M=0") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

412 
apply (auto simp add: FiniteFun.intros) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

413 
apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel (A, r  id (A))") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

414 
apply (rule_tac [2] one_step_implies_multirel) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

415 
apply (auto simp add: Mult_iff_multiset) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

416 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

417 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

418 
lemma empty_le_MultLe2 [simp]: "M \<in> Mult(A) ==> <0, M> \<in> MultLe(A, r)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

419 
by (simp add: Mult_iff_multiset) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

420 

24892  421 
lemma munion_mono: 
422 
"[ <M, N> \<in> MultLe(A, r); <K, L> \<in> MultLe(A, r) ] ==> 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

423 
<M +# K, N +# L> \<in> MultLe(A, r)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

424 
apply (unfold MultLe_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

425 
apply (auto intro: munion_multirel_mono1 munion_multirel_mono2 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

426 
munion_multirel_mono multiset_into_Mult simp add: Mult_iff_multiset) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

427 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

428 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

429 
lemma increasing_munion: 
24892  430 
"[ F \<in> Increasing.increasing(Mult(A), MultLe(A,r), f); 
431 
F \<in> Increasing.increasing(Mult(A), MultLe(A,r), g) ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

432 
==> F \<in> Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

433 
by (rule_tac h = munion in imp_increasing_comp2, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

434 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

435 
lemma Increasing_munion: 
24892  436 
"[ F \<in> Increasing(Mult(A), MultLe(A,r), f); 
437 
F \<in> Increasing(Mult(A), MultLe(A,r), g)] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

438 
==> F \<in> Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

439 
by (rule_tac h = munion in imp_Increasing_comp2, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

440 

24892  441 
lemma Always_munion: 
442 
"[ F \<in> Always({s \<in> state. <f1(s),f(s)> \<in> MultLe(A,r)}); 

443 
F \<in> Always({s \<in> state. <g1(s), g(s)> \<in> MultLe(A,r)}); 

444 
\<forall>x \<in> state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

445 
==> F \<in> Always({s \<in> state. <f1(s) +# g1(s), f(s) +# g(s)> \<in> MultLe(A,r)})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

446 
apply (rule_tac h = munion in imp_Always_comp2, simp_all) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

447 
apply (blast intro: munion_mono, simp_all) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

448 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

449 

24892  450 
lemma Follows_munion: 
451 
"[ F \<in> Follows(Mult(A), MultLe(A, r), f1, f); 

452 
F \<in> Follows(Mult(A), MultLe(A, r), g1, g) ] 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

453 
==> F \<in> Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

454 
by (rule_tac h = munion in imp_Follows_comp2, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

455 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

456 
(** Used in ClientImp **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

457 

24892  458 
lemma Follows_msetsum_UN: 
459 
"!!f. [ \<forall>i \<in> I. F \<in> Follows(Mult(A), MultLe(A, r), f'(i), f(i)); 

460 
\<forall>s. \<forall>i \<in> I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A & 

461 
multiset(f(i, s)) & mset_of(f(i, s))<=A ; 

462 
Finite(I); F \<in> program ] 

463 
==> F \<in> Follows(Mult(A), 

464 
MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A), 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

465 
%x. msetsum(%i. f(i, x), I, A))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

466 
apply (erule rev_mp) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

467 
apply (drule Finite_into_Fin) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

468 
apply (erule Fin_induct) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

469 
apply (simp (no_asm_simp)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

470 
apply (rule Follows_constantI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

471 
apply (simp_all (no_asm_simp) add: FiniteFun.intros) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

472 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

473 
apply (rule Follows_munion, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

474 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

475 

14052  476 
end 