src/HOL/TLA/Init.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42018 878f33040280
child 55382 9218fa411c15
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35108
e384e27c229f modernized syntax/translations;
wenzelm
parents: 26304
diff changeset
     1
(*  Title:      HOL/TLA/Init.thy
e384e27c229f modernized syntax/translations;
wenzelm
parents: 26304
diff changeset
     2
    Author:     Stephan Merz
e384e27c229f modernized syntax/translations;
wenzelm
parents: 26304
diff changeset
     3
    Copyright:  1998 University of Munich
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
     4
35108
e384e27c229f modernized syntax/translations;
wenzelm
parents: 26304
diff changeset
     5
Introduces type of temporal formulas.  Defines interface between
e384e27c229f modernized syntax/translations;
wenzelm
parents: 26304
diff changeset
     6
temporal formulas and its "subformulas" (state predicates and
e384e27c229f modernized syntax/translations;
wenzelm
parents: 26304
diff changeset
     7
actions).
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
     8
*)
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
     9
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    10
theory Init
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    11
imports Action
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    12
begin
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    13
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    14
typedecl behavior
35318
e1b61c5fd494 dropped axclass, going back to purely syntactic type classes
haftmann
parents: 35108
diff changeset
    15
arities behavior :: world
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    16
42018
878f33040280 modernized specifications;
wenzelm
parents: 35318
diff changeset
    17
type_synonym temporal = "behavior form"
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    18
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    19
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    20
consts
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    21
  Initial     :: "('w::world => bool) => temporal"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    22
  first_world :: "behavior => ('w::world)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    23
  st1         :: "behavior => state"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    24
  st2         :: "behavior => state"
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    25
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    26
syntax
35108
e384e27c229f modernized syntax/translations;
wenzelm
parents: 26304
diff changeset
    27
  "_TEMP"    :: "lift => 'a"                          ("(TEMP _)")
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    28
  "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    29
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    30
translations
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    31
  "TEMP F"   => "(F::behavior => _)"
35108
e384e27c229f modernized syntax/translations;
wenzelm
parents: 26304
diff changeset
    32
  "_Init"    == "CONST Initial"
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    33
  "sigma |= Init F"  <= "_Init F sigma"
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    34
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    35
defs
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    36
  Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    37
  fw_temp_def: "first_world == %sigma. sigma"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    38
  fw_stp_def:  "first_world == st1"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    39
  fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    40
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    41
lemma const_simps [int_rewrite, simp]:
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    42
  "|- (Init #True) = #True"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    43
  "|- (Init #False) = #False"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    44
  by (auto simp: Init_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    45
26304
02fbd0e7954a avoid rebinding of existing facts;
wenzelm
parents: 21624
diff changeset
    46
lemma Init_simps1 [int_rewrite]:
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    47
  "!!F. |- (Init ~F) = (~ Init F)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    48
  "|- (Init (P --> Q)) = (Init P --> Init Q)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    49
  "|- (Init (P & Q)) = (Init P & Init Q)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    50
  "|- (Init (P | Q)) = (Init P | Init Q)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    51
  "|- (Init (P = Q)) = ((Init P) = (Init Q))"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    52
  "|- (Init (!x. F x)) = (!x. (Init F x))"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    53
  "|- (Init (? x. F x)) = (? x. (Init F x))"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    54
  "|- (Init (?! x. F x)) = (?! x. (Init F x))"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    55
  by (auto simp: Init_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    56
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    57
lemma Init_stp_act: "|- (Init $P) = (Init P)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    58
  by (auto simp add: Init_def fw_act_def fw_stp_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    59
26304
02fbd0e7954a avoid rebinding of existing facts;
wenzelm
parents: 21624
diff changeset
    60
lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    61
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    62
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    63
lemma Init_temp: "|- (Init F) = F"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    64
  by (auto simp add: Init_def fw_temp_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    65
26304
02fbd0e7954a avoid rebinding of existing facts;
wenzelm
parents: 21624
diff changeset
    66
lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    67
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    68
(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    69
lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    70
  by (simp add: Init_def fw_stp_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    71
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    72
lemma Init_act: "(sigma |= Init A) = A (st1 sigma, st2 sigma)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    73
  by (simp add: Init_def fw_act_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    74
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    75
lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    76
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    77
end