src/HOL/TLA/Init.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 35318 e1b61c5fd494
child 42018 878f33040280
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm@35108
     1
(*  Title:      HOL/TLA/Init.thy
wenzelm@35108
     2
    Author:     Stephan Merz
wenzelm@35108
     3
    Copyright:  1998 University of Munich
wenzelm@6255
     4
wenzelm@35108
     5
Introduces type of temporal formulas.  Defines interface between
wenzelm@35108
     6
temporal formulas and its "subformulas" (state predicates and
wenzelm@35108
     7
actions).
wenzelm@6255
     8
*)
wenzelm@6255
     9
wenzelm@17309
    10
theory Init
wenzelm@17309
    11
imports Action
wenzelm@17309
    12
begin
wenzelm@17309
    13
wenzelm@17309
    14
typedecl behavior
haftmann@35318
    15
arities behavior :: world
wenzelm@6255
    16
wenzelm@6255
    17
types
wenzelm@17309
    18
  temporal = "behavior form"
wenzelm@6255
    19
wenzelm@6255
    20
wenzelm@6255
    21
consts
wenzelm@17309
    22
  Initial     :: "('w::world => bool) => temporal"
wenzelm@17309
    23
  first_world :: "behavior => ('w::world)"
wenzelm@17309
    24
  st1         :: "behavior => state"
wenzelm@17309
    25
  st2         :: "behavior => state"
wenzelm@6255
    26
wenzelm@6255
    27
syntax
wenzelm@35108
    28
  "_TEMP"    :: "lift => 'a"                          ("(TEMP _)")
wenzelm@17309
    29
  "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
wenzelm@6255
    30
wenzelm@6255
    31
translations
wenzelm@6255
    32
  "TEMP F"   => "(F::behavior => _)"
wenzelm@35108
    33
  "_Init"    == "CONST Initial"
wenzelm@6255
    34
  "sigma |= Init F"  <= "_Init F sigma"
wenzelm@6255
    35
wenzelm@6255
    36
defs
wenzelm@17309
    37
  Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
wenzelm@17309
    38
  fw_temp_def: "first_world == %sigma. sigma"
wenzelm@17309
    39
  fw_stp_def:  "first_world == st1"
wenzelm@17309
    40
  fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"
wenzelm@17309
    41
wenzelm@21624
    42
lemma const_simps [int_rewrite, simp]:
wenzelm@21624
    43
  "|- (Init #True) = #True"
wenzelm@21624
    44
  "|- (Init #False) = #False"
wenzelm@21624
    45
  by (auto simp: Init_def)
wenzelm@21624
    46
wenzelm@26304
    47
lemma Init_simps1 [int_rewrite]:
wenzelm@21624
    48
  "!!F. |- (Init ~F) = (~ Init F)"
wenzelm@21624
    49
  "|- (Init (P --> Q)) = (Init P --> Init Q)"
wenzelm@21624
    50
  "|- (Init (P & Q)) = (Init P & Init Q)"
wenzelm@21624
    51
  "|- (Init (P | Q)) = (Init P | Init Q)"
wenzelm@21624
    52
  "|- (Init (P = Q)) = ((Init P) = (Init Q))"
wenzelm@21624
    53
  "|- (Init (!x. F x)) = (!x. (Init F x))"
wenzelm@21624
    54
  "|- (Init (? x. F x)) = (? x. (Init F x))"
wenzelm@21624
    55
  "|- (Init (?! x. F x)) = (?! x. (Init F x))"
wenzelm@21624
    56
  by (auto simp: Init_def)
wenzelm@21624
    57
wenzelm@21624
    58
lemma Init_stp_act: "|- (Init $P) = (Init P)"
wenzelm@21624
    59
  by (auto simp add: Init_def fw_act_def fw_stp_def)
wenzelm@21624
    60
wenzelm@26304
    61
lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
wenzelm@21624
    62
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
wenzelm@21624
    63
wenzelm@21624
    64
lemma Init_temp: "|- (Init F) = F"
wenzelm@21624
    65
  by (auto simp add: Init_def fw_temp_def)
wenzelm@21624
    66
wenzelm@26304
    67
lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
wenzelm@21624
    68
wenzelm@21624
    69
(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
wenzelm@21624
    70
lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"
wenzelm@21624
    71
  by (simp add: Init_def fw_stp_def)
wenzelm@21624
    72
wenzelm@21624
    73
lemma Init_act: "(sigma |= Init A) = A (st1 sigma, st2 sigma)"
wenzelm@21624
    74
  by (simp add: Init_def fw_act_def)
wenzelm@21624
    75
wenzelm@21624
    76
lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
wenzelm@17309
    77
wenzelm@6255
    78
end