author | paulson |
Fri, 24 Jan 2003 18:13:59 +0100 | |
changeset 13786 | ab8f39f48a6f |
parent 11194 | ea13ff5a26d1 |
child 13812 | 91713a1915ee |
permissions | -rw-r--r-- |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/TimerArray.thy |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
A trivial example of reasoning about an array of processes |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
|
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
9 |
theory TimerArray = UNITY_Main: |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
types 'a state = "nat * 'a" (*second component allows new variables*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
constdefs |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
count :: "'a state => nat" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
"count s == fst s" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
decr :: "('a state * 'a state) set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
"decr == UN n uu. {((Suc n, uu), (n,uu))}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
|
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
20 |
Timer :: "'a state program" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
"Timer == mk_program (UNIV, {decr}, UNIV)" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
|
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
23 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
24 |
declare Timer_def [THEN def_prg_Init, simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
25 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
26 |
declare count_def [simp] decr_def [simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
27 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
28 |
(*Demonstrates induction, but not used in the following proof*) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
29 |
lemma Timer_leadsTo_zero: "Timer : UNIV leadsTo {s. count s = 0}" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
30 |
apply (rule_tac f = count in lessThan_induct, simp) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
31 |
apply (case_tac "m") |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
32 |
apply (force intro!: subset_imp_leadsTo) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
33 |
apply (unfold Timer_def, ensures_tac "decr") |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
34 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
35 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
36 |
lemma Timer_preserves_snd [iff]: "Timer : preserves snd" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
37 |
apply (rule preservesI) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
38 |
apply (unfold Timer_def, constrains) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
39 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
40 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
41 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
42 |
declare PLam_stable [simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
43 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
44 |
lemma TimerArray_leadsTo_zero: |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
45 |
"finite I |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
46 |
==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
47 |
apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
48 |
in finite_stable_completion [THEN leadsTo_weaken]) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
49 |
apply auto |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
50 |
(*Safety property, already reduced to the single Timer case*) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
51 |
prefer 2 |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
52 |
apply (simp add: Timer_def, constrains) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
53 |
(*Progress property for the array of Timers*) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
54 |
apply (rule_tac f = "sub i o fst" in lessThan_induct) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
55 |
apply (case_tac "m") |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
56 |
(*Annoying need to massage the conditions to have the form (... <*> UNIV)*) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
57 |
apply (auto intro: subset_imp_leadsTo |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
58 |
simp add: insert_absorb |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
59 |
lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
60 |
Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric]) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
61 |
apply (rename_tac "n") |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
62 |
apply (rule PLam_leadsTo_Basis) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
63 |
apply (auto simp add: lessThan_Suc [symmetric]) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
64 |
apply (unfold Timer_def, constrains) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
65 |
apply (rule_tac act = decr in transientI, auto) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
66 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
67 |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
68 |
end |