author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42018  878f33040280 
child 55382  9218fa411c15 
permissions  rwrr 
35108  1 
(* Title: HOL/TLA/Stfun.thy 
2 
Author: Stephan Merz 

3 
Copyright: 1998 University of Munich 

21624  4 
*) 
3807  5 

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

17309  8 
theory Stfun 
9 
imports Intensional 

10 
begin 

11 

12 
typedecl state 

13 

35318
e1b61c5fd494
dropped axclass, going back to purely syntactic type classes
haftmann
parents:
35108
diff
changeset

14 
arities state :: world 
3807  15 

42018  16 
type_synonym 'a stfun = "state => 'a" 
17 
type_synonym stpred = "bool stfun" 

3807  18 

19 

20 
consts 

6255  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 

12607  32 
"meta predicate" basevars, which is defined here. 
3807  33 
*) 
6255  34 
stvars :: "'a stfun => bool" 
3807  35 

36 
syntax 

35354  37 
"_PRED" :: "lift => 'a" ("PRED _") 
17309  38 
"_stvars" :: "lift => bool" ("basevars _") 
3807  39 

40 
translations 

6255  41 
"PRED P" => "(P::state => _)" 
35108  42 
"_stvars" == "CONST stvars" 
3807  43 

12607  44 
defs 
17309  45 
(* Base variables may be assigned arbitrary (typecorrect) values. 
12607  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. 

6255  50 
*) 
17309  51 
basevars_def: "stvars vs == range vs = UNIV" 
52 

21624  53 

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 

59 

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 

68 

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 

77 

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 

83 

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 

92 

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

94 
apply (erule basevars [THEN exE]) 

95 
apply blast 

96 
done 

97 

98 

99 
(*  

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

101 
*) 

102 

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 

3807  110 

111 
end 