src/HOL/UNITY/Project.thy
author paulson
Sun Feb 16 12:17:40 2003 +0100 (2003-02-16)
changeset 13819 78f5885b76a9
parent 13812 91713a1915ee
child 16417 9bc16273c2d4
permissions -rw-r--r--
minor revisions
paulson@7630
     1
(*  Title:      HOL/UNITY/Project.ML
paulson@7630
     2
    ID:         $Id$
paulson@7630
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7630
     4
    Copyright   1999  University of Cambridge
paulson@7630
     5
paulson@7630
     6
Projections of state sets (also of actions and programs)
paulson@7630
     7
paulson@7630
     8
Inheritance of GUARANTEES properties under extension
paulson@7630
     9
*)
paulson@7630
    10
paulson@13798
    11
header{*Projections of State Sets*}
paulson@13798
    12
paulson@13790
    13
theory Project = Extend:
paulson@7826
    14
paulson@7826
    15
constdefs
paulson@7826
    16
  projecting :: "['c program => 'c set, 'a*'b => 'c, 
paulson@7826
    17
		  'a program, 'c program set, 'a program set] => bool"
paulson@10064
    18
    "projecting C h F X' X ==
paulson@13819
    19
       \<forall>G. extend h F\<squnion>G \<in> X' --> F\<squnion>project h (C G) G \<in> X"
paulson@7826
    20
paulson@10064
    21
  extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
paulson@8055
    22
		 'c program set, 'a program set] => bool"
paulson@10064
    23
    "extending C h F Y' Y ==
paulson@13819
    24
       \<forall>G. extend h F  ok G --> F\<squnion>project h (C G) G \<in> Y
paulson@13819
    25
	      --> extend h F\<squnion>G \<in> Y'"
paulson@10064
    26
paulson@10064
    27
  subset_closed :: "'a set set => bool"
paulson@13812
    28
    "subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U"  
paulson@7826
    29
paulson@13790
    30
paulson@13790
    31
lemma (in Extend) project_extend_constrains_I:
paulson@13812
    32
     "F \<in> A co B ==> project h C (extend h F) \<in> A co B"
paulson@13790
    33
apply (auto simp add: extend_act_def project_act_def constrains_def)
paulson@13790
    34
done
paulson@13790
    35
paulson@13790
    36
paulson@13798
    37
subsection{*Safety*}
paulson@13790
    38
paulson@13790
    39
(*used below to prove Join_project_ensures*)
paulson@13798
    40
lemma (in Extend) project_unless [rule_format]:
paulson@13812
    41
     "[| G \<in> stable C;  project h C G \<in> A unless B |]  
paulson@13812
    42
      ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
paulson@13790
    43
apply (simp add: unless_def project_constrains)
paulson@13790
    44
apply (blast dest: stable_constrains_Int intro: constrains_weaken)
paulson@13790
    45
done
paulson@13790
    46
paulson@13819
    47
(*Generalizes project_constrains to the program F\<squnion>project h C G
paulson@13790
    48
  useful with guarantees reasoning*)
paulson@13790
    49
lemma (in Extend) Join_project_constrains:
paulson@13819
    50
     "(F\<squnion>project h C G \<in> A co B)  =   
paulson@13819
    51
        (extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) &   
paulson@13812
    52
         F \<in> A co B)"
paulson@13790
    53
apply (simp (no_asm) add: project_constrains)
paulson@13790
    54
apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] 
paulson@13790
    55
             dest: constrains_imp_subset)
paulson@13790
    56
done
paulson@13790
    57
paulson@13790
    58
(*The condition is required to prove the left-to-right direction
paulson@13812
    59
  could weaken it to G \<in> (C \<inter> extend_set h A) co C*)
paulson@13790
    60
lemma (in Extend) Join_project_stable: 
paulson@13819
    61
     "extend h F\<squnion>G \<in> stable C  
paulson@13819
    62
      ==> (F\<squnion>project h C G \<in> stable A)  =   
paulson@13819
    63
          (extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) &   
paulson@13812
    64
           F \<in> stable A)"
paulson@13790
    65
apply (unfold stable_def)
paulson@13790
    66
apply (simp only: Join_project_constrains)
paulson@13790
    67
apply (blast intro: constrains_weaken dest: constrains_Int)
paulson@13790
    68
done
paulson@13790
    69
paulson@13790
    70
(*For using project_guarantees in particular cases*)
paulson@13790
    71
lemma (in Extend) project_constrains_I:
paulson@13819
    72
     "extend h F\<squnion>G \<in> extend_set h A co extend_set h B  
paulson@13819
    73
      ==> F\<squnion>project h C G \<in> A co B"
paulson@13790
    74
apply (simp add: project_constrains extend_constrains)
paulson@13790
    75
apply (blast intro: constrains_weaken dest: constrains_imp_subset)
paulson@13790
    76
done
paulson@13790
    77
paulson@13790
    78
lemma (in Extend) project_increasing_I: 
paulson@13819
    79
     "extend h F\<squnion>G \<in> increasing (func o f)  
paulson@13819
    80
      ==> F\<squnion>project h C G \<in> increasing func"
paulson@13790
    81
apply (unfold increasing_def stable_def)
paulson@13790
    82
