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