author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42018  878f33040280 
child 55382  9218fa411c15 
permissions  rwrr 
35108  1 
(* Title: HOL/TLA/Init.thy 
2 
Author: Stephan Merz 

3 
Copyright: 1998 University of Munich 

6255  4 

35108  5 
Introduces type of temporal formulas. Defines interface between 
6 
temporal formulas and its "subformulas" (state predicates and 

7 
actions). 

6255  8 
*) 
9 

17309  10 
theory Init 
11 
imports Action 

12 
begin 

13 

14 
typedecl behavior 

35318
e1b61c5fd494
dropped axclass, going back to purely syntactic type classes
haftmann
parents:
35108
diff
changeset

15 
arities behavior :: world 
6255  16 

42018  17 
type_synonym temporal = "behavior form" 
6255  18 

19 

20 
consts 

17309  21 
Initial :: "('w::world => bool) => temporal" 
22 
first_world :: "behavior => ('w::world)" 

23 
st1 :: "behavior => state" 

24 
st2 :: "behavior => state" 

6255  25 

26 
syntax 

35108  27 
"_TEMP" :: "lift => 'a" ("(TEMP _)") 
17309  28 
"_Init" :: "lift => lift" ("(Init _)"[40] 50) 
6255  29 

30 
translations 

31 
"TEMP F" => "(F::behavior => _)" 

35108  32 
"_Init" == "CONST Initial" 
6255  33 
"sigma = Init F" <= "_Init F sigma" 
34 

35 
defs 

17309  36 
Init_def: "sigma = Init F == (first_world sigma) = F" 
37 
fw_temp_def: "first_world == %sigma. sigma" 

38 
fw_stp_def: "first_world == st1" 

39 
fw_act_def: "first_world == %sigma. (st1 sigma, st2 sigma)" 

40 

21624  41 
lemma const_simps [int_rewrite, simp]: 
42 
" (Init #True) = #True" 

43 
" (Init #False) = #False" 

44 
by (auto simp: Init_def) 

45 

26304  46 
lemma Init_simps1 [int_rewrite]: 
21624  47 
"!!F.  (Init ~F) = (~ Init F)" 
48 
" (Init (P > Q)) = (Init P > Init Q)" 

49 
" (Init (P & Q)) = (Init P & Init Q)" 

50 
" (Init (P  Q)) = (Init P  Init Q)" 

51 
" (Init (P = Q)) = ((Init P) = (Init Q))" 

52 
" (Init (!x. F x)) = (!x. (Init F x))" 

53 
" (Init (? x. F x)) = (? x. (Init F x))" 

54 
" (Init (?! x. F x)) = (?! x. (Init F x))" 

55 
by (auto simp: Init_def) 

56 

57 
lemma Init_stp_act: " (Init $P) = (Init P)" 

58 
by (auto simp add: Init_def fw_act_def fw_stp_def) 

59 

26304  60 
lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1 
21624  61 
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric] 
62 

63 
lemma Init_temp: " (Init F) = F" 

64 
by (auto simp add: Init_def fw_temp_def) 

65 

26304  66 
lemmas Init_simps = Init_temp [int_rewrite] Init_simps2 
21624  67 

68 
(* Trivial instances of the definitions that avoid introducing lambda expressions. *) 

69 
lemma Init_stp: "(sigma = Init P) = P (st1 sigma)" 

70 
by (simp add: Init_def fw_stp_def) 

71 

72 
lemma Init_act: "(sigma = Init A) = A (st1 sigma, st2 sigma)" 

73 
by (simp add: Init_def fw_act_def) 

74 

75 
lemmas Init_defs = Init_stp Init_act Init_temp [int_use] 

17309  76 

6255  77 
end 