src/HOL/UNITY/Comp.ML
author paulson
Mon, 07 Dec 1998 18:23:39 +0100
changeset 6018 8131f37f4ba3
parent 6012 1894bfc4aee9
child 6295 351b3c2b0d83
permissions -rw-r--r--
expandshort
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Comp.thy
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     5
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     6
Composition
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     7
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     8
From Chandy and Sanders, "Reasoning About Program Composition"
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     9
*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    10
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    11
(*split_all_tac causes a big blow-up*)
5706
21706a735c8d record_split_name;
wenzelm
parents: 5701
diff changeset
    12
claset_ref() := claset() delSWrapper record_split_name;
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    13
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    14
Delsimps [split_paired_All];
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    15
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    16
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    17
(*** component ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    18
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    19
Goalw [component_def] "component (SKIP (States F)) F";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    20
by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    21
qed "component_SKIP";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    22
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    23
Goalw [component_def] "component F F";
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    24
by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 1);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    25
qed "component_refl";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    26
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    27
AddIffs [component_SKIP, component_refl];
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    28
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    29
Goalw [component_def] "States F = States G ==> component F (F Join G)";
5968
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
    30
by (Blast_tac 1);
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
    31
qed "component_Join1";
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
    32
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    33
Goalw [component_def] "States F = States G ==> component G (F Join G)";
5968
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
    34
by (simp_tac (simpset() addsimps [Join_commute]) 1);
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    35
by (dtac sym 1);
5968
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
    36
by (Blast_tac 1);
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
    37
qed "component_Join2";
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
    38
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    39
Goalw [component_def, eqStates_def] 
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    40
    "[| i : I;  eqStates I F |] ==> component (F i) (JN i:I. (F i))";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    41
by (force_tac (claset() addIs [JN_absorb], simpset()) 1);
5968
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
    42
qed "component_JN";
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
    43
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    44
Goalw [component_def] "[| component F G; component G H |] ==> component F H";
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    45
by (force_tac (claset() addIs [Join_assoc RS sym], simpset()) 1);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    46
qed "component_trans";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    47
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    48
Goalw [component_def] "component F G ==> Acts F <= Acts G";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    49
by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1);
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5612
diff changeset
    50
qed "component_Acts";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    51
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    52
Goalw [component_def,Join_def] "component F G ==> Init G <= Init F";
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    53
by Auto_tac;
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5612
diff changeset
    54
qed "component_Init";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    55
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    56
Goalw [component_def] "component F G ==> States F = States G";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    57
by Auto_tac;
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    58
qed "component_States";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    59
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    60
Goal "[| component F G; component G F |] ==> F=G";
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    61
by (blast_tac (claset() addSIs [program_equalityI, component_States, 
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    62
				component_Init, component_Acts]) 1);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    63
qed "component_anti_sym";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    64
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
    65
