author | wenzelm |
Fri, 26 Jun 2015 14:53:15 +0200 | |
changeset 60588 | 750c533459b1 |
parent 60587 | 0318b43ee95c |
child 60590 | 479071e8778f |
permissions | -rw-r--r-- |
35108 | 1 |
(* Title: HOL/TLA/Stfun.thy |
2 |
Author: Stephan Merz |
|
3 |
Copyright: 1998 University of Munich |
|
21624 | 4 |
*) |
3807 | 5 |
|
58889 | 6 |
section {* 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 |
|
55382
9218fa411c15
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
42018
diff
changeset
|
13 |
instance state :: world .. |
3807 | 14 |
|
60588 | 15 |
type_synonym 'a stfun = "state \<Rightarrow> 'a" |
42018 | 16 |
type_synonym stpred = "bool stfun" |
3807 | 17 |
|
18 |
||
19 |
consts |
|
6255 | 20 |
(* Formalizing type "state" would require formulas to be tagged with |
21 |
their underlying state space and would result in a system that is |
|
22 |
much harder to use. (Unlike Hoare logic or Unity, TLA has quantification |
|
23 |
over state variables, and therefore one usually works with different |
|
24 |
state spaces within a single specification.) Instead, "state" is just |
|
25 |
an anonymous type whose only purpose is to provide "Skolem" constants. |
|
26 |
Moreover, we do not define a type of state variables separate from that |
|
27 |
of arbitrary state functions, again in order to simplify the definition |
|
28 |
of flexible quantification later on. Nevertheless, we need to distinguish |
|
29 |
state variables, mainly to define the enabledness of actions. The user |
|
30 |
identifies (tuples of) "base" state variables in a specification via the |
|
12607 | 31 |
"meta predicate" basevars, which is defined here. |
3807 | 32 |
*) |
60588 | 33 |
stvars :: "'a stfun \<Rightarrow> bool" |
3807 | 34 |
|
35 |
syntax |
|
60588 | 36 |
"_PRED" :: "lift \<Rightarrow> 'a" ("PRED _") |
37 |
"_stvars" :: "lift \<Rightarrow> bool" ("basevars _") |
|
3807 | 38 |
|
39 |
translations |
|
60588 | 40 |
"PRED P" => "(P::state \<Rightarrow> _)" |
35108 | 41 |
"_stvars" == "CONST stvars" |
3807 | 42 |
|
12607 | 43 |
defs |
17309 | 44 |
(* Base variables may be assigned arbitrary (type-correct) values. |
12607 | 45 |
Note that vs may be a tuple of variables. The correct identification |
46 |
of base variables is up to the user who must take care not to |
|
47 |
introduce an inconsistency. For example, "basevars (x,x)" would |
|
48 |
definitely be inconsistent. |
|
6255 | 49 |
*) |
17309 | 50 |
basevars_def: "stvars vs == range vs = UNIV" |
51 |
||
21624 | 52 |
|
60588 | 53 |
lemma basevars: "\<And>vs. basevars vs \<Longrightarrow> \<exists>u. vs u = c" |
21624 | 54 |
apply (unfold basevars_def) |
55 |
apply (rule_tac b = c and f = vs in rangeE) |
|
56 |
apply auto |
|
57 |
done |
|
58 |
||
60588 | 59 |
lemma base_pair1: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars x" |
21624 | 60 |
apply (simp (no_asm) add: basevars_def) |
61 |
apply (rule equalityI) |
|
62 |
apply (rule subset_UNIV) |
|
63 |
apply (rule subsetI) |
|
64 |
apply (drule_tac c = "(xa, arbitrary) " in basevars) |
|
65 |
apply auto |
|
66 |
done |
|
67 |
||
60588 | 68 |
lemma base_pair2: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars y" |
21624 | 69 |
apply (simp (no_asm) add: basevars_def) |
70 |
apply (rule equalityI) |
|
71 |
apply (rule subset_UNIV) |
|
72 |
apply (rule subsetI) |
|
73 |
apply (drule_tac c = "(arbitrary, xa) " in basevars) |
|
74 |
apply auto |
|
75 |
done |
|
76 |
||
60588 | 77 |
lemma base_pair: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars x & basevars y" |
21624 | 78 |
apply (rule conjI) |
79 |
apply (erule base_pair1) |
|
80 |
apply (erule base_pair2) |
|
81 |
done |
|
82 |
||
83 |
(* Since the unit type has just one value, any state function can be |
|
84 |
regarded as "base". The following axiom can sometimes be useful |
|
85 |
because it gives a trivial solution for "basevars" premises. |
|
86 |
*) |
|
87 |
lemma unit_base: "basevars (v::unit stfun)" |
|
88 |
apply (unfold basevars_def) |
|
89 |
apply auto |
|
90 |
done |
|
91 |
||
60588 | 92 |
lemma baseE: "\<lbrakk> basevars v; \<And>x. v x = c \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" |
21624 | 93 |
apply (erule basevars [THEN exE]) |
94 |
apply blast |
|
95 |
done |
|
96 |
||
97 |
||
98 |
(* ------------------------------------------------------------------------------- |
|
99 |
The following shows that there should not be duplicates in a "stvars" tuple: |
|
100 |
*) |
|
101 |
||
60588 | 102 |
lemma "\<And>v. basevars (v::bool stfun, v) \<Longrightarrow> False" |
21624 | 103 |
apply (erule baseE) |
104 |
apply (subgoal_tac "(LIFT (v,v)) x = (True, False)") |
|
105 |
prefer 2 |
|
106 |
apply assumption |
|
107 |
apply simp |
|
108 |
done |
|
3807 | 109 |
|
110 |
end |