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