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