6 Unordered Channel |
6 Unordered Channel |
7 |
7 |
8 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 |
8 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 |
9 *) |
9 *) |
10 |
10 |
11 Channel = WFair + |
11 theory Channel = UNITY_Main: |
12 |
12 |
13 types state = nat set |
13 types state = "nat set" |
14 |
14 |
15 consts |
15 consts |
16 F :: state program |
16 F :: "state program" |
17 |
17 |
18 constdefs |
18 constdefs |
19 minSet :: nat set => nat option |
19 minSet :: "nat set => nat option" |
20 "minSet A == if A={} then None else Some (LEAST x. x:A)" |
20 "minSet A == if A={} then None else Some (LEAST x. x:A)" |
21 |
21 |
22 rules |
22 axioms |
23 |
23 |
24 UC1 "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))" |
24 UC1: "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))" |
25 |
25 |
26 (* UC1 "F : {s. minSet s = x} co {s. x <= minSet s}" *) |
26 (* UC1 "F : {s. minSet s = x} co {s. x <= minSet s}" *) |
27 |
27 |
28 UC2 "F : (minSet -` {Some x}) leadsTo {s. x ~: s}" |
28 UC2: "F : (minSet -` {Some x}) leadsTo {s. x ~: s}" |
|
29 |
|
30 |
|
31 (*None represents "infinity" while Some represents proper integers*) |
|
32 lemma minSet_eq_SomeD: "minSet A = Some x ==> x : A" |
|
33 apply (unfold minSet_def) |
|
34 apply (simp split: split_if_asm) |
|
35 apply (fast intro: LeastI) |
|
36 done |
|
37 |
|
38 lemma minSet_empty [simp]: " minSet{} = None" |
|
39 by (unfold minSet_def, simp) |
|
40 |
|
41 lemma minSet_nonempty: "x:A ==> minSet A = Some (LEAST x. x: A)" |
|
42 by (unfold minSet_def, auto) |
|
43 |
|
44 lemma minSet_greaterThan: |
|
45 "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))" |
|
46 apply (rule leadsTo_weaken) |
|
47 apply (rule_tac x1=x in psp [OF UC2 UC1], safe) |
|
48 apply (auto dest: minSet_eq_SomeD simp add: linorder_neq_iff) |
|
49 done |
|
50 |
|
51 (*The induction*) |
|
52 lemma Channel_progress_lemma: |
|
53 "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))" |
|
54 apply (rule leadsTo_weaken_R) |
|
55 apply (rule_tac l = y and f = "the o minSet" and B = "{}" |
|
56 in greaterThan_bounded_induct, safe) |
|
57 apply (simp_all (no_asm_simp)) |
|
58 apply (drule_tac [2] minSet_nonempty) |
|
59 prefer 2 apply simp |
|
60 apply (rule minSet_greaterThan [THEN leadsTo_weaken], safe) |
|
61 apply simp_all |
|
62 apply (drule minSet_nonempty, simp) |
|
63 done |
|
64 |
|
65 |
|
66 lemma Channel_progress: "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}" |
|
67 apply (rule Channel_progress_lemma [THEN leadsTo_weaken_R], clarify) |
|
68 apply (frule minSet_nonempty) |
|
69 apply (auto dest: Suc_le_lessD not_less_Least) |
|
70 done |
29 |
71 |
30 end |
72 end |