src/HOL/TLA/Stfun.thy
author wenzelm
Fri Jun 26 14:53:15 2015 +0200 (2015-06-26)
changeset 60588 750c533459b1
parent 60587 0318b43ee95c
child 60590 479071e8778f
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/TLA/Stfun.thy
     2     Author:     Stephan Merz
     3     Copyright:  1998 University of Munich
     4 *)
     5 
     6 section {* States and state functions for TLA as an "intensional" logic *}
     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 defs
    44   (* Base variables may be assigned arbitrary (type-correct) values.
    45      Note that vs may be a tuple of variables. The correct identification
    46      of base variables is up to the user who must take care not to
    47      introduce an inconsistency. For example, "basevars (x,x)" would
    48      definitely be inconsistent.
    49   *)
    50   basevars_def:  "stvars vs == range vs = UNIV"
    51 
    52 
    53 lemma basevars: "\<And>vs. basevars vs \<Longrightarrow> \<exists>u. vs u = c"
    54   apply (unfold basevars_def)
    55   apply (rule_tac b = c and f = vs in rangeE)
    56    apply auto
    57   done
    58 
    59 lemma base_pair1: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars x"
    60   apply (simp (no_asm) add: basevars_def)
    61   apply (rule equalityI)
    62    apply (rule subset_UNIV)
    63   apply (rule subsetI)
    64   apply (drule_tac c = "(xa, arbitrary) " in basevars)
    65   apply auto
    66   done
    67 
    68 lemma base_pair2: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars y"
    69   apply (simp (no_asm) add: basevars_def)
    70   apply (rule equalityI)
    71    apply (rule subset_UNIV)
    72   apply (rule subsetI)
    73   apply (drule_tac c = "(arbitrary, xa) " in basevars)
    74   apply auto
    75   done
    76 
    77 lemma base_pair: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars x & basevars y"
    78   apply (rule conjI)
    79   apply (erule base_pair1)
    80   apply (erule base_pair2)
    81   done
    82 
    83 (* Since the unit type has just one value, any state function can be
    84    regarded as "base". The following axiom can sometimes be useful
    85    because it gives a trivial solution for "basevars" premises.
    86 *)
    87 lemma unit_base: "basevars (v::unit stfun)"
    88   apply (unfold basevars_def)
    89   apply auto
    90   done
    91 
    92 lemma baseE: "\<lbrakk> basevars v; \<And>x. v x = c \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
    93   apply (erule basevars [THEN exE])
    94   apply blast
    95   done
    96 
    97 
    98 (* -------------------------------------------------------------------------------
    99    The following shows that there should not be duplicates in a "stvars" tuple:
   100 *)
   101 
   102 lemma "\<And>v. basevars (v::bool stfun, v) \<Longrightarrow> False"
   103   apply (erule baseE)
   104   apply (subgoal_tac "(LIFT (v,v)) x = (True, False)")
   105    prefer 2
   106    apply assumption
   107   apply simp
   108   done
   109 
   110 end