src/HOL/UNITY/ProgressSets.thy
changeset 35416 d8d7d1b785af
parent 32960 69916a850301
child 44106 0e018cbcc0de
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -19,13 +19,12 @@
     1.4  
     1.5  subsection {*Complete Lattices and the Operator @{term cl}*}
     1.6  
     1.7 -constdefs
     1.8 -  lattice :: "'a set set => bool"
     1.9 +definition lattice :: "'a set set => bool" where
    1.10     --{*Meier calls them closure sets, but they are just complete lattices*}
    1.11     "lattice L ==
    1.12           (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"
    1.13  
    1.14 -  cl :: "['a set set, 'a set] => 'a set"
    1.15 +definition cl :: "['a set set, 'a set] => 'a set" where
    1.16     --{*short for ``closure''*}
    1.17     "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}"
    1.18  
    1.19 @@ -143,12 +142,11 @@
    1.20  text{*A progress set satisfies certain closure conditions and is a 
    1.21  simple way of including the set @{term "wens_set F B"}.*}
    1.22  
    1.23 -constdefs 
    1.24 -  closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
    1.25 +definition closed :: "['a program, 'a set, 'a set,  'a set set] => bool" where
    1.26     "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
    1.27                                T \<inter> (B \<union> wp act M) \<in> L"
    1.28  
    1.29 -  progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
    1.30 +definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where
    1.31     "progress_set F T B ==
    1.32        {L. lattice L & B \<in> L & T \<in> L & closed F T B L}"
    1.33  
    1.34 @@ -324,12 +322,11 @@
    1.35  subsubsection {*Lattices and Relations*}
    1.36  text{*From Meier's thesis, section 4.5.3*}
    1.37  
    1.38 -constdefs
    1.39 -  relcl :: "'a set set => ('a * 'a) set"
    1.40 +definition relcl :: "'a set set => ('a * 'a) set" where
    1.41      -- {*Derived relation from a lattice*}
    1.42      "relcl L == {(x,y). y \<in> cl L {x}}"
    1.43    
    1.44 -  latticeof :: "('a * 'a) set => 'a set set"
    1.45 +definition latticeof :: "('a * 'a) set => 'a set set" where
    1.46      -- {*Derived lattice from a relation: the set of upwards-closed sets*}
    1.47      "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}"
    1.48  
    1.49 @@ -405,8 +402,7 @@
    1.50  
    1.51  subsubsection {*Decoupling Theorems*}
    1.52  
    1.53 -constdefs
    1.54 -  decoupled :: "['a program, 'a program] => bool"
    1.55 +definition decoupled :: "['a program, 'a program] => bool" where
    1.56     "decoupled F G ==
    1.57          \<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)"
    1.58  
    1.59 @@ -469,8 +465,7 @@
    1.60  subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
    1.61  
    1.62  subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
    1.63 -constdefs 
    1.64 -  commutes :: "['a program, 'a set, 'a set,  'a set set] => bool"
    1.65 +definition commutes :: "['a program, 'a set, 'a set,  'a set set] => bool" where
    1.66     "commutes F T B L ==
    1.67         \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> 
    1.68             cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
    1.69 @@ -511,8 +506,7 @@
    1.70  
    1.71  
    1.72  text{*Possibly move to Relation.thy, after @{term single_valued}*}
    1.73 -constdefs
    1.74 -  funof :: "[('a*'b)set, 'a] => 'b"
    1.75 +definition funof :: "[('a*'b)set, 'a] => 'b" where
    1.76     "funof r == (\<lambda>x. THE y. (x,y) \<in> r)"
    1.77  
    1.78  lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y"