src/HOL/TLA/Stfun.thy
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51474 1e9e68247ad1
parent 42018 878f33040280
child 55382 9218fa411c15
permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
     1 (*  Title:      HOL/TLA/Stfun.thy
     2     Author:     Stephan Merz
     3     Copyright:  1998 University of Munich
     4 *)
     5 
     6 header {* States and state functions for TLA as an "intensional" logic *}
     7 
     8 theory Stfun
     9 imports Intensional
    10 begin
    11 
    12 typedecl state
    13 
    14 arities state :: world
    15 
    16 type_synonym 'a stfun = "state => 'a"
    17 type_synonym stpred  = "bool stfun"
    18 
    19 
    20 consts
    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
    32      "meta predicate" basevars, which is defined here.
    33   *)
    34   stvars    :: "'a stfun => bool"
    35 
    36 syntax
    37   "_PRED"   :: "lift => 'a"                          ("PRED _")
    38   "_stvars" :: "lift => bool"                        ("basevars _")
    39 
    40 translations
    41   "PRED P"   =>  "(P::state => _)"
    42   "_stvars"  ==  "CONST stvars"
    43 
    44 defs
    45   (* Base variables may be assigned arbitrary (type-correct) values.
    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.
    50   *)
    51   basevars_def:  "stvars vs == range vs = UNIV"
    52 
    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
   110 
   111 end