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