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

src/HOL/TLA/Stfun.thy

author | wenzelm |

Wed Sep 07 20:22:39 2005 +0200 (2005-09-07) | |

changeset 17309 | c43ed29bd197 |

parent 12607 | 16b63730cfbb |

child 21624 | 6f79647cf536 |

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

converted to Isar theory format;

1 (*

2 File: TLA/Stfun.thy

3 ID: $Id$

4 Author: Stephan Merz

5 Copyright: 1998 University of Munich

7 Theory Name: Stfun

8 Logic Image: HOL

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

11 *)

13 theory Stfun

14 imports Intensional

15 begin

17 typedecl state

19 instance state :: world ..

21 types

22 'a stfun = "state => 'a"

23 stpred = "bool stfun"

26 consts

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

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

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

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

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

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

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

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

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

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

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

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

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 defs

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

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

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

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

55 definitely be inconsistent.

56 *)

57 basevars_def: "stvars vs == range vs = UNIV"

59 ML {* use_legacy_bindings (the_context ()) *}

61 end