1 (* Title: HOL/UNITY/Channel |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Unordered Channel |
|
7 |
|
8 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 |
|
9 *) |
|
10 |
|
11 (*None represents "infinity" while Some represents proper integers*) |
|
12 Goalw [minSet_def] "minSet A = Some x --> x : A"; |
|
13 by (Simp_tac 1); |
|
14 by (fast_tac (claset() addIs [LeastI]) 1); |
|
15 qed_spec_mp "minSet_eq_SomeD"; |
|
16 |
|
17 Goalw [minSet_def] " minSet{} = None"; |
|
18 by (Asm_simp_tac 1); |
|
19 qed_spec_mp "minSet_empty"; |
|
20 Addsimps [minSet_empty]; |
|
21 |
|
22 Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)"; |
|
23 by Auto_tac; |
|
24 qed_spec_mp "minSet_nonempty"; |
|
25 |
|
26 Goal "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))"; |
|
27 by (rtac leadsTo_weaken 1); |
|
28 by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1); |
|
29 by Safe_tac; |
|
30 by (auto_tac (claset() addDs [minSet_eq_SomeD], |
|
31 simpset() addsimps [linorder_neq_iff])); |
|
32 qed "minSet_greaterThan"; |
|
33 |
|
34 (*The induction*) |
|
35 Goal "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))"; |
|
36 by (rtac leadsTo_weaken_R 1); |
|
37 by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")] |
|
38 greaterThan_bounded_induct 1); |
|
39 by Safe_tac; |
|
40 by (ALLGOALS Asm_simp_tac); |
|
41 by (dtac minSet_nonempty 2); |
|
42 by (Asm_full_simp_tac 2); |
|
43 by (rtac (minSet_greaterThan RS leadsTo_weaken) 1); |
|
44 by Safe_tac; |
|
45 by (ALLGOALS Asm_full_simp_tac); |
|
46 by (dtac minSet_nonempty 1); |
|
47 by (Asm_full_simp_tac 1); |
|
48 val lemma = result(); |
|
49 |
|
50 |
|
51 Goal "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}"; |
|
52 by (rtac (lemma RS leadsTo_weaken_R) 1); |
|
53 by (Clarify_tac 1); |
|
54 by (ftac minSet_nonempty 1); |
|
55 by (auto_tac (claset() addDs [Suc_le_lessD, not_less_Least], |
|
56 simpset())); |
|
57 qed "Channel_progress"; |
|