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