author | haftmann |
Fri, 11 Jun 2010 17:14:02 +0200 | |
changeset 37407 | 61dd8c145da7 |
parent 36866 | 426d5781bb25 |
child 42463 | f270e3e18be5 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
18556
diff
changeset
|
1 |
(* Title: HOL/UNITY/Comp/Counter.thy |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 2001 University of Cambridge |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
From Charpentier and Chandy, |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
Examples of Program Composition Illustrating the Use of Universal Properties |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
In J. Rolim (editor), Parallel and Distributed Processing, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
18556
diff
changeset
|
8 |
Springer LNCS 1586 (1999), pages 1215-1227. |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
|
14094 | 11 |
header{*A Family of Similar Counters: Original Version*} |
12 |
||
18556 | 13 |
theory Counter imports "../UNITY_Main" begin |
13792 | 14 |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
(* Variables are names *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
datatype name = C | c nat |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
17 |
types state = "name=>int" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
19 |
primrec sum :: "[nat,state]=>int" where |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
20 |
(* sum I s = sigma_{i<I}. s (c i) *) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
21 |
"sum 0 s = 0" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
22 |
| "sum (Suc i) s = s (c i) + sum i s" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
24 |
primrec sumj :: "[nat, nat, state]=>int" where |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
25 |
"sumj 0 i s = 0" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
26 |
| "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
types command = "(state*state)set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
30 |
definition a :: "nat=>command" where |
36866 | 31 |
"a i = {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
33 |
definition Component :: "nat => state program" where |
36866 | 34 |
"Component i = |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13792
diff
changeset
|
35 |
mk_total_program({s. s C = 0 & s (c i) = 0}, {a i}, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
18556
diff
changeset
|
36 |
\<Union>G \<in> preserves (%s. s (c i)). Acts G)" |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
37 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
38 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
39 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
40 |
declare Component_def [THEN def_prg_Init, simp] |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
41 |
declare a_def [THEN def_act_simp, simp] |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
42 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
43 |
(* Theorems about sum and sumj *) |
14094 | 44 |
lemma sum_upd_gt [rule_format]: "\<forall>n. I<n --> sum I (s(c n := x)) = sum I s" |
45 |
by (induct_tac "I", auto) |
|
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
46 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
47 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
48 |
lemma sum_upd_eq: "sum I (s(c I := x)) = sum I s" |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
49 |
apply (induct_tac "I") |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
50 |
apply (auto simp add: sum_upd_gt [unfolded fun_upd_def]) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
51 |
done |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
52 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
53 |
lemma sum_upd_C: "sum I (s(C := x)) = sum I s" |
14094 | 54 |
by (induct_tac "I", auto) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
55 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
56 |
lemma sumj_upd_ci: "sumj I i (s(c i := x)) = sumj I i s" |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
57 |
apply (induct_tac "I") |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
58 |
apply (auto simp add: sum_upd_eq [unfolded fun_upd_def]) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
59 |
done |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
60 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
61 |
lemma sumj_upd_C: "sumj I i (s(C := x)) = sumj I i s" |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
62 |
apply (induct_tac "I") |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
63 |
apply (auto simp add: sum_upd_C [unfolded fun_upd_def]) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
64 |
done |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
65 |
|
14094 | 66 |
lemma sumj_sum_gt [rule_format]: "\<forall>i. I<i--> (sumj I i s = sum I s)" |
67 |
by (induct_tac "I", auto) |
|
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
68 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
69 |
lemma sumj_sum_eq: "(sumj I I s = sum I s)" |
14094 | 70 |
apply (induct_tac "I", auto) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
71 |
apply (simp (no_asm) add: sumj_sum_gt) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
72 |
done |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
73 |
|
14094 | 74 |
lemma sum_sumj [rule_format]: "\<forall>i. i<I-->(sum I s = s (c i) + sumj I i s)" |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
75 |
apply (induct_tac "I") |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
76 |
apply (auto simp add: linorder_neq_iff sumj_sum_eq) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
77 |
done |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
78 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
79 |
(* Correctness proofs for Components *) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
80 |
(* p2 and p3 proofs *) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
81 |
lemma p2: "Component i \<in> stable {s. s C = s (c i) + k}" |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14094
diff
changeset
|
82 |
by (simp add: Component_def, safety) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
83 |
|
14094 | 84 |
lemma p3: "Component i \<in> stable {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v}" |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14094
diff
changeset
|
85 |
by (simp add: Component_def, safety) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
86 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
87 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
88 |
lemma p2_p3_lemma1: |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
89 |
"(\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k} |
14094 | 90 |
\<inter> {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v})) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
91 |
= (Component i \<in> stable {s. s C = s (c i) + sumj I i s})" |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
92 |
apply (simp add: Component_def mk_total_program_def) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
93 |
apply (auto simp add: constrains_def stable_def sumj_upd_C sumj_upd_ci) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
94 |
done |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
95 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
96 |
lemma p2_p3_lemma2: |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
97 |
"\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k} Int |
14094 | 98 |
{s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v})" |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
99 |
by (blast intro: stable_Int [OF p2 p3]) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
100 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
101 |
lemma p2_p3: "Component i \<in> stable {s. s C = s (c i) + sumj I i s}" |
14094 | 102 |
by (auto intro!: p2_p3_lemma2 simp add: p2_p3_lemma1 [symmetric]) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
103 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
104 |
(* Compositional Proof *) |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
105 |
|
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
106 |
lemma sum_0' [rule_format]: "(\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0" |
14094 | 107 |
by (induct_tac "I", auto) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
108 |
|
14094 | 109 |
(* I cannot be empty *) |
110 |
lemma safety: |
|
111 |
"0<I ==> (\<Squnion>i \<in> {i. i<I}. Component i) \<in> invariant {s. s C = sum I s}" |
|
112 |
apply (simp (no_asm) add: invariant_def JN_stable sum_sumj) |
|
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
113 |
apply (force intro: p2_p3 sum_0') |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
13812
diff
changeset
|
114 |
done |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13792
diff
changeset
|
115 |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
116 |
end |