author | Christian Sternagel |
Thu, 30 Aug 2012 15:44:03 +0900 | |
changeset 49093 | fdc301f592c4 |
parent 42463 | f270e3e18be5 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/Simple/Mutex.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 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
18556
diff
changeset
|
5 |
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra. |
11195
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 |
|
18556 | 8 |
theory Mutex imports "../UNITY_Main" begin |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
record state = |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
p :: bool |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
m :: int |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
n :: int |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
u :: bool |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
v :: bool |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
|
42463 | 17 |
type_synonym command = "(state*state) set" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
|
36866 | 19 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
(** The program for process U **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
|
36866 | 22 |
definition U0 :: command |
23 |
where "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
|
24 |
|
36866 | 25 |
definition U1 :: command |
26 |
where "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
|
27 |
|
36866 | 28 |
definition U2 :: command |
29 |
where "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
|
30 |
|
36866 | 31 |
definition U3 :: command |
32 |
where "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
|
33 |
|
36866 | 34 |
definition U4 :: command |
35 |
where "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
|
36 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
37 |
(** The program for process V **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
38 |
|
36866 | 39 |
definition V0 :: command |
40 |
where "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
|
41 |
|
36866 | 42 |
definition V1 :: command |
43 |
where "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
|
44 |
|
36866 | 45 |
definition V2 :: command |
46 |
where "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
|
47 |
|
36866 | 48 |
definition V3 :: command |
49 |
where "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
|
50 |
|
36866 | 51 |
definition V4 :: command |
52 |
where "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
|
53 |
|
36866 | 54 |
definition Mutex :: "state program" |
55 |
where "Mutex = mk_total_program |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
56 |
({s. ~ u s & ~ v s & m s = 0 & n s = 0}, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
18556
diff
changeset
|
57 |
{U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset
|
58 |
UNIV)" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
59 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
60 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
61 |
(** The correct invariants **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
62 |
|
36866 | 63 |
definition IU :: "state set" |
64 |
where "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
|
65 |
|
36866 | 66 |
definition IV :: "state set" |
67 |
where "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
|
68 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
69 |
(** The faulty invariant (for U alone) **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
70 |
|
36866 | 71 |
definition bad_IU :: "state set" |
72 |
where "bad_IU = {s. (u s = (1 \<le> m s & m s \<le> 3)) & |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
18556
diff
changeset
|
73 |
(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
|
74 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
75 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
76 |
declare Mutex_def [THEN def_prg_Init, simp] |
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 U0_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
79 |
declare U1_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
80 |
declare U2_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
81 |
declare U3_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
82 |
declare U4_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
83 |
declare V0_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
84 |
declare V1_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
85 |
declare V2_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
86 |
declare V3_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
87 |
declare V4_def [THEN def_act_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
88 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
89 |
declare IU_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
90 |
declare IV_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
91 |
declare bad_IU_def [THEN def_set_simp, simp] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
92 |
|
13806 | 93 |
lemma IU: "Mutex \<in> Always IU" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
94 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
95 |
apply (unfold Mutex_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
96 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
97 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
98 |
|
13806 | 99 |
lemma IV: "Mutex \<in> Always IV" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
100 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
101 |
apply (unfold Mutex_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
102 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
103 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
104 |
(*The safety property: mutual exclusion*) |
13806 | 105 |
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
|
106 |
apply (rule Always_weaken) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
107 |
apply (rule Always_Int_I [OF IU IV], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
108 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
109 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
110 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
111 |
(*The bad invariant FAILS in V1*) |
13806 | 112 |
lemma "Mutex \<in> Always bad_IU" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
113 |
apply (rule AlwaysI, force) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
114 |
apply (unfold Mutex_def, safety, auto) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
115 |
(*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
|
116 |
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
|
117 |
violating the invariant!*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
118 |
oops |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
119 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
120 |
|
13806 | 121 |
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
|
122 |
by arith |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
123 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
124 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
125 |
(*** Progress for U ***) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
126 |
|
13806 | 127 |
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
|
128 |
by (unfold Unless_def Mutex_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
129 |
|
13806 | 130 |
lemma U_F1: "Mutex \<in> {s. m s=1} LeadsTo {s. p s = v s & m s = 2}" |
131 |
by (unfold Mutex_def, ensures_tac U1) |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
132 |
|
13806 | 133 |
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
|
134 |
apply (cut_tac IU) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
135 |
apply (unfold Mutex_def, ensures_tac U2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
136 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
137 |
|
13806 | 138 |
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
|
139 |
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
|
140 |
apply (unfold Mutex_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
141 |
apply (ensures_tac U3) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
142 |
apply (ensures_tac U4) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
143 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
144 |
|
13806 | 145 |
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
|
146 |
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
147 |
Int_lower2 [THEN subset_imp_LeadsTo]]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
148 |
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
|
149 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
150 |
|
13806 | 151 |
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
|
152 |
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
|
153 |
|
13806 | 154 |
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
|
155 |
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
|
156 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
157 |
(*Misra's F4*) |
13806 | 158 |
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
|
159 |
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
|
160 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
161 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
162 |
(*** Progress for V ***) |
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 |
|
13806 | 165 |
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
|
166 |
by (unfold Unless_def Mutex_def, safety) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
167 |
|
13806 | 168 |
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
|
169 |
by (unfold Mutex_def, ensures_tac "V1") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
170 |
|
13806 | 171 |
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
|
172 |
apply (cut_tac IV) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
173 |
apply (unfold Mutex_def, ensures_tac "V2") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
174 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
175 |
|
13806 | 176 |
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
|
177 |
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
|
178 |
apply (unfold Mutex_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
179 |
apply (ensures_tac V3) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
180 |
apply (ensures_tac V4) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
181 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
182 |
|
13806 | 183 |
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
|
184 |
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
185 |
Int_lower2 [THEN subset_imp_LeadsTo]]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
186 |
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
|
187 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
188 |
|
13806 | 189 |
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
|
190 |
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
|
191 |
|
13806 | 192 |
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
|
193 |
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
|
194 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
195 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
196 |
(*Misra's F4*) |
13806 | 197 |
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
|
198 |
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
|
199 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
200 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
201 |
(** Absence of starvation **) |
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 |
(*Misra's F6*) |
13806 | 204 |
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
|
205 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
206 |
apply (rule_tac [2] U_F2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
207 |
apply (simp add: Collect_conj_eq) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
208 |
apply (subst Un_commute) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
209 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
210 |
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
|
211 |
apply (rule U_F1 [THEN LeadsTo_weaken_R], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
212 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
213 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
214 |
(*The same for V*) |
13806 | 215 |
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
|
216 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
217 |
apply (rule_tac [2] V_F2) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
218 |
apply (simp add: Collect_conj_eq) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
219 |
apply (subst Un_commute) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
220 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
221 |
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
|
222 |
apply (rule V_F1 [THEN LeadsTo_weaken_R], auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
223 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11868
diff
changeset
|
224 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
225 |
end |