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

src/HOL/TLA/Stfun.thy

author | hoelzl |

Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) | |

changeset 51474 | 1e9e68247ad1 |

parent 42018 | 878f33040280 |

child 55382 | 9218fa411c15 |

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

generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun

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 type_synonym 'a stfun = "state => 'a"

17 type_synonym stpred = "bool stfun"

20 consts

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

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

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

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

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

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

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

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

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

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

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

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

33 *)

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

36 syntax

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

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

40 translations

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

42 "_stvars" == "CONST stvars"

44 defs

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

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

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

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

49 definitely be inconsistent.

50 *)

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

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

55 apply (unfold basevars_def)

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

57 apply auto

58 done

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

61 apply (simp (no_asm) add: basevars_def)

62 apply (rule equalityI)

63 apply (rule subset_UNIV)

64 apply (rule subsetI)

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

66 apply auto

67 done

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

70 apply (simp (no_asm) add: basevars_def)

71 apply (rule equalityI)

72 apply (rule subset_UNIV)

73 apply (rule subsetI)

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

75 apply auto

76 done

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

79 apply (rule conjI)

80 apply (erule base_pair1)

81 apply (erule base_pair2)

82 done

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

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

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

87 *)

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

89 apply (unfold basevars_def)

90 apply auto

91 done

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

94 apply (erule basevars [THEN exE])

95 apply blast

96 done

99 (* -------------------------------------------------------------------------------

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

101 *)

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

104 apply (erule baseE)

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

106 prefer 2

107 apply assumption

108 apply simp

109 done

111 end