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;
     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 
    20 consts
    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"
    25 
    26 syntax
    27   "_TEMP"    :: "lift \<Rightarrow> 'a"                          ("(TEMP _)")
    28   "_Init"    :: "lift \<Rightarrow> lift"                        ("(Init _)"[40] 50)
    29 
    30 translations
    31   "TEMP F"   => "(F::behavior \<Rightarrow> _)"
    32   "_Init"    == "CONST Initial"
    33   "sigma \<Turnstile> Init F"  <= "_Init F sigma"
    34 
    35 defs
    36   Init_def:    "sigma \<Turnstile> Init F  ==  (first_world sigma) \<Turnstile> F"
    37 
    38 overloading
    39   fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
    40   fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
    41   fw_act \<equiv> "first_world :: behavior \<Rightarrow> state \<times> state"
    42 begin
    43 
    44 definition "first_world == \<lambda>sigma. sigma"
    45 definition "first_world == st1"
    46 definition "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
    47 
    48 end
    49 
    50 lemma const_simps [int_rewrite, simp]:
    51   "\<turnstile> (Init #True) = #True"
    52   "\<turnstile> (Init #False) = #False"
    53   by (auto simp: Init_def)
    54 
    55 lemma Init_simps1 [int_rewrite]:
    56   "\<And>F. \<turnstile> (Init \<not>F) = (\<not> Init F)"
    57   "\<turnstile> (Init (P \<longrightarrow> Q)) = (Init P \<longrightarrow> Init Q)"
    58   "\<turnstile> (Init (P \<and> Q)) = (Init P \<and> Init Q)"
    59   "\<turnstile> (Init (P \<or> Q)) = (Init P \<or> Init Q)"
    60   "\<turnstile> (Init (P = Q)) = ((Init P) = (Init Q))"
    61   "\<turnstile> (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))"
    62   "\<turnstile> (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))"
    63   "\<turnstile> (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))"
    64   by (auto simp: Init_def)
    65 
    66 lemma Init_stp_act: "\<turnstile> (Init $P) = (Init P)"
    67   by (auto simp add: Init_def fw_act_def fw_stp_def)
    68 
    69 lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
    70 lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
    71 
    72 lemma Init_temp: "\<turnstile> (Init F) = F"
    73   by (auto simp add: Init_def fw_temp_def)
    74 
    75 lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
    76 
    77 (* Trivial instances of the definitions that avoid introducing lambda expressions. *)
    78 lemma Init_stp: "(sigma \<Turnstile> Init P) = P (st1 sigma)"
    79   by (simp add: Init_def fw_stp_def)
    80 
    81 lemma Init_act: "(sigma \<Turnstile> Init A) = A (st1 sigma, st2 sigma)"
    82   by (simp add: Init_def fw_act_def)
    83 
    84 lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
    85 
    86 end