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