7513
|
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 |
|
7537
|
12 |
Addsimps [decr_def];
|
7513
|
13 |
|
|
14 |
(*Demonstrates induction, but not used in the following proof*)
|
|
15 |
Goal "Timer : UNIV leadsTo {0}";
|
|
16 |
by (res_inst_tac [("f", "id")] (allI RS lessThan_induct) 1);
|
|
17 |
by (Simp_tac 1);
|
|
18 |
by (exhaust_tac "m" 1);
|
|
19 |
by (blast_tac (claset() addSIs [subset_imp_leadsTo]) 1);
|
7537
|
20 |
by (ensures_tac "decr" 1);
|
7513
|
21 |
qed "Timer_leadsTo_zero";
|
|
22 |
|
|
23 |
Goal "finite I ==> (plam i: I. Timer) : UNIV leadsTo {s. ALL i:I. s i = 0}";
|
|
24 |
by (eres_inst_tac [("A'1", "%i. lift_set i {0}")]
|
|
25 |
(finite_stable_completion RS leadsTo_weaken) 1);
|
|
26 |
by Auto_tac;
|
7537
|
27 |
by (constrains_tac 2);
|
7513
|
28 |
by (res_inst_tac [("f", "sub i")] (allI RS lessThan_induct) 1);
|
|
29 |
by (exhaust_tac "m" 1);
|
|
30 |
by (auto_tac (claset() addIs [subset_imp_leadsTo],
|
|
31 |
simpset() addsimps [insert_absorb, lessThan_Suc RS sym]));
|
|
32 |
by (rename_tac "n" 1);
|
7537
|
33 |
by (rtac PLam_leadsTo_Basis 1);
|
7513
|
34 |
by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
|
|
35 |
by (constrains_tac 1);
|
8041
|
36 |
by (res_inst_tac [("act", "decr")] transientI 1);
|
7513
|
37 |
by (auto_tac (claset(), simpset() addsimps [Timer_def]));
|
|
38 |
qed "TimerArray_leadsTo_zero";
|