# HG changeset patch
# User paulson
# Date 935571488 -7200
# Node ID 532841541d73a3307bf8b874850efb5c075962b0
# Parent  d15bfea7c9437373559a244522ae38e379415380
project constants

diff -r d15bfea7c943 -r 532841541d73 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Wed Aug 25 10:57:06 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy	Wed Aug 25 10:58:08 1999 +0200
@@ -15,13 +15,23 @@
   extend_set :: "['a*'b => 'c, 'a set] => 'c set"
     "extend_set h A == h `` (A Times UNIV)"
 
-  extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c * 'c) set"
+  project_set :: "['a*'b => 'c, 'c set] => 'a set"
+    "project_set h C == {x. EX y. h(x,y) : C}"
+
+  extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
     "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
 
+  project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
+    "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}"
+
   extend :: "['a*'b => 'c, 'a program] => 'c program"
     "extend h F == mk_program (extend_set h (Init F),
 			       extend_act h `` Acts F)"
 
+  project :: "['a*'b => 'c, 'c program] => 'a program"
+    "project h F == mk_program (project_set h (Init F),
+			        project_act h `` Acts F)"
+
 locale Extend =
   fixes 
     f       :: 'c => 'a