src/HOL/UNITY/ProgressSets.thy
 author paulson Mon Mar 10 16:21:06 2003 +0100 (2003-03-10) changeset 13853 89131afa9f01 child 13861 0c18f31d901a permissions -rw-r--r--
New theory ProgressSets. Definition of closure sets
```     1 (*  Title:      HOL/UNITY/ProgressSets
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   2003  University of Cambridge
```
```     5
```
```     6 Progress Sets.  From
```
```     7
```
```     8     David Meier and Beverly Sanders,
```
```     9     Composing Leads-to Properties
```
```    10     Theoretical Computer Science 243:1-2 (2000), 339-361.
```
```    11 *)
```
```    12
```
```    13 header{*Progress Sets*}
```
```    14
```
```    15 theory ProgressSets = Transformers:
```
```    16
```
```    17 constdefs
```
```    18   closure_set :: "'a set set => bool"
```
```    19    "closure_set C ==
```
```    20 	 (\<forall>D. D \<subseteq> C --> \<Inter>D \<in> C) & (\<forall>D. D \<subseteq> C --> \<Union>D \<in> C)"
```
```    21
```
```    22   cl :: "['a set set, 'a set] => 'a set"
```
```    23    --{*short for ``closure''*}
```
```    24    "cl C r == \<Inter>{x. x\<in>C & r \<subseteq> x}"
```
```    25
```
```    26 lemma UNIV_in_closure_set: "closure_set C ==> UNIV \<in> C"
```
```    27 by (force simp add: closure_set_def)
```
```    28
```
```    29 lemma empty_in_closure_set: "closure_set C ==> {} \<in> C"
```
```    30 by (force simp add: closure_set_def)
```
```    31
```
```    32 lemma Union_in_closure_set: "[|D \<subseteq> C; closure_set C|] ==> \<Union>D \<in> C"
```
```    33 by (simp add: closure_set_def)
```
```    34
```
```    35 lemma Inter_in_closure_set: "[|D \<subseteq> C; closure_set C|] ==> \<Inter>D \<in> C"
```
```    36 by (simp add: closure_set_def)
```
```    37
```
```    38 lemma UN_in_closure_set:
```
```    39      "[|closure_set C; !!i. i\<in>I ==> r i \<in> C|] ==> (\<Union>i\<in>I. r i) \<in> C"
```
```    40 apply (simp add: Set.UN_eq)
```
```    41 apply (blast intro: Union_in_closure_set)
```
```    42 done
```
```    43
```
```    44 lemma IN_in_closure_set:
```
```    45      "[|closure_set C; !!i. i\<in>I ==> r i \<in> C|] ==> (\<Inter>i\<in>I. r i)  \<in> C"
```
```    46 apply (simp add: INT_eq)
```
```    47 apply (blast intro: Inter_in_closure_set)
```
```    48 done
```
```    49
```
```    50 lemma Un_in_closure_set: "[|x\<in>C; y\<in>C; closure_set C|] ==> x\<union>y \<in> C"
```
```    51 apply (simp only: Un_eq_Union)
```
```    52 apply (blast intro: Union_in_closure_set)
```
```    53 done
```
```    54
```
```    55 lemma Int_in_closure_set: "[|x\<in>C; y\<in>C; closure_set C|] ==> x\<inter>y \<in> C"
```
```    56 apply (simp only: Int_eq_Inter)
```
```    57 apply (blast intro: Inter_in_closure_set)
```
```    58 done
```
```    59
```
```    60 lemma closure_set_stable: "closure_set {X. F \<in> stable X}"
```
```    61 by (simp add: closure_set_def stable_def constrains_def, blast)
```
```    62
```
```    63 text{*The next three results state that @{term "cl C r"} is the minimal
```
```    64  element of @{term C} that includes @{term r}.*}
```
```    65 lemma cl_in_closure_set: "closure_set C ==> cl C r \<in> C"
```
```    66 apply (simp add: closure_set_def cl_def)
```
```    67 apply (erule conjE)
```
```    68 apply (drule spec, erule mp, blast)
```
```    69 done
```
```    70
```
```    71 lemma cl_least: "[|c\<in>C; r\<subseteq>c|] ==> cl C r \<subseteq> c"
```
```    72 by (force simp add: cl_def)
```
```    73
```
```    74 text{*The next three lemmas constitute assertion (4.61)*}
```
```    75 lemma cl_mono: "r \<subseteq> r' ==> cl C r \<subseteq> cl C r'"
```
```    76 by (simp add: cl_def, blast)
```
```    77
```
```    78 lemma subset_cl: "r \<subseteq> cl C r"
```
```    79 by (simp add: cl_def, blast)
```
```    80
```
```    81 lemma cl_UN_subset: "(\<Union>i\<in>I. cl C (r i)) \<subseteq> cl C (\<Union>i\<in>I. r i)"
```
```    82 by (simp add: cl_def, blast)
```
```    83
```
```    84 lemma cl_Un: "closure_set C ==> cl C (r\<union>s) = cl C r \<union> cl C s"
```
```    85 apply (rule equalityI)
```
```    86  prefer 2
```
```    87   apply (simp add: cl_def, blast)
```
```    88 apply (rule cl_least)
```
```    89  apply (blast intro: Un_in_closure_set cl_in_closure_set)
```
```    90 apply (blast intro: subset_cl [THEN subsetD])
```
```    91 done
```
```    92
```
```    93 lemma cl_UN: "closure_set C ==> cl C (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl C (r i))"
```
```    94 apply (rule equalityI)
```
```    95  prefer 2
```
```    96   apply (simp add: cl_def, blast)
```
```    97 apply (rule cl_least)
```
```    98  apply (blast intro: UN_in_closure_set cl_in_closure_set)
```
```    99 apply (blast intro: subset_cl [THEN subsetD])
```
```   100 done
```
```   101
```
```   102 lemma cl_idem [simp]: "cl C (cl C r) = cl C r"
```
```   103 by (simp add: cl_def, blast)
```
```   104
```
```   105 lemma cl_ident: "r\<in>C ==> cl C r = r"
```
```   106 by (force simp add: cl_def)
```
```   107
```
```   108 text{*Assertion (4.62)*}
```
```   109 lemma cl_ident_iff: "closure_set C ==> (cl C r = r) = (r\<in>C)"
```
```   110 apply (rule iffI)
```
```   111  apply (erule subst)
```
```   112  apply (erule cl_in_closure_set)
```
```   113 apply (erule cl_ident)
```
```   114 done
```
```   115
```
```   116 end
```