author | wenzelm |
Thu, 15 Feb 2018 12:11:00 +0100 | |
changeset 67613 | ce654b0e6d69 |
parent 60773 | d09c66a0ea10 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/Comp/Handshake.thy |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 1998 University of Cambridge |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
Handshake Protocol |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
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
|
8 |
*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
|
18556 | 10 |
theory Handshake imports "../UNITY_Main" begin |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
record state = |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
BB :: bool |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
NF :: nat |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
NG :: nat |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
|
36866 | 17 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
(*F's program*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
cmdF :: "(state*state) set" |
36866 | 20 |
where "cmdF = {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
|
36866 | 22 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
F :: "state program" |
36866 | 24 |
where "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 |
|
36866 | 26 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
(*G's program*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
cmdG :: "(state*state) set" |
36866 | 29 |
where "cmdG = {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
|
36866 | 31 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
G :: "state program" |
36866 | 33 |
where "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
|
34 |
|
36866 | 35 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
(*the joint invariant*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
37 |
invFG :: "state set" |
36866 | 38 |
where "invFG = {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
|
13786
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 |
declare F_def [THEN def_prg_Init, simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
42 |
G_def [THEN def_prg_Init, 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 |
cmdF_def [THEN def_act_simp, simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
45 |
cmdG_def [THEN def_act_simp, simp] |
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 |
invFG_def [THEN def_set_simp, simp] |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
48 |
|
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
49 |
|
67613 | 50 |
lemma invFG: "(F \<squnion> G) \<in> Always invFG" |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
51 |
apply (rule AlwaysI) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
52 |
apply force |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
53 |
apply (rule constrains_imp_Constrains [THEN StableI]) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
54 |
apply auto |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
55 |
apply (unfold F_def, safety) |
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
56 |
apply (unfold G_def, safety) |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
57 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
58 |
|
67613 | 59 |
lemma lemma2_1: "(F \<squnion> G) \<in> ({s. NF s = k} - {s. BB s}) LeadsTo |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
60 |
({s. NF s = k} Int {s. BB s})" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
61 |
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
|
62 |
apply (unfold F_def, safety) |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
63 |
apply (unfold G_def, ensures_tac "cmdG") |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
64 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
65 |
|
67613 | 66 |
lemma lemma2_2: "(F \<squnion> G) \<in> ({s. NF s = k} Int {s. BB s}) LeadsTo |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
67 |
{s. k < NF s}" |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
68 |
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
|
69 |
apply (unfold F_def, ensures_tac "cmdF") |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13812
diff
changeset
|
70 |
apply (unfold G_def, safety) |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
71 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
72 |
|
67613 | 73 |
lemma progress: "(F \<squnion> G) \<in> UNIV LeadsTo {s. m < NF s}" |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
74 |
apply (rule LeadsTo_weaken_R) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
75 |
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
|
76 |
in GreaterThan_bounded_induct) |
60773 | 77 |
(*The inductive step is (F \<squnion> G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*) |
13786
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
78 |
apply (auto intro!: lemma2_1 lemma2_2 |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
79 |
intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def) |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
80 |
done |
ab8f39f48a6f
More conversion of UNITY to Isar new-style theories
paulson
parents:
11194
diff
changeset
|
81 |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
82 |
end |