apply (simp del: Join_constrains
paulson@13790
    83
            add: project_constrains_I extend_set_eq_Collect)
paulson@13790
    84
done
paulson@13790
    85
paulson@13790
    86
lemma (in Extend) Join_project_increasing:
paulson@13819
    87
     "(F\<squnion>project h UNIV G \<in> increasing func)  =   
paulson@13819
    88
      (extend h F\<squnion>G \<in> increasing (func o f))"
paulson@13790
    89
apply (rule iffI)
paulson@13790
    90
apply (erule_tac [2] project_increasing_I)
paulson@13790
    91
apply (simp del: Join_stable
paulson@13790
    92
            add: increasing_def Join_project_stable)
paulson@13790
    93
apply (auto simp add: extend_set_eq_Collect extend_stable [THEN iffD1])
paulson@13790
    94
done
paulson@13790
    95
paulson@13790
    96
(*The UNIV argument is essential*)
paulson@13790
    97
lemma (in Extend) project_constrains_D:
paulson@13819
    98
     "F\<squnion>project h UNIV G \<in> A co B  
paulson@13819
    99
      ==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B"
paulson@13790
   100
by (simp add: project_constrains extend_constrains)
paulson@13790
   101
paulson@13790
   102
paulson@13798
   103
subsection{*"projecting" and union/intersection (no converses)*}
paulson@13790
   104
paulson@13790
   105
lemma projecting_Int: 
paulson@13790
   106
     "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
paulson@13812
   107
      ==> projecting C h F (XA' \<inter> XB') (XA \<inter> XB)"
paulson@13790
   108
by (unfold projecting_def, blast)
paulson@13790
   109
paulson@13790
   110
lemma projecting_Un: 
paulson@13790
   111
     "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
paulson@13812
   112
      ==> projecting C h F (XA' \<union> XB') (XA \<union> XB)"
paulson@13790
   113
by (unfold projecting_def, blast)
paulson@13790
   114
paulson@13790
   115
lemma projecting_INT: 
paulson@13812
   116
     "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]  
