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