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