34 |
34 |
35 defs |
35 defs |
36 Init_def: "sigma |= Init F == (first_world sigma) |= F" |
36 Init_def: "sigma |= Init F == (first_world sigma) |= F" |
37 |
37 |
38 defs (overloaded) |
38 defs (overloaded) |
39 fw_temp_def: "first_world == %sigma. sigma" |
39 fw_temp_def: "first_world == \<lambda>sigma. sigma" |
40 fw_stp_def: "first_world == st1" |
40 fw_stp_def: "first_world == st1" |
41 fw_act_def: "first_world == %sigma. (st1 sigma, st2 sigma)" |
41 fw_act_def: "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)" |
42 |
42 |
43 lemma const_simps [int_rewrite, simp]: |
43 lemma const_simps [int_rewrite, simp]: |
44 "|- (Init #True) = #True" |
44 "|- (Init #True) = #True" |
45 "|- (Init #False) = #False" |
45 "|- (Init #False) = #False" |
46 by (auto simp: Init_def) |
46 by (auto simp: Init_def) |
47 |
47 |
48 lemma Init_simps1 [int_rewrite]: |
48 lemma Init_simps1 [int_rewrite]: |
49 "!!F. |- (Init ~F) = (~ Init F)" |
49 "\<And>F. |- (Init \<not>F) = (\<not> Init F)" |
50 "|- (Init (P --> Q)) = (Init P --> Init Q)" |
50 "|- (Init (P --> Q)) = (Init P --> Init Q)" |
51 "|- (Init (P & Q)) = (Init P & Init Q)" |
51 "|- (Init (P & Q)) = (Init P & Init Q)" |
52 "|- (Init (P | Q)) = (Init P | Init Q)" |
52 "|- (Init (P | Q)) = (Init P | Init Q)" |
53 "|- (Init (P = Q)) = ((Init P) = (Init Q))" |
53 "|- (Init (P = Q)) = ((Init P) = (Init Q))" |
54 "|- (Init (!x. F x)) = (!x. (Init F x))" |
54 "|- (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))" |
55 "|- (Init (? x. F x)) = (? x. (Init F x))" |
55 "|- (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))" |
56 "|- (Init (?! x. F x)) = (?! x. (Init F x))" |
56 "|- (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))" |
57 by (auto simp: Init_def) |
57 by (auto simp: Init_def) |
58 |
58 |
59 lemma Init_stp_act: "|- (Init $P) = (Init P)" |
59 lemma Init_stp_act: "|- (Init $P) = (Init P)" |
60 by (auto simp add: Init_def fw_act_def fw_stp_def) |
60 by (auto simp add: Init_def fw_act_def fw_stp_def) |
61 |
61 |