author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 16184 | 80617b8d33c5 |
child 18556 | dc39832e9280 |
permissions | -rw-r--r-- |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Mutex.thy |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
|
16417 | 9 |
theory Mutex imports UNITY_Main begin |
11195
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 |
record state = |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
p :: bool |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
m :: int |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
n :: int |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
u :: bool |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
v :: bool |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
types command = "(state*state) set" |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
constdefs |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
(** The program for process U **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
U0 :: command |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
25 |
"U0 == {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
U1 :: command |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
28 |
"U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
U2 :: command |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
31 |
"U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
U3 :: command |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
34 |
"U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
U4 :: command |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
37 |
"U4 == {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
38 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
(** The program for process V **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
40 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
41 |
V0 :: command |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
42 |
"V0 == {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
43 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
44 |
V1 :: command |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
45 |
"V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
46 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
47 |
V2 :: command |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
48 |
"V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
49 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
50 |
V3 :: command |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
51 |
"V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
52 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
53 |
V4 :: command |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
54 |
"V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
55 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
56 |
Mutex :: "state program" |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
57 |
"Mutex == mk_total_program |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
58 |
({s. ~ u s & ~ v s & m s = 0 & n s = 0}, |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
59 |
{U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
60 |
UNIV)" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
61 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
62 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
63 |
(** The correct invariants **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
64 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
65 |
IU :: "state set" |
13806 | 66 |
"IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
67 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
68 |
IV :: "state set" |
13806 | 69 |
"IV == {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
70 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
71 |
(** The faulty invariant (for U alone) **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
72 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
73 |
bad_IU :: "state set" |
13806 | 74 |
"bad_IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) & |
75 |
(3 \<le> m s & m s \<le> 4 --> ~ p s)}" |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
76 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
77 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
78 |
declare Mutex_def [THEN def_prg_Init, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
79 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
80 |
declare U0_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
81 |
declare U1_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
82 |
declare U2_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
83 |
declare U3_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
84 |
declare U4_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
85 |
declare V0_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
86 |
declare V1_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
87 |
declare V2_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
88 |
declare V3_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
89 |
declare V4_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
90 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
91 |
declare IU_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
92 |
declare IV_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
93 |
declare bad_IU_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
94 |
|
13806 | 95 |
lemma IU: "Mutex \<in> Always IU" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
96 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
97 |
apply (unfold Mutex_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
98 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
99 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
100 |
|
13806 | 101 |
lemma IV: "Mutex \<in> Always IV" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
102 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
103 |
apply (unfold Mutex_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
104 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
105 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
106 |
(*The safety property: mutual exclusion*) |
13806 | 107 |
lemma mutual_exclusion: "Mutex \<in> Always {s. ~ (m s = 3 & n s = 3)}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
108 |
apply (rule Always_weaken) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
109 |
apply (rule Always_Int_I [OF IU IV], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
110 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
111 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
112 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
113 |
(*The bad invariant FAILS in V1*) |
13806 | 114 |
lemma "Mutex \<in> Always bad_IU" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
115 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
116 |
apply (unfold Mutex_def, safety, auto) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
117 |
(*Resulting state: n=1, p=false, m=4, u=false. |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
118 |
Execution of V1 (the command of process v guarded by n=1) sets p:=true, |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
119 |
violating the invariant!*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
120 |
oops |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
121 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
122 |
|
13806 | 123 |
lemma eq_123: "((1::int) \<le> i & i \<le> 3) = (i = 1 | i = 2 | i = 3)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
124 |
by arith |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
125 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
126 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
127 |
(*** Progress for U ***) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
128 |
|
13806 | 129 |
lemma U_F0: "Mutex \<in> {s. m s=2} Unless {s. m s=3}" |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
130 |
by (unfold Unless_def Mutex_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
131 |
|
13806 | 132 |
lemma U_F1: "Mutex \<in> {s. m s=1} LeadsTo {s. p s = v s & m s = 2}" |
133 |
by (unfold Mutex_def, ensures_tac U1) |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
134 |
|
13806 | 135 |
lemma U_F2: "Mutex \<in> {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
136 |
apply (cut_tac IU) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
137 |
apply (unfold Mutex_def, ensures_tac U2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
138 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
139 |
|
13806 | 140 |
lemma U_F3: "Mutex \<in> {s. m s = 3} LeadsTo {s. p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
141 |
apply (rule_tac B = "{s. m s = 4}" in LeadsTo_Trans) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
142 |
apply (unfold Mutex_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
143 |
apply (ensures_tac U3) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
144 |
apply (ensures_tac U4) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
145 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
146 |
|
13806 | 147 |
lemma U_lemma2: "Mutex \<in> {s. m s = 2} LeadsTo {s. p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
148 |
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
149 |
Int_lower2 [THEN subset_imp_LeadsTo]]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
150 |
apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
151 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
152 |
|
13806 | 153 |
lemma U_lemma1: "Mutex \<in> {s. m s = 1} LeadsTo {s. p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
154 |
by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
155 |
|
13806 | 156 |
lemma U_lemma123: "Mutex \<in> {s. 1 \<le> m s & m s \<le> 3} LeadsTo {s. p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
157 |
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
158 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
159 |
(*Misra's F4*) |
13806 | 160 |
lemma u_Leadsto_p: "Mutex \<in> {s. u s} LeadsTo {s. p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
161 |
by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
162 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
163 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
164 |
(*** Progress for V ***) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
165 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
166 |
|
13806 | 167 |
lemma V_F0: "Mutex \<in> {s. n s=2} Unless {s. n s=3}" |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
168 |
by (unfold Unless_def Mutex_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
169 |
|
13806 | 170 |
lemma V_F1: "Mutex \<in> {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
171 |
by (unfold Mutex_def, ensures_tac "V1") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
172 |
|
13806 | 173 |
lemma V_F2: "Mutex \<in> {s. p s & n s = 2} LeadsTo {s. n s = 3}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
174 |
apply (cut_tac IV) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
175 |
apply (unfold Mutex_def, ensures_tac "V2") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
176 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
177 |
|
13806 | 178 |
lemma V_F3: "Mutex \<in> {s. n s = 3} LeadsTo {s. ~ p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
179 |
apply (rule_tac B = "{s. n s = 4}" in LeadsTo_Trans) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
180 |
apply (unfold Mutex_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
181 |
apply (ensures_tac V3) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
182 |
apply (ensures_tac V4) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
183 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
184 |
|
13806 | 185 |
lemma V_lemma2: "Mutex \<in> {s. n s = 2} LeadsTo {s. ~ p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
186 |
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
187 |
Int_lower2 [THEN subset_imp_LeadsTo]]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
188 |
apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
189 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
190 |
|
13806 | 191 |
lemma V_lemma1: "Mutex \<in> {s. n s = 1} LeadsTo {s. ~ p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
192 |
by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
193 |
|
13806 | 194 |
lemma V_lemma123: "Mutex \<in> {s. 1 \<le> n s & n s \<le> 3} LeadsTo {s. ~ p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
195 |
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
196 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
197 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
198 |
(*Misra's F4*) |
13806 | 199 |
lemma v_Leadsto_not_p: "Mutex \<in> {s. v s} LeadsTo {s. ~ p s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
200 |
by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
201 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
202 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
203 |
(** Absence of starvation **) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
204 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
205 |
(*Misra's F6*) |
13806 | 206 |
lemma m1_Leadsto_3: "Mutex \<in> {s. m s = 1} LeadsTo {s. m s = 3}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
207 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
208 |
apply (rule_tac [2] U_F2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
209 |
apply (simp add: Collect_conj_eq) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
210 |
apply (subst Un_commute) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
211 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
212 |
apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
213 |
apply (rule U_F1 [THEN LeadsTo_weaken_R], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
214 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
215 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
216 |
(*The same for V*) |
13806 | 217 |
lemma n1_Leadsto_3: "Mutex \<in> {s. n s = 1} LeadsTo {s. n s = 3}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
218 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
219 |
apply (rule_tac [2] V_F2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
220 |
apply (simp add: Collect_conj_eq) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
221 |
apply (subst Un_commute) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
222 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
223 |
apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
224 |
apply (rule V_F1 [THEN LeadsTo_weaken_R], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
225 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
226 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
227 |
end |