paulson@13812
   117
      ==> projecting C h F (\<Inter>i \<in> I. X' i) (\<Inter>i \<in> I. X i)"
paulson@13790
   118
by (unfold projecting_def, blast)
paulson@13790
   119
paulson@13790
   120
lemma projecting_UN: 
paulson@13812
   121
     "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]  
paulson@13812
   122
      ==> projecting C h F (\<Union>i \<in> I. X' i) (\<Union>i \<in> I. X i)"
paulson@13790
   123
by (unfold projecting_def, blast)
paulson@13790
   124
paulson@13790
   125
lemma projecting_weaken: 
paulson@13812
   126
     "[| projecting C h F X' X;  U'<=X';  X \<subseteq> U |] ==> projecting C h F U' U"
paulson@13790
   127
by (unfold projecting_def, auto)
paulson@13790
   128
paulson@13790
   129
lemma projecting_weaken_L: 
paulson@13790
   130
     "[| projecting C h F X' X;  U'<=X' |] ==> projecting C h F U' X"
paulson@13790
   131
by (unfold projecting_def, auto)
paulson@13790
   132
paulson@13790
   133
lemma extending_Int: 
paulson@13790
   134
     "[| extending C h F YA' YA;  extending C h F YB' YB |]  
paulson@13812
   135
      ==> extending C h F (YA' \<inter> YB') (YA \<inter> YB)"
paulson@13790
   136
by (unfold extending_def, blast)
paulson@13790
   137
paulson@13790
   138
lemma extending_Un: 
paulson@13790
   139
     "[| extending C h F YA' YA;  extending C h F YB' YB |]  
paulson@13812
   140
      ==> extending C h F (YA' \<union> YB') (YA \<union> YB)"
paulson@13790
   141
by (unfold extending_def, blast)
paulson@13790
   142
paulson@13790
   143
lemma extending_INT: 
paulson@13812
   144
     "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]  
paulson@13812
   145
      ==> extending C h F (\<Inter>i \<in> I. Y' i) (\<Inter>i \<in> I. Y i)"
paulson@13790
   146
by (unfold extending_def, blast)
paulson@13790
   147
paulson@13790
   148
lemma extending_UN: 
paulson@13812
   149
     "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]  
paulson@13812
   150
      ==> extending C h F (\<Union>i \<in> I. Y' i) (\<Union>i \<in> I. Y i)"
paulson@13790
   151
by (unfold extending_def, blast)
paulson@13790
   152
paulson@13790
   153
lemma extending_weaken: 
paulson@13812
   154
     "[| extending C h F Y' Y;  Y'<=V';  V \<subseteq> Y |] ==> extending C h F V' V"
paulson@13790
   155
by (unfold extending_def, auto)
paulson@13790
   156
paulson@13790
   157
lemma extending_weaken_L: 
paulson@13790
   158
     "[| extending C h F Y' Y;  Y'<=V' |] ==> extending C h F V' Y"
paulson@13790
   159
by (unfold extending_def, auto)
paulson@13790
   160
paulson@13790
   161
lemma projecting_UNIV: "projecting C h F X' UNIV"
paulson@13790
   162
by (simp add: projecting_def)
paulson@13790
   163
paulson@13790
   164
lemma (in Extend) projecting_constrains: 
paulson@13790
   165
     "projecting C h F (extend_set h A co extend_set h B) (A co B)"
paulson@13790
   166
apply (unfold projecting_def)
paulson@13790
   167
apply (blast intro: project_constrains_I)
paulson@13790
   168
done
paulson@13790
   169
paulson@13790
   170
lemma (in Extend) projecting_stable: 
paulson@13790
   171
     "projecting C h F (stable (extend_set h A)) (stable A)"
paulson@13790
   172
apply (unfold stable_def)
paulson@13790
   173
apply (rule projecting_constrains)
paulson@13790
   174
done
paulson@13790
   175
paulson@13790
   176
lemma (in Extend) projecting_increasing: 
paulson@13790
   177
     "projecting C h F (increasing (func o f)) (increasing func)"
paulson@13790
   178
apply (unfold projecting_def)
paulson@13790
   179
apply (blast intro: project_increasing_I)
paulson@13790
   180
done
paulson@13790
   181
paulson@13790
   182
lemma (in Extend) extending_UNIV: "extending C h F UNIV Y"
paulson@13790
   183
apply (simp (no_asm) add: extending_def)
paulson@13790
   184
done
paulson@13790
   185
paulson@13790
   186
lemma (in Extend) extending_constrains: 
paulson@13790
   187
     "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)"
paulson@13790
   188
apply (unfold extending_def)
paulson@13790
   189
apply (blast intro: project_constrains_D)
paulson@13790
   190
done
paulson@13790
   191
paulson@13790
   192
lemma (in Extend) extending_stable: 
paulson@13790
   193
     "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)"
paulson@13790
   194
apply (unfold stable_def)
paulson@13790
   195
apply (rule extending_constrains)
paulson@13790
   196
done
paulson@13790
   197
paulson@13790
   198
lemma (in Extend) extending_increasing: 
paulson@13790
   199
     "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)"
paulson@13790
   200
by (force simp only: extending_def Join_project_increasing)
paulson@13790
   201
paulson@13790
   202
paulson@13798
   203
subsection{*Reachability and project*}
paulson@13790
   204
paulson@13790
   205
(*In practice, C = reachable(...): the inclusion is equality*)
paulson@13790
   206
lemma (in Extend) reachable_imp_reachable_project:
paulson@13819
   207
     "[| reachable (extend h F\<squnion>G) \<subseteq> C;   
paulson@13819
   208
         z \<in> reachable (extend h F\<squnion>G) |]  
paulson@13819
   209
      ==> f z \<in> reachable (F\<squnion>project h C G)"
paulson@13790
   210
apply (erule reachable.induct)
paulson@13790
   211
apply (force intro!: reachable.Init simp add: split_extended_all, auto)
paulson@13790
   212
 apply (rule_tac act = x in reachable.Acts)
paulson@13790
   213
 apply auto
paulson@13790
   214
 apply (erule extend_act_D)
paulson@13790
   215
apply (rule_tac act1 = "Restrict C act"
paulson@13790
   216
       in project_act_I [THEN [3] reachable.Acts], auto) 
paulson@13790
   217
done
paulson@13790
   218
paulson@13790
   219
lemma (in Extend) project_Constrains_D: 
paulson@13819
   220
     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B   
paulson@13819
   221
      ==> extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)"
paulson@13790
   222
apply (unfold Constrains_def)
paulson@13790
   223
apply (simp del: Join_constrains
paulson@13790
   224
            add: Join_project_constrains, clarify)
paulson@13790
   225
apply (erule constrains_weaken)
paulson@13790
   226
apply (auto intro: reachable_imp_reachable_project)
paulson@13790
   227
done
paulson@13790
   228
paulson@13790
   229
lemma (in Extend) project_Stable_D: 
paulson@13819
   230
     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A   
paulson@13819
   231
      ==> extend h F\<squnion>G \<in> Stable (extend_set h A)"
paulson@13790
   232
apply (unfold Stable_def)
paulson@13790
   233
apply (simp (no_asm_simp) add: project_Constrains_D)
paulson@13790
   234
done
paulson@13790
   235
paulson@13790
   236
lemma (in Extend) project_Always_D: 
paulson@13819
   237
     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A   
paulson@13819
   238
      ==> extend h F\<squnion>G \<in> Always (extend_set h A)"
paulson@13790
   239
apply (unfold Always_def)
paulson@13790
   240
apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
paulson@13790
   241
done
paulson@13790
   242
paulson@13790
   243
lemma (in Extend) project_Increasing_D: 
paulson@13819
   244
     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func   
paulson@13819
   245
      ==> extend h F\<squnion>G \<in> Increasing (func o f)"
paulson@13790
   246
apply (unfold Increasing_def, auto)
paulson@13790
   247
apply (subst extend_set_eq_Collect [symmetric])
paulson@13790
   248
apply (simp (no_asm_simp) add: project_Stable_D)
paulson@13790
   249
done
paulson@13790
   250
paulson@13790
   251
paulson@13798
   252
subsection{*Converse results for weak safety: benefits of the argument C *}
paulson@13790
   253
paulson@13790
   254
(*In practice, C = reachable(...): the inclusion is equality*)
paulson@13790
   255
lemma (in Extend) reachable_project_imp_reachable:
paulson@13819
   256
     "[| C \<subseteq> reachable(extend h F\<squnion>G);    
paulson@13819
   257
         x \<in> reachable (F\<squnion>project h C G) |]  
paulson@13819
   258
      ==> \<exists>y. h(x,y) \<in> reachable (extend h F\<squnion>G)"
paulson@13790
   259
apply (erule reachable.induct)
paulson@13790
   260
apply  (force intro: reachable.Init)
paulson@13790
   261
apply (auto simp add: project_act_def)
paulson@13790
   262
apply (force del: Id_in_Acts intro: reachable.Acts extend_act_D)+
paulson@13790
   263
done
paulson@13790
   264
paulson@13790
   265
lemma (in Extend) project_set_reachable_extend_eq:
paulson@13819
   266
     "project_set h (reachable (extend h F\<squnion>G)) =  
paulson@13819
   267
      reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)"
