1(*  Title:      HOL/TLA/Stfun.thy
2    Author:     Stephan Merz
3    Copyright:  1998 University of Munich
4*)
5
6section \<open>States and state functions for TLA as an "intensional" logic\<close>
7
8theory Stfun
9imports Intensional
10begin
11
12typedecl state
13instance state :: world ..
14
15type_synonym 'a stfun = "state \<Rightarrow> 'a"
16type_synonym stpred  = "bool stfun"
17
18
19consts
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
31     "meta predicate" basevars, which is defined here.
32  *)
33  stvars    :: "'a stfun \<Rightarrow> bool"
34
35syntax
36  "_PRED"   :: "lift \<Rightarrow> 'a"                          ("PRED _")
37  "_stvars" :: "lift \<Rightarrow> bool"                        ("basevars _")
38
39translations
40  "PRED P"   =>  "(P::state \<Rightarrow> _)"
41  "_stvars"  ==  "CONST stvars"
42
43(* Base variables may be assigned arbitrary (type-correct) values.
44   Note that vs may be a tuple of variables. The correct identification
45   of base variables is up to the user who must take care not to
46   introduce an inconsistency. For example, "basevars (x,x)" would
47   definitely be inconsistent.
48*)
49overloading stvars \<equiv> stvars
50begin
51  definition stvars :: "(state \<Rightarrow> 'a) \<Rightarrow> bool"
52    where basevars_def: "stvars vs == range vs = UNIV"
53end
54
55lemma basevars: "\<And>vs. basevars vs \<Longrightarrow> \<exists>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
60
61lemma base_pair1: "\<And>x y. basevars (x,y) \<Longrightarrow> 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, _) " in basevars)
67  apply auto
68  done
69
70lemma base_pair2: "\<And>x y. basevars (x,y) \<Longrightarrow> 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 = "(_, xa) " in basevars)
76  apply auto
77  done
78
79lemma base_pair: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars x & basevars y"
80  apply (rule conjI)
81  apply (erule base_pair1)
82  apply (erule base_pair2)
83  done
84
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*)
89lemma unit_base: "basevars (v::unit stfun)"
90  apply (unfold basevars_def)
91  apply auto
92  done
93
94lemma baseE: "\<lbrakk> basevars v; \<And>x. v x = c \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
95  apply (erule basevars [THEN exE])
96  apply blast
97  done
98
99
100(* -------------------------------------------------------------------------------
101   The following shows that there should not be duplicates in a "stvars" tuple:
102*)
103
104lemma "\<And>v. basevars (v::bool stfun, v) \<Longrightarrow> 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
111
112end
113