src/HOL/UNITY/Comp.thy
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 13819 78f5885b76a9
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
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
ehmety@11190
    10
Revised by Sidi Ehmety on January  2001 
ehmety@11190
    11
paulson@13805
    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
paulson@13792
    18
theory Comp = Union:
paulson@5597
    19
paulson@13792
    20
instance program :: (type) ord ..
paulson@5597
    21
paulson@7399
    22
defs
paulson@13805
    23
  component_def:          "F \<le> H == \<exists>G. F Join 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@13805
    30
  "F component_of H == \<exists>G. F ok G & F Join 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"
ehmety@11190
    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@13805
    48
lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F Join G)"
paulson@13792
    49
apply (unfold component_def, auto)
paulson@13792
    50
apply (rule_tac x = "G Join Ga" in exI)
paulson@13792
    51
apply (rule_tac [2] x = "G Join F" in exI)
paulson@13792
    52
apply (auto simp add: Join_ac)
paulson@13792
    53
done
paulson@13792
    54
paulson@13792
    55
lemma component_eq_subset: 
paulson@13805
    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@13805
    75
lemma component_Join1: "F \<le> (F Join G)"
paulson@13792
    76
by (unfold component_def, blast)
paulson@13792
    77
paulson@13805
    78
lemma component_Join2: "G \<le> (F Join 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@13805
    83
lemma Join_absorb1: "F \<le> G ==> F Join G = G"
paulson@13792
    84
by (auto simp add: component_def Join_left_absorb)
paulson@13792
    85
paulson@13805
    86
lemma Join_absorb2: "G \<le> F ==> F Join 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@13805
   107
lemma Join_component_iff: "((F Join 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@13792
   113
(*Used in Guar.thy to show that programs are partially ordered*)
paulson@13792
   114
lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
paulson@13792
   115
paulson@13792
   116
paulson@13798
   117
subsection{*The preserves property*}
paulson@13792
   118
paulson@13805
   119
lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
paulson@13792
   120
by (unfold preserves_def, blast)
paulson@13792
   121
paulson@13792
   122
lemma preserves_imp_eq: 
paulson@13805
   123
     "[| F \<in> preserves v;  act \<in> Acts F;  (s,s') \<in> act |] ==> v s = v s'"
paulson@13792
   124
apply (unfold preserves_def stable_def constrains_def, force)
paulson@13792
   125
done
paulson@13792
   126
paulson@13792
   127
lemma Join_preserves [iff]: 
paulson@13805
   128
     "(F Join G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
paulson@13792
   129
apply (unfold preserves_def, auto)
paulson@13792
   130
done
paulson@13792
   131
paulson@13792
   132
lemma JN_preserves [iff]:
paulson@13805
   133
     "(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)"
paulson@13798
   134
apply (simp add: JN_stable preserves_def, blast)
paulson@13792
   135
done
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@13805
   185
     "[| F \<in> stable {s. P (v s) (w s)};    
paulson@13805
   186
         G \<in> preserves v;  G \<in> preserves w |]                
paulson@13805
   187
      ==> F Join 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@13792
   190
 prefer 2 apply simp 
paulson@13805
   191
apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
paulson@13792
   192
done
paulson@13792
   193
paulson@13792
   194
lemma Increasing_preserves_Stable:
paulson@13805
   195
     "[| F \<in> stable {s. v s \<le> w s};  G \<in> preserves v;        
paulson@13805
   196
         F Join G \<in> Increasing w |]                
paulson@13805
   197
      ==> F Join 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
apply (case_tac "act: Acts F", blast)
paulson@13792
   203
(*We have a G-action, so delete assumptions about F-actions*)
paulson@13805
   204
apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
paulson@13805
   205
apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)
paulson@13792
   206
apply (subgoal_tac "v x = v xa")
paulson@13792
   207
prefer 2 apply blast
paulson@13792
   208
apply auto
paulson@13792
   209
apply (erule order_trans, blast)
paulson@13792
   210
done
paulson@13792
   211
paulson@13792
   212
(** component_of **)
paulson@13792
   213
paulson@13805
   214
(*  component_of is stronger than \<le> *)
paulson@13805
   215
lemma component_of_imp_component: "F component_of H ==> F \<le> H"
paulson@13792
   216
by (unfold component_def component_of_def, blast)
paulson@13792
   217
paulson@13792
   218
paulson@13805
   219
(* component_of satisfies many of the same properties as \<le> *)
paulson@13792
   220
lemma component_of_refl [simp]: "F component_of F"
paulson@13792
   221
apply (unfold component_of_def)
paulson@13792
   222
apply (rule_tac x = SKIP in exI, auto)
paulson@13792
   223
done
paulson@13792
   224
paulson@13792
   225
lemma component_of_SKIP [simp]: "SKIP component_of F"
paulson@13792
   226
by (unfold component_of_def, auto)
paulson@13792
   227
paulson@13792
   228
lemma component_of_trans: 
paulson@13792
   229
     "[| F component_of G; G component_of H |] ==> F component_of H"
paulson@13792
   230
apply (unfold component_of_def)
paulson@13792
   231
apply (blast intro: Join_assoc [symmetric])
paulson@13792
   232
done
paulson@13792
   233
paulson@13792
   234
lemmas strict_component_of_eq =
paulson@13792
   235
    strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
paulson@13792
   236
paulson@13792
   237
(** localize **)
paulson@13792
   238
lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
paulson@13798
   239
by (simp add: localize_def)
paulson@13792
   240
paulson@13792
   241
lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
paulson@13798
   242
by (simp add: localize_def)
paulson@13792
   243
paulson@13792
   244
lemma localize_AllowedActs_eq [simp]: 
paulson@13805
   245
 "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
paulson@13798
   246
by (unfold localize_def, auto)
paulson@13792
   247
paulson@5597
   248
end