src/HOL/UNITY/Comp.ML
author paulson
Fri, 09 Oct 1998 11:24:46 +0200
changeset 5630 fc2c299187c0
parent 5620 3ac11c4af76a
child 5637 a06006a320a1
permissions -rw-r--r--
new guarantees laws
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*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    12
claset_ref() := claset() delSWrapper "split_all_tac";
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
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    19
Goalw [component_def] "component SKIP F";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    20
by (blast_tac (claset() addIs [Join_SKIP_left]) 1);
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";
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    24
by (blast_tac (claset() addIs [Join_SKIP_right]) 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
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    29
Goalw [component_def] "[| component F G; component G H |] ==> component F H";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    30
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    31
qed "component_trans";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    32
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    33
Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G";
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    34
by Auto_tac;
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5612
diff changeset
    35
qed "component_Acts";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    36
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    37
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
    38
by Auto_tac;
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5612
diff changeset
    39
qed "component_Init";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    40
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    41
Goal "[| component F G; component G F |] ==> F=G";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    42
by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI, 
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5612
diff changeset
    43
				      component_Acts, component_Init]) 1);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    44
qed "component_anti_sym";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    45
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    46
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    47
(*** existential properties ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    48
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    49
Goalw [ex_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    50
     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    51
by (etac finite_induct 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    52
by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    53
qed_spec_mp "ex1";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    54
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    55
Goalw [ex_prop_def]
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    56
     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    57
by (Clarify_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    58
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
    59
by Auto_tac;
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    60
qed "ex2";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    61
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    62
(*Chandy & Sanders take this as a definition*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    63
Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    64
by (blast_tac (claset() addIs [ex1,ex2]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    65
qed "ex_prop_finite";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    66
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    67
(*Their "equivalent definition" given at the end of section 3*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    68
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
    69
by Auto_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    70
by (rewrite_goals_tac [ex_prop_def, component_def]);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    71
by (Blast_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    72
by Safe_tac;
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    73
by (stac Join_commute 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    74
by (ALLGOALS Blast_tac);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    75
qed "ex_prop_equiv";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    76
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    77
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    78
(*** universal properties ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    79
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    80
Goalw [uv_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    81
     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    82
by (etac finite_induct 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    83
by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    84
qed_spec_mp "uv1";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    85
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    86
Goalw [uv_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    87
     "ALL GG. finite GG & GG <= X --> (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
    88
by (rtac conjI 1);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    89
by (Clarify_tac 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    90
by (dres_inst_tac [("x", "{F,G}")] spec 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    91
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
    92
by Auto_tac;
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    93
qed "uv2";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    94
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    95
(*Chandy & Sanders take this as a definition*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    96
Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    97
by (blast_tac (claset() addIs [uv1,uv2]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    98
qed "uv_prop_finite";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    99
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   100
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   101
(*** guarantees ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   102
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   103
Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   104
by (Blast_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   105
qed "subset_imp_guarantees";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   106
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   107
(*Remark at end of section 4.1*)
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   108
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
   109
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
   110
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
   111
qed "ex_prop_equiv2";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   112
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   113
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   114
     "(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
   115
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   116
qed "INT_guarantees_left";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   117
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   118
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   119
     "(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
   120
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   121
qed "INT_guarantees_right";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   122
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   123
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
   124
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   125
qed "shunting";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   126
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   127
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
   128
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   129
qed "contrapositive";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   130
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   131
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   132
    "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
   133
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   134
qed "combining1";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   135
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   136
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   137
    "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
   138
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   139
qed "combining2";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   140
5630
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   141
Goalw [guarantees_def]
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   142
     "ALL z:I. F : A guarantees (B z) ==> F : A guarantees (INT z:I. B z)";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   143
by (Blast_tac 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   144
qed "all_guarantees";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   145
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   146
Goalw [guarantees_def]
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   147
     "EX z:I. F : A guarantees (B z) ==> F : A guarantees (UN z:I. B z)";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   148
by (Blast_tac 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   149
qed "ex_guarantees";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   150
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   151
Goalw [guarantees_def, component_def]
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   152
      "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   153
by (Blast_tac 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   154
qed "guarantees_eq";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   155
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   156
val prems = Goalw [guarantees_def, component_def]
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   157
      "(!!G. F Join G : A ==> F Join G : B) ==> F : A guarantees B";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   158
by (blast_tac (claset() addIs prems) 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   159
qed "guaranteesI";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   160
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   161
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   162
(*** well-definedness ***)
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   163
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   164
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
   165
by Auto_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   166
qed "Join_welldef_D1";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   167
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   168
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
   169
by Auto_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   170
qed "Join_welldef_D2";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   171
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   172
(*** refinement ***)
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 [refines_def] "F refines F wrt X";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   175
by (Blast_tac 1);
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   176
qed "refines_refl";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   177
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   178
Goalw [refines_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   179
     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   180
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   181
qed "refines_trans";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   182
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   183
Goalw [strict_ex_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   184
     "strict_ex_prop X \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   185
\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   186
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   187
qed "strict_ex_refine_lemma";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   188
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   189
Goalw [strict_ex_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   190
     "strict_ex_prop X \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   191
\     ==> (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
   192
\         (F: welldef Int X --> G:X)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   193
by Safe_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   194
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
   195
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
   196
qed "strict_ex_refine_lemma_v";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   197
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   198
Goal "[| strict_ex_prop X;  \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   199
\        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
   200
\     ==> (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
   201
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
   202
    THEN assume_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   203
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
   204
					   strict_ex_refine_lemma_v]) 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   205
qed "ex_refinement_thm";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   206
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   207
Goalw [strict_uv_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   208
     "strict_uv_prop X \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   209
\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   210
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   211
qed "strict_uv_refine_lemma";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   212
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   213
Goalw [strict_uv_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   214
     "strict_uv_prop X \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   215
\     ==> (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
   216
\         (F: welldef Int X --> G:X)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   217
by Safe_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   218
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
   219
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
   220
	      simpset()));
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   221
qed "strict_uv_refine_lemma_v";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   222
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   223
Goal "[| strict_uv_prop X;  \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   224
\        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
   225
\     ==> (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
   226
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
   227
    THEN assume_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   228
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
   229
					   strict_uv_refine_lemma_v]) 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   230
qed "uv_refinement_thm";