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
```