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