src/HOL/UNITY/Project.thy
author paulson
Mon Oct 18 16:16:03 1999 +0200 (1999-10-18)
changeset 7880 62fb24e28e5e
parent 7878 43b03d412b82
child 7947 b999c1ab9327
permissions -rw-r--r--
exchanged the first two args of "project" and "drop_prog"
     1 (*  Title:      HOL/UNITY/Project.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 
     6 Projections of state sets (also of actions and programs)
     7 
     8 Inheritance of GUARANTEES properties under extension
     9 *)
    10 
    11 Project = Extend +
    12 
    13 constdefs
    14   projecting :: "['c program => 'c set, 'a*'b => 'c, 
    15 		  'a program, 'c program set, 'a program set] => bool"
    16   "projecting C h F X' X ==
    17      ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
    18 
    19   extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
    20 		 'c program set, 'c program set, 'a program set] => bool"
    21   "extending C h F X' Y' Y ==
    22      ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
    23             Disjoint UNIV (extend h F) G
    24             --> extend h F Join G : Y'"
    25 
    26 end