author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

1 
(* Title: ZF/UNITY/Follows.thy 
14052  2 
Author: Sidi O Ehmety, Cambridge University Computer Laboratory 
3 
Copyright 2002 University of Cambridge 

4 

5 
Theory ported from HOL. 

6 
*) 

7 

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

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

9 

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

11 

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

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

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

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

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

20 
abbreviation 

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

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

14052  23 

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

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

27 

28 
abbreviation 

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

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

14052  31 

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

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

14052  35 

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

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

39 

40 
abbreviation 

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

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

43 
"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

44 

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 
(*Does this hold for "invariant"?*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

47 

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

49 
"[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

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

51 

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

52 

24892  53 
lemma subset_Always_comp: 
54 
"[ 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

55 
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

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

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

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

59 

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

62 
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

63 
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

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

65 

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

66 

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

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

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

71 
\<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

72 
==> 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

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

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

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

76 

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

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

78 

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

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

82 
(\<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

83 
(\<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

84 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

98 

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

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

102 
\<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

103 
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

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

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

106 

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

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

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

111 
\<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

112 
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

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

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

115 
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

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

117 
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

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

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

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

121 
apply (force simp add: part_order_def refl_def) 
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 (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]) 
46823  124 
apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) \<longrightarrow> ?d (x,y) \<in> t" in bspec [THEN bspec]) 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

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

126 
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

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

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

129 

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

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

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

134 
\<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

135 
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

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

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

138 
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

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

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

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

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

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

144 
apply (force simp add: part_order_def refl_def) 
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 (drule_tac x = "f (x) " and x1 = "f (sa) " in bspec [THEN bspec]) 
46823  147 
apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) \<longrightarrow> ?d (x,y) \<in> t" in bspec [THEN bspec]) 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

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

149 
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

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

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

152 

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

153 
(** This general result is used to prove Follows Un, munion, etc. **) 
24892  154 
lemma imp_LeadsTo_comp2: 
46823  155 
"[ F \<in> Increasing(A, r, f1) \<inter> Increasing(B, s, g); 
24892  156 
\<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r}; 
157 
\<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s}; 

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

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

160 
==> 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

161 
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

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

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

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

165 

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

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

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

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

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

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

171 

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

172 
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

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

174 

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

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

177 
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

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

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

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

181 

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

183 
"[ 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

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

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

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

187 

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

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

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

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

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

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

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

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

197 
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

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

199 

24892  200 
lemma imp_Follows_comp: 
201 
"[ 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

202 
==> 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

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

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

205 

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

206 
(* 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

207 

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

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

212 
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

213 
==> 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

232 

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 
lemma Follows_trans: 
24892  235 
"[ 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

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

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

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

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

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

241 
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

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

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

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

245 

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

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

247 

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

249 
"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

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

251 

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

253 
"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

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

255 

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

257 
"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

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

259 

24892  260 
lemma Follows_imp_LeadsTo: 
261 
"[ 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

262 
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

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

264 

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

265 
lemma Follows_LeadsTo_pfixLe: 
24892  266 
"[ 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

267 
==> 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

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

269 

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

270 
lemma Follows_LeadsTo_pfixGe: 
24892  271 
"[ 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

272 
==> 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

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

274 

24892  275 
lemma Always_Follows1: 
276 
"[ 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

277 
\<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

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

279 
apply (simp add: INT_iff, auto) 
24892  280 
apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

281 
and A = "{s \<in> state. <k, h (s)> \<in> r}" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

282 
and A' = "{s \<in> state. <k, f(s)> \<in> r}" in Always_LeadsTo_weaken) 
24892  283 
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

284 
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

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

286 
apply (drule Always_Int_I, assumption) 
24892  287 
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

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

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

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

291 

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

292 

24892  293 
lemma Always_Follows2: 
294 
"[ 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

295 
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

296 
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

297 
apply (simp add: INT_iff, auto) 
24892  298 
apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }" 
299 
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

300 
and A' = "{s \<in> state. <k, f (s) > \<in> r}" in Always_LeadsTo_weaken) 
24892  301 
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

302 
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

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

304 
apply (drule Always_Int_I, assumption) 
24892  305 
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

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

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

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

309 

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

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

311 

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

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

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

314 

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

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

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

317 

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

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

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

320 

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

321 
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

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

323 

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

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

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

328 
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

329 

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

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

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

334 
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

335 

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

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

339 
==> F \<in> Always({s \<in> state. f1(s) \<union> g1(s) \<subseteq> f(s) \<union> g(s)})" 

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

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

341 

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

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

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

346 
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

347 

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

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

349 

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

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

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

352 

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

354 
"[ 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

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

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

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

358 

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

359 
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

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

361 

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

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

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

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

367 

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

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

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

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

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

372 

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

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

374 
"[ <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

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

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

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

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

379 

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

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

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

383 
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

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

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

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

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

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

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

390 

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

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

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

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

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

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

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

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

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

400 

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

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

402 
"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

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

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

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

406 

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

408 
"[ 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

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

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

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

412 
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

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

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

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

416 

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

417 
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

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

419 

24892  420 
lemma munion_mono: 
421 
"[ <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

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

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

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

425 
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

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

427 

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

428 
lemma increasing_munion: 
24892  429 
"[ F \<in> Increasing.increasing(Mult(A), MultLe(A,r), f); 
430 
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

431 
==> 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

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

433 

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

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

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

437 
==> 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

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

439 

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

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

443 
\<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

444 
==> 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

445 
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

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

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

448 

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

451 
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

452 
==> 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

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

454 

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

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

456 

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

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

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

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

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

463 
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

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

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

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

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

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

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

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

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

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

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

474 

14052  475 
end 