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

src/HOL/TLA/Stfun.thy

author | wenzelm |

Sat Dec 02 02:52:02 2006 +0100 (2006-12-02) | |

changeset 21624 | 6f79647cf536 |

parent 17309 | c43ed29bd197 |

child 35108 | e384e27c229f |

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

TLA: converted legacy ML scripts;

1 (*

2 File: TLA/Stfun.thy

3 ID: $Id$

4 Author: Stephan Merz

5 Copyright: 1998 University of Munich

6 *)

8 header {* States and state functions for TLA as an "intensional" logic *}

10 theory Stfun

11 imports Intensional

12 begin

14 typedecl state

16 instance state :: world ..

18 types

19 'a stfun = "state => 'a"

20 stpred = "bool stfun"

23 consts

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

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

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

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

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

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

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

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

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

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

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

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

36 *)

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

39 syntax

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

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

43 translations

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

45 "_stvars" == "stvars"

47 defs

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

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

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

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

52 definitely be inconsistent.

53 *)

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

57 lemma basevars: "!!vs. basevars vs ==> EX u. vs u = c"

58 apply (unfold basevars_def)

59 apply (rule_tac b = c and f = vs in rangeE)

60 apply auto

61 done

63 lemma base_pair1: "!!x y. basevars (x,y) ==> basevars x"

64 apply (simp (no_asm) add: basevars_def)

65 apply (rule equalityI)

66 apply (rule subset_UNIV)

67 apply (rule subsetI)

68 apply (drule_tac c = "(xa, arbitrary) " in basevars)

69 apply auto

70 done

72 lemma base_pair2: "!!x y. basevars (x,y) ==> basevars y"

73 apply (simp (no_asm) add: basevars_def)

74 apply (rule equalityI)

75 apply (rule subset_UNIV)

76 apply (rule subsetI)

77 apply (drule_tac c = "(arbitrary, xa) " in basevars)

78 apply auto

79 done

81 lemma base_pair: "!!x y. basevars (x,y) ==> basevars x & basevars y"

82 apply (rule conjI)

83 apply (erule base_pair1)

84 apply (erule base_pair2)

85 done

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

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

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

90 *)

91 lemma unit_base: "basevars (v::unit stfun)"

92 apply (unfold basevars_def)

93 apply auto

94 done

96 lemma baseE: "[| basevars v; !!x. v x = c ==> Q |] ==> Q"

97 apply (erule basevars [THEN exE])

98 apply blast

99 done

102 (* -------------------------------------------------------------------------------

103 The following shows that there should not be duplicates in a "stvars" tuple:

104 *)

106 lemma "!!v. basevars (v::bool stfun, v) ==> False"

107 apply (erule baseE)

108 apply (subgoal_tac "(LIFT (v,v)) x = (True, False)")

109 prefer 2

110 apply assumption

111 apply simp

112 done

114 end