20 "drop_set i A == (%f. f i) `` A" |
20 "drop_set i A == (%f. f i) `` A" |
21 |
21 |
22 lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set" |
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}" |
23 "lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}" |
24 |
24 |
25 (*Argument C allows weak safety laws to be projected*) |
25 drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set" |
26 drop_act :: "[('a=>'b) set, 'a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set" |
26 "drop_act i act == {(f i, f' i) | f f'. (f,f'): act}" |
27 "drop_act C i act == {(f i, f' i) | f f'. (f,f'): act & f: C}" |
|
28 |
27 |
29 lift_prog :: "['a, 'b program] => ('a => 'b) program" |
28 lift_prog :: "['a, 'b program] => ('a => 'b) program" |
30 "lift_prog i F == |
29 "lift_prog i F == |
31 mk_program (lift_set i (Init F), |
30 mk_program (lift_set i (Init F), |
32 lift_act i `` Acts F)" |
31 lift_act i `` Acts F)" |
33 |
32 |
|
33 (*Argument C allows weak safety laws to be projected*) |
34 drop_prog :: "[('a=>'b) set, 'a, ('a=>'b) program] => 'b program" |
34 drop_prog :: "[('a=>'b) set, 'a, ('a=>'b) program] => 'b program" |
35 "drop_prog C i F == |
35 "drop_prog C i F == |
36 mk_program (drop_set i (Init F), |
36 mk_program (drop_set i (Init F), |
37 drop_act C i `` (Acts F))" |
37 drop_act i `` Restrict C `` (Acts F))" |
38 |
38 |
39 (*simplifies the expression of specifications*) |
39 (*simplifies the expression of specifications*) |
40 constdefs |
40 constdefs |
41 sub :: ['a, 'a=>'b] => 'b |
41 sub :: ['a, 'a=>'b] => 'b |
42 "sub i f == f i" |
42 "sub i f == f i" |