author | nipkow |
Fri, 27 Nov 1998 17:00:30 +0100 | |
changeset 5983 | 79e301a6a51b |
parent 5706 | 21706a735c8d |
child 6012 | 1894bfc4aee9 |
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*) |
|
5706 | 12 |
claset_ref() := claset() delSWrapper record_split_name; |
5252 | 13 |
|
5648 | 14 |
Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init]; |
15 |
program_defs_ref := [F_def, G_def]; |
|
16 |
||
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5340
diff
changeset
|
17 |
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
|
18 |
|
5252 | 19 |
(*Simplification for records*) |
20 |
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
|
21 |
Addsimps [simp_of_set invFG_def]; |
5252 | 22 |
|
23 |
||
5648 | 24 |
Goal "(F Join G) : Invariant invFG"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
25 |
by (rtac InvariantI 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
26 |
by (Force_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
27 |
by (rtac (constrains_imp_Constrains RS StableI) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
28 |
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
|
29 |
by (constrains_tac 2); |
5252 | 30 |
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
|
31 |
by (constrains_tac 1); |
5252 | 32 |
qed "invFG"; |
33 |
||
5648 | 34 |
Goal "(F Join G) : LeadsTo ({s. NF s = k} - {s. BB s}) \ |
5340 | 35 |
\ ({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
|
36 |
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
|
37 |
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
|
38 |
by (constrains_tac 1); |
5252 | 39 |
qed "lemma2_1"; |
40 |
||
5648 | 41 |
Goal "(F Join G) : LeadsTo ({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
|
42 |
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
|
43 |
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
|
44 |
by (ensures_tac "cmdF" 1); |
5252 | 45 |
qed "lemma2_2"; |
46 |
||
47 |
||
5648 | 48 |
Goal "(F Join G) : LeadsTo UNIV {s. m < NF s}"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
49 |
by (rtac LeadsTo_weaken_R 1); |
5258 | 50 |
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
|
51 |
GreaterThan_bounded_induct 1); |
5258 | 52 |
by (auto_tac (claset(), simpset() addsimps [vimage_def])); |
5648 | 53 |
(*The inductive step: (F Join G) : LeadsTo {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
|
54 |
by (rtac LeadsTo_Diff 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
55 |
by (rtac lemma2_2 2); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
56 |
by (rtac LeadsTo_Trans 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
57 |
by (rtac lemma2_2 2); |
5584 | 58 |
by (rtac lemma2_1 1); |
5258 | 59 |
qed "progress"; |