author | wenzelm |
Sun, 15 Oct 2000 19:50:35 +0200 | |
changeset 10220 | 2a726de6e124 |
parent 9403 | aad13b59b8d9 |
permissions | -rw-r--r-- |
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 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
12 |
Addsimps [count_def, decr_def]; |
7513 | 13 |
|
14 |
(*Demonstrates induction, but not used in the following proof*) |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
15 |
Goal "Timer : UNIV leadsTo {s. count s = 0}"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
16 |
by (res_inst_tac [("f", "count")] lessThan_induct 1); |
7513 | 17 |
by (Simp_tac 1); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
18 |
by (case_tac "m" 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
19 |
by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1); |
7537 | 20 |
by (ensures_tac "decr" 1); |
7513 | 21 |
qed "Timer_leadsTo_zero"; |
22 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
23 |
Goal "Timer : preserves snd"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
24 |
by (rtac preservesI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
25 |
by (constrains_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
26 |
qed "Timer_preserves_snd"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
27 |
AddIffs [Timer_preserves_snd]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
28 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
29 |
Addsimps [PLam_stable]; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
30 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
31 |
Goal "finite I \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
32 |
\ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"; |
8703 | 33 |
by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")] |
7513 | 34 |
(finite_stable_completion RS leadsTo_weaken) 1); |
35 |
by Auto_tac; |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
36 |
(*Safety property, already reduced to the single Timer case*) |
7537 | 37 |
by (constrains_tac 2); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
38 |
(*Progress property for the array of Timers*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
39 |
by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
40 |
by (case_tac "m" 1); |
8703 | 41 |
(*Annoying need to massage the conditions to have the form (... <*> UNIV)*) |
7513 | 42 |
by (auto_tac (claset() addIs [subset_imp_leadsTo], |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
43 |
simpset() addsimps [insert_absorb, lessThan_Suc RS sym, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
44 |
lift_set_Un_distrib RS sym, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
45 |
Times_Un_distrib1 RS sym, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8041
diff
changeset
|
46 |
Times_Diff_distrib1 RS sym])); |
7513 | 47 |
by (rename_tac "n" 1); |
7537 | 48 |
by (rtac PLam_leadsTo_Basis 1); |
7513 | 49 |
by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym])); |
50 |
by (constrains_tac 1); |
|
8041 | 51 |
by (res_inst_tac [("act", "decr")] transientI 1); |
7513 | 52 |
by (auto_tac (claset(), simpset() addsimps [Timer_def])); |
53 |
qed "TimerArray_leadsTo_zero"; |