author | wenzelm |
Fri, 26 Jun 2015 15:55:44 +0200 | |
changeset 60591 | e0b77517f9a9 |
parent 60588 | 750c533459b1 |
child 62145 | 5b946c81dfbf |
permissions | -rw-r--r-- |
35108 | 1 |
(* Title: HOL/TLA/Init.thy |
2 |
Author: Stephan Merz |
|
3 |
Copyright: 1998 University of Munich |
|
6255 | 4 |
|
35108 | 5 |
Introduces type of temporal formulas. Defines interface between |
6 |
temporal formulas and its "subformulas" (state predicates and |
|
7 |
actions). |
|
6255 | 8 |
*) |
9 |
||
17309 | 10 |
theory Init |
11 |
imports Action |
|
12 |
begin |
|
13 |
||
14 |
typedecl behavior |
|
55382
9218fa411c15
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
42018
diff
changeset
|
15 |
instance behavior :: world .. |
6255 | 16 |
|
42018 | 17 |
type_synonym temporal = "behavior form" |
6255 | 18 |
|
19 |
||
20 |
consts |
|
60588 | 21 |
Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal" |
22 |
first_world :: "behavior \<Rightarrow> ('w::world)" |
|
23 |
st1 :: "behavior \<Rightarrow> state" |
|
24 |
st2 :: "behavior \<Rightarrow> state" |
|
6255 | 25 |
|
26 |
syntax |
|
60588 | 27 |
"_TEMP" :: "lift \<Rightarrow> 'a" ("(TEMP _)") |
28 |
"_Init" :: "lift \<Rightarrow> lift" ("(Init _)"[40] 50) |
|
6255 | 29 |
|
30 |
translations |
|
60588 | 31 |
"TEMP F" => "(F::behavior \<Rightarrow> _)" |
35108 | 32 |
"_Init" == "CONST Initial" |
60591 | 33 |
"sigma \<Turnstile> Init F" <= "_Init F sigma" |
6255 | 34 |
|
35 |
defs |
|
60588 | 36 |
Init_def: "sigma \<Turnstile> Init F == (first_world sigma) \<Turnstile> F" |
57510 | 37 |
|
38 |
defs (overloaded) |
|
60587 | 39 |
fw_temp_def: "first_world == \<lambda>sigma. sigma" |
17309 | 40 |
fw_stp_def: "first_world == st1" |
60587 | 41 |
fw_act_def: "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)" |
17309 | 42 |
|
21624 | 43 |
lemma const_simps [int_rewrite, simp]: |
60588 | 44 |
"\<turnstile> (Init #True) = #True" |
45 |
"\<turnstile> (Init #False) = #False" |
|
21624 | 46 |
by (auto simp: Init_def) |
47 |
||
26304 | 48 |
lemma Init_simps1 [int_rewrite]: |
60588 | 49 |
"\<And>F. \<turnstile> (Init \<not>F) = (\<not> Init F)" |
50 |
"\<turnstile> (Init (P \<longrightarrow> Q)) = (Init P \<longrightarrow> Init Q)" |
|
60591 | 51 |
"\<turnstile> (Init (P \<and> Q)) = (Init P \<and> Init Q)" |
52 |
"\<turnstile> (Init (P \<or> Q)) = (Init P \<or> Init Q)" |
|
60588 | 53 |
"\<turnstile> (Init (P = Q)) = ((Init P) = (Init Q))" |
54 |
"\<turnstile> (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))" |
|
55 |
"\<turnstile> (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))" |
|
56 |
"\<turnstile> (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))" |
|
21624 | 57 |
by (auto simp: Init_def) |
58 |
||
60588 | 59 |
lemma Init_stp_act: "\<turnstile> (Init $P) = (Init P)" |
21624 | 60 |
by (auto simp add: Init_def fw_act_def fw_stp_def) |
61 |
||
26304 | 62 |
lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1 |
21624 | 63 |
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric] |
64 |
||
60588 | 65 |
lemma Init_temp: "\<turnstile> (Init F) = F" |
21624 | 66 |
by (auto simp add: Init_def fw_temp_def) |
67 |
||
26304 | 68 |
lemmas Init_simps = Init_temp [int_rewrite] Init_simps2 |
21624 | 69 |
|
70 |
(* Trivial instances of the definitions that avoid introducing lambda expressions. *) |
|
60588 | 71 |
lemma Init_stp: "(sigma \<Turnstile> Init P) = P (st1 sigma)" |
21624 | 72 |
by (simp add: Init_def fw_stp_def) |
73 |
||
60588 | 74 |
lemma Init_act: "(sigma \<Turnstile> Init A) = A (st1 sigma, st2 sigma)" |
21624 | 75 |
by (simp add: Init_def fw_act_def) |
76 |
||
77 |
lemmas Init_defs = Init_stp Init_act Init_temp [int_use] |
|
17309 | 78 |
|
6255 | 79 |
end |