|
7186
|
1 |
(* Title: HOL/UNITY/Lift_prog.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1999 University of Cambridge
|
|
|
5 |
|
|
|
6 |
lift_prog, etc: replication of components
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Lift_prog = Union + Comp +
|
|
|
10 |
|
|
|
11 |
constdefs
|
|
|
12 |
|
|
|
13 |
lift_set :: "['a, 'b set] => ('a => 'b) set"
|
|
|
14 |
"lift_set i A == {f. f i : A}"
|
|
|
15 |
|
|
|
16 |
drop_set :: "['a, ('a=>'b) set] => 'b set"
|
|
|
17 |
"drop_set i A == (%f. f i) `` A"
|
|
|
18 |
|
|
|
19 |
lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
|
|
|
20 |
"lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}"
|
|
|
21 |
|
|
|
22 |
drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
|
|
|
23 |
"drop_act i act == (%(f,f'). (f i, f' i)) `` act"
|
|
|
24 |
|
|
|
25 |
lift_prog :: "['a, 'b program] => ('a => 'b) program"
|
|
|
26 |
"lift_prog i F ==
|
|
|
27 |
mk_program (lift_set i (Init F),
|
|
|
28 |
lift_act i `` Acts F)"
|
|
|
29 |
|
|
|
30 |
drop_prog :: "['a, ('a=>'b) program] => 'b program"
|
|
|
31 |
"drop_prog i F ==
|
|
|
32 |
mk_program (drop_set i (Init F),
|
|
|
33 |
drop_act i `` (Acts F))"
|
|
|
34 |
|
|
|
35 |
(*simplifies the expression of specifications*)
|
|
|
36 |
constdefs
|
|
|
37 |
sub :: ['a, 'a=>'b] => 'b
|
|
|
38 |
"sub i f == f i"
|
|
|
39 |
|
|
|
40 |
|
|
|
41 |
end
|