Goalw [component_def]
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
    66
      "component F H = (EX G. F Join G = H & Disjoint F G)";
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    67
by (blast_tac (claset() addSIs [Disjoint_States_eq, 
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    68
				Diff_Disjoint, Join_Diff2]) 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
    69
qed "component_eq";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    70
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    71
(*** existential properties ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    72
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    73
Goalw [ex_prop_def]
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    74
     "[| ex_prop X;  finite GG |] \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    75
\     ==> eqStates GG (%x. x) --> GG Int X ~= {} --> (JN G:GG. G) : X";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    76
by (etac finite_induct 1);
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    77
by (Simp_tac 1);
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    78
by (rename_tac "GG J" 1);
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    79
by (full_simp_tac (simpset() addsimps [Int_insert_left]) 1);
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    80
by (dres_inst_tac [("x","J")] spec 1);
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    81
by (Force_tac 1);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    82
qed_spec_mp "ex1";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    83
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    84
Goalw [ex_prop_def]
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    85
     "ALL GG. finite GG & eqStates GG (%x. x) & GG Int X ~= {} \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    86
\       --> (JN G:GG. G) : X ==> ex_prop X";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    87
by (Clarify_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    88
by (dres_inst_tac [("x", "{F,G}")] spec 1);
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    89
by Auto_tac;
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    90
qed "ex2";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    91
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    92
(*Chandy & Sanders take this as a definition*)
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    93
Goal "ex_prop X = \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    94
\       (ALL GG. finite GG & eqStates GG (%x. x) & GG Int X ~= {} \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
    95
\          --> (JN G:GG. G) : X)";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    96
by (blast_tac (claset() addIs [ex1,ex2]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    97
qed "ex_prop_finite";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    98
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    99
(*Their "equivalent definition" given at the end of section 3*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   100
Goal "ex_prop X = (ALL G. G:X = (ALL H. component G H --> H: X))";
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   101
by Auto_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   102
by (rewrite_goals_tac [ex_prop_def, component_def]);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   103
by (Blast_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   104
by Safe_tac;
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   105
by (stac Join_commute 2);
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   106
by (dtac sym 2);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   107
by (ALLGOALS Blast_tac);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   108
qed "ex_prop_equiv";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   109
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   110
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   111
(*** universal properties ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   112
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   113
Goalw [uv_prop_def]
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   114
     "[| uv_prop X; finite GG |] \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   115
\     ==> eqStates GG (%x. x) --> GG <= X --> (JN G:GG. G) : X";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   116
by (etac finite_induct 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   117
by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   118
qed_spec_mp "uv1";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   119
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   120
Goalw [uv_prop_def]
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   121
     "ALL GG. finite GG & eqStates GG (%x. x) & GG <= X \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   122
\       --> (JN G:GG. G) : X  ==> uv_prop X";
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   123
by (rtac conjI 1);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   124
by (Clarify_tac 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   125
by (dres_inst_tac [("x", "{F,G}")] spec 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   126
by (dres_inst_tac [("x", "{}")] spec 1);
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   127
by Auto_tac;
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   128
qed "uv2";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   129
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   130
(*Chandy & Sanders take this as a definition*)
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   131
Goal "uv_prop X = (ALL GG. finite GG & eqStates GG (%x. x) & GG <= X \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   132
\       --> (JN G:GG. G) : X)";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   133
by (blast_tac (claset() addIs [uv1,uv2]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   134
qed "uv_prop_finite";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   135
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   136
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   137
(*** guarantees ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   138
5668
9ddc4e836d3e moved a theorem
paulson
parents: 5637
diff changeset
   139
(*This equation is more intuitive than the official definition*)
5968
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
   140
Goal "(F : X guarantees Y) = \
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
   141
\     (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   142
by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
5668
9ddc4e836d3e moved a theorem
paulson
parents: 5637
diff changeset
   143
by (Blast_tac 1);
9ddc4e836d3e moved a theorem
paulson
parents: 5637
diff changeset
   144
qed "guarantees_eq";
9ddc4e836d3e moved a theorem
paulson
parents: 5637
diff changeset
   145
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   146
Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   147
by (Blast_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   148
qed "subset_imp_guarantees";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   149
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   150
(*Remark at end of section 4.1*)
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   151
Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guarantees Y)";
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   152
by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   153
by (blast_tac (claset() addEs [equalityE]) 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   154
qed "ex_prop_equiv2";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   155
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   156
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   157
     "(INT X:XX. X guarantees Y) = (UN X:XX. X) guarantees Y";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   158
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   159
qed "INT_guarantees_left";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   160
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   161
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   162
     "(INT Y:YY. X guarantees Y) = X guarantees (INT Y:YY. Y)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   163
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   164
qed "INT_guarantees_right";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   165
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   166
Goalw [guarantees_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   167
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   168
qed "shunting";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   169
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   170
Goalw [guarantees_def] "(X guarantees Y) = -Y guarantees -X";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   171
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   172
qed "contrapositive";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   173
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   174
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   175
    "V guarantees X Int ((X Int Y) guarantees Z) <= (V Int Y) guarantees Z";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   176
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   177
qed "combining1";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   178
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   179
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   180
    "V guarantees (X Un Y) Int (Y guarantees Z) <= V guarantees (X Un Z)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   181
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   182
qed "combining2";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   183
5630
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   184
Goalw [guarantees_def]
5968
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
   185
     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
5630
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   186
by (Blast_tac 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   187
qed "all_guarantees";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   188
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   189
Goalw [guarantees_def]
5968
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
   190
     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
5630
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   191
by (Blast_tac 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   192
qed "ex_guarantees";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   193
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   194
val prems = Goal
5968
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
   195
     "(!!G. [| F Join G : X;  Disjoint F G |] ==> F Join G : Y) \
06f9dbfff032 renamed vars
paulson
parents: 5804
diff changeset
   196
\     ==> F : X guarantees Y";
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   197
by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
5630
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   198
by (blast_tac (claset() addIs prems) 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   199
qed "guaranteesI";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   200
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   201
Goalw [guarantees_def, component_def]
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   202
     "[| F : X guarantees Y;  F Join G : X;  States F = States G |] \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   203
\     ==> F Join G : Y";
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   204
by (Blast_tac 1);
5637
a06006a320a1 new rule
paulson
parents: 5630
diff changeset
   205
qed "guaranteesD";
a06006a320a1 new rule
paulson
parents: 5630
diff changeset
   206
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   207
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   208
(*** well-definedness ***)
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   209
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   210
Goalw [welldef_def] "F Join G: welldef ==> F: welldef";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   211
by Auto_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   212
qed "Join_welldef_D1";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   213
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   214
Goalw [welldef_def] "F Join G: welldef ==> G: welldef";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   215
by Auto_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   216
qed "Join_welldef_D2";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   217
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   218
(*** refinement ***)
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   219
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   220
Goalw [refines_def] "F refines F wrt X";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   221
by (Blast_tac 1);
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   222
qed "refines_refl";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   223
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   224
Goalw [refines_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   225
     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X";
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   226
by Auto_tac;
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   227
qed "refines_trans";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   228
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   229
Goalw [strict_ex_prop_def]
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   230
     "[| strict_ex_prop X;  States F = States G |] \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   231
\     ==> (ALL H. States F = States H & F Join H : X --> G Join H : X) = \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   232
\         (F:X --> G:X)";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   233
by Safe_tac;
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   234
by (Blast_tac 1);
6018
8131f37f4ba3 expandshort
paulson
parents: 6012
diff changeset
   235
by Auto_tac;
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   236
qed "strict_ex_refine_lemma";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   237
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   238
Goalw [strict_ex_prop_def]
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   239
     "[| strict_ex_prop X;  States F = States G |] \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   240
\     ==> (ALL H. States F = States H & F Join H : welldef & F Join H : X \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   241
\           --> G Join H : X) = \
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   242
\         (F: welldef Int X --> G:X)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   243
by Safe_tac;
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   244
by (eres_inst_tac [("x","SKIP ?A"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   245
by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset()));
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   246
qed "strict_ex_refine_lemma_v";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   247
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   248
Goal "[| strict_ex_prop X;  States F = States G;  \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   249
\        ALL H. States F = States H & F Join H : welldef Int X \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   250
\          --> G Join H : welldef |] \
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   251
\     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
6018
8131f37f4ba3 expandshort
paulson
parents: 6012
diff changeset
   252
by (dtac sym 1);
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   253
by (res_inst_tac [("x","SKIP (States G)")] allE 1
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   254
    THEN assume_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   255
by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   256
					   strict_ex_refine_lemma_v]) 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   257
qed "ex_refinement_thm";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   258
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   259
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   260
(***
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   261
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   262
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   263
Goalw [strict_uv_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   264
     "strict_uv_prop X \
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   265
\     ==> (ALL H. States F = States H & F Join H : X --> G Join H : X) = (F:X --> G:X)";
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   266
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   267
qed "strict_uv_refine_lemma";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   268
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   269
Goalw [strict_uv_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   270
     "strict_uv_prop X \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   271
\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   272
\         (F: welldef Int X --> G:X)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   273
by Safe_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   274
by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   275
by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2],
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   276
	      simpset()));
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   277
qed "strict_uv_refine_lemma_v";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   278
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   279
Goal "[| strict_uv_prop X;  \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   280
\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   281
\     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   282
by (res_inst_tac [("x","SKIP")] allE 1
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   283
    THEN assume_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   284
by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   285
					   strict_uv_refine_lemma_v]) 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   286
qed "uv_refinement_thm";
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5968
diff changeset
   287
***)