author | paulson |
Thu, 03 Jul 2003 12:56:48 +0200 | |
changeset 14088 | 61bd46feb919 |
parent 14087 | cb07c3948668 |
child 15274 | c18f5b076e53 |
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/Priority |
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: Sidi O Ehmety, Cambridge University Computer Laboratory |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
Copyright 2001 University of Cambridge |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
5 |
*) |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
|
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
7 |
header{*The priority system*} |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
8 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
9 |
theory Priority = PriorityAux: |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
10 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
11 |
text{*From Charpentier and Chandy, |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
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
|
13 |
In J. Rolim (editor), Parallel and Distributed Processing, |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
14 |
Spriner LNCS 1586 (1999), pages 1215-1227.*} |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
types state = "(vertex*vertex)set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
types command = "vertex=>(state*state)set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
consts |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
(* the initial state *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
init :: "(vertex*vertex)set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
constdefs |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
(* from the definitions given in section 4.4 *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
(* i has highest priority in r *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
highest :: "[vertex, (vertex*vertex)set]=>bool" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
"highest i r == A i r = {}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
(* i has lowest priority in r *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
lowest :: "[vertex, (vertex*vertex)set]=>bool" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
"lowest i r == R i r = {}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
act :: command |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
34 |
"act i == {(s, s'). s'=reverse i s & highest i s}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
(* All components start with the same initial state *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
37 |
Component :: "vertex=>state program" |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13796
diff
changeset
|
38 |
"Component i == mk_total_program({init}, {act i}, UNIV)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
40 |
(* Abbreviations *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
41 |
Highest :: "vertex=>state set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
42 |
"Highest i == {s. highest i s}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
43 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
44 |
Lowest :: "vertex=>state set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
45 |
"Lowest i == {s. lowest i s}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
46 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
47 |
Acyclic :: "state set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
48 |
"Acyclic == {s. acyclic s}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
49 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
50 |
(* Every above set has a maximal vertex: two equivalent defs. *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
51 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
52 |
Maximal :: "state set" |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
53 |
"Maximal == \<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
54 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
55 |
Maximal' :: "state set" |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
56 |
"Maximal' == \<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
57 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
58 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
59 |
Safety :: "state set" |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
60 |
"Safety == \<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
61 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
62 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
63 |
(* Composition of a finite set of component; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
64 |
the vertex 'UNIV' is finite by assumption *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
65 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
66 |
system :: "state program" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
67 |
"system == JN i. Component i" |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
68 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
69 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
70 |
declare highest_def [simp] lowest_def [simp] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
71 |
declare Highest_def [THEN def_set_simp, simp] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
72 |
and Lowest_def [THEN def_set_simp, simp] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
73 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
74 |
declare Component_def [THEN def_prg_Init, simp] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
75 |
declare act_def [THEN def_act_simp, simp] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
76 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
77 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
78 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
79 |
subsection{*Component correctness proofs*} |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
80 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
81 |
(* neighbors is stable *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
82 |
lemma Component_neighbors_stable: "Component i \<in> stable {s. neighbors k s = n}" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
83 |
by (simp add: Component_def, constrains, auto) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
84 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
85 |
(* property 4 *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
86 |
lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
87 |
by (simp add: Component_def, constrains) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
88 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
89 |
(* property 5: charpentier and Chandy mistakenly express it as |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
90 |
'transient Highest i'. Consider the case where i has neighbors *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
91 |
lemma Component_yields_priority: |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
92 |
"Component i: {s. neighbors i s \<noteq> {}} Int Highest i |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
93 |
ensures - Highest i" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
94 |
apply (simp add: Component_def) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
95 |
apply (ensures_tac "act i", blast+) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
96 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
97 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
98 |
(* or better *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
99 |
lemma Component_yields_priority': "Component i \<in> Highest i ensures Lowest i" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
100 |
apply (simp add: Component_def) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
101 |
apply (ensures_tac "act i", blast+) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
102 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
103 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
104 |
(* property 6: Component doesn't introduce cycle *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
105 |
lemma Component_well_behaves: "Component i \<in> Highest i co Highest i Un Lowest i" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
106 |
by (simp add: Component_def, constrains, fast) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
107 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
108 |
(* property 7: local axiom *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
109 |
lemma locality: "Component i \<in> stable {s. \<forall>j k. j\<noteq>i & k\<noteq>i--> ((j,k):s) = b j k}" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
110 |
by (simp add: Component_def, constrains) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
111 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
112 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
113 |
subsection{*System properties*} |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
114 |
(* property 8: strictly universal *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
115 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
116 |
lemma Safety: "system \<in> stable Safety" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
117 |
apply (unfold Safety_def) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
118 |
apply (rule stable_INT) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
119 |
apply (simp add: system_def, constrains, fast) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
120 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
121 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
122 |
(* property 13: universal *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
123 |
lemma p13: "system \<in> {s. s = q} co {s. s=q} Un {s. \<exists>i. derive i q s}" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
124 |
by (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains, blast) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
125 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
126 |
(* property 14: the 'above set' of a Component that hasn't got |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
127 |
priority doesn't increase *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
128 |
lemma above_not_increase: |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
14087
diff
changeset
|
129 |
"system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}" |
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
14087
diff
changeset
|
130 |
apply (insert reach_lemma [of concl: j]) |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
131 |
apply (simp add: system_def Component_def mk_total_program_def totalize_JN, |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
132 |
constrains) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
14087
diff
changeset
|
133 |
apply (simp add: trancl_converse, blast) |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
134 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
135 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
136 |
lemma above_not_increase': |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
137 |
"system \<in> -Highest i Int {s. above i s = x} co {s. above i s <= x}" |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
14087
diff
changeset
|
138 |
apply (insert above_not_increase [of i]) |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
139 |
apply (simp add: trancl_converse constrains_def, blast) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
140 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
141 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
142 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
143 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
144 |
(* p15: universal property: all Components well behave *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
145 |
lemma system_well_behaves [rule_format]: |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
146 |
"\<forall>i. system \<in> Highest i co Highest i Un Lowest i" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
147 |
apply clarify |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
148 |
apply (simp add: system_def Component_def mk_total_program_def totalize_JN, |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
149 |
constrains, auto) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
150 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
151 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
152 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
153 |
lemma Acyclic_eq: "Acyclic = (\<Inter>i. {s. i\<notin>above i s})" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
154 |
by (auto simp add: Acyclic_def acyclic_def trancl_converse) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
155 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
156 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
157 |
lemmas system_co = |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
158 |
constrains_Un [OF above_not_increase [rule_format] system_well_behaves] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
159 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
160 |
lemma Acyclic_stable: "system \<in> stable Acyclic" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
161 |
apply (simp add: stable_def Acyclic_eq) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
162 |
apply (auto intro!: constrains_INT system_co [THEN constrains_weaken] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
163 |
simp add: image0_r_iff_image0_trancl trancl_converse) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
164 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
165 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
166 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
167 |
lemma Acyclic_subset_Maximal: "Acyclic <= Maximal" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
168 |
apply (unfold Acyclic_def Maximal_def, clarify) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
169 |
apply (drule above_lemma_b, auto) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
170 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
171 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
172 |
(* property 17: original one is an invariant *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
173 |
lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)" |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
14087
diff
changeset
|
174 |
by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable) |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
175 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
176 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
177 |
(* propert 5: existential property *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
178 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
179 |
lemma Highest_leadsTo_Lowest: "system \<in> Highest i leadsTo Lowest i" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
180 |
apply (simp add: system_def Component_def mk_total_program_def totalize_JN) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
181 |
apply (ensures_tac "act i", auto) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
182 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
183 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
184 |
(* a lowest i can never be in any abover set *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
185 |
lemma Lowest_above_subset: "Lowest i <= (\<Inter>k. {s. i\<notin>above k s})" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
186 |
by (auto simp add: image0_r_iff_image0_trancl trancl_converse) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
187 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
188 |
(* property 18: a simpler proof than the original, one which uses psp *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
189 |
lemma Highest_escapes_above: "system \<in> Highest i leadsTo (\<Inter>k. {s. i\<notin>above k s})" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
190 |
apply (rule leadsTo_weaken_R) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
191 |
apply (rule_tac [2] Lowest_above_subset) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
192 |
apply (rule Highest_leadsTo_Lowest) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
193 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
194 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
195 |
lemma Highest_escapes_above': |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
196 |
"system \<in> Highest j Int {s. j \<in> above i s} leadsTo {s. j\<notin>above i s}" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
197 |
by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower]) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
198 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
199 |
(*** The main result: above set decreases ***) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
200 |
(* The original proof of the following formula was wrong *) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
201 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
202 |
lemma Highest_iff_above0: "Highest i = {s. above i s ={}}" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
203 |
by (auto simp add: image0_trancl_iff_image0_r) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
204 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
205 |
lemmas above_decreases_lemma = |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
206 |
psp [THEN leadsTo_weaken, OF Highest_escapes_above' above_not_increase'] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
207 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
208 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
209 |
lemma above_decreases: |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
210 |
"system \<in> (\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
211 |
leadsTo {s. above i s < x}" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
212 |
apply (rule leadsTo_UN) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
213 |
apply (rule single_leadsTo_I, clarify) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
214 |
apply (rule_tac x2 = "above i x" in above_decreases_lemma) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
14087
diff
changeset
|
215 |
apply (simp_all (no_asm_use) add: Highest_iff_above0) |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
216 |
apply blast+ |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
217 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
218 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
219 |
(** Just a massage of conditions to have the desired form ***) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
220 |
lemma Maximal_eq_Maximal': "Maximal = Maximal'" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
221 |
by (unfold Maximal_def Maximal'_def Highest_def, blast) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
222 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
223 |
lemma Acyclic_subset: |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
224 |
"x\<noteq>{} ==> |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
225 |
Acyclic Int {s. above i s = x} <= |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
226 |
(\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j)" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
227 |
apply (rule_tac B = "Maximal' Int {s. above i s = x}" in subset_trans) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
228 |
apply (simp (no_asm) add: Maximal_eq_Maximal' [symmetric]) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
229 |
apply (blast intro: Acyclic_subset_Maximal [THEN subsetD]) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
230 |
apply (simp (no_asm) del: above_def add: Maximal'_def Highest_iff_above0) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
231 |
apply blast |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
232 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
233 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
234 |
lemmas above_decreases' = leadsTo_weaken_L [OF above_decreases Acyclic_subset] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
235 |
lemmas above_decreases_psp = psp_stable [OF above_decreases' Acyclic_stable] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
236 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
237 |
lemma above_decreases_psp': |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
238 |
"x\<noteq>{}==> system \<in> Acyclic Int {s. above i s = x} leadsTo |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
239 |
Acyclic Int {s. above i s < x}" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
240 |
by (erule above_decreases_psp [THEN leadsTo_weaken], blast, auto) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
241 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
242 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
243 |
lemmas finite_psubset_induct = wf_finite_psubset [THEN leadsTo_wf_induct] |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
244 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
245 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
246 |
lemma Progress: "system \<in> Acyclic leadsTo Highest i" |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
247 |
apply (rule_tac f = "%s. above i s" in finite_psubset_induct) |
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
14087
diff
changeset
|
248 |
apply (simp del: above_def |
14087
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
249 |
add: Highest_iff_above0 vimage_def finite_psubset_def, clarify) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
250 |
apply (case_tac "m={}") |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
251 |
apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L]) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
252 |
apply (force simp add: leadsTo_refl) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
253 |
apply (rule_tac A' = "Acyclic Int {x. above i x < m}" in leadsTo_weaken_R) |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
254 |
apply (blast intro: above_decreases_psp')+ |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
255 |
done |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
256 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
257 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
258 |
text{*We have proved all (relevant) theorems given in the paper. We didn't |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
259 |
assume any thing about the relation @{term r}. It is not necessary that |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
260 |
@{term r} be a priority relation as assumed in the original proof. It |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
261 |
suffices that we start from a state which is finite and acyclic.*} |
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
262 |
|
cb07c3948668
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents:
13812
diff
changeset
|
263 |
|
14088
61bd46feb919
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
paulson
parents:
14087
diff
changeset
|
264 |
end |