src/HOL/UNITY/Project.thy
changeset 7826 c6a8b73b6c2a
parent 7689 affe0c2fdfbf
child 7878 43b03d412b82
     1.1 --- a/src/HOL/UNITY/Project.thy	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Project.thy	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -8,4 +8,19 @@
     1.4  Inheritance of GUARANTEES properties under extension
     1.5  *)
     1.6  
     1.7 -Project = Extend
     1.8 +Project = Extend +
     1.9 +
    1.10 +constdefs
    1.11 +  projecting :: "['c program => 'c set, 'a*'b => 'c, 
    1.12 +		  'a program, 'c program set, 'a program set] => bool"
    1.13 +  "projecting C h F X' X ==
    1.14 +     ALL G. extend h F Join G : X' --> F Join project (C G) h G : X"
    1.15 +
    1.16 +  extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
    1.17 +		 'c program set, 'c program set, 'a program set] => bool"
    1.18 +  "extending C h F X' Y' Y ==
    1.19 +     ALL G. F Join project (C G) h G : Y & extend h F Join G : X' &
    1.20 +            Disjoint (extend h F) G
    1.21 +            --> extend h F Join G : Y'"
    1.22 +
    1.23 +end