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