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

src/HOL/TLA/Stfun.thy

author | wenzelm |

Fri Dec 17 17:43:54 2010 +0100 (2010-12-17) | |

changeset 41229 | d797baa3d57c |

parent 35354 | 2e8dc3c64430 |

child 42018 | 878f33040280 |

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

replaced command 'nonterminals' by slightly modernized version 'nonterminal';

1 (* Title: HOL/TLA/Stfun.thy

2 Author: Stephan Merz

3 Copyright: 1998 University of Munich

4 *)

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

8 theory Stfun

9 imports Intensional

10 begin

12 typedecl state

14 arities state :: world

16 types

17 'a stfun = "state => 'a"

18 stpred = "bool stfun"

21 consts

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

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

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

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

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

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

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

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

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

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

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

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

34 *)

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

37 syntax

38 "_PRED" :: "lift => 'a" ("PRED _")

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

41 translations

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

43 "_stvars" == "CONST stvars"

45 defs

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

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

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

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

50 definitely be inconsistent.

51 *)

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

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

56 apply (unfold basevars_def)

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

58 apply auto

59 done

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

62 apply (simp (no_asm) add: basevars_def)

63 apply (rule equalityI)

64 apply (rule subset_UNIV)

65 apply (rule subsetI)

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

67 apply auto

68 done

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

71 apply (simp (no_asm) add: basevars_def)

72 apply (rule equalityI)

73 apply (rule subset_UNIV)

74 apply (rule subsetI)

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

76 apply auto

77 done

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

80 apply (rule conjI)

81 apply (erule base_pair1)

82 apply (erule base_pair2)

83 done

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

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

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

88 *)

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

90 apply (unfold basevars_def)

91 apply auto

92 done

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

95 apply (erule basevars [THEN exE])

96 apply blast

97 done

100 (* -------------------------------------------------------------------------------

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

102 *)

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

105 apply (erule baseE)

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

107 prefer 2

108 apply assumption

109 apply simp

110 done

112 end