paulson@13790
   268
by (auto dest: subset_refl [THEN reachable_imp_reachable_project] 
paulson@13790
   269
               subset_refl [THEN reachable_project_imp_reachable])
paulson@13790
   270
paulson@13790
   271
(*UNUSED*)
paulson@13790
   272
lemma (in Extend) reachable_extend_Join_subset:
paulson@13819
   273
     "reachable (extend h F\<squnion>G) \<subseteq> C   
paulson@13819
   274
      ==> reachable (extend h F\<squnion>G) \<subseteq>  
paulson@13819
   275
          extend_set h (reachable (F\<squnion>project h C G))"
paulson@13790
   276
apply (auto dest: reachable_imp_reachable_project)
paulson@13790
   277
done
paulson@13790
   278
paulson@13790
   279
lemma (in Extend) project_Constrains_I: 
paulson@13819
   280
     "extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)   
paulson@13819
   281
      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B"
paulson@13790
   282
apply (unfold Constrains_def)
paulson@13790
   283
apply (simp del: Join_constrains
paulson@13790
   284
            add: Join_project_constrains extend_set_Int_distrib)
paulson@13790
   285
apply (rule conjI)
paulson@13790
   286
 prefer 2 
paulson@13790
   287
 apply (force elim: constrains_weaken_L
paulson@13790
   288
              dest!: extend_constrains_project_set
paulson@13790
   289
                     subset_refl [THEN reachable_project_imp_reachable])
paulson@13790
   290
apply (blast intro: constrains_weaken_L)
paulson@13790
   291
done
paulson@13790
   292
paulson@13790
   293
lemma (in Extend) project_Stable_I: 
paulson@13819
   294
     "extend h F\<squnion>G \<in> Stable (extend_set h A)   
paulson@13819
   295
      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A"
paulson@13790
   296
apply (unfold Stable_def)
paulson@13790
   297
apply (simp (no_asm_simp) add: project_Constrains_I)
paulson@13790
   298
done
paulson@13790
   299
paulson@13790
   300
lemma (in Extend) project_Always_I: 
paulson@13819
   301
     "extend h F\<squnion>G \<in> Always (extend_set h A)   
paulson@13819
   302
      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A"
paulson@13790
   303
apply (unfold Always_def)
paulson@13790
   304
apply (auto simp add: project_Stable_I)
paulson@13790
   305
apply (unfold extend_set_def, blast)
paulson@13790
   306
done
paulson@13790
   307
paulson@13790
   308
lemma (in Extend) project_Increasing_I: 
paulson@13819
   309
    "extend h F\<squnion>G \<in> Increasing (func o f)   
paulson@13819
   310
     ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func"
paulson@13790
   311
apply (unfold Increasing_def, auto)
paulson@13790
   312
apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
paulson@13790
   313
done
paulson@13790
   314
paulson@13790
   315
lemma (in Extend) project_Constrains:
paulson@13819
   316
     "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B)  =   
paulson@13819
   317
      (extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))"
paulson@13790
   318
apply (blast intro: project_Constrains_I project_Constrains_D)
paulson@13790
   319
done
paulson@13790
   320
paulson@13790
   321
lemma (in Extend) project_Stable: 
paulson@13819
   322
     "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A)  =   
paulson@13819
   323
      (extend h F\<squnion>G \<in> Stable (extend_set h A))"
paulson@13790
   324
apply (unfold Stable_def)
paulson@13790
   325
apply (rule project_Constrains)
paulson@13790
   326
done
paulson@13790
   327
paulson@13790
   328
lemma (in Extend) project_Increasing: 
paulson@13819
   329
   "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func)  =  
paulson@13819
   330
    (extend h F\<squnion>G \<in> Increasing (func o f))"
paulson@13790
   331
apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
paulson@13790
   332
done
paulson@13790
   333
paulson@13798
   334
subsection{*A lot of redundant theorems: all are proved to facilitate reasoning
paulson@13798
   335
    about guarantees.*}
paulson@13790
   336
paulson@13790
   337
lemma (in Extend) projecting_Constrains: 
paulson@13819
   338
     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   339
                 (extend_set h A Co extend_set h B) (A Co B)"
paulson@13790
   340
paulson@13790
   341
apply (unfold projecting_def)
paulson@13790
   342
apply (blast intro: project_Constrains_I)
paulson@13790
   343
done
paulson@13790
   344
