equal
deleted
inserted
replaced
13 |
13 |
14 (*Demonstrates induction, but not used in the following proof*) |
14 (*Demonstrates induction, but not used in the following proof*) |
15 Goal "Timer : UNIV leadsTo {s. count s = 0}"; |
15 Goal "Timer : UNIV leadsTo {s. count s = 0}"; |
16 by (res_inst_tac [("f", "count")] lessThan_induct 1); |
16 by (res_inst_tac [("f", "count")] lessThan_induct 1); |
17 by (Simp_tac 1); |
17 by (Simp_tac 1); |
18 by (cases_tac "m" 1); |
18 by (case_tac "m" 1); |
19 by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1); |
19 by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1); |
20 by (ensures_tac "decr" 1); |
20 by (ensures_tac "decr" 1); |
21 qed "Timer_leadsTo_zero"; |
21 qed "Timer_leadsTo_zero"; |
22 |
22 |
23 Goal "Timer : preserves snd"; |
23 Goal "Timer : preserves snd"; |
34 by Auto_tac; |
34 by Auto_tac; |
35 (*Safety property, already reduced to the single Timer case*) |
35 (*Safety property, already reduced to the single Timer case*) |
36 by (constrains_tac 2); |
36 by (constrains_tac 2); |
37 (*Progress property for the array of Timers*) |
37 (*Progress property for the array of Timers*) |
38 by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1); |
38 by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1); |
39 by (cases_tac "m" 1); |
39 by (case_tac "m" 1); |
40 (*Annoying need to massage the conditions to have the form (... Times UNIV)*) |
40 (*Annoying need to massage the conditions to have the form (... Times UNIV)*) |
41 by (auto_tac (claset() addIs [subset_imp_leadsTo], |
41 by (auto_tac (claset() addIs [subset_imp_leadsTo], |
42 simpset() addsimps [insert_absorb, lessThan_Suc RS sym, |
42 simpset() addsimps [insert_absorb, lessThan_Suc RS sym, |
43 lift_set_Un_distrib RS sym, |
43 lift_set_Un_distrib RS sym, |
44 Times_Un_distrib1 RS sym, |
44 Times_Un_distrib1 RS sym, |