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