src/HOL/UNITY/Project.thy

updated;

(*  Title:      HOL/UNITY/Project.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1999  University of Cambridge

Projections of state sets (also of actions and programs)

Inheritance of GUARANTEES properties under extension
*)

Project = Extend +

constdefs
  projecting :: "['c program => 'c set, 'a*'b => 'c, 
		  'a program, 'c program set, 'a program set] => bool"
  "projecting C h F X' X ==
     ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"

  extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
		 'c program set, 'c program set, 'a program set] => bool"
  "extending C h F X' Y' Y ==
     ALL G. F Join project h (C G) G : Y & extend h F Join G : X'
            --> extend h F Join G : Y'"

end