author | paulson |
Mon, 05 Oct 1998 10:22:49 +0200 | |
changeset 5611 | 6957f124ca97 |
parent 5584 | aad639e56d4e |
child 5648 | fe887910e32e |
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 |
||
11 |
(*split_all_tac causes a big blow-up*) |
|
12 |
claset_ref() := claset() delSWrapper "split_all_tac"; |
|
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 [prgF_def RS def_prg_simps]; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
15 |
Addsimps [prgG_def RS def_prg_simps]; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
16 |
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
|
17 |
|
5252 | 18 |
(*Simplification for records*) |
19 |
Addsimps (thms"state.update_defs"); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
20 |
Addsimps [simp_of_set invFG_def]; |
5252 | 21 |
|
22 |
||
5611 | 23 |
Goal "Invariant (prgF Join prgG) invFG"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
24 |
by (rtac InvariantI 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
25 |
by (Force_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
26 |
by (rtac (constrains_imp_Constrains RS StableI) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
27 |
by (auto_tac (claset(), simpset() addsimps [constrains_Join])); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
28 |
by (constrains_tac 2); |
5252 | 29 |
by (auto_tac (claset() addIs [le_anti_sym] 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
|
30 |
by (constrains_tac 1); |
5252 | 31 |
qed "invFG"; |
32 |
||
5611 | 33 |
Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} - {s. BB s}) \ |
5340 | 34 |
\ ({s. NF s = k} Int {s. BB s})"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
35 |
by (rtac (ensures_stable_Join1 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
|
36 |
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
|
37 |
by (constrains_tac 1); |
5252 | 38 |
qed "lemma2_1"; |
39 |
||
5611 | 40 |
Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
41 |
by (rtac (ensures_stable_Join2 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
|
42 |
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
|
43 |
by (ensures_tac "cmdF" 1); |
5252 | 44 |
qed "lemma2_2"; |
45 |
||
46 |
||
5611 | 47 |
Goal "LeadsTo (prgF Join prgG) UNIV {s. m < NF s}"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
48 |
by (rtac LeadsTo_weaken_R 1); |
5258 | 49 |
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
|
50 |
GreaterThan_bounded_induct 1); |
5258 | 51 |
by (auto_tac (claset(), simpset() addsimps [vimage_def])); |
5611 | 52 |
(*The inductive step: LeadsTo (prgF Join prgG) {x. NF x = ma} {x. ma < NF x}*) |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
53 |
by (rtac LeadsTo_Diff 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
54 |
by (rtac lemma2_2 2); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
55 |
by (rtac LeadsTo_Trans 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
56 |
by (rtac lemma2_2 2); |
5584 | 57 |
by (rtac lemma2_1 1); |
5258 | 58 |
qed "progress"; |