src/HOL/TLA/Stfun.thy
 author nipkow Fri Aug 28 18:52:41 2009 +0200 (2009-08-28) changeset 32436 10cd49e0c067 parent 21624 6f79647cf536 child 35108 e384e27c229f permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
```     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
```