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"
```