author | paulson |
Wed, 08 Sep 1999 15:50:11 +0200 | |
changeset 7523 | 3a716ebc2fc0 |
parent 7403 | c318acb88251 |
child 9403 | aad13b59b8d9 |
permissions | -rw-r--r-- |
5252 | 1 |
(* Title: HOL/UNITY/Handshake |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Handshake Protocol |
|
7 |
||
8 |
From Misra, "Asynchronous Compositions of Programs", Section 5.3.2 |
|
9 |
*) |
|
10 |
||
5648 | 11 |
Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init]; |
12 |
program_defs_ref := [F_def, G_def]; |
|
13 |
||
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
14 |
Addsimps (map simp_of_act [cmdF_def, cmdG_def]); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
15 |
Addsimps [simp_of_set invFG_def]; |
5252 | 16 |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
17 |
|
6570 | 18 |
Goal "(F Join G) : Always invFG"; |
19 |
by (rtac AlwaysI 1); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
20 |
by (Force_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
21 |
by (rtac (constrains_imp_Constrains RS StableI) 1); |
7523 | 22 |
by (auto_tac (claset(), simpset() addsimps [Join_constrains])); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
23 |
by (constrains_tac 2); |
6676 | 24 |
by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset())); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
25 |
by (constrains_tac 1); |
5252 | 26 |
qed "invFG"; |
27 |
||
6536 | 28 |
Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \ |
6632 | 29 |
\ ({s. NF s = k} Int {s. BB s})"; |
7523 | 30 |
by (rtac (stable_Join_ensures1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
31 |
by (ensures_tac "cmdG" 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
32 |
by (constrains_tac 1); |
5252 | 33 |
qed "lemma2_1"; |
34 |
||
6536 | 35 |
Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}"; |
7523 | 36 |
by (rtac (stable_Join_ensures2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
37 |
by (constrains_tac 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
38 |
by (ensures_tac "cmdF" 1); |
5252 | 39 |
qed "lemma2_2"; |
40 |
||
6536 | 41 |
Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
42 |
by (rtac LeadsTo_weaken_R 1); |
5258 | 43 |
by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5258
diff
changeset
|
44 |
GreaterThan_bounded_induct 1); |
7403 | 45 |
(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*) |
46 |
by (auto_tac (claset() addSIs [lemma2_1, lemma2_2] |
|
47 |
addIs[LeadsTo_Trans, LeadsTo_Diff], |
|
48 |
simpset() addsimps [vimage_def])); |
|
5258 | 49 |
qed "progress"; |