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