paulson@13790
   345
lemma (in Extend) projecting_Stable: 
paulson@13819
   346
     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   347
                 (Stable (extend_set h A)) (Stable A)"
paulson@13790
   348
apply (unfold Stable_def)
paulson@13790
   349
apply (rule projecting_Constrains)
paulson@13790
   350
done
paulson@13790
   351
paulson@13790
   352
lemma (in Extend) projecting_Always: 
paulson@13819
   353
     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   354
                 (Always (extend_set h A)) (Always A)"
paulson@13790
   355
apply (unfold projecting_def)
paulson@13790
   356
apply (blast intro: project_Always_I)
paulson@13790
   357
done
paulson@13790
   358
paulson@13790
   359
lemma (in Extend) projecting_Increasing: 
paulson@13819
   360
     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   361
                 (Increasing (func o f)) (Increasing func)"
paulson@13790
   362
apply (unfold projecting_def)
paulson@13790
   363
apply (blast intro: project_Increasing_I)
paulson@13790
   364
done
paulson@13790
   365
paulson@13790
   366
lemma (in Extend) extending_Constrains: 
paulson@13819
   367
     "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   368
                  (extend_set h A Co extend_set h B) (A Co B)"
paulson@13790
   369
apply (unfold extending_def)
paulson@13790
   370
apply (blast intro: project_Constrains_D)
paulson@13790
   371
done
paulson@13790
   372
paulson@13790
   373
lemma (in Extend) extending_Stable: 
paulson@13819
   374
     "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   375
                  (Stable (extend_set h A)) (Stable A)"
paulson@13790
   376
apply (unfold extending_def)
paulson@13790
   377
apply (blast intro: project_Stable_D)
paulson@13790
   378
done
paulson@13790
   379
paulson@13790
   380
lemma (in Extend) extending_Always: 
paulson@13819
   381
     "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   382
                  (Always (extend_set h A)) (Always A)"
paulson@13790
   383
apply (unfold extending_def)
paulson@13790
   384
apply (blast intro: project_Always_D)
paulson@13790
   385
done
paulson@13790
   386
paulson@13790
   387
lemma (in Extend) extending_Increasing: 
paulson@13819
   388
     "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   389
                  (Increasing (func o f)) (Increasing func)"
paulson@13790
   390
apply (unfold extending_def)
paulson@13790
   391
apply (blast intro: project_Increasing_D)
paulson@13790
   392
done
paulson@13790
   393
paulson@13790
   394
paulson@13798
   395
subsection{*leadsETo in the precondition (??)*}
paulson@13790
   396
paulson@13798
   397
subsubsection{*transient*}
paulson@13790
   398
paulson@13790
   399
lemma (in Extend) transient_extend_set_imp_project_transient: 
paulson@13812
   400
     "[| G \<in> transient (C \<inter> extend_set h A);  G \<in> stable C |]   
paulson@13812
   401
      ==> project h C G \<in> transient (project_set h C \<inter> A)"
paulson@13812
   402
apply (auto simp add: transient_def Domain_project_act)
paulson@13812
   403
apply (subgoal_tac "act `` (C \<inter> extend_set h A) \<subseteq> - extend_set h A")
paulson@13812
   404
 prefer 2
paulson@13790
   405
 apply (simp add: stable_def constrains_def, blast) 
paulson@13790
   406
(*back to main goal*)
paulson@13812
   407
apply (erule_tac V = "?AA \<subseteq> -C \<union> ?BB" in thin_rl)
paulson@13790
   408
apply (drule bspec, assumption) 
paulson@13790
   409
apply (simp add: extend_set_def project_act_def, blast)
paulson@13790
   410
done
paulson@13790
   411
paulson@13790
   412
(*converse might hold too?*)
paulson@13790
   413
lemma (in Extend) project_extend_transient_D: 
paulson@13812
   414
     "project h C (extend h F) \<in> transient (project_set h C \<inter> D)  
paulson@13812
   415
      ==> F \<in> transient (project_set h C \<inter> D)"
paulson@13812
   416
apply (simp add: transient_def Domain_project_act, safe)
paulson@13812
   417
apply blast+
paulson@13790
   418
done
paulson@13790
   419
paulson@13790
   420
paulson@13798
   421
subsubsection{*ensures -- a primitive combining progress with safety*}
paulson@13790
   422
paulson@13790
   423
(*Used to prove project_leadsETo_I*)
paulson@13790
   424
lemma (in Extend) ensures_extend_set_imp_project_ensures:
paulson@13812
   425
     "[| extend h F \<in> stable C;  G \<in> stable C;   
paulson@13819
   426
         extend h F\<squnion>G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]   
paulson@13819
   427
      ==> F\<squnion>project h C G   
paulson@13812
   428
            \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
paulson@13812
   429
apply (simp add: ensures_def project_constrains Join_transient extend_transient,
paulson@13812
   430
       clarify)
paulson@13790
   431
apply (intro conjI) 
paulson@13790
   432
(*first subgoal*)
paulson@13790
   433
apply (blast intro: extend_stable_project_set 
paulson@13790
   434
                  [THEN stableD, THEN constrains_Int, THEN constrains_weaken] 
paulson@13790
   435
             dest!: extend_constrains_project_set equalityD1)
