equal
deleted
inserted
replaced
17 |
17 |
18 theory ProgressSets imports Transformers begin |
18 theory ProgressSets imports Transformers begin |
19 |
19 |
20 subsection {*Complete Lattices and the Operator @{term cl}*} |
20 subsection {*Complete Lattices and the Operator @{term cl}*} |
21 |
21 |
22 constdefs |
22 definition lattice :: "'a set set => bool" where |
23 lattice :: "'a set set => bool" |
|
24 --{*Meier calls them closure sets, but they are just complete lattices*} |
23 --{*Meier calls them closure sets, but they are just complete lattices*} |
25 "lattice L == |
24 "lattice L == |
26 (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)" |
25 (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)" |
27 |
26 |
28 cl :: "['a set set, 'a set] => 'a set" |
27 definition cl :: "['a set set, 'a set] => 'a set" where |
29 --{*short for ``closure''*} |
28 --{*short for ``closure''*} |
30 "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}" |
29 "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}" |
31 |
30 |
32 lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L" |
31 lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L" |
33 by (force simp add: lattice_def) |
32 by (force simp add: lattice_def) |
141 |
140 |
142 subsection {*Progress Sets and the Main Lemma*} |
141 subsection {*Progress Sets and the Main Lemma*} |
143 text{*A progress set satisfies certain closure conditions and is a |
142 text{*A progress set satisfies certain closure conditions and is a |
144 simple way of including the set @{term "wens_set F B"}.*} |
143 simple way of including the set @{term "wens_set F B"}.*} |
145 |
144 |
146 constdefs |
145 definition closed :: "['a program, 'a set, 'a set, 'a set set] => bool" where |
147 closed :: "['a program, 'a set, 'a set, 'a set set] => bool" |
|
148 "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L --> |
146 "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L --> |
149 T \<inter> (B \<union> wp act M) \<in> L" |
147 T \<inter> (B \<union> wp act M) \<in> L" |
150 |
148 |
151 progress_set :: "['a program, 'a set, 'a set] => 'a set set set" |
149 definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where |
152 "progress_set F T B == |
150 "progress_set F T B == |
153 {L. lattice L & B \<in> L & T \<in> L & closed F T B L}" |
151 {L. lattice L & B \<in> L & T \<in> L & closed F T B L}" |
154 |
152 |
155 lemma closedD: |
153 lemma closedD: |
156 "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] |
154 "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] |
322 |
320 |
323 |
321 |
324 subsubsection {*Lattices and Relations*} |
322 subsubsection {*Lattices and Relations*} |
325 text{*From Meier's thesis, section 4.5.3*} |
323 text{*From Meier's thesis, section 4.5.3*} |
326 |
324 |
327 constdefs |
325 definition relcl :: "'a set set => ('a * 'a) set" where |
328 relcl :: "'a set set => ('a * 'a) set" |
|
329 -- {*Derived relation from a lattice*} |
326 -- {*Derived relation from a lattice*} |
330 "relcl L == {(x,y). y \<in> cl L {x}}" |
327 "relcl L == {(x,y). y \<in> cl L {x}}" |
331 |
328 |
332 latticeof :: "('a * 'a) set => 'a set set" |
329 definition latticeof :: "('a * 'a) set => 'a set set" where |
333 -- {*Derived lattice from a relation: the set of upwards-closed sets*} |
330 -- {*Derived lattice from a relation: the set of upwards-closed sets*} |
334 "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}" |
331 "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}" |
335 |
332 |
336 |
333 |
337 lemma relcl_refl: "(a,a) \<in> relcl L" |
334 lemma relcl_refl: "(a,a) \<in> relcl L" |
403 by (simp add: relcl_def cl_latticeof) |
400 by (simp add: relcl_def cl_latticeof) |
404 |
401 |
405 |
402 |
406 subsubsection {*Decoupling Theorems*} |
403 subsubsection {*Decoupling Theorems*} |
407 |
404 |
408 constdefs |
405 definition decoupled :: "['a program, 'a program] => bool" where |
409 decoupled :: "['a program, 'a program] => bool" |
|
410 "decoupled F G == |
406 "decoupled F G == |
411 \<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)" |
407 \<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)" |
412 |
408 |
413 |
409 |
414 text{*Rao's Decoupling Theorem*} |
410 text{*Rao's Decoupling Theorem*} |
467 |
463 |
468 |
464 |
469 subsection{*Composition Theorems Based on Monotonicity and Commutativity*} |
465 subsection{*Composition Theorems Based on Monotonicity and Commutativity*} |
470 |
466 |
471 subsubsection{*Commutativity of @{term "cl L"} and assignment.*} |
467 subsubsection{*Commutativity of @{term "cl L"} and assignment.*} |
472 constdefs |
468 definition commutes :: "['a program, 'a set, 'a set, 'a set set] => bool" where |
473 commutes :: "['a program, 'a set, 'a set, 'a set set] => bool" |
|
474 "commutes F T B L == |
469 "commutes F T B L == |
475 \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> |
470 \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> |
476 cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))" |
471 cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))" |
477 |
472 |
478 |
473 |
509 simp add: progress_set_def commutativity1_lemma commutes lattice BL TL) |
504 simp add: progress_set_def commutativity1_lemma commutes lattice BL TL) |
510 |
505 |
511 |
506 |
512 |
507 |
513 text{*Possibly move to Relation.thy, after @{term single_valued}*} |
508 text{*Possibly move to Relation.thy, after @{term single_valued}*} |
514 constdefs |
509 definition funof :: "[('a*'b)set, 'a] => 'b" where |
515 funof :: "[('a*'b)set, 'a] => 'b" |
|
516 "funof r == (\<lambda>x. THE y. (x,y) \<in> r)" |
510 "funof r == (\<lambda>x. THE y. (x,y) \<in> r)" |
517 |
511 |
518 lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y" |
512 lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y" |
519 by (simp add: funof_def single_valued_def, blast) |
513 by (simp add: funof_def single_valued_def, blast) |
520 |
514 |