1 (* Title: HOL/UNITY/TimerArray.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 A trivial example of reasoning about an array of processes |
|
7 *) |
|
8 |
|
9 Addsimps [Timer_def RS def_prg_Init]; |
|
10 program_defs_ref := [Timer_def]; |
|
11 |
|
12 Addsimps [count_def, decr_def]; |
|
13 |
|
14 (*Demonstrates induction, but not used in the following proof*) |
|
15 Goal "Timer : UNIV leadsTo {s. count s = 0}"; |
|
16 by (res_inst_tac [("f", "count")] lessThan_induct 1); |
|
17 by (Simp_tac 1); |
|
18 by (case_tac "m" 1); |
|
19 by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1); |
|
20 by (ensures_tac "decr" 1); |
|
21 qed "Timer_leadsTo_zero"; |
|
22 |
|
23 Goal "Timer : preserves snd"; |
|
24 by (rtac preservesI 1); |
|
25 by (constrains_tac 1); |
|
26 qed "Timer_preserves_snd"; |
|
27 AddIffs [Timer_preserves_snd]; |
|
28 |
|
29 Addsimps [PLam_stable]; |
|
30 |
|
31 Goal "finite I \ |
|
32 \ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"; |
|
33 by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")] |
|
34 (finite_stable_completion RS leadsTo_weaken) 1); |
|
35 by Auto_tac; |
|
36 (*Safety property, already reduced to the single Timer case*) |
|
37 by (constrains_tac 2); |
|
38 (*Progress property for the array of Timers*) |
|
39 by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1); |
|
40 by (case_tac "m" 1); |
|
41 (*Annoying need to massage the conditions to have the form (... <*> UNIV)*) |
|
42 by (auto_tac (claset() addIs [subset_imp_leadsTo], |
|
43 simpset() addsimps [insert_absorb, lessThan_Suc RS sym, |
|
44 lift_set_Un_distrib RS sym, |
|
45 Times_Un_distrib1 RS sym, |
|
46 Times_Diff_distrib1 RS sym])); |
|
47 by (rename_tac "n" 1); |
|
48 by (rtac PLam_leadsTo_Basis 1); |
|
49 by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym])); |
|
50 by (constrains_tac 1); |
|
51 by (res_inst_tac [("act", "decr")] transientI 1); |
|
52 by (auto_tac (claset(), simpset() addsimps [Timer_def])); |
|
53 qed "TimerArray_leadsTo_zero"; |
|