author | nipkow |
Wed, 28 Jan 2009 16:29:16 +0100 | |
changeset 29667 | 53103fc8ffa3 |
parent 18556 | dc39832e9280 |
child 36866 | 426d5781bb25 |
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.thy |
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 |
|
18556 | 11 |
theory Handshake imports "../UNITY_Main" begin |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
record state = |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
BB :: bool |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
NF :: nat |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
NG :: nat |
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 |
constdefs |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
(*F's program*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
cmdF :: "(state*state) set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
"cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
F :: "state program" |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13786
diff
changeset
|
24 |
"F == mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
(*G's program*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
cmdG :: "(state*state) set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
"cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
G :: "state program" |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13786
diff
changeset
|
31 |
"G == mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
(*the joint invariant*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
34 |
invFG :: "state set" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
"invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
|
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
37 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
38 |
declare F_def [THEN def_prg_Init, simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
39 |
G_def [THEN def_prg_Init, simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
40 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
41 |
cmdF_def [THEN def_act_simp, simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
42 |
cmdG_def [THEN def_act_simp, simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
43 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
44 |
invFG_def [THEN def_set_simp, simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
45 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
46 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
47 |
lemma invFG: "(F Join G) : Always invFG" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
48 |
apply (rule AlwaysI) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
49 |
apply force |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
50 |
apply (rule constrains_imp_Constrains [THEN StableI]) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
51 |
apply auto |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
52 |
apply (unfold F_def, safety) |
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
53 |
apply (unfold G_def, safety) |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
54 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
55 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
56 |
lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
57 |
({s. NF s = k} Int {s. BB s})" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
58 |
apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo]) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
59 |
apply (unfold F_def, safety) |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
60 |
apply (unfold G_def, ensures_tac "cmdG") |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
61 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
62 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
63 |
lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
64 |
{s. k < NF s}" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
65 |
apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo]) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
66 |
apply (unfold F_def, ensures_tac "cmdF") |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
67 |
apply (unfold G_def, safety) |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
68 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
69 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
70 |
lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
71 |
apply (rule LeadsTo_weaken_R) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
72 |
apply (rule_tac f = "NF" and l = "Suc m" and B = "{}" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
73 |
in GreaterThan_bounded_induct) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
74 |
(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
75 |
apply (auto intro!: lemma2_1 lemma2_2 |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
76 |
intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
77 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
78 |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
79 |
end |