author | paulson |
Mon, 22 Oct 2001 11:54:22 +0200 | |
changeset 11868 | 56db9f3a6b3e |
parent 11194 | ea13ff5a26d1 |
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/Handshake |
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: Lawrence C Paulson, Cambridge University Computer Laboratory |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
Handshake Protocol |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
From Misra, "Asynchronous Compositions of Programs", Section 5.3.2 |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init]; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
program_defs_ref := [F_def, G_def]; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
Addsimps (map simp_of_act [cmdF_def, cmdG_def]); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
Addsimps [simp_of_set invFG_def]; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
Goal "(F Join G) : Always invFG"; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
by (rtac AlwaysI 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
by (Force_tac 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
by (rtac (constrains_imp_Constrains RS StableI) 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
by Auto_tac; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
by (constrains_tac 2); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset())); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
by (constrains_tac 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
qed "invFG"; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \ |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
\ ({s. NF s = k} Int {s. BB s})"; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
by (rtac (stable_Join_ensures1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
by (ensures_tac "cmdG" 2); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
by (constrains_tac 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
qed "lemma2_1"; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
34 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}"; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
by (rtac (stable_Join_ensures2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
37 |
by (constrains_tac 2); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
38 |
by (ensures_tac "cmdF" 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
qed "lemma2_2"; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
40 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
41 |
Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}"; |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
42 |
by (rtac LeadsTo_weaken_R 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
43 |
by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
44 |
GreaterThan_bounded_induct 1); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
45 |
(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
46 |
by (auto_tac (claset() addSIs [lemma2_1, lemma2_2] |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
47 |
addIs[LeadsTo_Trans, LeadsTo_Diff], |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
48 |
simpset() addsimps [vimage_def])); |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
49 |
qed "progress"; |