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