src/HOL/UNITY/Comp.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 35416 d8d7d1b785af
child 46912 e0cd5c4df8e6
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Title:      HOL/UNITY/Comp.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Sidi Ehmety
     4 
     5 Composition.
     6 
     7 From Chandy and Sanders, "Reasoning About Program Composition",
     8 Technical Report 2000-003, University of Florida, 2000.
     9 *)
    10 
    11 header{*Composition: Basic Primitives*}
    12 
    13 theory Comp
    14 imports Union
    15 begin
    16 
    17 instantiation program :: (type) ord
    18 begin
    19 
    20 definition
    21   component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)"
    22 
    23 definition
    24   strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)"
    25 
    26 instance ..
    27 
    28 end
    29 
    30 definition component_of :: "'a program =>'a program=> bool" (infixl "component'_of" 50) where
    31   "F component_of H == \<exists>G. F ok G & F\<squnion>G = H"
    32 
    33 definition strict_component_of :: "'a program\<Rightarrow>'a program=> bool" (infixl "strict'_component'_of" 50)  where
    34   "F strict_component_of H == F component_of H & F\<noteq>H"
    35 
    36 definition preserves :: "('a=>'b) => 'a program set" where
    37     "preserves v == \<Inter>z. stable {s. v s = z}"
    38 
    39 definition localize :: "('a=>'b) => 'a program => 'a program" where
    40   "localize v F == mk_program(Init F, Acts F,
    41                               AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))"
    42 
    43 definition funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" where
    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\<squnion>G)"
    49 apply (unfold component_def, auto)
    50 apply (rule_tac x = "G\<squnion>Ga" in exI)
    51 apply (rule_tac [2] x = "G\<squnion>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\<squnion>G)"
    76 by (unfold component_def, blast)
    77 
    78 lemma component_Join2: "G \<le> (F\<squnion>G)"
    79 apply (unfold component_def)
    80 apply (simp add: Join_commute, blast)
    81 done
    82 
    83 lemma Join_absorb1: "F \<le> G ==> F\<squnion>G = G"
    84 by (auto simp add: component_def Join_left_absorb)
    85 
    86 lemma Join_absorb2: "G \<le> F ==> F\<squnion>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\<squnion>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 lemma component_stable: "[| F \<le> G; G \<in> stable A |] ==> F \<in> stable A"
   114 by (auto simp add: stable_def component_constrains)
   115 
   116 (*Used in Guar.thy to show that programs are partially ordered*)
   117 lemmas program_less_le = strict_component_def
   118 
   119 
   120 subsection{*The preserves property*}
   121 
   122 lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
   123 by (unfold preserves_def, blast)
   124 
   125 lemma preserves_imp_eq:
   126      "[| F \<in> preserves v;  act \<in> Acts F;  (s,s') \<in> act |] ==> v s = v s'"
   127 by (unfold preserves_def stable_def constrains_def, force)
   128 
   129 lemma Join_preserves [iff]:
   130      "(F\<squnion>G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
   131 by (unfold preserves_def, auto)
   132 
   133 lemma JN_preserves [iff]:
   134      "(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)"
   135 by (simp add: JN_stable preserves_def, blast)
   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.thy **)
   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\<squnion>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], 
   192        auto)
   193 done
   194 
   195 lemma Increasing_preserves_Stable:
   196      "[| F \<in> stable {s. v s \<le> w s};  G \<in> preserves v; F\<squnion>G \<in> Increasing w |]
   197       ==> F\<squnion>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 (*We have a G-action, so delete assumptions about F-actions*)
   203 apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
   204 apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)
   205 apply (subgoal_tac "v x = v xa")
   206  apply auto
   207 apply (erule order_trans, blast)
   208 done
   209 
   210 (** component_of **)
   211 
   212 (*  component_of is stronger than \<le> *)
   213 lemma component_of_imp_component: "F component_of H ==> F \<le> H"
   214 by (unfold component_def component_of_def, blast)
   215 
   216 
   217 (* component_of satisfies many of the same properties as \<le> *)
   218 lemma component_of_refl [simp]: "F component_of F"
   219 apply (unfold component_of_def)
   220 apply (rule_tac x = SKIP in exI, auto)
   221 done
   222 
   223 lemma component_of_SKIP [simp]: "SKIP component_of F"
   224 by (unfold component_of_def, auto)
   225 
   226 lemma component_of_trans:
   227      "[| F component_of G; G component_of H |] ==> F component_of H"
   228 apply (unfold component_of_def)
   229 apply (blast intro: Join_assoc [symmetric])
   230 done
   231 
   232 lemmas strict_component_of_eq = strict_component_of_def
   233 
   234 (** localize **)
   235 lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
   236 by (simp add: localize_def)
   237 
   238 lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
   239 by (simp add: localize_def)
   240 
   241 lemma localize_AllowedActs_eq [simp]:
   242    "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
   243 by (unfold localize_def, auto)
   244 
   245 end