|
41589
|
1 |
(* Title: HOL/TLA/Memory/RPCMemoryParams.thy
|
|
|
2 |
Author: Stephan Merz, University of Munich
|
|
21624
|
3 |
*)
|
|
3807
|
4 |
|
|
21624
|
5 |
header {* Basic declarations for the RPC-memory example *}
|
|
3807
|
6 |
|
|
17309
|
7 |
theory RPCMemoryParams
|
|
|
8 |
imports Main
|
|
|
9 |
begin
|
|
3807
|
10 |
|
|
42018
|
11 |
type_synonym bit = "bool"
|
|
|
12 |
(* Signal wires for the procedure interface.
|
|
|
13 |
Defined as bool for simplicity. All I should really need is
|
|
|
14 |
the existence of two distinct values. *)
|
|
3807
|
15 |
|
|
|
16 |
(* all of these are simple (HOL) types *)
|
|
11703
|
17 |
typedecl Locs (* "syntactic" value type *)
|
|
|
18 |
typedecl Vals (* "syntactic" value type *)
|
|
|
19 |
typedecl PrIds (* process id's *)
|
|
3807
|
20 |
|
|
|
21 |
end
|