src/HOL/UNITY/Comp.thy
author paulson
Fri Jan 31 20:12:44 2003 +0100 (2003-01-31)
changeset 13798 4c1a53627500
parent 13792 d1811693899c
child 13805 3786b2fd6808
permissions -rw-r--r--
conversion to new-style theories and tidying
     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 From Chandy and Sanders, "Reasoning About Program Composition",
     8 Technical Report 2000-003, University of Florida, 2000.
     9 
    10 Revised by Sidi Ehmety on January  2001 
    11 
    12 Added: a strong form of the <= relation (component_of) and localize 
    13 
    14 *)
    15 
    16 header{*Composition: Basic Primitives*}
    17 
    18 theory Comp = Union:
    19 
    20 instance program :: (type) ord ..
    21 
    22 defs
    23   component_def:          "F <= H == EX G. F Join G = H"
    24   strict_component_def:   "(F < (H::'a program)) == (F <= H & F ~= H)"
    25 
    26 
    27 constdefs
    28   component_of :: "'a program=>'a program=> bool"
    29                                     (infixl "component'_of" 50)
    30   "F component_of H == EX G. F ok G & F Join G = H"
    31 
    32   strict_component_of :: "'a program\<Rightarrow>'a program=> bool"
    33                                     (infixl "strict'_component'_of" 50)
    34   "F strict_component_of H == F component_of H & F~=H"
    35   
    36   preserves :: "('a=>'b) => 'a program set"
    37     "preserves v == INT z. stable {s. v s = z}"
    38 
    39   localize  :: "('a=>'b) => 'a program => 'a program"
    40   "localize v F == mk_program(Init F, Acts F,
    41 			      AllowedActs F Int (UN G:preserves v. Acts G))"
    42 
    43   funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
    44   "funPair f g == %x. (f x, g x)"
    45 
    46 
    47 subsection{*The component relation*}
    48 lemma componentI: 
    49      "H <= F | H <= G ==> H <= (F Join G)"
    50 apply (unfold component_def, auto)
    51 apply (rule_tac x = "G Join Ga" in exI)
    52 apply (rule_tac [2] x = "G Join F" in exI)
    53 apply (auto simp add: Join_ac)
    54 done
    55 
    56 lemma component_eq_subset: 
    57      "(F <= G) =  
    58       (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)"
    59 apply (unfold component_def)
    60 apply (force intro!: exI program_equalityI)
    61 done
    62 
    63 lemma component_SKIP [iff]: "SKIP <= F"
    64 apply (unfold component_def)
    65 apply (force intro: Join_SKIP_left)
    66 done
    67 
    68 lemma component_refl [iff]: "F <= (F :: 'a program)"
    69 apply (unfold component_def)
    70 apply (blast intro: Join_SKIP_right)
    71 done
    72 
    73 lemma SKIP_minimal: "F <= SKIP ==> F = SKIP"
    74 by (auto intro!: program_equalityI simp add: component_eq_subset)
    75 
    76 lemma component_Join1: "F <= (F Join G)"
    77 by (unfold component_def, blast)
    78 
    79 lemma component_Join2: "G <= (F Join G)"
    80 apply (unfold component_def)
    81 apply (simp add: Join_commute, blast)
    82 done
    83 
    84 lemma Join_absorb1: "F<=G ==> F Join G = G"
    85 by (auto simp add: component_def Join_left_absorb)
    86 
    87 lemma Join_absorb2: "G<=F ==> F Join G = F"
    88 by (auto simp add: Join_ac component_def)
    89 
    90 lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)"
    91 by (simp add: component_eq_subset, blast)
    92 
    93 lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))"
    94 apply (unfold component_def)
    95 apply (blast intro: JN_absorb)
    96 done
    97 
    98 lemma component_trans: "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"
    99 apply (unfold component_def)
   100 apply (blast intro: Join_assoc [symmetric])
   101 done
   102 
   103 lemma component_antisym: "[| F <= G; G <= F |] ==> F = (G :: 'a program)"
   104 apply (simp (no_asm_use) add: component_eq_subset)
   105 apply (blast intro!: program_equalityI)
   106 done
   107 
   108 lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)"
   109 by (simp add: component_eq_subset, blast)
   110 
   111 lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B"
   112 by (auto simp add: constrains_def component_eq_subset)
   113 
   114 (*Used in Guar.thy to show that programs are partially ordered*)
   115 lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
   116 
   117 
   118 subsection{*The preserves property*}
   119 
   120 lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v"
   121 by (unfold preserves_def, blast)
   122 
   123 lemma preserves_imp_eq: 
   124      "[| F : preserves v;  act : Acts F;  (s,s') : act |] ==> v s = v s'"
   125 apply (unfold preserves_def stable_def constrains_def, force)
   126 done
   127 
   128 lemma Join_preserves [iff]: 
   129      "(F Join G : preserves v) = (F : preserves v & G : preserves v)"
   130 apply (unfold preserves_def, auto)
   131 done
   132 
   133 lemma JN_preserves [iff]:
   134      "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"
   135 apply (simp add: JN_stable preserves_def, blast)
   136 done
   137 
   138 lemma SKIP_preserves [iff]: "SKIP : preserves v"
   139 by (auto simp add: preserves_def)
   140 
   141 lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)"
   142 by (simp add:  funPair_def)
   143 
   144 lemma preserves_funPair: "preserves (funPair v w) = preserves v Int preserves w"
   145 by (auto simp add: preserves_def stable_def constrains_def, blast)
   146 
   147 (* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
   148 declare preserves_funPair [THEN eqset_imp_iff, iff]
   149 
   150 
   151 lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)"
   152 by (simp add: funPair_def o_def)
   153 
   154 lemma fst_o_funPair [simp]: "fst o (funPair f g) = f"
   155 by (simp add: funPair_def o_def)
   156 
   157 lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
   158 by (simp add: funPair_def o_def)
   159 
   160 lemma subset_preserves_o: "preserves v <= preserves (w o v)"
   161 by (force simp add: preserves_def stable_def constrains_def)
   162 
   163 lemma preserves_subset_stable: "preserves v <= stable {s. P (v s)}"
   164 apply (auto simp add: preserves_def stable_def constrains_def)
   165 apply (rename_tac s' s)
   166 apply (subgoal_tac "v s = v s'")
   167 apply (force+)
   168 done
   169 
   170 lemma preserves_subset_increasing: "preserves v <= increasing v"
   171 by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def)
   172 
   173 lemma preserves_id_subset_stable: "preserves id <= stable A"
   174 by (force simp add: preserves_def stable_def constrains_def)
   175 
   176 
   177 (** For use with def_UNION_ok_iff **)
   178 
   179 lemma safety_prop_preserves [iff]: "safety_prop (preserves v)"
   180 by (auto intro: safety_prop_INTER1 simp add: preserves_def)
   181 
   182 
   183 (** Some lemmas used only in Client.ML **)
   184 
   185 lemma stable_localTo_stable2:
   186      "[| F : stable {s. P (v s) (w s)};    
   187          G : preserves v;  G : preserves w |]                
   188       ==> F Join G : stable {s. P (v s) (w s)}"
   189 apply (simp (no_asm_simp))
   190 apply (subgoal_tac "G: preserves (funPair v w) ")
   191  prefer 2 apply simp 
   192 apply (drule_tac P1 = "split ?Q" in  preserves_subset_stable [THEN subsetD], auto)
   193 done
   194 
   195 lemma Increasing_preserves_Stable:
   196      "[| F : stable {s. v s <= w s};  G : preserves v;        
   197          F Join G : Increasing w |]                
   198       ==> F Join G : Stable {s. v s <= w s}"
   199 apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
   200 apply (blast intro: constrains_weaken)
   201 (*The G case remains*)
   202 apply (auto simp add: preserves_def stable_def constrains_def)
   203 apply (case_tac "act: Acts F", blast)
   204 (*We have a G-action, so delete assumptions about F-actions*)
   205 apply (erule_tac V = "ALL act:Acts F. ?P act" in thin_rl)
   206 apply (erule_tac V = "ALL z. ALL act:Acts F. ?P z act" in thin_rl)
   207 apply (subgoal_tac "v x = v xa")
   208 prefer 2 apply blast
   209 apply auto
   210 apply (erule order_trans, blast)
   211 done
   212 
   213 (** component_of **)
   214 
   215 (*  component_of is stronger than <= *)
   216 lemma component_of_imp_component: "F component_of H ==> F <= H"
   217 by (unfold component_def component_of_def, blast)
   218 
   219 
   220 (* component_of satisfies many of the <='s properties *)
   221 lemma component_of_refl [simp]: "F component_of F"
   222 apply (unfold component_of_def)
   223 apply (rule_tac x = SKIP in exI, auto)
   224 done
   225 
   226 lemma component_of_SKIP [simp]: "SKIP component_of F"
   227 by (unfold component_of_def, auto)
   228 
   229 lemma component_of_trans: 
   230      "[| F component_of G; G component_of H |] ==> F component_of H"
   231 apply (unfold component_of_def)
   232 apply (blast intro: Join_assoc [symmetric])
   233 done
   234 
   235 lemmas strict_component_of_eq =
   236     strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
   237 
   238 (** localize **)
   239 lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
   240 by (simp add: localize_def)
   241 
   242 lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
   243 by (simp add: localize_def)
   244 
   245 lemma localize_AllowedActs_eq [simp]: 
   246  "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"
   247 by (unfold localize_def, auto)
   248 
   249 end