paulson@13790
   436
(*2nd subgoal*)
paulson@13790
   437
apply (erule stableD [THEN constrains_Int, THEN constrains_weaken])
paulson@13790
   438
    apply assumption
paulson@13790
   439
   apply (simp (no_asm_use) add: extend_set_def)
paulson@13790
   440
   apply blast
paulson@13790
   441
 apply (simp add: extend_set_Int_distrib extend_set_Un_distrib)
paulson@13790
   442
 apply (blast intro!: extend_set_project_set [THEN subsetD], blast)
paulson@13790
   443
(*The transient part*)
paulson@13790
   444
apply auto
paulson@13790
   445
 prefer 2
paulson@13790
   446
 apply (force dest!: equalityD1
paulson@13790
   447
              intro: transient_extend_set_imp_project_transient
paulson@13790
   448
                         [THEN transient_strengthen])
paulson@13790
   449
apply (simp (no_asm_use) add: Int_Diff)
paulson@13790
   450
apply (force dest!: equalityD1 
paulson@13790
   451
             intro: transient_extend_set_imp_project_transient 
paulson@13790
   452
               [THEN project_extend_transient_D, THEN transient_strengthen])
paulson@13790
   453
done
paulson@13790
   454
paulson@13812
   455
text{*Transferring a transient property upwards*}
paulson@13812
   456
lemma (in Extend) project_transient_extend_set:
paulson@13812
   457
     "project h C G \<in> transient (project_set h C \<inter> A - B)
paulson@13812
   458
      ==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)"
paulson@13812
   459
apply (simp add: transient_def project_set_def extend_set_def project_act_def)
paulson@13812
   460
apply (elim disjE bexE)
paulson@13812
   461
 apply (rule_tac x=Id in bexI)  
paulson@13812
   462
  apply (blast intro!: rev_bexI )+
paulson@13812
   463
done
paulson@13812
   464
paulson@13812
   465
lemma (in Extend) project_unless2 [rule_format]:
paulson@13812
   466
     "[| G \<in> stable C;  project h C G \<in> (project_set h C \<inter> A) unless B |]  
paulson@13812
   467
      ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
paulson@13812
   468
by (auto dest: stable_constrains_Int intro: constrains_weaken
paulson@13812
   469
         simp add: unless_def project_constrains Diff_eq Int_assoc 
paulson@13812
   470
                   Int_extend_set_lemma)
paulson@13812
   471
paulson@13812
   472
paulson@13812
   473
lemma (in Extend) extend_unless:
paulson@13812
   474
   "[|extend h F \<in> stable C; F \<in> A unless B|]
paulson@13812
   475
    ==> extend h F \<in> C \<inter> extend_set h A unless extend_set h B"
paulson@13812
   476
apply (simp add: unless_def stable_def)
paulson@13812
   477
apply (drule constrains_Int) 
paulson@13812
   478
apply (erule extend_constrains [THEN iffD2]) 
paulson@13812
   479
apply (erule constrains_weaken, blast) 
paulson@13812
   480
apply blast 
paulson@13812
   481
done
paulson@13812
   482
paulson@13790
   483
(*Used to prove project_leadsETo_D*)
paulson@13798
   484
lemma (in Extend) Join_project_ensures [rule_format]:
paulson@13819
   485
     "[| extend h F\<squnion>G \<in> stable C;   
paulson@13819
   486
         F\<squnion>project h C G \<in> A ensures B |]  
paulson@13819
   487
      ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
paulson@13812
   488
apply (auto simp add: ensures_eq extend_unless project_unless)
paulson@13812
   489
apply (blast intro:  extend_transient [THEN iffD2] transient_strengthen)  
paulson@13812
   490
apply (blast intro: project_transient_extend_set transient_strengthen)  
paulson@13790
   491
done
paulson@13790
   492
paulson@13798
   493
text{*Lemma useful for both STRONG and WEAK progress, but the transient
paulson@13798
   494
    condition's very strong*}
paulson@13790
   495
paulson@13790
   496
(*The strange induction formula allows induction over the leadsTo
paulson@13790
   497
  assumption's non-atomic precondition*)
paulson@13790
   498
lemma (in Extend) PLD_lemma:
paulson@13819
   499
     "[| extend h F\<squnion>G \<in> stable C;   
paulson@13819
   500
         F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
paulson@13819
   501
      ==> extend h F\<squnion>G \<in>  
paulson@13812
   502
          C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
paulson@13790
   503
apply (erule leadsTo_induct)
paulson@13790
   504
  apply (blast intro: leadsTo_Basis Join_project_ensures)
paulson@13790
   505
 apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans)
paulson@13790
   506
apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union)
paulson@13790
   507
done
paulson@13790
   508
paulson@13790
   509
lemma (in Extend) project_leadsTo_D_lemma:
paulson@13819
   510
     "[| extend h F\<squnion>G \<in> stable C;   
paulson@13819
   511
         F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
paulson@13819
   512
      ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
paulson@13790
   513
apply (rule PLD_lemma [THEN leadsTo_weaken])
paulson@13790
   514
apply (auto simp add: split_extended_all)
paulson@13790
   515
done
paulson@13790
   516
paulson@13790
   517
lemma (in Extend) Join_project_LeadsTo:
paulson@13819
   518
     "[| C = (reachable (extend h F\<squnion>G));  
