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