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