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"
paulson@7630
     1
(*  Title:      HOL/UNITY/Project.ML
paulson@7630
     2
    ID:         $Id$
paulson@7630
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7630
     4
    Copyright   1999  University of Cambridge
paulson@7630
     5
paulson@7630
     6
Projections of state sets (also of actions and programs)
paulson@7630
     7
paulson@7630
     8
Inheritance of GUARANTEES properties under extension
paulson@7630
     9
*)
paulson@7630
    10
paulson@7826
    11
Project = Extend +
paulson@7826
    12
paulson@7826
    13
constdefs
paulson@7826
    14
  projecting :: "['c program => 'c set, 'a*'b => 'c, 
paulson@7826
    15
		  'a program, 'c program set, 'a program set] => bool"
paulson@7826
    16
  "projecting C h F X' X ==
paulson@7880
    17
     ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
paulson@7826
    18
paulson@7826
    19
  extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
paulson@7826
    20
		 'c program set, 'c program set, 'a program set] => bool"
paulson@7826
    21
  "extending C h F X' Y' Y ==
paulson@7880
    22
     ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
paulson@7878
    23
            Disjoint UNIV (extend h F) G
paulson@7826
    24
            --> extend h F Join G : Y'"
paulson@7826
    25
paulson@7826
    26
end