summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/TLA/Stfun.thy

author | nipkow |

Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) | |

changeset 15140 | 322485b816ac |

parent 12607 | 16b63730cfbb |

child 17309 | c43ed29bd197 |

permissions | -rw-r--r-- |

import -> imports

1 (*

2 File: TLA/Stfun.thy

3 Author: Stephan Merz

4 Copyright: 1998 University of Munich

6 Theory Name: Stfun

7 Logic Image: HOL

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

10 *)

12 Stfun = Intensional +

14 types

15 state

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

17 stpred = "bool stfun"

19 arities

20 state :: type

22 instance

23 state :: world

25 consts

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

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

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

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

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

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

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

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

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

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

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

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

38 *)

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

41 syntax

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

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

45 translations

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

47 "_stvars" == "stvars"

49 defs

50 (* Base variables may be assigned arbitrary (type-correct) values.

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

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

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

54 definitely be inconsistent.

55 *)

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

58 end