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