author | paulson |
Thu, 06 Aug 1998 15:47:26 +0200 | |
changeset 5277 | e4297d03e5d2 |
parent 5253 | 82a5ca6290aa |
child 5625 | 77e9ab9cd7b1 |
permissions | -rw-r--r-- |
4776 | 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 |
AddIffs [skip]; |
|
12 |
||
13 |
(*None represents "infinity" while Some represents proper integers*) |
|
5111 | 14 |
Goalw [minSet_def] "minSet A = Some x --> x : A"; |
4776 | 15 |
by (Simp_tac 1); |
16 |
by (fast_tac (claset() addIs [LeastI]) 1); |
|
17 |
qed_spec_mp "minSet_eq_SomeD"; |
|
18 |
||
5069 | 19 |
Goalw [minSet_def] " minSet{} = None"; |
4776 | 20 |
by (Asm_simp_tac 1); |
21 |
qed_spec_mp "minSet_empty"; |
|
22 |
Addsimps [minSet_empty]; |
|
23 |
||
5111 | 24 |
Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)"; |
4776 | 25 |
by (ALLGOALS Asm_simp_tac); |
26 |
by (Blast_tac 1); |
|
27 |
qed_spec_mp "minSet_nonempty"; |
|
28 |
||
5253 | 29 |
Goal "leadsTo acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))"; |
4776 | 30 |
by (rtac leadsTo_weaken 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
31 |
by (rtac ([UC2, UC1] MRS psp) 1); |
4776 | 32 |
by (ALLGOALS Asm_simp_tac); |
33 |
by (Blast_tac 1); |
|
34 |
by Safe_tac; |
|
35 |
by (auto_tac (claset() addDs [minSet_eq_SomeD], |
|
36 |
simpset() addsimps [le_def, nat_neq_iff])); |
|
37 |
qed "minSet_greaterThan"; |
|
38 |
||
39 |
||
40 |
(*The induction*) |
|
5253 | 41 |
Goal "leadsTo acts (UNIV-{{}}) (minSet -`` (Some``atLeast y))"; |
4776 | 42 |
by (rtac leadsTo_weaken_R 1); |
43 |
by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")] |
|
44 |
greaterThan_bounded_induct 1); |
|
45 |
by Safe_tac; |
|
46 |
by (ALLGOALS Asm_simp_tac); |
|
47 |
by (dtac minSet_nonempty 2); |
|
48 |
by (Asm_full_simp_tac 2); |
|
49 |
by (rtac (minSet_greaterThan RS leadsTo_weaken) 1); |
|
50 |
by Safe_tac; |
|
51 |
by (ALLGOALS Asm_full_simp_tac); |
|
52 |
by (dtac minSet_nonempty 1); |
|
53 |
by (Asm_full_simp_tac 1); |
|
54 |
val lemma = result(); |
|
55 |
||
56 |
||
5253 | 57 |
Goal "!!y::nat. leadsTo acts (UNIV-{{}}) {s. y ~: s}"; |
4776 | 58 |
by (rtac (lemma RS leadsTo_weaken_R) 1); |
59 |
by (Clarify_tac 1); |
|
60 |
by (forward_tac [minSet_nonempty] 1); |
|
61 |
by (asm_full_simp_tac (simpset() addsimps [Suc_le_eq]) 1); |
|
62 |
by (blast_tac (claset() addDs [Suc_le_lessD, not_less_Least]) 1); |
|
63 |
qed "Channel_progress"; |