paulson@13819
   519
         F\<squnion>project h C G \<in> A LeadsTo B |]  
paulson@13819
   520
      ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
paulson@13790
   521
by (simp del: Join_stable    add: LeadsTo_def project_leadsTo_D_lemma
paulson@13790
   522
                                  project_set_reachable_extend_eq)
paulson@13790
   523
paulson@13790
   524
paulson@13798
   525
subsection{*Towards the theorem @{text project_Ensures_D}*}
paulson@13790
   526
paulson@13790
   527
lemma (in Extend) project_ensures_D_lemma:
paulson@13812
   528
     "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));   
paulson@13819
   529
         F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B;   
paulson@13819
   530
         extend h F\<squnion>G \<in> stable C |]  
paulson@13819
   531
      ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
paulson@13790
   532
(*unless*)
paulson@13790
   533
apply (auto intro!: project_unless2 [unfolded unless_def] 
paulson@13790
   534
            intro: project_extend_constrains_I 
paulson@13790
   535
            simp add: ensures_def)
paulson@13790
   536
(*transient*)
paulson@13790
   537
(*A G-action cannot occur*)
paulson@13790
   538
 prefer 2
paulson@13812
   539
 apply (blast intro: project_transient_extend_set) 
paulson@13790
   540
(*An F-action*)
paulson@13790
   541
apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen]
paulson@13790
   542
             simp add: split_extended_all)
paulson@13790
   543
done
paulson@13790
   544
paulson@13790
   545
lemma (in Extend) project_ensures_D:
paulson@13819
   546
     "[| F\<squnion>project h UNIV G \<in> A ensures B;   
paulson@13812
   547
         G \<in> stable (extend_set h A - extend_set h B) |]  
paulson@13819
   548
      ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
paulson@13790
   549
apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
paulson@13790
   550
done
paulson@13790
   551
paulson@13790
   552
lemma (in Extend) project_Ensures_D: 
paulson@13819
   553
     "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Ensures B;   
paulson@13819
   554
         G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A -  
paulson@13790
   555
                     extend_set h B) |]  
paulson@13819
   556
      ==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
paulson@13790
   557
apply (unfold Ensures_def)
paulson@13790
   558
apply (rule project_ensures_D_lemma [THEN revcut_rl])
paulson@13790
   559
apply (auto simp add: project_set_reachable_extend_eq [symmetric])
paulson@13790
   560
done
paulson@13790
   561
paulson@13790
   562
paulson@13798
   563
subsection{*Guarantees*}
paulson@13790
   564
paulson@13790
   565
lemma (in Extend) project_act_Restrict_subset_project_act:
paulson@13812
   566
     "project_act h (Restrict C act) \<subseteq> project_act h act"
paulson@13790
   567
apply (auto simp add: project_act_def)
paulson@13790
   568
done
paulson@13790
   569
					   
paulson@13790
   570
							   
paulson@13790
   571
lemma (in Extend) subset_closed_ok_extend_imp_ok_project:
paulson@13790
   572
     "[| extend h F ok G; subset_closed (AllowedActs F) |]  
paulson@13790
   573
      ==> F ok project h C G"
paulson@13790
   574
apply (auto simp add: ok_def)
paulson@13790
   575
apply (rename_tac act) 
paulson@13790
   576
apply (drule subsetD, blast)
paulson@13790
   577
apply (rule_tac x = "Restrict C  (extend_act h act)" in rev_image_eqI)
paulson@13790
   578
apply simp +
paulson@13790
   579
apply (cut_tac project_act_Restrict_subset_project_act)
paulson@13790
   580
apply (auto simp add: subset_closed_def)
paulson@13790
   581
done
paulson@13790
   582
paulson@13790
   583
paulson@13790
   584
(*Weak precondition and postcondition
paulson@13790
   585
  Not clear that it has a converse [or that we want one!]*)
paulson@13790
   586
paulson@13790
   587
(*The raw version; 3rd premise could be weakened by adding the
paulson@13819
   588
  precondition extend h F\<squnion>G \<in> X' *)
paulson@13790
   589
lemma (in Extend) project_guarantees_raw:
paulson@13812
   590
 assumes xguary:  "F \<in> X guarantees Y"
paulson@13790
   591
     and closed:  "subset_closed (AllowedActs F)"
paulson@13819
   592
     and project: "!!G. extend h F\<squnion>G \<in> X' 
paulson@13819
   593
                        ==> F\<squnion>project h (C G) G \<in> X"
paulson@13819
   594
     and extend:  "!!G. [| F\<squnion>project h (C G) G \<in> Y |]  
paulson@13819
   595
                        ==> extend h F\<squnion>G \<in> Y'"
paulson@13812
   596
 shows "extend h F \<in> X' guarantees Y'"
paulson@13790
   597
apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
paulson@13790
   598
apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
paulson@13790
   599
apply (erule project)
paulson@13790
   600
done
paulson@13790
   601
paulson@13790
   602
lemma (in Extend) project_guarantees:
paulson@13812
   603
     "[| F \<in> X guarantees Y;  subset_closed (AllowedActs F);  
paulson@13790
   604
         projecting C h F X' X;  extending C h F Y' Y |]  
