author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
Fri, 23 May 2014 15:19:32 +0100 | |
changeset 36 | af38526275f8 |
child 37 | c820ac0f3088 |
permissions | -rw-r--r-- |
36
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
theory Test |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
imports Precedence_ord |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
begin |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
type_synonym thread = nat -- {* Type for thread identifiers. *} |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
type_synonym priority = nat -- {* Type for priorities. *} |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
type_synonym cs = nat -- {* Type for critical sections (or critical resources). *} |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
datatype event = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
Create thread priority |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
| Exit thread |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
| P thread cs |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
| V thread cs |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
| Set thread priority |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
type_synonym state = "event list" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
fun threads :: "state \<Rightarrow> thread set" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
where |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
"threads [] = {}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
| "threads (Create th prio#s) = {th} \<union> threads s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
| "threads (Exit th # s) = (threads s) - {th}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
| "threads (_#s) = threads s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
where |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
"priority th [] = 0" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
| "priority th (Create th' prio#s) = (if th' = th then prio else priority th s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
| "priority th (Set th' prio#s) = (if th' = th then prio else priority th s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
| "priority th (_#s) = priority th s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
where |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
"last_set th [] = 0" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
| "last_set th ((Create th' prio)#s) = (if (th = th') then length s else last_set th s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
| "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
| "last_set th (_#s) = last_set th s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
where "preced th s \<equiv> Prc (priority th s) (last_set th s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
definition |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
"holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
definition |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
"waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
datatype node = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
Th "thread" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
| Cs "cs" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
definition |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
"RAG wq \<equiv> {(Th th, Cs cs) | th cs. waits wq th cs} \<union> {(Cs cs, Th th) | cs th. holds wq th cs}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
definition |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
"dependants wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
record schedule_state = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
wq_fun :: "cs \<Rightarrow> thread list" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
cprec_fun :: "thread \<Rightarrow> precedence" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
where |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
"cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
65 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
66 |
abbreviation |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
67 |
"all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
abbreviation |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
"initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
abbreviation |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
73 |
"release qs \<equiv> case qs of |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
[] => [] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
75 |
| (_#qs) => (SOME q. distinct q \<and> set q = set qs)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
76 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
77 |
fun schs :: "state \<Rightarrow> schedule_state" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
78 |
where |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
79 |
"schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
80 |
| "schs (Create th prio # s) = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
81 |
(let wq = wq_fun (schs s) in |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
82 |
(|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
| "schs (Exit th # s) = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
84 |
(let wq = wq_fun (schs s) in |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
85 |
(|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
86 |
| "schs (Set th prio # s) = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
87 |
(let wq = wq_fun (schs s) in |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
88 |
(|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
89 |
| "schs (P th cs # s) = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
90 |
(let wq = wq_fun (schs s) in |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
91 |
let new_wq = wq(cs := (wq cs @ [th])) in |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
92 |
(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
93 |
| "schs (V th cs # s) = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
94 |
(let wq = wq_fun (schs s) in |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
95 |
let new_wq = wq(cs := release (wq cs)) in |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
96 |
(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
97 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
98 |
definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
99 |
where "wq s = wq_fun (schs s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
100 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
102 |
where "cp s \<equiv> cprec_fun (schs s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
103 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
104 |
definition |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
105 |
"holds2 s \<equiv> holds (wq_fun (schs s))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
106 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
107 |
definition |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
108 |
"waits2 s \<equiv> waits (wq_fun (schs s))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
109 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
definition |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
"RAG2 s \<equiv> RAG (wq_fun (schs s))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
112 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
113 |
definition |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
114 |
"dependants2 s \<equiv> dependants (wq_fun (schs s))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
116 |
definition readys :: "state \<Rightarrow> thread set" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
117 |
where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waits2 s th cs)}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
118 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
119 |
definition runing :: "state \<Rightarrow> thread set" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
120 |
where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
121 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
122 |
definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
123 |
where "holding s th \<equiv> {cs . holds2 s th cs}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
124 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
125 |
lemma holding_RAG: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
126 |
"holding s th = {cs . (Cs cs, Th th) \<in> RAG2 s}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
127 |
unfolding holding_def |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
128 |
unfolding holds2_def |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
129 |
unfolding RAG2_def RAG_def |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
130 |
unfolding holds_def waits_def |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
131 |
by auto |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
132 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
133 |
inductive step :: "state \<Rightarrow> event \<Rightarrow> bool" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
134 |
where |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
135 |
step_Create: "\<lbrakk>th \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create th prio)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
136 |
| step_Exit: "\<lbrakk>th \<in> runing s; holding s th = {}\<rbrakk> \<Longrightarrow> step s (Exit th)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
137 |
| step_P: "\<lbrakk>th \<in> runing s; (Cs cs, Th th) \<notin> (RAG2 s)^+\<rbrakk> \<Longrightarrow> step s (P th cs)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
138 |
| step_V: "\<lbrakk>th \<in> runing s; holds2 s th cs\<rbrakk> \<Longrightarrow> step s (V th cs)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
139 |
| step_Set: "\<lbrakk>th \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set th prio)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
140 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
141 |
inductive vt :: "state \<Rightarrow> bool" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
142 |
where |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
143 |
vt_nil[intro]: "vt []" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
144 |
| vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
145 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
146 |
lemma runing_ready: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
147 |
shows "runing s \<subseteq> readys s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
148 |
unfolding runing_def readys_def |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
149 |
by auto |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
150 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
151 |
lemma readys_threads: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
152 |
shows "readys s \<subseteq> threads s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
153 |
unfolding readys_def |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
154 |
by auto |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
155 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
156 |
lemma wq_distinct_step: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
157 |
assumes "step s e" "distinct (wq s cs)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
158 |
shows "distinct (wq (e # s) cs)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
159 |
using assms |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
160 |
apply(induct) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
161 |
apply(auto simp add: wq_def Let_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
162 |
apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def)[1] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
163 |
apply(auto split: list.split) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
164 |
apply(rule someI2) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
165 |
apply(auto) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
166 |
done |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
167 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
168 |
lemma wq_distinct: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
169 |
assumes "vt s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
170 |
shows "distinct (wq s cs)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
171 |
using assms |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
172 |
apply(induct) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
173 |
apply(simp add: wq_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
174 |
apply(simp add: wq_distinct_step) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
175 |
done |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
176 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
177 |
lemma RAG_set_unchanged[simp]: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
178 |
shows "RAG2 (Set th prio # s) = RAG2 s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
179 |
unfolding RAG2_def |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
180 |
by (simp add: Let_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
181 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
182 |
lemma RAG_create_unchanged[simp]: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
183 |
"RAG2 (Create th prio # s) = RAG2 s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
184 |
unfolding RAG2_def |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
185 |
by (simp add: Let_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
186 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
187 |
lemma RAG_exit_unchanged[simp]: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
188 |
shows "RAG2 (Exit th # s) = RAG2 s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
189 |
unfolding RAG2_def |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
190 |
by (simp add: Let_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
191 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
192 |
lemma RAG_p1: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
193 |
assumes "wq s cs = []" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
194 |
shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Cs cs, Th th)}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
195 |
using assms |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
196 |
apply(auto simp add: RAG2_def RAG_def wq_def Let_def waits_def holds_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
197 |
apply (metis in_set_insert insert_Nil list.distinct(1)) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
198 |
done |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
199 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
200 |
lemma RAG_p2: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
201 |
assumes "vt (P th cs#s)" "wq s cs \<noteq> []" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
202 |
shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Th th, Cs cs)}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
203 |
using assms |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
204 |
apply(simp add: RAG2_def Let_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
205 |
apply(erule_tac vt.cases) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
206 |
apply(simp) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
207 |
apply(clarify) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
208 |
apply(simp) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
209 |
apply(erule_tac step.cases) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
210 |
apply(simp_all) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
211 |
apply(simp add: wq_def RAG_def RAG2_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
212 |
apply(simp add: waits_def holds_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
213 |
apply(auto) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
214 |
done |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
215 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
216 |
definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
217 |
where "next_th s th cs t = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
218 |
(\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> t = hd (SOME q. distinct q \<and> set q = set rest))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
219 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
220 |
lemma RAG_v: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
221 |
assumes vt:"vt (V th cs#s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
222 |
shows " |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
223 |
RAG2 (V th cs # s) = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
224 |
RAG2 s - {(Cs cs, Th th)} - |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
225 |
{(Th th', Cs cs) |th'. next_th s th cs th'} \<union> |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
226 |
{(Cs cs, Th th') |th'. next_th s th cs th'}" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
227 |
apply (insert vt, unfold RAG2_def RAG_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
228 |
sorry |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
229 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
230 |
lemma waiting_unique: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
231 |
assumes "vt s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
232 |
and "waits2 s th cs1" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
233 |
and "waits2 s th cs2" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
234 |
shows "cs1 = cs2" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
235 |
sorry |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
236 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
237 |
lemma singleton_Un: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
238 |
shows "A \<union> {x} = insert x A" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
239 |
by simp |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
240 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
241 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
242 |
lemma acyclic_RAG_step: |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
243 |
assumes vt: "vt s" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
244 |
and stp: "step s e" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
245 |
and ac: "acyclic (RAG2 s)" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
246 |
shows "acyclic (RAG2 (e # s))" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
247 |
using stp vt ac |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
248 |
proof (induct) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
249 |
case (step_P th s cs) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
250 |
have vt: "vt s" by fact |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
251 |
have ac: "acyclic (RAG2 s)" by fact |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
252 |
have rn: "th \<in> runing s" by fact |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
253 |
have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
254 |
have vtt: "vt (P th cs#s)" using vt rn ds by (metis step.step_P vt_cons) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
255 |
{ assume a: "wq s cs = []" -- "case waiting queue is empty" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
256 |
have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>*" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
257 |
proof |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
258 |
assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>*" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
259 |
then have "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
260 |
then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
261 |
with a show False by (auto simp: RAG2_def RAG_def wq_def waits_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
262 |
qed |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
263 |
with acyclic_insert ac |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
264 |
have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
265 |
then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] by simp |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
266 |
} |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
267 |
moreover |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
268 |
{ assume a: "wq s cs \<noteq> []" -- "case waiting queue is not empty" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
269 |
from ds have "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
270 |
with acyclic_insert ac |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
271 |
have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by auto |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
272 |
then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF vtt a] by simp |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
273 |
} |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
274 |
ultimately show "acyclic (RAG2 (P th cs # s))" by metis |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
275 |
next |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
276 |
case (step_V th s cs) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
277 |
have vt: "vt s" by fact |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
278 |
have ac: "acyclic (RAG2 s)" by fact |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
279 |
have rn: "th \<in> runing s" by fact |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
280 |
have hd: "holds2 s th cs" by fact |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
281 |
from hd |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
282 |
have th_in: "th \<in> set (wq s cs)" and |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
283 |
eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
284 |
then obtain rest where |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
285 |
eq_wq: "wq s cs = th # rest" by (cases "wq s cs") (auto) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
286 |
show ?case |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
287 |
apply(subst RAG_v) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
288 |
apply(rule vt_cons) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
289 |
apply(rule vt) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
290 |
apply(rule step.step_V) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
291 |
apply(rule rn) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
292 |
apply(rule hd) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
293 |
using eq_wq |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
294 |
apply(cases "rest = []") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
295 |
apply(subgoal_tac "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
296 |
apply(simp) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
297 |
apply(rule acyclic_subset) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
298 |
apply(rule ac) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
299 |
apply(auto)[1] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
300 |
apply(auto simp add: next_th_def)[1] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
301 |
-- "case wq more than a singleton" |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
302 |
apply(subgoal_tac "{(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest)))} = |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
303 |
{(Cs cs, Th th') |th'. next_th s th cs th'}") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
304 |
apply(rotate_tac 2) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
305 |
apply(drule sym) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
306 |
apply(simp only: singleton_Un) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
307 |
apply(simp only: acyclic_insert) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
308 |
apply(rule conjI) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
309 |
apply(rule acyclic_subset) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
310 |
apply(rule ac) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
311 |
apply(auto)[1] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
312 |
apply(rotate_tac 2) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
313 |
apply(thin_tac "?X") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
314 |
defer |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
315 |
apply(simp add: next_th_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
316 |
apply(clarify) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
317 |
apply(simp add: rtrancl_eq_or_trancl) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
318 |
apply(drule tranclD) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
319 |
apply(erule exE) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
320 |
apply(drule conjunct1) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
321 |
apply(subgoal_tac "(Th (hd (SOME q. distinct q \<and> set q = set rest)), z) \<in> RAG2 s") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
322 |
prefer 2 |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
323 |
apply(simp) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
324 |
apply(case_tac z) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
325 |
apply(simp add: RAG2_def RAG_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
326 |
apply(clarify) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
327 |
apply(simp) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
328 |
apply(simp add: next_th_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
329 |
apply(rule waiting_unique) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
330 |
apply(rule vt) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
331 |
apply(simp add: RAG2_def RAG_def waits2_def waits_def wq_def) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
332 |
apply(rotate_tac 2) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
333 |
apply(thin_tac "?X") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
334 |
apply(subgoal_tac "distinct (wq s cs)") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
335 |
prefer 2 |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
336 |
apply(rule wq_distinct) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
337 |
apply(rule vt) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
338 |
apply (unfold waits2_def waits_def wq_def, auto) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
339 |
apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
340 |
prefer 2 |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
341 |
apply (metis (mono_tags) set_empty tfl_some) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
342 |
apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
343 |
set (SOME q. distinct q \<and> set q = set rest)") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
344 |
prefer 2 |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
345 |
apply(auto)[1] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
346 |
apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
347 |
prefer 2 |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
348 |
apply(rule someI2) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
349 |
apply(auto)[2] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
350 |
apply(auto)[1] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
351 |
apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
352 |
prefer 2 |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
353 |
apply (metis (mono_tags) set_empty tfl_some) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
354 |
apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
355 |
set (SOME q. distinct q \<and> set q = set rest)") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
356 |
prefer 2 |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
357 |
apply(auto)[1] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
358 |
apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
359 |
prefer 2 |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
360 |
apply(rule someI2) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
361 |
apply(auto)[2] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
362 |
apply(auto)[1] |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
363 |
done |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
364 |
qed (simp_all) |
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
365 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
366 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
367 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
368 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
369 |
|
af38526275f8
added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
370 |