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