author | wenzelm |
Sat, 24 Mar 2018 20:51:42 +0100 | |
changeset 67945 | 984c3dc46cc0 |
parent 62146 | 324bc1ffba12 |
child 80914 | d97fdabd9e2b |
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 |
consts |
|
60588 | 20 |
first_world :: "behavior \<Rightarrow> ('w::world)" |
21 |
st1 :: "behavior \<Rightarrow> state" |
|
22 |
st2 :: "behavior \<Rightarrow> state" |
|
6255 | 23 |
|
62146 | 24 |
definition Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal" |
25 |
where Init_def: "Initial F sigma = F (first_world sigma)" |
|
26 |
||
6255 | 27 |
syntax |
60588 | 28 |
"_TEMP" :: "lift \<Rightarrow> 'a" ("(TEMP _)") |
29 |
"_Init" :: "lift \<Rightarrow> lift" ("(Init _)"[40] 50) |
|
6255 | 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 |
|
62145 | 35 |
overloading |
36 |
fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior" |
|
37 |
fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state" |
|
38 |
fw_act \<equiv> "first_world :: behavior \<Rightarrow> state \<times> state" |
|
39 |
begin |
|
40 |
||
41 |
definition "first_world == \<lambda>sigma. sigma" |
|
42 |
definition "first_world == st1" |
|
43 |
definition "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)" |
|
44 |
||
45 |
end |
|
17309 | 46 |
|
21624 | 47 |
lemma const_simps [int_rewrite, simp]: |
60588 | 48 |
"\<turnstile> (Init #True) = #True" |
49 |
"\<turnstile> (Init #False) = #False" |
|
21624 | 50 |
by (auto simp: Init_def) |
51 |
||
26304 | 52 |
lemma Init_simps1 [int_rewrite]: |
60588 | 53 |
"\<And>F. \<turnstile> (Init \<not>F) = (\<not> Init F)" |
54 |
"\<turnstile> (Init (P \<longrightarrow> Q)) = (Init P \<longrightarrow> Init Q)" |
|
60591 | 55 |
"\<turnstile> (Init (P \<and> Q)) = (Init P \<and> Init Q)" |
56 |
"\<turnstile> (Init (P \<or> Q)) = (Init P \<or> Init Q)" |
|
60588 | 57 |
"\<turnstile> (Init (P = Q)) = ((Init P) = (Init Q))" |
58 |
"\<turnstile> (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))" |
|
59 |
"\<turnstile> (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))" |
|
60 |
"\<turnstile> (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))" |
|
21624 | 61 |
by (auto simp: Init_def) |
62 |
||
60588 | 63 |
lemma Init_stp_act: "\<turnstile> (Init $P) = (Init P)" |
21624 | 64 |
by (auto simp add: Init_def fw_act_def fw_stp_def) |
65 |
||
26304 | 66 |
lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1 |
21624 | 67 |
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric] |
68 |
||
60588 | 69 |
lemma Init_temp: "\<turnstile> (Init F) = F" |
21624 | 70 |
by (auto simp add: Init_def fw_temp_def) |
71 |
||
26304 | 72 |
lemmas Init_simps = Init_temp [int_rewrite] Init_simps2 |
21624 | 73 |
|
74 |
(* Trivial instances of the definitions that avoid introducing lambda expressions. *) |
|
60588 | 75 |
lemma Init_stp: "(sigma \<Turnstile> Init P) = P (st1 sigma)" |
21624 | 76 |
by (simp add: Init_def fw_stp_def) |
77 |
||
60588 | 78 |
lemma Init_act: "(sigma \<Turnstile> Init A) = A (st1 sigma, st2 sigma)" |
21624 | 79 |
by (simp add: Init_def fw_act_def) |
80 |
||
81 |
lemmas Init_defs = Init_stp Init_act Init_temp [int_use] |
|
17309 | 82 |
|
6255 | 83 |
end |