author | wenzelm |
Sat, 02 Apr 2016 15:06:41 +0200 | |
changeset 62813 | 3e001fe6f16a |
parent 54863 | 82acc20ded73 |
child 63146 | f1ecba0272f9 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/Simple/Common.thy |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 1998 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
Common Meeting Time example from Misra (1994) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
The state is identified with the one variable in existence. |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1. |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
|
32692 | 12 |
theory Common |
13 |
imports "../UNITY_Main" |
|
14 |
begin |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
consts |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
17 |
ftime :: "nat=>nat" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
18 |
gtime :: "nat=>nat" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
|
44871 | 20 |
axiomatization where |
21 |
fmono: "m \<le> n ==> ftime m \<le> ftime n" and |
|
22 |
gmono: "m \<le> n ==> gtime m \<le> gtime n" and |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
|
44871 | 24 |
fasc: "m \<le> ftime n" and |
13806 | 25 |
gasc: "m \<le> gtime n" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32697
diff
changeset
|
27 |
definition common :: "nat set" where |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
"common == {n. ftime n = n & gtime n = n}" |
65ede8dfe304
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:
32697
diff
changeset
|
30 |
definition maxfg :: "nat => nat set" where |
13806 | 31 |
"maxfg m == {t. t \<le> max (ftime m) (gtime m)}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
33 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
34 |
(*Misra's property CMT4: t exceeds no common meeting time*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
35 |
lemma common_stable: |
13806 | 36 |
"[| \<forall>m. F \<in> {m} Co (maxfg m); n \<in> common |] |
37 |
==> F \<in> Stable (atMost n)" |
|
38 |
apply (drule_tac M = "{t. t \<le> n}" in Elimination_sing) |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
39 |
apply (simp add: atMost_def Stable_def common_def maxfg_def le_max_iff_disj) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
40 |
apply (erule Constrains_weaken_R) |
21026 | 41 |
apply (blast intro: order_eq_refl le_trans dest: fmono gmono) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
42 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
43 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
44 |
lemma common_safety: |
13806 | 45 |
"[| Init F \<subseteq> atMost n; |
46 |
\<forall>m. F \<in> {m} Co (maxfg m); n \<in> common |] |
|
47 |
==> F \<in> Always (atMost n)" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
48 |
by (simp add: AlwaysI common_stable) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
49 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
50 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
51 |
(*** Some programs that implement the safety property above ***) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
52 |
|
13806 | 53 |
lemma "SKIP \<in> {m} co (maxfg m)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
54 |
by (simp add: constrains_def maxfg_def le_max_iff_disj fasc) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
55 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
56 |
(*This one is t := ftime t || t := gtime t*) |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
57 |
lemma "mk_total_program |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
58 |
(UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) |
13806 | 59 |
\<in> {m} co (maxfg m)" |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
60 |
apply (simp add: mk_total_program_def) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
61 |
apply (simp add: constrains_def maxfg_def le_max_iff_disj fasc) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
62 |
done |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
63 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
64 |
(*This one is t := max (ftime t) (gtime t)*) |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
65 |
lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) |
13806 | 66 |
\<in> {m} co (maxfg m)" |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
67 |
apply (simp add: mk_total_program_def) |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
44871
diff
changeset
|
68 |
apply (simp add: constrains_def maxfg_def gasc max.absorb2) |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
69 |
done |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
70 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
71 |
(*This one is t := t+1 if t <max (ftime t) (gtime t) *) |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
72 |
lemma "mk_total_program |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
73 |
(UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV) |
13806 | 74 |
\<in> {m} co (maxfg m)" |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
75 |
apply (simp add: mk_total_program_def) |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
44871
diff
changeset
|
76 |
apply (simp add: constrains_def maxfg_def gasc max.absorb2) |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
77 |
done |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
78 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
79 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
80 |
(*It remans to prove that they satisfy CMT3': t does not decrease, |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
81 |
and that CMT3' implies that t stops changing once common(t) holds.*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
82 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
83 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
84 |
(*** Progress under weak fairness ***) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
85 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
86 |
lemma leadsTo_common_lemma: |
32629 | 87 |
assumes "\<forall>m. F \<in> {m} Co (maxfg m)" |
88 |
and "\<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m)" |
|
89 |
and "n \<in> common" |
|
90 |
shows "F \<in> (atMost n) LeadsTo common" |
|
91 |
proof (rule LeadsTo_weaken_R) |
|
92 |
show "F \<in> {..n} LeadsTo {..n} \<inter> id -` {n..} \<union> common" |
|
93 |
proof (induct rule: GreaterThan_bounded_induct [of n _ _ id]) |
|
94 |
case 1 |
|
95 |
from assms have "\<forall>m\<in>{..<n}. F \<in> {..n} \<inter> {m} LeadsTo {..n} \<inter> {m<..} \<union> common" |
|
96 |
by (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R) |
|
97 |
then show ?case by simp |
|
98 |
qed |
|
99 |
next |
|
100 |
from `n \<in> common` |
|
101 |
show "{..n} \<inter> id -` {n..} \<union> common \<subseteq> common" |
|
102 |
by (simp add: atMost_Int_atLeast) |
|
103 |
qed |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
104 |
|
13806 | 105 |
(*The "\<forall>m \<in> -common" form echoes CMT6.*) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
106 |
lemma leadsTo_common: |
13806 | 107 |
"[| \<forall>m. F \<in> {m} Co (maxfg m); |
108 |
\<forall>m \<in> -common. F \<in> {m} LeadsTo (greaterThan m); |
|
109 |
n \<in> common |] |
|
110 |
==> F \<in> (atMost (LEAST n. n \<in> common)) LeadsTo common" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
111 |
apply (rule leadsTo_common_lemma) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
112 |
apply (simp_all (no_asm_simp)) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
113 |
apply (erule_tac [2] LeastI) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
114 |
apply (blast dest!: not_less_Least) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
115 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
116 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
117 |
end |