author | paulson |
Tue, 04 May 1999 10:26:00 +0200 | |
changeset 6570 | a7d7985050a9 |
parent 6536 | 281d44905cab |
child 6632 | 3f807540e939 |
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 |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
23 |
|
6570 | 24 |
Goal "(F Join G) : Always invFG"; |
25 |
by (rtac AlwaysI 1); |
|
5313
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 |
||
6536 | 34 |
Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \ |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
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); |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5706
diff
changeset
|
39 |
by Auto_tac; |
5252 | 40 |
qed "lemma2_1"; |
41 |
||
6536 | 42 |
Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
43 |
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
|
44 |
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
|
45 |
by (ensures_tac "cmdF" 1); |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5706
diff
changeset
|
46 |
by Auto_tac; |
5252 | 47 |
qed "lemma2_2"; |
48 |
||
49 |
||
6536 | 50 |
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
|
51 |
by (rtac LeadsTo_weaken_R 1); |
5258 | 52 |
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
|
53 |
GreaterThan_bounded_induct 1); |
5258 | 54 |
by (auto_tac (claset(), simpset() addsimps [vimage_def])); |
6536 | 55 |
(*The inductive step: (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*) |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
56 |
by (rtac LeadsTo_Diff 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
57 |
by (rtac lemma2_2 2); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
58 |
by (rtac LeadsTo_Trans 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
59 |
by (rtac lemma2_2 2); |
5584 | 60 |
by (rtac lemma2_1 1); |
5258 | 61 |
qed "progress"; |