paulson@13812
   605
      ==> extend h F \<in> X' guarantees Y'"
paulson@13790
   606
apply (rule guaranteesI)
paulson@13790
   607
apply (auto simp add: guaranteesD projecting_def extending_def
paulson@13790
   608
                      subset_closed_ok_extend_imp_ok_project)
paulson@13790
   609
done
paulson@13790
   610
paulson@13790
   611
paulson@13790
   612
(*It seems that neither "guarantees" law can be proved from the other.*)
paulson@13790
   613
paulson@13790
   614
paulson@13798
   615
subsection{*guarantees corollaries*}
paulson@13790
   616
paulson@13798
   617
subsubsection{*Some could be deleted: the required versions are easy to prove*}
paulson@13790
   618
paulson@13790
   619
lemma (in Extend) extend_guar_increasing:
paulson@13812
   620
     "[| F \<in> UNIV guarantees increasing func;   
paulson@13790
   621
         subset_closed (AllowedActs F) |]  
paulson@13812
   622
      ==> extend h F \<in> X' guarantees increasing (func o f)"
paulson@13790
   623
apply (erule project_guarantees)
paulson@13790
   624
apply (rule_tac [3] extending_increasing)
paulson@13790
   625
apply (rule_tac [2] projecting_UNIV, auto)
paulson@13790
   626
done
paulson@13790
   627
paulson@13790
   628
lemma (in Extend) extend_guar_Increasing:
paulson@13812
   629
     "[| F \<in> UNIV guarantees Increasing func;   
paulson@13790
   630
         subset_closed (AllowedActs F) |]  
paulson@13812
   631
      ==> extend h F \<in> X' guarantees Increasing (func o f)"
paulson@13790
   632
apply (erule project_guarantees)
paulson@13790
   633
apply (rule_tac [3] extending_Increasing)
paulson@13790
   634
apply (rule_tac [2] projecting_UNIV, auto)
paulson@13790
   635
done
paulson@13790
   636
paulson@13790
   637
lemma (in Extend) extend_guar_Always:
paulson@13812
   638
     "[| F \<in> Always A guarantees Always B;   
paulson@13790
   639
         subset_closed (AllowedActs F) |]  
paulson@13790
   640
      ==> extend h F                    
paulson@13812
   641
            \<in> Always(extend_set h A) guarantees Always(extend_set h B)"
paulson@13790
   642
apply (erule project_guarantees)
paulson@13790
   643
apply (rule_tac [3] extending_Always)
paulson@13790
   644
apply (rule_tac [2] projecting_Always, auto)
paulson@13790
   645
done
paulson@13790
   646
paulson@13790
   647
paulson@13812
   648
subsubsection{*Guarantees with a leadsTo postcondition*}
paulson@13790
   649
paulson@13790
   650
lemma (in Extend) project_leadsTo_D:
paulson@13819
   651
     "F\<squnion>project h UNIV G \<in> A leadsTo B
paulson@13819
   652
      ==> extend h F\<squnion>G \<in> (extend_set h A) leadsTo (extend_set h B)"
paulson@13812
   653
apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto)
paulson@13790
   654
done
paulson@13790
   655
paulson@13790
   656
lemma (in Extend) project_LeadsTo_D:
paulson@13819
   657
     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A LeadsTo B   
paulson@13819
   658
       ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
paulson@13812
   659
apply (rule refl [THEN Join_project_LeadsTo], auto)
paulson@13790
   660
done
paulson@13790
   661
paulson@13790
   662
lemma (in Extend) extending_leadsTo: 
paulson@13812
   663
     "extending (%G. UNIV) h F  
paulson@13812
   664
                (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
paulson@13790
   665
apply (unfold extending_def)
paulson@13790
   666
apply (blast intro: project_leadsTo_D)
paulson@13790
   667
done
paulson@13790
   668
paulson@13790
   669
lemma (in Extend) extending_LeadsTo: 
paulson@13819
   670
     "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13812
   671
                (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
paulson@13790
   672
apply (unfold extending_def)
paulson@13790
   673
apply (blast intro: project_LeadsTo_D)
paulson@13790
   674
done
paulson@13790
   675
paulson@13790
   676
ML
paulson@13790
   677
{*
paulson@13790
   678
val projecting_Int = thm "projecting_Int";
paulson@13790
   679
val projecting_Un = thm "projecting_Un";
paulson@13790
   680
val projecting_INT = thm "projecting_INT";
paulson@13790
   681
val projecting_UN = thm "projecting_UN";
paulson@13790
   682
val projecting_weaken = thm "projecting_weaken";
paulson@13790
   683
val projecting_weaken_L = thm "projecting_weaken_L";
paulson@13790
   684
val extending_Int = thm "extending_Int";
paulson@13790
   685
val extending_Un = thm "extending_Un";
paulson@13790
   686
val extending_INT = thm "extending_INT";
paulson@13790
   687
val extending_UN = thm "extending_UN";
paulson@13790
   688
val extending_weaken = thm "extending_weaken";
paulson@13790
   689
val extending_weaken_L = thm "extending_weaken_L";
paulson@13790
   690
val projecting_UNIV = thm "projecting_UNIV";
paulson@13790
   691
*}
paulson@13790
   692
paulson@7826
   693
end