author | paulson |
Tue, 30 Nov 1999 16:54:10 +0100 | |
changeset 8041 | e3237d8c18d6 |
parent 7947 | b999c1ab9327 |
child 8122 | b43ad07660b9 |
permissions | -rw-r--r-- |
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 |
||
8041 | 9 |
Lift_prog = ELT + |
7186 | 10 |
|
11 |
constdefs |
|
12 |
||
7482 | 13 |
lift_map :: "['a, 'b * ('a => 'b)] => ('a => 'b)" |
14 |
"lift_map i == %(s,f). f(i := s)" |
|
15 |
||
7186 | 16 |
lift_set :: "['a, 'b set] => ('a => 'b) set" |
17 |
"lift_set i A == {f. f i : A}" |
|
18 |
||
19 |
drop_set :: "['a, ('a=>'b) set] => 'b set" |
|
20 |
"drop_set i A == (%f. f i) `` A" |
|
21 |
||
22 |
lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set" |
|
23 |
"lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}" |
|
24 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7688
diff
changeset
|
25 |
drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set" |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7688
diff
changeset
|
26 |
"drop_act i act == {(f i, f' i) | f f'. (f,f'): act}" |
7186 | 27 |
|
28 |
lift_prog :: "['a, 'b program] => ('a => 'b) program" |
|
29 |
"lift_prog i F == |
|
30 |
mk_program (lift_set i (Init F), |
|
31 |
lift_act i `` Acts F)" |
|
32 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7688
diff
changeset
|
33 |
(*Argument C allows weak safety laws to be projected*) |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
34 |
drop_prog :: "['a, ('a=>'b) set, ('a=>'b) program] => 'b program" |
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
35 |
"drop_prog i C F == |
7186 | 36 |
mk_program (drop_set i (Init F), |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7688
diff
changeset
|
37 |
drop_act i `` Restrict C `` (Acts F))" |
7186 | 38 |
|
39 |
(*simplifies the expression of specifications*) |
|
40 |
constdefs |
|
41 |
sub :: ['a, 'a=>'b] => 'b |
|
7947 | 42 |
"sub == %i f. f i" |
7186 | 43 |
|
44 |
||
45 |
end |