src/HOL/TLA/Stfun.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 62145 5b946c81dfbf
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
     1 (*  Title:      HOL/TLA/Stfun.thy
     2     Author:     Stephan Merz
     3     Copyright:  1998 University of Munich
     4 *)
     5 
     6 section \<open>States and state functions for TLA as an "intensional" logic\<close>
     7 
     8 theory Stfun
     9 imports Intensional
    10 begin
    11 
    12 typedecl state
    13 instance state :: world ..
    14 
    15 type_synonym 'a stfun = "state \<Rightarrow> 'a"
    16 type_synonym stpred  = "bool stfun"
    17 
    18 
    19 consts
    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 
    35 syntax
    36   "_PRED"   :: "lift \<Rightarrow> 'a"                          ("PRED _")
    37   "_stvars" :: "lift \<Rightarrow> bool"                        ("basevars _")
    38 
    39 translations
    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 *)
    49 overloading stvars \<equiv> stvars
    50 begin
    51   definition stvars :: "(state \<Rightarrow> 'a) \<Rightarrow> bool"
    52     where basevars_def: "stvars vs == range vs = UNIV"
    53 end
    54 
    55 lemma 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 
    61 lemma 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 
    70 lemma 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 
    79 lemma 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 *)
    89 lemma unit_base: "basevars (v::unit stfun)"
    90   apply (unfold basevars_def)
    91   apply auto
    92   done
    93 
    94 lemma 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 
   104 lemma "\<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 
   112 end