src/HOL/TLA/Init.thy
author wenzelm
Sat, 24 Mar 2018 20:51:42 +0100
changeset 67945 984c3dc46cc0
parent 62146 324bc1ffba12
child 80914 d97fdabd9e2b
permissions -rw-r--r--
tuned output;
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
55382
9218fa411c15 prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents: 42018
diff changeset
    15
instance 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
consts
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    20
  first_world :: "behavior \<Rightarrow> ('w::world)"
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    21
  st1         :: "behavior \<Rightarrow> state"
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    22
  st2         :: "behavior \<Rightarrow> state"
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    23
62146
324bc1ffba12 eliminated old defs;
wenzelm
parents: 62145
diff changeset
    24
definition Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
324bc1ffba12 eliminated old defs;
wenzelm
parents: 62145
diff changeset
    25
  where Init_def: "Initial F sigma = F (first_world sigma)"
324bc1ffba12 eliminated old defs;
wenzelm
parents: 62145
diff changeset
    26
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    27
syntax
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    28
  "_TEMP"    :: "lift \<Rightarrow> 'a"                          ("(TEMP _)")
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    29
  "_Init"    :: "lift \<Rightarrow> lift"                        ("(Init _)"[40] 50)
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    30
translations
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    31
  "TEMP F"   => "(F::behavior \<Rightarrow> _)"
35108
e384e27c229f modernized syntax/translations;
wenzelm
parents: 26304
diff changeset
    32
  "_Init"    == "CONST Initial"
60591
e0b77517f9a9 more symbols;
wenzelm
parents: 60588
diff changeset
    33
  "sigma \<Turnstile> Init F"  <= "_Init F sigma"
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    34
62145
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    35
overloading
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    36
  fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    37
  fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    38
  fw_act \<equiv> "first_world :: behavior \<Rightarrow> state \<times> state"
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    39
begin
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    40
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    41
definition "first_world == \<lambda>sigma. sigma"
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    42
definition "first_world == st1"
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    43
definition "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    44
5b946c81dfbf eliminated old defs;
wenzelm
parents: 60591
diff changeset
    45
end
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    46
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    47
lemma const_simps [int_rewrite, simp]:
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    48
  "\<turnstile> (Init #True) = #True"
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    49
  "\<turnstile> (Init #False) = #False"
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    50
  by (auto simp: Init_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    51
26304
02fbd0e7954a avoid rebinding of existing facts;
wenzelm
parents: 21624
diff changeset
    52
lemma Init_simps1 [int_rewrite]:
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    53
  "\<And>F. \<turnstile> (Init \<not>F) = (\<not> Init F)"
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    54
  "\<turnstile> (Init (P \<longrightarrow> Q)) = (Init P \<longrightarrow> Init Q)"
60591
e0b77517f9a9 more symbols;
wenzelm
parents: 60588
diff changeset
    55
  "\<turnstile> (Init (P \<and> Q)) = (Init P \<and> Init Q)"
e0b77517f9a9 more symbols;
wenzelm
parents: 60588
diff changeset
    56
  "\<turnstile> (Init (P \<or> Q)) = (Init P \<or> Init Q)"
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    57
  "\<turnstile> (Init (P = Q)) = ((Init P) = (Init Q))"
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    58
  "\<turnstile> (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))"
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    59
  "\<turnstile> (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))"
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    60
  "\<turnstile> (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))"
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    61
  by (auto simp: Init_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    62
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    63
lemma Init_stp_act: "\<turnstile> (Init $P) = (Init P)"
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    64
  by (auto simp add: Init_def fw_act_def fw_stp_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_simps2 = Init_stp_act [int_rewrite] Init_simps1
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    67
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    68
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    69
lemma Init_temp: "\<turnstile> (Init F) = F"
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    70
  by (auto simp add: Init_def fw_temp_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    71
26304
02fbd0e7954a avoid rebinding of existing facts;
wenzelm
parents: 21624
diff changeset
    72
lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    73
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    74
(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    75
lemma Init_stp: "(sigma \<Turnstile> Init P) = P (st1 sigma)"
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    76
  by (simp add: Init_def fw_stp_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    77
60588
750c533459b1 more symbols;
wenzelm
parents: 60587
diff changeset
    78
lemma Init_act: "(sigma \<Turnstile> Init A) = A (st1 sigma, st2 sigma)"
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    79
  by (simp add: Init_def fw_act_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    80
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    81
lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    82
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents:
diff changeset
    83
end