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

src/HOL/TLA/Stfun.thy

author | wenzelm |

Fri Oct 05 23:58:52 2001 +0200 (2001-10-05) | |

changeset 11703 | 6e5de8d4290a |

parent 6255 | db63752140c7 |

child 12338 | de0f4a63baa5 |

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

tuned;

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 :: term

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" stvars.

38 NOTE: There should not be duplicates in the tuple!

39 *)

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

42 syntax

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

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

46 translations

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

48 "_stvars" == "stvars"

50 rules

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

52 Note that vs may be a tuple of variables. The rule would be unsound

53 if vs contained duplicates.

54 *)

55 basevars "basevars vs ==> EX u. vs u = c"

56 base_pair "basevars (x,y) ==> basevars x & basevars y"

57 (* Since the unit type has just one value, any state function can be

58 regarded as "base". The following axiom can sometimes be useful

59 because it gives a trivial solution for "basevars" premises.

60 *)

61 unit_base "basevars (v::unit stfun)"

63 end