equal
deleted
inserted
replaced
33 apply (unfold Timer_def, ensures_tac "decr") |
33 apply (unfold Timer_def, ensures_tac "decr") |
34 done |
34 done |
35 |
35 |
36 lemma Timer_preserves_snd [iff]: "Timer : preserves snd" |
36 lemma Timer_preserves_snd [iff]: "Timer : preserves snd" |
37 apply (rule preservesI) |
37 apply (rule preservesI) |
38 apply (unfold Timer_def, constrains) |
38 apply (unfold Timer_def, safety) |
39 done |
39 done |
40 |
40 |
41 |
41 |
42 declare PLam_stable [simp] |
42 declare PLam_stable [simp] |
43 |
43 |
47 apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)" |
47 apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)" |
48 in finite_stable_completion [THEN leadsTo_weaken]) |
48 in finite_stable_completion [THEN leadsTo_weaken]) |
49 apply auto |
49 apply auto |
50 (*Safety property, already reduced to the single Timer case*) |
50 (*Safety property, already reduced to the single Timer case*) |
51 prefer 2 |
51 prefer 2 |
52 apply (simp add: Timer_def, constrains) |
52 apply (simp add: Timer_def, safety) |
53 (*Progress property for the array of Timers*) |
53 (*Progress property for the array of Timers*) |
54 apply (rule_tac f = "sub i o fst" in lessThan_induct) |
54 apply (rule_tac f = "sub i o fst" in lessThan_induct) |
55 apply (case_tac "m") |
55 apply (case_tac "m") |
56 (*Annoying need to massage the conditions to have the form (... <*> UNIV)*) |
56 (*Annoying need to massage the conditions to have the form (... <*> UNIV)*) |
57 apply (auto intro: subset_imp_leadsTo |
57 apply (auto intro: subset_imp_leadsTo |
59 lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric] |
59 lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric] |
60 Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric]) |
60 Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric]) |
61 apply (rename_tac "n") |
61 apply (rename_tac "n") |
62 apply (rule PLam_leadsTo_Basis) |
62 apply (rule PLam_leadsTo_Basis) |
63 apply (auto simp add: lessThan_Suc [symmetric]) |
63 apply (auto simp add: lessThan_Suc [symmetric]) |
64 apply (unfold Timer_def mk_total_program_def, constrains) |
64 apply (unfold Timer_def mk_total_program_def, safety) |
65 apply (rule_tac act = decr in totalize_transientI, auto) |
65 apply (rule_tac act = decr in totalize_transientI, auto) |
66 done |
66 done |
67 |
67 |
68 end |
68 end |