src/HOL/UNITY/Comp.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 16417 9bc16273c2d4 child 24147 edc90be09ac1 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     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 imports Union begin
```
```    19
```
```    20 instance program :: (type) ord ..
```
```    21
```
```    22 defs
```
```    23   component_def:          "F \<le> H == \<exists>G. F\<squnion>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\<squnion>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\<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 [THEN meta_eq_to_obj_eq]
```
```   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.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\<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 =
```
```   233     strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
```
```   234
```
```   235 (** localize **)
```
```   236 lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
```
```   237 by (simp add: localize_def)
```
```   238
```
```   239 lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
```
```   240 by (simp add: localize_def)
```
```   241
```
```   242 lemma localize_AllowedActs_eq [simp]:
```
```   243    "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
```
```   244 by (unfold localize_def, auto)
```
```   245
```
```   246 end
```