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

src/HOL/TLA/Stfun.thy

author | wenzelm |

Wed Oct 08 11:50:33 1997 +0200 (1997-10-08) | |

changeset 3807 | 82a99b090d9d |

child 6255 | db63752140c7 |

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

A formalization of TLA in HOL -- by Stephan Merz;

1 (*

2 File: TLA/Stfun.thy

3 Author: Stephan Merz

4 Copyright: 1997 University of Munich

6 Theory Name: Stfun

7 Logic Image: HOL

9 States and state functions for TLA

10 *)

12 Stfun = Prod +

14 types

15 state

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

17 stpred = "bool stfun"

19 arities

20 state :: term

22 consts

23 (* For simplicity, we do not syntactically distinguish between state variables

24 and state functions, and treat "state" as an anonymous type. But we need a

25 "meta-predicate" to identify "base" state variables that represent the state

26 components of a system, in particular to define the enabledness of actions.

27 *)

28 base_var :: "'a stfun => bool"

30 (* lift tupling to state functions *)

31 pairSF :: "['a stfun, 'b stfun] => ('a * 'b) stfun"

33 syntax

34 "@tupleSF" :: "args => ('a * 'b) stfun" ("(1<_>)")

36 translations

37 "<x,y,z>" == "<x, <y,z> >"

38 "<x,y>" == "pairSF x y"

39 "<x>" => "x"

41 rules

42 (* tupling *)

43 pairSF_def "<v,w>(s) = (v(s),w(s))"

45 (* "base" variables may be assigned arbitrary values by states.

46 NB: It's really stronger than that because "u" doesn't depend

47 on either c or v. In particular, if "==>" were replaced

48 with "==", base_pair would (still) not be derivable.

49 *)

50 base_var "base_var v ==> EX u. v u = c"

52 (* a tuple of variables is "base" if each variable is "base" *)

53 base_pair "base_var <v,w> = (base_var v & base_var w)"

54 end

56 ML