1(* Title: ZF/UNITY/Follows.thy 2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory 3 Copyright 2002 University of Cambridge 4 5Theory ported from HOL. 6*) 7 8section\<open>The "Follows" relation of Charpentier and Sivilotte\<close> 9 10theory Follows imports SubstAx Increasing begin 11 12definition 13 Follows :: "[i, i, i=>i, i=>i] => i" where 14 "Follows(A, r, f, g) == 15 Increasing(A, r, g) Int 16 Increasing(A, r,f) Int 17 Always({s \<in> state. <f(s), g(s)>:r}) Int 18 (\<Inter>k \<in> A. {s \<in> state. <k, g(s)>:r} \<longmapsto>w {s \<in> state. <k,f(s)>:r})" 19 20abbreviation 21 Incr :: "[i=>i]=>i" where 22 "Incr(f) == Increasing(list(nat), prefix(nat), f)" 23 24abbreviation 25 n_Incr :: "[i=>i]=>i" where 26 "n_Incr(f) == Increasing(nat, Le, f)" 27 28abbreviation 29 s_Incr :: "[i=>i]=>i" where 30 "s_Incr(f) == Increasing(Pow(nat), SetLe(nat), f)" 31 32abbreviation 33 m_Incr :: "[i=>i]=>i" where 34 "m_Incr(f) == Increasing(Mult(nat), MultLe(nat, Le), f)" 35 36abbreviation 37 n_Fols :: "[i=>i, i=>i]=>i" (infixl "n'_Fols" 65) where 38 "f n_Fols g == Follows(nat, Le, f, g)" 39 40abbreviation 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)" 44 45 46(*Does this hold for "invariant"?*) 47 48lemma Follows_cong: 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')" 50by (simp add: Increasing_def Follows_def) 51 52 53lemma subset_Always_comp: 54"[| mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==> 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})" 56apply (unfold mono1_def metacomp_def) 57apply (auto simp add: Always_eq_includes_reachable) 58done 59 60lemma 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 |] ==> 63 F \<in> Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})" 64by (blast intro: subset_Always_comp [THEN subsetD]) 65 66 67lemma 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 |] 72 ==> F \<in> Always({x \<in> state. <h(f1(x), g1(x)), h(f(x), g(x))> \<in> t})" 73apply (auto simp add: Always_eq_includes_reachable mono2_def) 74apply (auto dest!: subsetD) 75done 76 77(* comp LeadsTo *) 78 79lemma 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} \<longmapsto>w {s \<in> state. <j,f(s)> \<in> r}) <= 83 (\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} \<longmapsto>w {x \<in> state. <k, (h comp f)(x)> \<in> s})" 84 85apply (unfold mono1_def metacomp_def, clarify) 86apply (simp_all (no_asm_use) add: INT_iff) 87apply auto 88apply (rule single_LeadsTo_I) 89prefer 2 apply (blast dest: LeadsTo_type [THEN subsetD], auto) 90apply (rotate_tac 5) 91apply (drule_tac x = "g (sa) " in bspec) 92apply (erule_tac [2] LeadsTo_weaken) 93apply (auto simp add: part_order_def refl_def) 94apply (rule_tac b = "h (g (sa))" in trans_onD) 95apply blast 96apply auto 97done 98 99lemma imp_LeadsTo_comp: 100"[| F:(\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} \<longmapsto>w {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 |] ==> 103 F:(\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} \<longmapsto>w {x \<in> state. <k, (h comp f)(x)> \<in> s})" 104apply (rule subset_LeadsTo_comp [THEN subsetD], auto) 105done 106 107lemma 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} \<longmapsto>w {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 |] ==> 112 F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f1(x), g(x))> \<in> t}" 113apply (unfold mono2_def Increasing_def) 114apply (rule single_LeadsTo_I, auto) 115apply (drule_tac x = "g (sa) " and A = B in bspec) 116apply auto 117apply (drule_tac x = "f (sa) " and P = "%j. F \<in> X(j) \<longmapsto>w Y(j)" for X Y in bspec) 118apply auto 119apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast) 120apply auto 121apply (force simp add: part_order_def refl_def) 122apply (force simp add: part_order_def refl_def) 123apply (drule_tac x = "f1 (x)" and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. P (x,y,u)" for P in bspec [THEN bspec]) 124apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. P (x,y) \<longrightarrow> d (x,y) \<in> t" for P d in bspec [THEN bspec]) 125apply auto 126apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD) 127apply (auto simp add: part_order_def) 128done 129 130lemma 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} \<longmapsto>w {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 |] ==> 135 F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f(x), g1(x))> \<in> t}" 136apply (unfold mono2_def Increasing_def) 137apply (rule single_LeadsTo_I, auto) 138apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (X (k))" for X in bspec) 139apply auto 140apply (drule_tac x = "g (sa) " in bspec) 141apply auto 142apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast) 143apply auto 144apply (force simp add: part_order_def refl_def) 145apply (force simp add: part_order_def refl_def) 146apply (drule_tac x = "f (x) " and x1 = "f (sa) " in bspec [THEN bspec]) 147apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. P (x,y) \<longrightarrow> d (x,y) \<in> t" for P d in bspec [THEN bspec]) 148apply auto 149apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD) 150apply (auto simp add: part_order_def) 151done 152 153(** This general result is used to prove Follows Un, munion, etc. **) 154lemma imp_LeadsTo_comp2: 155"[| F \<in> Increasing(A, r, f1) \<inter> Increasing(B, s, g); 156 \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} \<longmapsto>w {s \<in> state. <j,f1(s)> \<in> r}; 157 \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} \<longmapsto>w {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 |] 160 ==> F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f1(x), g1(x))> \<in> t}" 161apply (rule_tac B = "{x \<in> state. <k, h (f1 (x), g (x))> \<in> t}" in LeadsTo_Trans) 162apply (blast intro: imp_LeadsTo_comp_right) 163apply (blast intro: imp_LeadsTo_comp_left) 164done 165 166(* Follows type *) 167lemma Follows_type: "Follows(A, r, f, g)<=program" 168apply (unfold Follows_def) 169apply (blast dest: Increasing_type [THEN subsetD]) 170done 171 172lemma Follows_into_program [TC]: "F \<in> Follows(A, r, f, g) ==> F \<in> program" 173by (blast dest: Follows_type [THEN subsetD]) 174 175lemma FollowsD: 176"F \<in> Follows(A, r, f, g)==> 177 F \<in> program & (\<exists>a. a \<in> A) & (\<forall>x \<in> state. f(x):A & g(x):A)" 178apply (unfold Follows_def) 179apply (blast dest: IncreasingD) 180done 181 182lemma Follows_constantI: 183 "[| F \<in> program; c \<in> A; refl(A, r) |] ==> F \<in> Follows(A, r, %x. c, %x. c)" 184apply (unfold Follows_def, auto) 185apply (auto simp add: refl_def) 186done 187 188lemma subset_Follows_comp: 189"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] 190 ==> Follows(A, r, f, g) \<subseteq> Follows(B, s, h comp f, h comp g)" 191apply (unfold Follows_def, clarify) 192apply (frule_tac f = g in IncreasingD) 193apply (frule_tac f = f in IncreasingD) 194apply (rule IntI) 195apply (rule_tac [2] h = h in imp_LeadsTo_comp) 196prefer 5 apply assumption 197apply (auto intro: imp_Increasing_comp imp_Always_comp simp del: INT_simps) 198done 199 200lemma imp_Follows_comp: 201"[| F \<in> Follows(A, r, f, g); mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] 202 ==> F \<in> Follows(B, s, h comp f, h comp g)" 203apply (blast intro: subset_Follows_comp [THEN subsetD]) 204done 205 206(* 2-place monotone operation \<in> this general result is used to prove Follows_Un, Follows_munion *) 207 208(* 2-place monotone operation \<in> this general result is 209 used to prove Follows_Un, Follows_munion *) 210lemma 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) |] 213 ==> F \<in> Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))" 214apply (unfold Follows_def, clarify) 215apply (frule_tac f = g in IncreasingD) 216apply (frule_tac f = f in IncreasingD) 217apply (rule IntI, safe) 218apply (rule_tac [3] h = h in imp_Always_comp2) 219prefer 5 apply assumption 220apply (rule_tac [2] h = h in imp_Increasing_comp2) 221prefer 4 apply assumption 222apply (rule_tac h = h in imp_Increasing_comp2) 223prefer 3 apply assumption 224apply simp_all 225apply (blast dest!: IncreasingD) 226apply (rule_tac h = h in imp_LeadsTo_comp2) 227prefer 4 apply assumption 228apply auto 229 prefer 3 apply (simp add: mono2_def) 230apply (blast dest: IncreasingD)+ 231done 232 233 234lemma Follows_trans: 235 "[| F \<in> Follows(A, r, f, g); F \<in> Follows(A,r, g, h); 236 trans[A](r) |] ==> F \<in> Follows(A, r, f, h)" 237apply (frule_tac f = f in FollowsD) 238apply (frule_tac f = g in FollowsD) 239apply (simp add: Follows_def) 240apply (simp add: Always_eq_includes_reachable INT_iff, auto) 241apply (rule_tac [2] B = "{s \<in> state. <k, g (s) > \<in> r}" in LeadsTo_Trans) 242apply (rule_tac b = "g (x) " in trans_onD) 243apply blast+ 244done 245 246(** Destruction rules for Follows **) 247 248lemma Follows_imp_Increasing_left: 249 "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, f)" 250by (unfold Follows_def, blast) 251 252lemma Follows_imp_Increasing_right: 253 "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, g)" 254by (unfold Follows_def, blast) 255 256lemma Follows_imp_Always: 257 "F :Follows(A, r, f, g) ==> F \<in> Always({s \<in> state. <f(s),g(s)> \<in> r})" 258by (unfold Follows_def, blast) 259 260lemma Follows_imp_LeadsTo: 261 "[| F \<in> Follows(A, r, f, g); k \<in> A |] ==> 262 F: {s \<in> state. <k,g(s)> \<in> r } \<longmapsto>w {s \<in> state. <k,f(s)> \<in> r}" 263by (unfold Follows_def, blast) 264 265lemma Follows_LeadsTo_pfixLe: 266 "[| F \<in> Follows(list(nat), gen_prefix(nat, Le), f, g); k \<in> list(nat) |] 267 ==> F \<in> {s \<in> state. k pfixLe g(s)} \<longmapsto>w {s \<in> state. k pfixLe f(s)}" 268by (blast intro: Follows_imp_LeadsTo) 269 270lemma Follows_LeadsTo_pfixGe: 271 "[| F \<in> Follows(list(nat), gen_prefix(nat, Ge), f, g); k \<in> list(nat) |] 272 ==> F \<in> {s \<in> state. k pfixGe g(s)} \<longmapsto>w {s \<in> state. k pfixGe f(s)}" 273by (blast intro: Follows_imp_LeadsTo) 274 275lemma Always_Follows1: 276"[| F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h); 277 \<forall>x \<in> state. g(x):A |] ==> F \<in> Follows(A, r, g, h)" 278apply (unfold Follows_def Increasing_def Stable_def) 279apply (simp add: INT_iff, auto) 280apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}" 281 and A = "{s \<in> state. <k, h (s)> \<in> r}" 282 and A' = "{s \<in> state. <k, f(s)> \<in> r}" in Always_LeadsTo_weaken) 283apply (erule_tac A = "{s \<in> state. <k,f(s) > \<in> r}" 284 and A' = "{s \<in> state. <k,f(s) > \<in> r}" in Always_Constrains_weaken) 285apply auto 286apply (drule Always_Int_I, assumption) 287apply (erule_tac A = "{s \<in> state. f(s)=g(s)} \<inter> {s \<in> state. <f(s), h(s)> \<in> r}" 288 in Always_weaken) 289apply auto 290done 291 292 293lemma Always_Follows2: 294"[| F \<in> Always({s \<in> state. g(s) = h(s)}); 295 F \<in> Follows(A, r, f, g); \<forall>x \<in> state. h(x):A |] ==> F \<in> Follows(A, r, f, h)" 296apply (unfold Follows_def Increasing_def Stable_def) 297apply (simp add: INT_iff, auto) 298apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }" 299 and A = "{s \<in> state. <k, g (s) > \<in> r}" 300 and A' = "{s \<in> state. <k, f (s) > \<in> r}" in Always_LeadsTo_weaken) 301apply (erule_tac A = "{s \<in> state. <k, g(s)> \<in> r}" 302 and A' = "{s \<in> state. <k, g(s)> \<in> r}" in Always_Constrains_weaken) 303apply auto 304apply (drule Always_Int_I, assumption) 305apply (erule_tac A = "{s \<in> state. g(s)=h(s)} \<inter> {s \<in> state. <f(s), g(s)> \<in> r}" 306 in Always_weaken) 307apply auto 308done 309 310(** Union properties (with the subset ordering) **) 311 312lemma refl_SetLe [simp]: "refl(Pow(A), SetLe(A))" 313by (unfold refl_def SetLe_def, auto) 314 315lemma trans_on_SetLe [simp]: "trans[Pow(A)](SetLe(A))" 316by (unfold trans_on_def SetLe_def, auto) 317 318lemma antisym_SetLe [simp]: "antisym(SetLe(A))" 319by (unfold antisym_def SetLe_def, auto) 320 321lemma part_order_SetLe [simp]: "part_order(Pow(A), SetLe(A))" 322by (unfold part_order_def, auto) 323 324lemma increasing_Un: 325 "[| F \<in> Increasing.increasing(Pow(A), SetLe(A), f); 326 F \<in> Increasing.increasing(Pow(A), SetLe(A), g) |] 327 ==> F \<in> Increasing.increasing(Pow(A), SetLe(A), %x. f(x) \<union> g(x))" 328by (rule_tac h = "(Un)" in imp_increasing_comp2, auto) 329 330lemma Increasing_Un: 331 "[| F \<in> Increasing(Pow(A), SetLe(A), f); 332 F \<in> Increasing(Pow(A), SetLe(A), g) |] 333 ==> F \<in> Increasing(Pow(A), SetLe(A), %x. f(x) \<union> g(x))" 334by (rule_tac h = "(Un)" in imp_Increasing_comp2, auto) 335 336lemma Always_Un: 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)})" 340by (simp add: Always_eq_includes_reachable, blast) 341 342lemma Follows_Un: 343"[| F \<in> Follows(Pow(A), SetLe(A), f1, f); 344 F \<in> Follows(Pow(A), SetLe(A), g1, g) |] 345 ==> F \<in> Follows(Pow(A), SetLe(A), %s. f1(s) \<union> g1(s), %s. f(s) \<union> g(s))" 346by (rule_tac h = "(Un)" in imp_Follows_comp2, auto) 347 348(** Multiset union properties (with the MultLe ordering) **) 349 350lemma refl_MultLe [simp]: "refl(Mult(A), MultLe(A,r))" 351by (unfold MultLe_def refl_def, auto) 352 353lemma MultLe_refl1 [simp]: 354 "[| multiset(M); mset_of(M)<=A |] ==> <M, M> \<in> MultLe(A, r)" 355apply (unfold MultLe_def id_def lam_def) 356apply (auto simp add: Mult_iff_multiset) 357done 358 359lemma MultLe_refl2 [simp]: "M \<in> Mult(A) ==> <M, M> \<in> MultLe(A, r)" 360by (unfold MultLe_def id_def lam_def, auto) 361 362 363lemma trans_on_MultLe [simp]: "trans[Mult(A)](MultLe(A,r))" 364apply (unfold MultLe_def trans_on_def) 365apply (auto intro: trancl_trans simp add: multirel_def) 366done 367 368lemma MultLe_type: "MultLe(A, r)<= (Mult(A) * Mult(A))" 369apply (unfold MultLe_def, auto) 370apply (drule multirel_type [THEN subsetD], auto) 371done 372 373lemma MultLe_trans: 374 "[| <M,K> \<in> MultLe(A,r); <K,N> \<in> MultLe(A,r) |] ==> <M,N> \<in> MultLe(A,r)" 375apply (cut_tac A=A in trans_on_MultLe) 376apply (drule trans_onD, assumption) 377apply (auto dest: MultLe_type [THEN subsetD]) 378done 379 380lemma part_order_imp_part_ord: 381 "part_order(A, r) ==> part_ord(A, r-id(A))" 382apply (unfold part_order_def part_ord_def) 383apply (simp add: refl_def id_def lam_def irrefl_def, auto) 384apply (simp (no_asm) add: trans_on_def) 385apply auto 386apply (blast dest: trans_onD) 387apply (simp (no_asm_use) add: antisym_def) 388apply auto 389done 390 391lemma antisym_MultLe [simp]: 392 "part_order(A, r) ==> antisym(MultLe(A,r))" 393apply (unfold MultLe_def antisym_def) 394apply (drule part_order_imp_part_ord, auto) 395apply (drule irrefl_on_multirel) 396apply (frule multirel_type [THEN subsetD]) 397apply (drule multirel_trans) 398apply (auto simp add: irrefl_def) 399done 400 401lemma part_order_MultLe [simp]: 402 "part_order(A, r) ==> part_order(Mult(A), MultLe(A, r))" 403apply (frule antisym_MultLe) 404apply (auto simp add: part_order_def) 405done 406 407lemma empty_le_MultLe [simp]: 408"[| multiset(M); mset_of(M)<= A|] ==> <0, M> \<in> MultLe(A, r)" 409apply (unfold MultLe_def) 410apply (case_tac "M=0") 411apply (auto simp add: FiniteFun.intros) 412apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel (A, r - id (A))") 413apply (rule_tac [2] one_step_implies_multirel) 414apply (auto simp add: Mult_iff_multiset) 415done 416 417lemma empty_le_MultLe2 [simp]: "M \<in> Mult(A) ==> <0, M> \<in> MultLe(A, r)" 418by (simp add: Mult_iff_multiset) 419 420lemma munion_mono: 421"[| <M, N> \<in> MultLe(A, r); <K, L> \<in> MultLe(A, r) |] ==> 422 <M +# K, N +# L> \<in> MultLe(A, r)" 423apply (unfold MultLe_def) 424apply (auto intro: munion_multirel_mono1 munion_multirel_mono2 425 munion_multirel_mono multiset_into_Mult simp add: Mult_iff_multiset) 426done 427 428lemma increasing_munion: 429 "[| F \<in> Increasing.increasing(Mult(A), MultLe(A,r), f); 430 F \<in> Increasing.increasing(Mult(A), MultLe(A,r), g) |] 431 ==> F \<in> Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))" 432by (rule_tac h = munion in imp_increasing_comp2, auto) 433 434lemma Increasing_munion: 435 "[| F \<in> Increasing(Mult(A), MultLe(A,r), f); 436 F \<in> Increasing(Mult(A), MultLe(A,r), g)|] 437 ==> F \<in> Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))" 438by (rule_tac h = munion in imp_Increasing_comp2, auto) 439 440lemma 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)|] 444 ==> F \<in> Always({s \<in> state. <f1(s) +# g1(s), f(s) +# g(s)> \<in> MultLe(A,r)})" 445apply (rule_tac h = munion in imp_Always_comp2, simp_all) 446apply (blast intro: munion_mono, simp_all) 447done 448 449lemma Follows_munion: 450"[| F \<in> Follows(Mult(A), MultLe(A, r), f1, f); 451 F \<in> Follows(Mult(A), MultLe(A, r), g1, g) |] 452 ==> F \<in> Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))" 453by (rule_tac h = munion in imp_Follows_comp2, auto) 454 455(** Used in ClientImp **) 456 457lemma 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), 464 %x. msetsum(%i. f(i, x), I, A))" 465apply (erule rev_mp) 466apply (drule Finite_into_Fin) 467apply (erule Fin_induct) 468apply (simp (no_asm_simp)) 469apply (rule Follows_constantI) 470apply (simp_all (no_asm_simp) add: FiniteFun.intros) 471apply auto 472apply (rule Follows_munion, auto) 473done 474 475end 476