1(*  Title:      HOL/TLA/Init.thy
2    Author:     Stephan Merz
3    Copyright:  1998 University of Munich
4
5Introduces type of temporal formulas.  Defines interface between
6temporal formulas and its "subformulas" (state predicates and
7actions).
8*)
9
10theory Init
11imports Action
12begin
13
14typedecl behavior
15instance behavior :: world ..
16
17type_synonym temporal = "behavior form"
18
19consts
20  first_world :: "behavior \<Rightarrow> ('w::world)"
21  st1         :: "behavior \<Rightarrow> state"
22  st2         :: "behavior \<Rightarrow> state"
23
24definition Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
25  where Init_def: "Initial F sigma = F (first_world sigma)"
26
27syntax
28  "_TEMP"    :: "lift \<Rightarrow> 'a"                          ("(TEMP _)")
29  "_Init"    :: "lift \<Rightarrow> lift"                        ("(Init _)"[40] 50)
30translations
31  "TEMP F"   => "(F::behavior \<Rightarrow> _)"
32  "_Init"    == "CONST Initial"
33  "sigma \<Turnstile> Init F"  <= "_Init F sigma"
34
35overloading
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"
39begin
40
41definition "first_world == \<lambda>sigma. sigma"
42definition "first_world == st1"
43definition "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
44
45end
46
47lemma const_simps [int_rewrite, simp]:
48  "\<turnstile> (Init #True) = #True"
49  "\<turnstile> (Init #False) = #False"
50  by (auto simp: Init_def)
51
52lemma Init_simps1 [int_rewrite]:
53  "\<And>F. \<turnstile> (Init \<not>F) = (\<not> Init F)"
54  "\<turnstile> (Init (P \<longrightarrow> Q)) = (Init P \<longrightarrow> Init Q)"
55  "\<turnstile> (Init (P \<and> Q)) = (Init P \<and> Init Q)"
56  "\<turnstile> (Init (P \<or> Q)) = (Init P \<or> Init Q)"
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))"
61  by (auto simp: Init_def)
62
63lemma Init_stp_act: "\<turnstile> (Init $P) = (Init P)"
64  by (auto simp add: Init_def fw_act_def fw_stp_def)
65
66lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
67lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
68
69lemma Init_temp: "\<turnstile> (Init F) = F"
70  by (auto simp add: Init_def fw_temp_def)
71
72lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
73
74(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
75lemma Init_stp: "(sigma \<Turnstile> Init P) = P (st1 sigma)"
76  by (simp add: Init_def fw_stp_def)
77
78lemma Init_act: "(sigma \<Turnstile> Init A) = A (st1 sigma, st2 sigma)"
79  by (simp add: Init_def fw_act_def)
80
81lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
82
83end
84