src/HOL/UNITY/Comp.ML
author paulson
Fri, 06 Nov 1998 13:20:29 +0100
changeset 5804 8e0a4c4fd67b
parent 5706 21706a735c8d
child 5968 06f9dbfff032
permissions -rw-r--r--
Revising the Client proof as suggested by Michel Charpentier. New lemmas about composition (in Union.ML), etc. Also changed "length" to "size" because it is displayed as "size" in any event.
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
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
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
    46
Goalw [component_def]
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
    47
      "component F H = (EX G. F Join G = H & Disjoint F G)";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
    48
by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
    49
qed "component_eq";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    50
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    51
(*** existential properties ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    52
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    53
Goalw [ex_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    54
     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    55
by (etac finite_induct 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    56
by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    57
qed_spec_mp "ex1";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    58
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    59
Goalw [ex_prop_def]
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    60
     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    61
by (Clarify_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    62
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
    63
by Auto_tac;
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    64
qed "ex2";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    65
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    66
(*Chandy & Sanders take this as a definition*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    67
Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    68
by (blast_tac (claset() addIs [ex1,ex2]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    69
qed "ex_prop_finite";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    70
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    71
(*Their "equivalent definition" given at the end of section 3*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    72
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
    73
by Auto_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    74
by (rewrite_goals_tac [ex_prop_def, component_def]);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    75
by (Blast_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    76
by Safe_tac;
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    77
by (stac Join_commute 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    78
by (ALLGOALS Blast_tac);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    79
qed "ex_prop_equiv";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    80
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    81
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    82
(*** universal properties ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    83
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    84
Goalw [uv_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    85
     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    86
by (etac finite_induct 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    87
by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    88
qed_spec_mp "uv1";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    89
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    90
Goalw [uv_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    91
     "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
    92
by (rtac conjI 1);
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    93
by (Clarify_tac 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    94
by (dres_inst_tac [("x", "{F,G}")] spec 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    95
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
    96
by Auto_tac;
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    97
qed "uv2";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    98
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    99
(*Chandy & Sanders take this as a definition*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   100
Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   101
by (blast_tac (claset() addIs [uv1,uv2]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   102
qed "uv_prop_finite";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   103
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   104
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   105
(*** guarantees ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   106
5668
9ddc4e836d3e moved a theorem
paulson
parents: 5637
diff changeset
   107
(*This equation is more intuitive than the official definition*)
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   108
Goal "(F : A guarantees B) = \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   109
\     (ALL G. F Join G : A & Disjoint F G --> F Join G : B)";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   110
by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
5668
9ddc4e836d3e moved a theorem
paulson
parents: 5637
diff changeset
   111
by (Blast_tac 1);
9ddc4e836d3e moved a theorem
paulson
parents: 5637
diff changeset
   112
qed "guarantees_eq";
9ddc4e836d3e moved a theorem
paulson
parents: 5637
diff changeset
   113
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   114
Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   115
by (Blast_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   116
qed "subset_imp_guarantees";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   117
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   118
(*Remark at end of section 4.1*)
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   119
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
   120
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
   121
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
   122
qed "ex_prop_equiv2";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   123
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   124
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   125
     "(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
   126
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   127
qed "INT_guarantees_left";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   128
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   129
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   130
     "(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
   131
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   132
qed "INT_guarantees_right";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   133
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   134
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
   135
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   136
qed "shunting";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   137
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   138
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
   139
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   140
qed "contrapositive";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   141
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   142
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   143
    "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
   144
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   145
qed "combining1";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   146
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   147
Goalw [guarantees_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   148
    "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
   149
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   150
qed "combining2";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   151
5630
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   152
Goalw [guarantees_def]
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   153
     "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
   154
by (Blast_tac 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   155
qed "all_guarantees";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   156
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   157
Goalw [guarantees_def]
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   158
     "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
   159
by (Blast_tac 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   160
qed "ex_guarantees";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   161
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   162
val prems = Goal
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   163
     "(!!G. [| F Join G : A;  Disjoint F G |] ==> F Join G : B) \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   164
\     ==> F : A guarantees B";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   165
by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
5630
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   166
by (blast_tac (claset() addIs prems) 1);
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   167
qed "guaranteesI";
fc2c299187c0 new guarantees laws
paulson
parents: 5620
diff changeset
   168
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   169
Goalw [guarantees_def, component_def]
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   170
     "[| F : A guarantees B;  F Join G : A |] ==> F Join G : B";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5706
diff changeset
   171
by (Blast_tac 1);
5637
a06006a320a1 new rule
paulson
parents: 5630
diff changeset
   172
qed "guaranteesD";
a06006a320a1 new rule
paulson
parents: 5630
diff changeset
   173
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   174
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   175
(*** well-definedness ***)
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   176
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   177
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
   178
by Auto_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   179
qed "Join_welldef_D1";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   180
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   181
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
   182
by Auto_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   183
qed "Join_welldef_D2";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   184
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   185
(*** refinement ***)
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   186
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   187
Goalw [refines_def] "F refines F wrt X";
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   188
by (Blast_tac 1);
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   189
qed "refines_refl";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   190
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   191
Goalw [refines_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   192
     "[| 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
   193
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   194
qed "refines_trans";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   195
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   196
Goalw [strict_ex_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   197
     "strict_ex_prop X \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   198
\     ==> (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
   199
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   200
qed "strict_ex_refine_lemma";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   201
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   202
Goalw [strict_ex_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   203
     "strict_ex_prop X \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   204
\     ==> (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
   205
\         (F: welldef Int X --> G:X)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   206
by Safe_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   207
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
   208
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
   209
qed "strict_ex_refine_lemma_v";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   210
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   211
Goal "[| strict_ex_prop X;  \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   212
\        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
   213
\     ==> (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
   214
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
   215
    THEN assume_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   216
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
   217
					   strict_ex_refine_lemma_v]) 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   218
qed "ex_refinement_thm";
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 [strict_uv_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   221
     "strict_uv_prop X \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   222
\     ==> (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
   223
by (Blast_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   224
qed "strict_uv_refine_lemma";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   225
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   226
Goalw [strict_uv_prop_def]
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   227
     "strict_uv_prop X \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   228
\     ==> (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
   229
\         (F: welldef Int X --> G:X)";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   230
by Safe_tac;
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   231
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
   232
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
   233
	      simpset()));
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   234
qed "strict_uv_refine_lemma_v";
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   235
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   236
Goal "[| strict_uv_prop X;  \
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   237
\        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
   238
\     ==> (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
   239
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
   240
    THEN assume_tac 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   241
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
   242
					   strict_uv_refine_lemma_v]) 1);
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
   243
qed "uv_refinement_thm";