wenzelm@3807

1 
(*

wenzelm@3807

2 
File: TLA/Stfun.thy

wenzelm@3807

3 
Author: Stephan Merz

wenzelm@6255

4 
Copyright: 1998 University of Munich

wenzelm@3807

5 

wenzelm@3807

6 
Theory Name: Stfun

wenzelm@3807

7 
Logic Image: HOL

wenzelm@3807

8 

wenzelm@6255

9 
States and state functions for TLA as an "intensional" logic.

wenzelm@3807

10 
*)

wenzelm@3807

11 

wenzelm@6255

12 
Stfun = Intensional +

wenzelm@3807

13 

wenzelm@3807

14 
types

wenzelm@3807

15 
state

wenzelm@3807

16 
'a stfun = "state => 'a"

wenzelm@3807

17 
stpred = "bool stfun"

wenzelm@3807

18 

wenzelm@3807

19 
arities

wenzelm@12338

20 
state :: type

wenzelm@6255

21 

wenzelm@6255

22 
instance

wenzelm@6255

23 
state :: world

wenzelm@3807

24 

wenzelm@3807

25 
consts

wenzelm@6255

26 
(* Formalizing type "state" would require formulas to be tagged with

wenzelm@6255

27 
their underlying state space and would result in a system that is

wenzelm@6255

28 
much harder to use. (Unlike Hoare logic or Unity, TLA has quantification

wenzelm@6255

29 
over state variables, and therefore one usually works with different

wenzelm@6255

30 
state spaces within a single specification.) Instead, "state" is just

wenzelm@6255

31 
an anonymous type whose only purpose is to provide "Skolem" constants.

wenzelm@6255

32 
Moreover, we do not define a type of state variables separate from that

wenzelm@6255

33 
of arbitrary state functions, again in order to simplify the definition

wenzelm@6255

34 
of flexible quantification later on. Nevertheless, we need to distinguish

wenzelm@6255

35 
state variables, mainly to define the enabledness of actions. The user

wenzelm@6255

36 
identifies (tuples of) "base" state variables in a specification via the

wenzelm@12607

37 
"meta predicate" basevars, which is defined here.

wenzelm@3807

38 
*)

wenzelm@6255

39 
stvars :: "'a stfun => bool"

wenzelm@3807

40 

wenzelm@3807

41 
syntax

wenzelm@6255

42 
"PRED" :: lift => 'a ("PRED _")

wenzelm@6255

43 
"_stvars" :: lift => bool ("basevars _")

wenzelm@3807

44 

wenzelm@3807

45 
translations

wenzelm@6255

46 
"PRED P" => "(P::state => _)"

wenzelm@6255

47 
"_stvars" == "stvars"

wenzelm@3807

48 

wenzelm@12607

49 
defs

wenzelm@6255

50 
(* Base variables may be assigned arbitrary (typecorrect) values.

wenzelm@12607

51 
Note that vs may be a tuple of variables. The correct identification

wenzelm@12607

52 
of base variables is up to the user who must take care not to

wenzelm@12607

53 
introduce an inconsistency. For example, "basevars (x,x)" would

wenzelm@12607

54 
definitely be inconsistent.

wenzelm@6255

55 
*)

wenzelm@12607

56 
basevars_def "stvars vs == range vs = UNIV"

wenzelm@3807

57 

wenzelm@3807

58 
end
