new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
authorpaulson
Tue Aug 31 15:58:38 1999 +0200 (1999-08-31)
changeset 7400fbd5582761e6
parent 7399 cf780c2bcccf
child 7401 e355f626b2f9
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
for the overloading of <, while .ML file gets proofs about renaming constants
src/HOL/IsaMakefile
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/Guar.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Aug 31 15:56:56 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Aug 31 15:58:38 1999 +0200
     1.3 @@ -186,6 +186,7 @@
     1.4    UNITY/Alloc.ML UNITY/Alloc.thy\
     1.5    UNITY/Channel.ML UNITY/Channel.thy UNITY/Common.ML UNITY/Common.thy\
     1.6    UNITY/Client.ML UNITY/Client.thy  UNITY/Comp.ML UNITY/Comp.thy\
     1.7 +  UNITY/Guar.ML UNITY/Guar.thy\
     1.8    UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/FP.ML UNITY/FP.thy\
     1.9    UNITY/Union.ML UNITY/Union.thy UNITY/Handshake.ML UNITY/Handshake.thy\
    1.10    UNITY/Extend.ML UNITY/Extend.thy\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/Guar.ML	Tue Aug 31 15:58:38 1999 +0200
     2.3 @@ -0,0 +1,299 @@
     2.4 +(*  Title:      HOL/UNITY/Guar.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1999  University of Cambridge
     2.8 +
     2.9 +Guarantees, etc.
    2.10 +
    2.11 +From Chandy and Sanders, "Reasoning About Program Composition"
    2.12 +*)
    2.13 +
    2.14 +(*** existential properties ***)
    2.15 +
    2.16 +Goalw [ex_prop_def]
    2.17 +     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
    2.18 +by (etac finite_induct 1);
    2.19 +by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
    2.20 +qed_spec_mp "ex1";
    2.21 +
    2.22 +Goalw [ex_prop_def]
    2.23 +     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
    2.24 +by (Clarify_tac 1);
    2.25 +by (dres_inst_tac [("x", "{F,G}")] spec 1);
    2.26 +by Auto_tac;
    2.27 +qed "ex2";
    2.28 +
    2.29 +(*Chandy & Sanders take this as a definition*)
    2.30 +Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
    2.31 +by (blast_tac (claset() addIs [ex1,ex2]) 1);
    2.32 +qed "ex_prop_finite";
    2.33 +
    2.34 +(*Their "equivalent definition" given at the end of section 3*)
    2.35 +Goal "ex_prop X = (ALL G. G:X = (ALL H. G <= H --> H: X))";
    2.36 +by Auto_tac;
    2.37 +by (rewrite_goals_tac [ex_prop_def, component_def]);
    2.38 +by (Blast_tac 1);
    2.39 +by Safe_tac;
    2.40 +by (stac Join_commute 2);
    2.41 +by (ALLGOALS Blast_tac);
    2.42 +qed "ex_prop_equiv";
    2.43 +
    2.44 +
    2.45 +(*** universal properties ***)
    2.46 +
    2.47 +Goalw [uv_prop_def]
    2.48 +     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
    2.49 +by (etac finite_induct 1);
    2.50 +by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
    2.51 +qed_spec_mp "uv1";
    2.52 +
    2.53 +Goalw [uv_prop_def]
    2.54 +     "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X  ==> uv_prop X";
    2.55 +by (rtac conjI 1);
    2.56 +by (Clarify_tac 2);
    2.57 +by (dres_inst_tac [("x", "{F,G}")] spec 2);
    2.58 +by (dres_inst_tac [("x", "{}")] spec 1);
    2.59 +by Auto_tac;
    2.60 +qed "uv2";
    2.61 +
    2.62 +(*Chandy & Sanders take this as a definition*)
    2.63 +Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
    2.64 +by (blast_tac (claset() addIs [uv1,uv2]) 1);
    2.65 +qed "uv_prop_finite";
    2.66 +
    2.67 +
    2.68 +(*** guarantees ***)
    2.69 +
    2.70 +val prems = Goal
    2.71 +     "(!!G. [| F Join G : X;  Disjoint F G |] ==> F Join G : Y) \
    2.72 +\     ==> F : X guarantees Y";
    2.73 +by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
    2.74 +by (blast_tac (claset() addIs prems) 1);
    2.75 +qed "guaranteesI";
    2.76 +
    2.77 +Goalw [guar_def, component_def]
    2.78 +     "[| F : X guarantees Y;  F Join G : X |] ==> F Join G : Y";
    2.79 +by (Blast_tac 1);
    2.80 +qed "guaranteesD";
    2.81 +
    2.82 +(*This version of guaranteesD matches more easily in the conclusion*)
    2.83 +Goalw [guar_def]
    2.84 +     "[| F : X guarantees Y;  H : X;  F <= H |] ==> H : Y";
    2.85 +by (Blast_tac 1);
    2.86 +qed "component_guaranteesD";
    2.87 +
    2.88 +(*This equation is more intuitive than the official definition*)
    2.89 +Goal "(F : X guarantees Y) = \
    2.90 +\     (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
    2.91 +by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
    2.92 +by (Blast_tac 1);
    2.93 +qed "guarantees_eq";
    2.94 +
    2.95 +Goalw [guar_def]
    2.96 +     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
    2.97 +by (Blast_tac 1);
    2.98 +qed "guarantees_weaken";
    2.99 +
   2.100 +Goalw [guar_def]
   2.101 +     "[| F: X guarantees Y; F <= F' |] ==> F': X guarantees Y";
   2.102 +by (blast_tac (claset() addIs [component_trans]) 1);
   2.103 +qed "guarantees_weaken_prog";
   2.104 +
   2.105 +Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
   2.106 +by (Blast_tac 1);
   2.107 +qed "subset_imp_guarantees_UNIV";
   2.108 +
   2.109 +(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
   2.110 +Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
   2.111 +by (Blast_tac 1);
   2.112 +qed "subset_imp_guarantees";
   2.113 +
   2.114 +(*Remark at end of section 4.1*)
   2.115 +Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
   2.116 +by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   2.117 +by (blast_tac (claset() addEs [equalityE]) 1);
   2.118 +qed "ex_prop_equiv2";
   2.119 +
   2.120 +(** Distributive laws.  Re-orient to perform miniscoping **)
   2.121 +
   2.122 +Goalw [guar_def]
   2.123 +     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
   2.124 +by (Blast_tac 1);
   2.125 +qed "guarantees_UN_left";
   2.126 +
   2.127 +Goalw [guar_def]
   2.128 +    "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
   2.129 +by (Blast_tac 1);
   2.130 +qed "guarantees_Un_left";
   2.131 +
   2.132 +Goalw [guar_def]
   2.133 +     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
   2.134 +by (Blast_tac 1);
   2.135 +qed "guarantees_INT_right";
   2.136 +
   2.137 +Goalw [guar_def]
   2.138 +    "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
   2.139 +by (Blast_tac 1);
   2.140 +qed "guarantees_Int_right";
   2.141 +
   2.142 +Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
   2.143 +by (Blast_tac 1);
   2.144 +qed "shunting";
   2.145 +
   2.146 +Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
   2.147 +by (Blast_tac 1);
   2.148 +qed "contrapositive";
   2.149 +
   2.150 +(** The following two can be expressed using intersection and subset, which
   2.151 +    is more faithful to the text but looks cryptic.
   2.152 +**)
   2.153 +
   2.154 +Goalw [guar_def]
   2.155 +    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
   2.156 +\    ==> F : (V Int Y) guarantees Z";
   2.157 +by (Blast_tac 1);
   2.158 +qed "combining1";
   2.159 +
   2.160 +Goalw [guar_def]
   2.161 +    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
   2.162 +\    ==> F : V guarantees (X Un Z)";
   2.163 +by (Blast_tac 1);
   2.164 +qed "combining2";
   2.165 +
   2.166 +(** The following two follow Chandy-Sanders, but the use of object-quantifiers
   2.167 +    does not suit Isabelle... **)
   2.168 +
   2.169 +(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
   2.170 +Goalw [guar_def]
   2.171 +     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
   2.172 +by (Blast_tac 1);
   2.173 +qed "all_guarantees";
   2.174 +
   2.175 +(*Premises should be [| F: X guarantees Y i; i: I |] *)
   2.176 +Goalw [guar_def]
   2.177 +     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
   2.178 +by (Blast_tac 1);
   2.179 +qed "ex_guarantees";
   2.180 +
   2.181 +(*** Additional guarantees laws, by lcp ***)
   2.182 +
   2.183 +Goalw [guar_def]
   2.184 +    "[| F: U guarantees V;  G: X guarantees Y |] \
   2.185 +\    ==> F Join G: (U Int X) guarantees (V Int Y)";
   2.186 +by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
   2.187 +by (Blast_tac 1);
   2.188 +qed "guarantees_Join_Int";
   2.189 +
   2.190 +Goalw [guar_def]
   2.191 +    "[| F: U guarantees V;  G: X guarantees Y |]  \
   2.192 +\    ==> F Join G: (U Un X) guarantees (V Un Y)";
   2.193 +by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
   2.194 +by (Blast_tac 1);
   2.195 +qed "guarantees_Join_Un";
   2.196 +
   2.197 +Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
   2.198 +by (simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1);
   2.199 +by (Blast_tac 1);
   2.200 +qed "JN_component_iff";
   2.201 +
   2.202 +Goalw [guar_def]
   2.203 +    "[| ALL i:I. F i : X i guarantees Y i |] \
   2.204 +\    ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
   2.205 +by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
   2.206 +by (Blast_tac 1);
   2.207 +bind_thm ("guarantees_JN_INT", ballI RS result());
   2.208 +
   2.209 +Goalw [guar_def]
   2.210 +    "[| ALL i:I. F i : X i guarantees Y i |] \
   2.211 +\    ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
   2.212 +by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
   2.213 +by (Blast_tac 1);
   2.214 +bind_thm ("guarantees_JN_UN", ballI RS result());
   2.215 +
   2.216 +
   2.217 +(*** guarantees laws for breaking down the program, by lcp ***)
   2.218 +
   2.219 +Goalw [guar_def]
   2.220 +    "F: X guarantees Y | G: X guarantees Y ==> F Join G: X guarantees Y";
   2.221 +by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
   2.222 +by (Blast_tac 1);
   2.223 +qed "guarantees_Join_I";
   2.224 +
   2.225 +Goalw [guar_def]
   2.226 +     "[| i : I;  F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y";
   2.227 +by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
   2.228 +by (Blast_tac 1);
   2.229 +qed "guarantees_JN_I";
   2.230 +
   2.231 +
   2.232 +(*** well-definedness ***)
   2.233 +
   2.234 +Goalw [welldef_def] "F Join G: welldef ==> F: welldef";
   2.235 +by Auto_tac;
   2.236 +qed "Join_welldef_D1";
   2.237 +
   2.238 +Goalw [welldef_def] "F Join G: welldef ==> G: welldef";
   2.239 +by Auto_tac;
   2.240 +qed "Join_welldef_D2";
   2.241 +
   2.242 +(*** refinement ***)
   2.243 +
   2.244 +Goalw [refines_def] "F refines F wrt X";
   2.245 +by (Blast_tac 1);
   2.246 +qed "refines_refl";
   2.247 +
   2.248 +Goalw [refines_def]
   2.249 +     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X";
   2.250 +by Auto_tac;
   2.251 +qed "refines_trans";
   2.252 +
   2.253 +Goalw [strict_ex_prop_def]
   2.254 +     "strict_ex_prop X \
   2.255 +\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   2.256 +by (Blast_tac 1);
   2.257 +qed "strict_ex_refine_lemma";
   2.258 +
   2.259 +Goalw [strict_ex_prop_def]
   2.260 +     "strict_ex_prop X \
   2.261 +\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
   2.262 +\         (F: welldef Int X --> G:X)";
   2.263 +by Safe_tac;
   2.264 +by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   2.265 +by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset()));
   2.266 +qed "strict_ex_refine_lemma_v";
   2.267 +
   2.268 +Goal "[| strict_ex_prop X;  \
   2.269 +\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
   2.270 +\     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   2.271 +by (res_inst_tac [("x","SKIP")] allE 1
   2.272 +    THEN assume_tac 1);
   2.273 +by (asm_full_simp_tac
   2.274 +    (simpset() addsimps [refines_def, iso_refines_def,
   2.275 +			 strict_ex_refine_lemma_v]) 1);
   2.276 +qed "ex_refinement_thm";
   2.277 +
   2.278 +
   2.279 +Goalw [strict_uv_prop_def]
   2.280 +     "strict_uv_prop X \
   2.281 +\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   2.282 +by (Blast_tac 1);
   2.283 +qed "strict_uv_refine_lemma";
   2.284 +
   2.285 +Goalw [strict_uv_prop_def]
   2.286 +     "strict_uv_prop X \
   2.287 +\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
   2.288 +\         (F: welldef Int X --> G:X)";
   2.289 +by Safe_tac;
   2.290 +by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   2.291 +by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2],
   2.292 +	      simpset()));
   2.293 +qed "strict_uv_refine_lemma_v";
   2.294 +
   2.295 +Goal "[| strict_uv_prop X;  \
   2.296 +\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
   2.297 +\     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   2.298 +by (res_inst_tac [("x","SKIP")] allE 1
   2.299 +    THEN assume_tac 1);
   2.300 +by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
   2.301 +					   strict_uv_refine_lemma_v]) 1);
   2.302 +qed "uv_refinement_thm";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/Guar.thy	Tue Aug 31 15:58:38 1999 +0200
     3.3 @@ -0,0 +1,52 @@
     3.4 +(*  Title:      HOL/UNITY/Guar.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1999  University of Cambridge
     3.8 +
     3.9 +Guarantees, etc.
    3.10 +
    3.11 +From Chandy and Sanders, "Reasoning About Program Composition"
    3.12 +*)
    3.13 +
    3.14 +Guar = Comp +
    3.15 +
    3.16 +instance program :: (term) order
    3.17 +                    (component_refl, component_trans, component_antisym,
    3.18 +                     program_less_le)
    3.19 +
    3.20 +constdefs
    3.21 +
    3.22 +  (*Existential and Universal properties.  I formalize the two-program
    3.23 +    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
    3.24 +
    3.25 +  ex_prop  :: 'a program set => bool
    3.26 +   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
    3.27 +
    3.28 +  strict_ex_prop  :: 'a program set => bool
    3.29 +   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
    3.30 +
    3.31 +  uv_prop  :: 'a program set => bool
    3.32 +   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
    3.33 +
    3.34 +  strict_uv_prop  :: 'a program set => bool
    3.35 +   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
    3.36 +
    3.37 +  (*Ill-defined programs can arise through "Join"*)
    3.38 +  welldef :: 'a program set  
    3.39 +   "welldef == {F. Init F ~= {}}"
    3.40 +
    3.41 +  guar :: ['a program set, 'a program set] => 'a program set
    3.42 +   (infixl "guarantees" 55)    (*higher than membership, lower than Co*)
    3.43 +   "X guarantees Y == {F. ALL H. F <= H --> H:X --> H:Y}"
    3.44 +
    3.45 +  refines :: ['a program, 'a program, 'a program set] => bool
    3.46 +			("(3_ refines _ wrt _)" [10,10,10] 10)
    3.47 +   "G refines F wrt X ==
    3.48 +      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
    3.49 +
    3.50 +  iso_refines :: ['a program, 'a program, 'a program set] => bool
    3.51 +			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
    3.52 +   "G iso_refines F wrt X ==
    3.53 +      F : welldef Int X --> G : welldef Int X"
    3.54 +
    3.55 +end