--- 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